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

[Ahn, Ki Yung]

Using GADTs and functional dependencies, we can define GADT lists
that statically distinguishes even length lists from odd length lists.

> data Even
> data Odd
>
> class Flip b c | b -> c, c -> b where
>
> instance Flip Even Odd where
> instance Flip Odd Even where
>
> data List a b where
>   Nil  :: List a Even
>   Cons :: Flip b c => a -> List a b -> List a c

For example,

Nil :: forall a. List a Even
Cons True Nil :: List Bool Odd
Cons False (Cons True Nil) :: List Bool Even


We were able to define the function that returns the head.

> headList :: List a b -> a
> headList (Cons x _) = x

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

Is there a way to define the tailList function within the current
GHC type system implementation (maybe using some other language
extensions), or do we need to improve the type system regarding
GADTs and functional dependencies?

$ ghci -fglasgow-exts EOlist.hs
GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( EOlist.lhs, interpreted )

EOlist.lhs:30:25:
    Couldn't match expected type `c' against inferred type `b1'
      `c' is a rigid type variable bound by
          the type signature for `tailList' at EOlist.lhs:29:21
      `b1' is a rigid type variable bound by
           the constructor `Cons' at EOlist.lhs:30:12
      Expected type: List a c
      Inferred type: List a b1
    In the expression: xs
    In the definition of `tailList': tailList (Cons _ xs) = xs
Failed, modules loaded: none.
Prelude>

Note: You can save this message content as EOList.lhs and load the
script with ghci to observe the type error message above.