[GHC] #4347: Bug in unification of polymorphic and not-yet-polymorphic type (was: Asymmetry of (impredicative) instantiation/higher rank types)

[GHC]

#4347: Bug in unification of polymorphic and not-yet-polymorphic type
----------------------------------------+-----------------------------------
    Reporter:  dolio                    |        Owner:                           
        Type:  bug                      |       Status:  new                      
    Priority:  normal                   |    Milestone:  7.4.1                    
   Component:  Compiler (Type checker)  |      Version:  7.1                      
    Keywords:                           |     Testcase:                           
   Blockedby:                           |   Difficulty:                           
          Os:  Linux                    |     Blocking:                           
Architecture:  x86_64 (amd64)           |      Failure:  GHC rejects valid program
----------------------------------------+-----------------------------------
Changes (by Blaisorblade):

 * cc: p.giarrusso@… (added)


Comment:

 I think I'm seeing two instances of this bug in rather more simple
 contexts. The first involves the id function:

 {{{
 $ ghci -XScopedTypeVariables -XRank2Types
 Prelude> let (id2 :: forall t. t -> t) = \x -> x

 <interactive>:1:33:
     Couldn't match expected type `t0 -> t1'
                 with actual type `forall t. t -> t'
     The lambda expression `\ x -> x' has one argument,
     but its type `forall t. t -> t' has none
     In the expression: \ x -> x
     In a pattern binding: (id2 :: forall t. t -> t) = \ x -> x
 }}}

 To me, it seems already buggy that the code is rejected without
 Rank2Types, because only rank-1 types are involved. I guess that the code
 requires first-class polymorphism, or that the message might appear only
 of the main failure. But that unification error? I think it reflects the
 fact that a term of type (forall t. t -> t), in System F, expects a type
 argument before a term argument.
 That's consistent with the errors shown
 [http://stackoverflow.com/questions/5885479/weird-error-when-using-scoped-
 type-variables-and-the-y-combinator-in-haskell here on Stackoverflow].

 With polymorphic recursion, one gets even no clue about what's happening,
 just a "couldn't match" message, even if probably due to the same problem.
 Aren't similar errors supposed to produce similar messages?

 {{{
 Prelude> let a :: forall b. b -> b = a a

 <interactive>:1:31:
     Couldn't match expected type `forall b. b -> b'
                 with actual type `b0 -> b0'
     In the first argument of `a', namely `a'
     In the expression: a a
     In a pattern binding: a :: forall b. b -> b = a a
 }}}

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