[Haskell-cafe] Type class for sequences with dependent types

[Robbert Krebbers]

Hello,

in a Haskell development I have to represent paths that have elements of 
alternating types. GADTs allow me to do this easily:

data AltList :: * -> * -> * where
   Nil   :: AltList a a
   ICons :: Int -> AltList Int b -> AltList () b
   UCons :: () -> AltList () b -> AltList Int b

Since I have various kinds of these data structures I defined a type 
class for common operations on such data structures.

class DepSequence l where
   nil :: l a a
   app :: l a b -> l b c -> l a c

The instance for AltList is as follows:

instance DepSequence AltList where
   nil = Nil
   Nil       `app` k = k
   ICons i l `app` k = ICons i (l `app` k)
   UCons i l `app` k = UCons i (l `app` k)

This all works nicely, however, I also want ordinary lists to be an 
instance of this class too. I tried the following:

type IntListAlt a b = [Int]
instance DepSequence IntListAlt where
   nil = []
   app = (++)

But GHC does not like this, it yields:

   Type synonym `IntListAlt' should have 2 arguments, but has been
   given none In the instance declaration for `DepList IntListAlt'

The following alternative works, but it is quite ugly

newtype IntList a b = IntList { getList :: [Int] }
instance DepSequence IntList where
   nil     = IntList []
   app l k = IntList (getList l ++ getList k)

and also does not give me a nil of type [Int] and an app of type [Int] 
-> [Int] -> [Int].

Does anyone know whether Haskell allows me to do this in a better way?

Best,

Robbert