Stefan O'Rear stefanor at cox.net
Mon Feb 26 01:15:25 EST 2007

```On Mon, Feb 26, 2007 at 03:42:56PM +1000, Matthew Brecknell wrote:
> 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).
>
I can't find it now, but there was a post saying this couldn't be done
because system fc is strict in type arguments, such as bound by forall t.
```