GADTs documentation, a start - Haskell

https://haskell.zettel.page/5956fd49.html

I think good insight on GADTs can be that they're no more than sugar around "implicit fields" - like, ignoring restrictions on typeclass instance manipulation, you could write them by hand with normal ADTs:

data Query result where
  Query_NotesByTag :: Tag -> Query [Note]
  Query_AllTags :: Query [Tag]

could be written as:

data Query result
  = Query_NotesByTag (Iso result [Note]) Tag
  | Query_AllTags (Iso result [Tag])

Similarly:

data Showable where
  Showable :: Show a => a -> Showable

could be written as:

data Showable = forall a. Showable (Show a) a

If GHC let us explicitly pass instances around (or Show was a normal record).

You don't want to do that in Haskell - this way you would have to manually apply "coercions" and pass instances around, and compiler wouldn't be that clever in exhaustivity checking - but it can help you realize what GADTs can and cannot do.

First-class type equality is also an important part of it.

Knowing the "index type" of a GADT can tell you something about what constructors are possible for a GADT value. http://wiki.haskell.org/Generalised_algebraic_datatype#Example_with_lists Is that captured in the "implicit fields" explanation, or a further fact?

@Daniel Díaz Carrete let's copy that example there:

data Empty
data NonEmpty
data List x y where
     Nil :: List a Empty
     Cons:: a -> List a b ->  List a NonEmpty

and rewrite it in terms of explicit fields:

-- You'll see why I'm doing this later on
newtype Empty    = Empty{ unEmpty :: Void }
data    NonEmpty = NonEmpty

data List x y
  = Nil (Iso y Empty)
  | forall z. Cons (Iso y NonEmpty) x (List x z)

Now, safeHead would be:

safeHead :: List x NonEmpty -> x
safeHead (Cons _ x _) = x
safeHead (Nil i)      = absurd $ unEmpty $ from i NonEmpty

Basically, in unreachable case you can create Void by using nonexistent Iso Empty NonEmpty, making both typechecker and exhaustivity checker happy