[Haskell-cafe] Writing functions over GADTs

[Dominic Mulligan]

Dear all,

I'm working on a small proof assistant in Haskell.  In the logic that
I'm implementing it's very important that I distinguish between `large'
and `small' types for consistency reasons.  I have worked to get this
distinction reflected in my types with the use of GADTs, like so:

data Type   :: * -> * where
  SVariable :: Decoration -> Type Small
  LVariable :: Decoration -> Type Large
  Bound     :: Index      -> Type Small
  Universal :: Decoration -> Type a        -> Type Large
  LFormer   :: Decoration -> ArgList Large -> Variety    -> Type Large
  SFormer   :: Decoration -> ArgList Small -> Variety    -> Type Small

where:

data ArgList :: * -> * where
  Empty      :: ArgList a
  SmallCons  :: Type Small -> ArgList a -> ArgList a
  LargeCons  :: Type Large -> ArgList a -> ArgList Large

Great, but one problem.  How do you write functions over these data
types?  Consider as an example the function `toList', which drops an
`ArgList a' down into a vanilla Haskell list `[a]'.  Attempting a
straightforward implementation like so:

toList :: ArgList a -> [Type a]
toList Empty           = []
toList (SmallCons h t) = h : toList t
toList (LargeCons h t) = h : toList t

Gives a type error, as the type variable `a' gets instantiated to Small
when typechecking the second clause of the function definition, and
Large when type checking the third clause.  Perversely, it's much easier
to write a more complex function:

forget :: (forall a. Type a -> b) -> ArgList a -> [b]
forget f Empty           = []
forget f (SmallCons h t) = f h : forget f t
forget f (LargeCons h t) = f h : forget f t

As we can use RankNTypes to make things `more polymorphic', and prevent
type variables being instantiated too soon.  It seems plausible that
`toList' could be defined in terms of `forget', taking `f' to be the
identity function, but this does not work either as we then get type
errors about inferred types being less polymorphic than expected.

So, is there a standard way writing function like `toList' in Haskell?
Am I going about thinking of using GADTs in the wrong way?  I've
searched everywhere and cannot seem to find the correct solution (and
I'm now at the very border of my Haskell knowledge).

My coworker showed me a way of doing this in O'Caml using polymorphic
variants.  This allows us to form a subtype of both `Small' and `Large'.
I'm taken to believe that HList can simulate many of the properties that
polymorphic variants enjoy, so perhaps the answer lies there?

Any help gratefully received.

Regards,
Dominic Mulligan