[Haskell] Re: How to define tail function for Even/Odd GADT lists?

However, we were not able to write a function that returns the tail.

...

tailList :: Flip b c => List a b -> List a c tailList (Cons _ xs) = xs

The problem here is that the caller will probably not know which "Flip b c". OTOH the Cons of type "List a b" already contains a "Flip b c" proof, so you really don't need to receive it. Of course, in order to be able to write "List a c" you still need to introduce a "c" variable somewhere. This should be done as follows: tailList: List a b -> (Flip b c => List a c) -- Stefan