Mimicking GADTs using RankNTypes, ExistentialQuantification, and TypeFamilies

GADT1.hs

{-# OPTIONS_GHC -Wincomplete-patterns #-}
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}

newtype LEq a b = LEq { getLEq :: forall f. f a -> f b }
data Void

data Z
data S n

data List a n
  = Nil (LEq Z n)
  | forall m. Cons a (List a m) (LEq (S m) n)

type family F n where
  F Z     = ()
  F (S m) = Void

newtype G n = G { getG :: F n }

hd :: List a (S n) -> a
hd (Nil e) = case getG (getLEq e (G ())) of { }
hd (Cons x xs e) = x

GADT2.hs

{-# OPTIONS_GHC -Wincomplete-patterns #-}
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE TypeFamilies #-}

data Z
data S n

type family CaseN a b n where
  CaseN a b Z     = a
  CaseN a b (S n) = b n

data Nil = Nil
data Cons a b n = Cons a (b n)
data List a n = List (CaseN Nil (Cons a (List a)) n)

hd :: List a (S n) -> a
hd (List (Cons x xs)) = x