existential & GADT & escape

[kahl at cas.mcmaster.ca]

Jim Apple <japple at freeshell.org> wrote:
 > 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