[GHC] #7220: Confusing error message in type checking related to type family, fundep, and higher-rank type

[GHC]

#7220: Confusing error message in type checking related to type family, fundep,
and higher-rank type
------------------------------+---------------------------------------------
 Reporter:  tsuyoshi          |          Owner:                         
     Type:  bug               |         Status:  new                    
 Priority:  normal            |      Component:  Compiler (Type checker)
  Version:  7.6.1-rc1         |       Keywords:                         
       Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple       
  Failure:  None/Unknown      |       Testcase:                         
Blockedby:                    |       Blocking:                         
  Related:                    |  
------------------------------+---------------------------------------------
 (This is related to, but different from, the message which I posted to
 glasgow-haskell-users mailing list: http://www.haskell.org/pipermail
 /glasgow-haskell-users/2012-September/022815.html.)

 GHC 7.6.1-rc1 (7.6.0.20120810; 64-bit Windows) rejects the attached code
 (Test2.hs) 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
 }}}

 I am not sure whether the code is supposed to be accepted or rejected, but
 even if it is correct to reject the code, this error message does not look
 right to me.  If I am not mistaken, the error message is saying that the
 type checker expects the argument of `(f :: (forall b. (C A b, TF b ~ Y)
 => b) -> X)` to have type `Y`, but I cannot think of any reason why it
 should relate the type `(forall b. (C A b, TF b ~ Y) => b)` with `Y`.

 The same code is available also at https://gist.github.com/3606856.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7220>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler