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