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