#7264: Adding GHC's inferred type signatures to a working program can make it
fail
with Rank2Types
---------------------------------+------------------------------------------
Reporter: guest | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.4.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------
Changes (by simonpj):
* cc: dimitris@… (added)
* difficulty: => Unknown
Comment:
This is bad. Here's a slightly cut down example:
{{{
{-# LANGUAGE Rank2Types #-}
module T7264 where
data Foo = Foo (forall r . r -> String)
mmap :: (a->b) -> Maybe a -> Maybe b
mmap f (Just x) = f x
mmap f Nothing = Nothing
-- mkFoo2 :: (forall r. r -> String) -> Maybe Foo
mkFoo2 val = mmap Foo (Just val)
}}}
* The commented-out type sig is inferred, because GHC assigns unknown
type `alpha` to `val`; then instantiates `mmap`'s type with `beta` and
`gamma`; then unifies `beta`:=`forall r. r->String`.
* But when the commented out type sig is provided ghc ''instantiates'' it
at the occurrence of `val`.
You need to call `mmap` at a polymorphic type, which means you need
impredicativity. Lacking `ImpredicativeTypes` the no-signature program
should be rejected. The fact that it isn't is a bug.
Even if that bug is fixed, the progam shows, again, how tricky
impredicativity is. We don't have a decent implementation of
`ImpredicativeTypes`.
At least it's not a show-stopper for anyone.
Simon
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7264#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
