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.