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

[Stefan Monnier]

> 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