existential & GADT & escape

[Jim Apple]

 > data Z
 > data S a
 >
 > data L a n where
 >     Nil :: L a Z
 >     Con :: a -> L a b -> L a (S b)
 >
 > data LL a = forall n . LL (L a n)
 > 
                                                                      > 
class Append p q r where
 >     nappend' :: L a p -> L a q -> L a r
 >
 > instance Append Z q q where
 >     nappend' _ y = y
 >
 > instance (Append p q r) => Append (S p) q (S r) where
 >     nappend' (Con x y) z = Con x (nappend' y z)
 >
 > nappend (LL x) (LL y) = LL (nappend' x y)

No instance for (Append n n1 r)
       arising from use of `nappend'' at NList.lhs: :29-36
     Probable fix: add (Append n n1 r) to the existential context for `LL'
     In the first argument of `LL', namely `(nappend' x y)'
     In the definition of `nappend': nappend (LL x) (LL y) = LL 
(nappend' x y)


Clearly I can write nappend like:

  nappend :: LL a -> LL a -> LL a
  nappend (LL Nil) y = y
  nappend (LL (Con x Nil)) (LL z) = LL (Con x z)
  nappend (LL (Con x y)) (LL z) = nappend (LL (Con x Nil))
                                           (nappend (LL y) (LL z))

but I'd rather keep the nice guarentee from nappend'.

Any ideas?

Jim