Constraint error related to type family and higher-rank type

[Tsuyoshi Ito]

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