I dont remember where i saw it, but i think someone had an example of a list whose type is the maximum element in the list. I've been trying to reproduce that with GADT's. data One = One data Two = Two data Three = Three data MaxList t where Elem1 :: MaxList One Elem2 :: MaxList Two ML1Cons1 :: MaxList One -> MaxList One -> MaxList One ML1Cons2 :: MaxList One -> MaxList Two -> MaxList Two ML2Cons1 :: MaxList Two -> MaxList One -> MaxList Two ML2Cons2 :: MaxList Two -> MaxList Two -> MaxList Two a = ML2Cons2 Elem2 $ ML2Cons1 Elem2 $ ML1Cons1 Elem1 $ Elem1 so one problem is the tedium of defining a cons for each possible combination. The other problem is that i cant define a usefull tail that makes any sense. mlTail :: MaxList Two -> MaxList t mlTail (ML2Cons2 a b) = b mlTail (ML2Cons1 a b) = b this one doesn't work, and probably because there is nothing that i could do with the return value. mlTail :: MaxList Two -> MaxList Two mlTail (ML2Cons2 a b) = b mlTail (ML2Cons1 a b) = b --wont compile because b is a MaxList One will only work for lists that only contain Two's, which is not what i want either. So is this somehow possible? Thanks