GHC: Ticket #4347: Bug in unification of polymorphic and not-yet-polymorphic type
http://ghc.haskell.org/trac/ghc/ticket/4347
<p>
The new type checker in GHC 7 seems to reject some cases of impredicative instantiation that prior versions allowed. I was initially alerted to this by Simon Marlow, who sent a patch for vector-algorithms removing a use of <tt>($)</tt> where it would have to be instantiated impredicatively.
</p>
<p>
Initially, I thought this was due to a planned removal of impredicativity, but this cannot be the case, because:
</p>
<pre class="wiki">const :: a -> (forall b. b) -> a
</pre><p>
is accepted by the type checker. However, the simple:
</p>
<pre class="wiki">id :: (forall a. a) -> (forall b. b)
</pre><p>
is not, giving an error message:
</p>
<pre class="wiki"> Couldn't match type `b' with `forall a. a'
`b' is a rigid type variable bound by
an expression type signature at <interactive>:1:32
In the expression: id :: (forall a. a) -> (forall b. b)
</pre><p>
This would seem to indicate that the type is being rewritten to:
</p>
<pre class="wiki">forall b. (forall a. a) -> b
</pre><p>
and then the <tt>forall a. a</tt> matched with the bare <tt>b</tt>. It is, of course, fine to rewrite the type this way, since the two are isomorphic, but it is unfortunate that it causes the checker to reject what would otherwise be a valid instantiation.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/4347
Trac 1.0.1ganeshTue, 28 Sep 2010 15:00:50 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:1
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:1
<ul>
<li><strong>cc</strong>
<em>ganesh</em> added
</li>
</ul>
TicketiglooSat, 13 Nov 2010 13:13:38 GMTmilestone set
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:2
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:2
<ul>
<li><strong>milestone</strong>
set to <em>7.2.1</em>
</li>
</ul>
TicketcarlhowellsMon, 02 May 2011 09:46:22 GMT
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:3
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:3
<p>
I've recently run into this. It's not fun when my code that worked on GHC 6.12 doesn't work on GHC 7. Any chance this'll get done before 7.4?
</p>
TicketcarlhowellsMon, 02 May 2011 09:47:11 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:4
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:4
<ul>
<li><strong>cc</strong>
<em>chowells79@…</em> added
</li>
</ul>
TicketsimonpjMon, 02 May 2011 09:53:07 GMT
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:5
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:5
<p>
Impredicativity has <em>always</em> been a very experimental feature. Although I advertised that we'd remove it altogether, GHC 7 does still support a simple form of impredicativity, but it's simpler than 6.12. For what it's worth, the new support is closely modeled on QML <a class="ext-link" href="http://research.microsoft.com/en-us/um/people/crusso/qml/"><span class="icon"></span>http://research.microsoft.com/en-us/um/people/crusso/qml/</a>
</p>
<p>
Let's be concrete: can you give a small test case, that worked before but not now?
</p>
<p>
Simon
</p>
TicketcarlhowellsMon, 02 May 2011 10:11:26 GMT
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:6
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:6
<p>
Yes, I have a very small example:
</p>
<pre class="wiki">{-# LANGUAGE ImpredicativeTypes #-}
import Control.Concurrent.MVar
import System.Random
dumbTrick :: IO (forall a. Random a => (forall g. RandomGen g => g -> (a, g)) -> IO a)
dumbTrick = do
gen <- newMVar =<< newStdGen
let apply :: forall b. Random b => (forall g'. RandomGen g' => g' -> (b, g')) -> IO b
apply f = modifyMVar gen $ (\(a, b) -> return (b, a)) . f
return apply
</pre>
TicketcarlhowellsMon, 02 May 2011 19:32:16 GMT
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:7
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:7
<p>
The thing that gets to me is this:
</p>
<pre class="wiki">DumbTrick.hs:11:12:
Couldn't match expected type `forall a.
Random a =>
(forall g. RandomGen g => g -> (a, g)) -> IO a'
with actual type `(forall g'. RandomGen g' => g' -> (b0, g'))
-> IO b0'
In the first argument of `return', namely `apply'
In the expression: return apply
In the expression:
do { gen <- newMVar =<< newStdGen;
let apply ::
forall b. Random b =>
(forall g'. RandomGen g' => g' -> (b, g')) -> IO b
apply f = modifyMVar gen $ (\ (a, b) -> ...) . f;
return apply }
</pre><p>
It's telling me that it can't unify two types, there the only difference between the reported types is whether the rank-1 polymorphism is implicit or explicit. (I'm ignoring the lack of reporting on the class constraint because I'm pretty sure that's not relevant.)
</p>
<p>
Furthermore, it does that even when I explicitly quantify the value it's telling me is implicitly quantified.
</p>
<p>
Between those two factors, this feels like a bug, rather a decision to remove a little-used (if awesome) feature.
</p>
TicketsimonpjWed, 04 May 2011 21:05:30 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:8
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:8
<ul>
<li><strong>cc</strong>
<em>dimitris@…</em> added
</li>
</ul>
<p>
Here's a version that works
</p>
<pre class="wiki">type Blob = (forall a. Random a => (forall g. RandomGen g => g -> (a, g)) -> IO a)
dumbTrick :: IO Blob
dumbTrick = do
gen <- newMVar =<< newStdGen
let apply :: forall b. Random b => (forall g'. RandomGen g' => g' -> (b, g')) -> IO b
apply f = modifyMVar gen (\x -> (\(a, b) -> return (b, a)) (f x))
(return :: Blob -> IO Blob) apply
-- ((return apply) :: IO Blob)
</pre><p>
The <tt>(return :: Blob -> IO Blob)</tt> fixes the instantiation of <tt>return :: forall a. a -> IO a</tt> to instantiate <tt>a := Blob</tt>, and then all is well. Bu the commented out line does not work, becuase apply is implicitly instantiated.
</p>
<p>
What GHC lacks at the moment is a "rigid type signature" in the QML sense. If we have that we could write
</p>
<pre class="wiki"> return (apply ! :: Blob)
</pre><p>
where I'm using "<tt>!</tt> to indicate a rigid signature. The "rigid" part means that the polymorphic type is not instantiated, so all will be well.
</p>
<p>
I plan to add rigid type signatures to GHC, but I keep hesitating over syntax. It's quite attractive to use <tt>(apply ::: Blob)</tt>, but <tt>(:::)</tt> is currently available for users so it seems bad to steal it. But maybe worth it. Other ideas welcome.
</p>
<p>
Read the QML paper: it's well explained.
</p>
TicketcarlhowellsWed, 04 May 2011 21:14:38 GMT
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:9
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:9
<p>
Thank you, Simon. The more I thought about the QML overview (I didn't read the full paper), the more I suspected there was an answer like this - "It's possible, but in a way I won't guess without reading the paper or thinking about it a lot. And there's probably some syntax that could make it easier that I don't know about."
</p>
<p>
Now that I see what you did, that does make sense. I wish the error message was a little clearer, though.
</p>
<p>
I guess I need to read the QML paper for the details of this system, though.
</p>
TicketBlaisorbladeSat, 21 May 2011 12:42:33 GMTcc, summary changed
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:10
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:10
<ul>
<li><strong>cc</strong>
<em>p.giarrusso@…</em> added
</li>
<li><strong>summary</strong>
changed from <em>Asymmetry of (impredicative) instantiation/higher rank types</em> to <em>Bug in unification of polymorphic and not-yet-polymorphic type</em>
</li>
</ul>
<p>
I think I'm seeing two instances of this bug in rather more simple contexts. The first involves the id function:
</p>
<pre class="wiki">$ ghci -XScopedTypeVariables -XRank2Types
Prelude> let (id2 :: forall t. t -> t) = \x -> x
<interactive>:1:33:
Couldn't match expected type `t0 -> t1'
with actual type `forall t. t -> t'
The lambda expression `\ x -> x' has one argument,
but its type `forall t. t -> t' has none
In the expression: \ x -> x
In a pattern binding: (id2 :: forall t. t -> t) = \ x -> x
</pre><p>
To me, it seems already buggy that the code is rejected without Rank2Types, because only rank-1 types are involved. I guess that the code requires first-class polymorphism, or that the message might appear only of the main failure. But that unification error? I think it reflects the fact that a term of type (forall t. t -> t), in System F, expects a type argument before a term argument.
That's consistent with the errors shown <a class="ext-link" href="http://stackoverflow.com/questions/5885479/weird-error-when-using-scoped-type-variables-and-the-y-combinator-in-haskell"><span class="icon"></span>here on Stackoverflow</a>.
</p>
<p>
With polymorphic recursion, one gets even no clue about what's happening, just a "couldn't match" message, even if probably due to the same problem. Aren't similar errors supposed to produce similar messages?
</p>
<pre class="wiki">Prelude> let a :: forall b. b -> b = a a
<interactive>:1:31:
Couldn't match expected type `forall b. b -> b'
with actual type `b0 -> b0'
In the first argument of `a', namely `a'
In the expression: a a
In a pattern binding: a :: forall b. b -> b = a a
</pre>
TicketiglooThu, 09 Feb 2012 14:58:07 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:11
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:11
<ul>
<li><strong>milestone</strong>
changed from <em>7.4.1</em> to <em>7.6.1</em>
</li>
</ul>
TicketiglooWed, 12 Sep 2012 11:12:00 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:12
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:12
<ul>
<li><strong>milestone</strong>
changed from <em>7.6.1</em> to <em>7.6.2</em>
</li>
</ul>
Ticket