[Haskell-cafe] Safe lists with GADT's

[Matthew Brecknell]

Neil Mitchell wrote:
> data ConsT a
> data NilT
> 
> data List a t where
>     Cons :: a -> List a b -> List a (ConsT b)
>     Nil  :: List a NilT

Stefan O'Rear wrote:
> data VarList a = forall t. VarList (List a t)
> 
> fromListV :: [a] -> VarList a
> fromListV []     = VarList Nil
> fromListV (x:xs) = case fromListV xs of
>                      VarList xs' -> VarList (Cons x xs')
> 
> fromListC :: [a] -> (forall t. List a t -> r) -> r
> fromListC [] fn = fn Nil
> fromListC (x:xs) fn = fromListC xs (\sl -> fn (Cons x sl))

I noticed that fromListV and fromListC always force traversal of the
input list. I made various attempts to modify them to preserve laziness,
but this always resulted in a type error. For example:

> fromListV (x:xs) = case fromListV xs of
>   ~(VarList l) -> VarList (Cons x l)

Couldn't match the rigid variable `a' against the rigid variable `a1'
  `a' is bound by the type signature for `fromListV'
  `a1' is bound by the pattern for `VarList' at gadt-list.hs:33:42-50
  Expected type: List a b
  Inferred type: List a1 t
In the second argument of `Cons', namely `l'
In the first argument of `VarList', namely `(Cons x l)'

I guess the strict traversal of the input list is inevitable,
considering that the concrete type of any (List a t) depends on the
length of the list (even when hidden behind an existential).