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 <code>($)</code> 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 <code>forall a. a</code> matched with the bare <code>b</code>. 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.2ganeshTue, 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 <code>(return :: Blob -> IO Blob)</code> fixes the instantiation of <code>return :: forall a. a -> IO a</code> to instantiate <code>a := Blob</code>, 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 "<code>!</code> 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 <code>(apply ::: Blob)</code>, but <code>(:::)</code> 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>
TicketthoughtpoliceMon, 14 Jul 2014 13:04:47 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:13
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:13
<ul>
<li><strong>milestone</strong>
changed from <em>7.6.2</em> to <em>7.10.1</em>
</li>
</ul>
<p>
Moving to 7.10.1.
</p>
TicketthomieSun, 30 Nov 2014 19:23:36 GMTdifficulty set
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:14
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:14
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
<p>
With HEAD, the example from the description works (fails with 7.8.3). I don't know if this is incidental, or if anything got really fixed?
</p>
<pre class="wiki">$ ghci -XRankNTypes
GHCi, version 7.9.20141125: ...
Prelude> let f = id :: (forall a. a) -> (forall b. b)
Prelude>
</pre>
TicketdolioMon, 01 Dec 2014 17:40:48 GMT
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:15
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:15
<p>
To be honest, I'd be fine with closing this ticket. I filed it right around the 6 -> 7 cutover, and evidently thought that the new type checker was still supposed to handle impredicative instantiation. But, the truth is, I think, that if the new algorithm does handle certain impredicative cases, it's more a happy accident than a design principle. So my const example happened to work, but id didn't at the time. I interpreted that as a bug with id rather than being happy that it worked at all for const.
</p>
<p>
I'll leave it to the implementors to decide. If the id example works in 7.10, that's handy. But I've long since stopped considering 'regressions' in impredicative instantiation relative to 6.x actual regressions. It's merely the result a different set of tradeoffs.
</p>
TicketsimonpjMon, 01 Dec 2014 21:47:18 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:16
http://ghc.haskell.org/trac/ghc/ticket/4347#comment:16
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>wontfix</em>
</li>
</ul>
<p>
Dolio is right here. I've backed off from making ANY claims about what GHC does or does not do for impredicative polymorphism. Really the language extension flag should be deprecated because it is not supported either by proper theory about what inference should do, or by an implementation of that theory. Whatever happens right now happens by luck.
</p>
<p>
I'm sure there is a route to a better story for impredicativity; but it is complex territory and there has been much else to do.
</p>
<p>
So yes I'll close this ticket
</p>
<p>
Simon
</p>
Ticket