gistfile1.txt

<Ferdirand> i'm trying to define a type for lists of two alternating types
<Ferdirand> data Chain a b l where
<Ferdirand>     Nil  :: Chain a b b
<Ferdirand>     (:@) :: a -> Chain b a l -> Chain a b l
<Ferdirand> l represents the statically-known type of the last element
<Ferdirand> now, for the type Chain (a b a), which has the same type for the first and last element, i know that if a and b are different types, then the list cannot be empty
<Ferdirand> and i'd like to write a type-safe `last` function that reflects that

<Ferdirand> data Chain a b l where
<Ferdirand>     Nil  :: Chain a b b
<Ferdirand>     (:@) :: a -> Chain b a l -> Chain a b l