[GHC] #8808: ImpredicativeTypes type checking fails depending on syntax of arguments

[GHC]

#8808: ImpredicativeTypes type checking fails depending on syntax of arguments
-------------------------------------+-------------------------------------
       Reporter:  guest              |             Owner:
           Type:  bug                |            Status:  new
       Priority:  normal             |         Milestone:
      Component:  Compiler (Type     |           Version:  7.8.1-rc1
  checker)                           |  Operating System:  Unknown/Multiple
       Keywords:                     |   Type of failure:  GHC rejects
   Architecture:  Unknown/Multiple   |  valid program
     Difficulty:  Unknown            |         Test Case:
     Blocked By:                     |          Blocking:
Related Tickets:                     |
-------------------------------------+-------------------------------------
 g1 and g2 below type check, but g1', g2', and g2'' don't even though the
 types are exactly the same.
 {{{
 {-# LANGUAGE ImpredicativeTypes, NoMonomorphismRestriction #-}
 module Test where
 f1 :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
 f1 (Just g) = Just (g [3], g "hello")
 f1 Nothing  = Nothing

 f2 :: [forall a. [a] -> [a]] -> Maybe ([Int], [Char])
 f2 [g] = Just (g [3], g "hello")
 f2 []  = Nothing

 g1 = (f1 . Just) reverse
 g1' = f1 (Just reverse)

 g2 = f2 [reverse]
 g2' = f2 ((:[]) reverse)
 g2'' = f2 (reverse : [])
 }}}
 Compiling it with HEAD gives these errors:
 {{{
 [1 of 1] Compiling Test             ( test.hs, test.o )

 test.hs:12:16:
     Couldn't match expected type ‛forall a. [a] -> [a]’
                 with actual type ‛[a2] -> [a2]’
     In the first argument of ‛Just’, namely ‛reverse’
     In the first argument of ‛f1’, namely ‛(Just reverse)’

 test.hs:15:17:
     Couldn't match expected type ‛forall a. [a] -> [a]’
                 with actual type ‛[a0] -> [a0]’
     In the first argument of ‛: []’, namely ‛reverse’
     In the first argument of ‛f2’, namely ‛((: []) reverse)’

 test.hs:16:12:
     Couldn't match expected type ‛forall a. [a] -> [a]’
                 with actual type ‛[a1] -> [a1]’
     In the first argument of ‛(:)’, namely ‛reverse’
     In the first argument of ‛f2’, namely ‛(reverse : [])’
 }}}

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