[GHC] #12749: Typechecker regression involving RankNTypes

[GHC]

#12749: Typechecker regression involving RankNTypes
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following code compiles on GHC 7.0.4 through 7.10.3, but not with GHC
 8.0.1, 8.0.2, or HEAD:

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}
 module Bug where

 type NatTrans f g = forall x. f x -> g x

 -- NatTrans analog of id
 applyNT :: NatTrans f g -> NatTrans f g
 applyNT x = x

 b :: Bool
 b = True

 eitherToMaybe :: NatTrans (Either a) Maybe
 eitherToMaybe (Left _)  = Nothing
 eitherToMaybe (Right x) = Just x

 trans :: NatTrans (Either a) Maybe -> NatTrans (Either a) Maybe
 trans x = x

 applyNTCheck :: NatTrans (Either a) Maybe
 applyNTCheck = (if b then trans else applyNT) eitherToMaybe
 }}}

 {{{
 $ /opt/ghc/8.0.1/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:21:27: error:
     • Couldn't match type ‘NatTrans (Either a) Maybe’
                      with ‘Either a0 x0 -> Maybe x0’
       Expected type: (Either a0 x0 -> Maybe x0) -> Either a x -> Maybe x
         Actual type: NatTrans (Either a) Maybe -> Either a x -> Maybe x
     • In the expression: trans
       In the expression: if b then trans else applyNT
       In the expression: (if b then trans else applyNT) eitherToMaybe
     • Relevant bindings include
         applyNTCheck :: Either a x -> Maybe x (bound at Bug.hs:21:1)
 }}}

 (Originally spotted [https://github.com/ku-fpg/natural-
 transformation/pull/13#issuecomment-255378141 here].)

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