{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Test2 where

class C a b | b -> a

data A = A
data X a = X
data Y = Y

type family TF b

f :: (forall b. (C a b, TF b ~ Y) => b) -> X a
f _ = undefined

u :: (C A b, TF b ~ Y) => b
u = undefined

v :: X A
v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X A) u -- This line causes an error (see below)

{-
GHC 7.6.1-rc1 (7.6.0.20120810) rejects this code with the following error message.

Test2.hs:24:52:
    Couldn't match expected type `Y'
                with actual type `TF (forall b. (C A b, TF b ~ Y) => b)'
    In the first argument of `f ::
                                (forall b. (C A b, TF b ~ Y) => b) -> X', namely
      `u'
    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

GHC 7.4.1 rejected this code with a different error message:

Test2.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
-}