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 |