Adding GHC's inferred type signatures to a working program can make it fail with Rank2Types

{-# LANGUAGE Rank2Types #-}
module Test where

data Foo = Foo { unFoo :: forall r . (RealFrac r) => r -> String }

mkFoo1 :: (forall r. RealFrac r => r -> String) -> Maybe Foo
mkFoo1 val = Just $ Foo val

--mkFoo2 :: (forall r. RealFrac r => r -> String) -> Maybe Foo
mkFoo2 val = Foo `fmap` Just val

Without the commented-out type signature, the program typechecks without complaint. With it, the program fails to compile with the error:

Test.hs:10:30:
    Couldn't match expected type `forall r. RealFrac r => r -> String'
                with actual type `r0 -> String'
    In the first argument of `Just', namely `val'
    In the second argument of `fmap', namely `Just val'
    In the expression: Foo `fmap` Just val

Note that the commented-out type is exactly what's inferred by GHC.

Also note that (with ImpredicativeTypes also enabled), this is fine (but mkFoo2 still fails if its type signature is included):

mkFoo3 :: (forall r. RealFrac r => r -> String) -> Maybe Foo
mkFoo3 val = Foo `fmap` (Just :: (forall s. RealFrac s => s -> String) -> (Maybe (forall s. RealFrac s => s -> String))) val

It's confusing that adding a valid, GHC-inferred type signature to a program can break it, and the error message leaves something to be desired.

Trac metadata

Trac field	Value
Version	7.4.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture