Type family and higher-rank type

Test1.hs

{-# 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 7.6.1-rc1 (7.6.0.20120810) rejects it 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_e b, TF b ~ Y)
      bound by a type expected by the context: (C a_e b, TF b ~ Y) => b
      at Test1.hs:24:5-7
    Possible fix: 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

    GHC 7.4.1 also rejected this code with the following error message,
    which was basically the same as what GHC 7.6.1-rc1 says.

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.
    See https://gist.github.com/3606856.
-}