Hello, Can anyone please explain why the following code is rejected by GHC (7.4.1)? The same code is also available at https://gist.github.com/3606849. ----- {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} module Test1 where class C a b | b -> a data A = A data X = X data Y = Y type family TF b f :: (forall b. (C a b, TF b ~ Y) => b) -> X f _ = undefined u :: (C A b, TF b ~ Y) => b u = undefined v :: X v = f u -- This line causes an error (see below) ----- (1) GHC rejects this code with the following error message. Test1.hs:24:7: Could not deduce (C A b) arising from a use of `u' from the context (C a_c b, TF b ~ Y) bound by a type expected by the context: (C a_c b, TF b ~ Y) => b at Test1.hs:24:5-7 Possible fix: add (C A b) to the context of a type expected by the context: (C a_c b, TF b ~ Y) => b or add an instance declaration for (C A b) In the first argument of `f', namely `u' In the expression: f u In an equation for `v': v = f u (2) If I remove “TF b ~ Y” from the type of the argument of f and the type of u, then the code compiles. This suggests that the error message in (1) might not be the accurate description of the problem. (3) If I write “(f :: (forall b. (C A b, TF b ~ Y) => b) -> X)” instead of just “f” in the definition of v, then GHC reports a different error: Test1.hs:24:6: Cannot deal with a type function under a forall type: forall b. (C A b, TF b ~ Y) => b In the expression: f :: (forall b. (C A b, TF b ~ Y) => b) -> X In the expression: (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u In an equation for `v': v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u Item (3) might be related to a fixed Ticket #4310: http://hackage.haskell.org/trac/ghc/ticket/4310#comment:2 Best regards, Tsuyoshi