GHC: Ticket #7264: Adding GHC's inferred type signatures to a working program can make it fail with Rank2Types
http://ghc.haskell.org/trac/ghc/ticket/7264
<pre class="wiki">{-# 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
</pre><p>
Without the commented-out type signature, the program typechecks without complaint. With it, the program fails to compile with the error:
</p>
<pre class="wiki">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
</pre><p>
Note that the commented-out type is exactly what's inferred by GHC.
</p>
<p>
Also note that (with ImpredicativeTypes also enabled), this is fine (but mkFoo2 still fails if its type signature is included):
</p>
<pre class="wiki">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
</pre><p>
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.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/7264
Trac 1.2simonpjFri, 05 Oct 2012 11:03:33 GMTcc, difficulty set
http://ghc.haskell.org/trac/ghc/ticket/7264#comment:1
http://ghc.haskell.org/trac/ghc/ticket/7264#comment:1
<ul>
<li><strong>cc</strong>
<em>dimitris@…</em> added
</li>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
<p>
This is bad. Here's a slightly cut down example:
</p>
<pre class="wiki">{-# 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)
</pre><ul><li>The commented-out type sig is inferred, because GHC assigns unknown type <code>alpha</code> to <code>val</code>; then instantiates <code>mmap</code>'s type with <code>beta</code> and <code>gamma</code>; then unifies <code>beta</code>:=<code>forall r. r->String</code>. And then later unifies <code>alpha</code> and <code>beta</code>.
</li></ul><ul><li>But when the commented out type sig is provided ghc <em>instantiates</em> it at the occurrence of <code>val</code>.
</li></ul><p>
You need to call <code>mmap</code> at a polymorphic type, which means you need impredicativity. Lacking <code>ImpredicativeTypes</code> the no-signature program should be rejected. The fact that it isn't is a bug.
</p>
<p>
Even if that bug is fixed, the progam shows, again, how tricky impredicativity is. We don't have a decent implementation of <code>ImpredicativeTypes</code>.
</p>
<p>
At least it's not a show-stopper for anyone.
</p>
<p>
Simon
</p>
Ticketsimonpj@…Wed, 31 Oct 2012 09:18:11 GMT
http://ghc.haskell.org/trac/ghc/ticket/7264#comment:2
http://ghc.haskell.org/trac/ghc/ticket/7264#comment:2
<p>
commit <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/10f83429ba493699af95cb8c3b16d179d78b7749/ghc" title="Do not instantiate unification variables with polytypes
Without ...">10f83429ba493699af95cb8c3b16d179d78b7749</a>
</p>
<pre class="wiki">Author: Simon Peyton Jones <simonpj@microsoft.com>
Date: Wed Oct 31 09:08:39 2012 +0000
Do not instantiate unification variables with polytypes
Without -XImpredicativeTypes, the typing rules say that a function
should be instantiated only at a *monotype*. In implementation terms,
that means that a unification variable should not unify with a type
involving foralls. But we were not enforcing that rule, and that
gave rise to some confusing error messages, such as
Trac #7264, #6069
This patch adds the test for foralls. There are consequences
* I put the test in occurCheckExpand, since that is where we see if a
type can unify with a given unification variable. So
occurCheckExpand has to get DynFlags, so it can test for
-XImpredicativeTypes
* We want this to work
foo :: (forall a. a -> a) -> Int
foo = error "foo"
But that means instantiating error at a polytype! But error is special
already because you can instantiate it at an unboxed type like Int#.
So I extended the specialness to allow type variables of openTypeKind
to unify with polytypes, regardless of -XImpredicativeTypes.
Conveniently, this works in TcUnify.matchExpectedFunTys, which generates
unification variable for the function arguments, which can be polymorphic.
* GHC has a special typing rule for ($) (see Note [Typing rule
for ($)] in TcExpr). It unifies the argument and result with a
unification variable to exclude unboxed types -- but that means I
now need a kind of unificatdion variable that *can* unify with a
polytype.
So for this sole case I added PolyTv to the data type TcType.MetaInfo.
I suspect we'll find mor uses for this, and the changes are tiny,
but it still feel a bit of a hack. Well the special rule for ($)
is a hack!
There were some consequential changes in error reporting (TcErrors).
compiler/typecheck/TcCanonical.lhs | 21 +++---
compiler/typecheck/TcErrors.lhs | 62 +++++++++++++------
compiler/typecheck/TcExpr.lhs | 9 ++-
compiler/typecheck/TcHsType.lhs | 15 +++--
compiler/typecheck/TcMType.lhs | 10 +++-
compiler/typecheck/TcType.lhs | 118 ++++++++++++++++++++++++-----------
compiler/typecheck/TcUnify.lhs | 79 +++++++++++++++++++-----
7 files changed, 223 insertions(+), 91 deletions(-)
</pre>
TicketsimonpjWed, 31 Oct 2012 09:47:02 GMTstatus changed; testcase, resolution set
http://ghc.haskell.org/trac/ghc/ticket/7264#comment:3
http://ghc.haskell.org/trac/ghc/ticket/7264#comment:3
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>testcase</strong>
set to <em>typecheck/should_fail/T7264</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
Now GHC does not instantiate <code>mmap</code> at a polymorphic type, and we get this error message from the program without the type signature
</p>
<pre class="wiki">T7264.hs:11:19:
Couldn't match type `a' with `forall r. r -> String'
`a' is a rigid type variable bound by
the inferred type of mkFoo2 :: a -> Maybe Foo at T7264.hs:11:1
Expected type: a -> Foo
Actual type: (forall r. r -> String) -> Foo
Relevant bindings include
mkFoo2 :: a -> Maybe Foo (bound at T7264.hs:11:1)
val :: a (bound at T7264.hs:11:8)
In the first argument of `mmap', namely `Foo'
In the expression: mmap Foo (Just val)
In an equation for `mkFoo2': mkFoo2 val = mmap Foo (Just val)
</pre><p>
It's not a fantastic message, but it's on the money, and (without <code>-XImpredicativeTypes</code>) the program should certainly be rejected.
</p>
<p>
Simon
</p>
Ticket