This should compile, shouldn't it? -- ghc -c -fglasgow-exts TestInfer.hs module TestInfer where { class C t a b | t a -> b; instance C Char a Bool; data P t a = forall b. (C t a b) => MkP b; data Q t = MkQ (forall a. P t a); f' :: Q Char; f' = MkQ (MkP True :: forall a. P Char a); f :: Q Char; f = MkQ (MkP True); } GHC 5.04.2 for MacOS X complains about f, but not about f': TestInfer.hs:15: Could not deduce (C t a Bool) from the context () Probable fix: Add (C t a Bool) to the When generalising the type of an expression Or add an instance declaration for (C t a Bool) arising from use of `MkP' at TestInfer.hs:15 In the first argument of `MkQ', namely `(MkP True)' In the definition of `f': MkQ (MkP True) -- Ashley Yakeley, Seattle WA