How can I desugar my GADTs?

Question

I was reading Coercions and Roles for Dummies and the author off handedly mentioned that GADTs were just syntactic sugar.

GADTs are syntactic sugar on top of (~) so expect GADTs to have nominal role type parameters.

Now the author didn't go into this any further because this wasn't the point of the blog post. However I am intrigued. How can I go about desugaring my GADTs?

For example here is a simple Heterogeneous list using a GADT.

{-# Language GADTs, DataKinds, TypeOperators #-}

data HList a where
  Empty :: HList '[]
  Cons  :: a -> HList b -> HList (a ': b)

What would the desugared version look like?

Answer 1

You could desugar your GADT into this one:

data HList t where
  Empty :: t ~ '[]      => HList t
  Cons  :: t ~ (a ': b) => a -> HList b -> HList t

This is no longer a "real" GADT, since every constructor returns the general type HList t, like it happens in plain old algebraic data types.

The trick is that the type variable t looks unconstrained in the result type HList t, but is actually restricted by the type equality constraints t ~ ..., so to obtain the same semantics as the original type.

If you want to remove the GADT syntax completely, you can do as follows. You'll still need to turn on some extensions to use ~ constraints.

{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, ExistentialQuantification #-}
data HList2 t
   = t ~ '[] => Empty2
   | forall a b .  t ~ (a ': b) => Cons2 a (HList2 b)

The paper you mention is probably pointing out that, since t is involved in equality constraints, it has a nominal role.