Jim Apple
Date: Wed, 20 Apr 2005 16:42:35 -0400
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?
Not tested: class N where -- no members instance N Z where -- no members instance N a => N (s a) where -- no members data LL a = forall n . N n => LL (L a n) Assuming N embodies the guarentee you mentioned. Wolfram