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