ambiguous type variables in existential classes

Hal Daume III hdaume@ISI.EDU
Thu, 22 Aug 2002 13:48:03 -0700 (PDT)


Sorry for the incomprehensible subject, I couldn't think of anything
better.  I've tried to come up with a short example of the error I'm
getting, but haven't been able to get it too short, so here's what I have:

class Foo p where
  foo :: Eq e => p e -> e -> (forall p' . Foo p' e -> a) -> a

-- note, foo is basically supposed to be:
-- foo :: (Eq a , exists p' . Foo p' e) => p e -> e -> p' e
-- but we can't do this directly, so we use CPS

data Const e = Const

instance Foo Const where
  foo p e q = q p

newtype Wrap p e = Wrap (p e)

instance (Eq e, Foo p) => Foo (Wrap p) where
  foo (Bar p) e q = foo p e q

data DList e = DNil
             | forall q . Foo q => (e, q e) :> (DList e)

-- a list of members of this class

instance Foo DList where
  foo DNil e q = q Const
  foo ((e',p) :> ps) e q
    | e == e'   = q (Bar p)
    | otherwise = foo ps e q

----


Okay, that's the code.  This produces the following error in GHC:

/home/hdaume/projects/NLP/Foo.hs:23:
    Ambiguous type variable(s) `e' in the constraint `Eq e'
    arising from use of `q' at /home/hdaume/projects/NLP/Foo.hs:23
    In the definition of `foo': q (Bar p)

line 23 is the line which reads "    | e == e'   = q (Bar p)".

The interesting thing is that if I change the instance declaration of Foo
(Bar p) to:

  instance Foo p => Foo (Bar p) where
     ...same as before...

this error goes away.  Certainly having the constraint on the instance
declaration doesn't really *do* anything since you need to have Eq to use
any of the methods, but I have no idea why it would cause this program to
be ill typed.

Can someone explain this?

--
Hal Daume III

 "Computer science is no more about computers    | hdaume@isi.edu
  than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume