GHC: Ticket #6069: Rank 2 Polymorphism Compile Error
http://ghc.haskell.org/trac/ghc/ticket/6069
<p>
Not sure if this is a bug, perhaps this should be a feature request.
</p>
<p>
Given the following code:
</p>
<pre class="wiki">{-# LANGUAGE Rank2Types #-}
import Control.Monad.ST
import Data.STRef
fourty_two :: forall s. ST s Int
fourty_two = do
x <- newSTRef (42::Int)
readSTRef x
main = (print . runST) fourty_two -- (1)
main = (print . runST) $ fourty_two -- (2)
main = ((print . runST) $) fourty_two -- (3)
</pre><p>
(1) and (3) compile successfully, but (2) does not. I'm not sure why this is the case.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/6069
Trac 1.2clintonWed, 02 May 2012 02:25:26 GMTos, architecture changed
http://ghc.haskell.org/trac/ghc/ticket/6069#comment:1
http://ghc.haskell.org/trac/ghc/ticket/6069#comment:1
<ul>
<li><strong>os</strong>
changed from <em>Windows</em> to <em>Unknown/Multiple</em>
</li>
<li><strong>architecture</strong>
changed from <em>x86_64 (amd64)</em> to <em>Unknown/Multiple</em>
</li>
</ul>
TicketiglooTue, 09 Oct 2012 14:58:07 GMTowner, difficulty, milestone set
http://ghc.haskell.org/trac/ghc/ticket/6069#comment:2
http://ghc.haskell.org/trac/ghc/ticket/6069#comment:2
<ul>
<li><strong>owner</strong>
set to <em>simonpj</em>
</li>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
<li><strong>milestone</strong>
set to <em>7.8.1</em>
</li>
</ul>
<p>
Simon, this looks like your area.
</p>
TicketsimonpjTue, 09 Oct 2012 21:32:14 GMT
http://ghc.haskell.org/trac/ghc/ticket/6069#comment:3
http://ghc.haskell.org/trac/ghc/ticket/6069#comment:3
<p>
Really all three should be rejected without <code>-XImpredicativeTypes</code>, because all require instantiating <code>(.)</code> at a polymorphic type. The inconsistent behaviour is a bug.
</p>
<p>
Simon
</p>
Ticketsimonpj@…Wed, 31 Oct 2012 09:18:11 GMT
http://ghc.haskell.org/trac/ghc/ticket/6069#comment:4
http://ghc.haskell.org/trac/ghc/ticket/6069#comment:4
<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:55:46 GMTstatus changed; testcase, resolution set
http://ghc.haskell.org/trac/ghc/ticket/6069#comment:5
http://ghc.haskell.org/trac/ghc/ticket/6069#comment:5
<ul>
<li><strong>testcase</strong>
set to <em>typecheck/should_fail/T6069</em>
</li>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
Now all three fail, as they should, and fail in the same way:
</p>
<pre class="wiki">T6069.hs:13:15:
Couldn't match type `ST s0 Int' with `forall s. ST s b0'
Expected type: ST s0 Int -> b0
Actual type: (forall s. ST s b0) -> b0
In the second argument of `(.)', namely `runST'
In the expression: print . runST
In the expression: (print . runST) fourty_two
T6069.hs:14:15:
Couldn't match type `ST s1 Int' with `forall s. ST s b1'
Expected type: ST s1 Int -> b1
Actual type: (forall s. ST s b1) -> b1
In the second argument of `(.)', namely `runST'
In the expression: (print . runST)
In the expression: (print . runST) $ fourty_two
T6069.hs:15:16:
Couldn't match type `ST s2 Int' with `forall s. ST s b2'
Expected type: ST s2 Int -> b2
Actual type: (forall s. ST s b2) -> b2
In the second argument of `(.)', namely `runST'
In the first argument of `($)', namely `(print . runST)'
In the expression: (print . runST) $
</pre>
Ticket