GHC: Ticket #6065: Suggested type signature causes a type error (even though it appears correct)
http://ghc.haskell.org/trac/ghc/ticket/6065
<p>
The attached file, MWE.hs, contains an experiment attempting a rudimentary encoding of extensible ASTs in Haskell (without using compdata or a similar package relying upon OverlappingInstances and so forth). The definition of the upcast function appears to be correct. Compiling without a type signature produces a warning and the suggestion to include a type signature. Including the suggested type signature (which appears to be the correct one) causes a type error.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/6065
Trac 1.2tvynrMon, 30 Apr 2012 18:03:01 GMTattachment set
http://ghc.haskell.org/trac/ghc/ticket/6065
http://ghc.haskell.org/trac/ghc/ticket/6065
<ul>
<li><strong>attachment</strong>
set to <em>MWE.hs</em>
</li>
</ul>
<p>
Example Source
</p>
Ticketrpglover64Tue, 01 May 2012 21:32:17 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:1
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:1
<ul>
<li><strong>cc</strong>
<em>rpglover64</em> added
</li>
</ul>
TicketguestMon, 04 Jun 2012 20:27:52 GMT
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:2
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:2
<p>
I reduced your test case. The following file compiles, but if inferred type signature to "upcast" is added, it doesn't.
</p>
<pre class="wiki">{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}
class AstOp ast result where
astop :: ast -> result
-- upcast :: AstOp ast ((ast -> t) -> t) => ast -> t
upcast ast = astop ast upcast
</pre>
TicketsimonpjTue, 05 Jun 2012 08:03:11 GMTdifficulty set
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:3
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:3
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
<p>
Generally speaking GHC is now much better about <em>not</em> suggesting a type signature that then doesn't work. But it's not perfect and there's a good reason for that. Here's why, if you care, but partly just to record the thinking in the ticket.
</p>
<p>
I'll use a yet-simpler example that demonstrates the problem
</p>
<pre class="wiki">{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}
module T6065 where
class AstOp a b where
astop :: a -> b -> Int
-- upcast :: AstOp a (a -> Int) => a -> Int
upcast ast = astop ast upcast
</pre><p>
When GHC typechecks the RHS of <code>upcast</code> it provisionally gives <code>upcast</code> the (monomorphic) type <code>upcast :: alpha -> beta</code>, where <code>alpha</code> and <code>beta</code> are fresh unification variables. Then it typechecks the RHS of <code>upcast</code>, getting
</p>
<pre class="wiki"> (\ast -> astop ast upcast)
Type :: alpha -> Int
Constraint :: AstOp alpha (alpha -> Int)
(arising from the call to 'astop')
</pre><p>
(<code>beta</code> gets unified to <code>Int</code>.) Now it generalises that type to get
</p>
<pre class="wiki"> upcast :: forall c. AstOp c (c -> Int) => c -> Int
</pre><p>
And that is the type GHE suggests:
</p>
<pre class="wiki">T6065.hs:9:1: Warning:
Top-level binding with no type signature:
upcast :: forall a. AstOp a (a -> Int) => a -> Int
</pre><p>
BUT if we <em>provide</em> this type signature, and then re-type-check the entire definition, we typecheck it with <code>upcast</code> having the above <em>polymorphic</em> type, NOT the old <em>monomorphic</em> type. So the recursive call to <code>upcast</code> is instantiated by instantiating <code>c</code> with a fresh unknown type, say <code>gamma</code>.
So we get this:
</p>
<pre class="wiki"> (\ast -> astop ast upcast)
Type :: alpha -> beta
Constraint :: AstOp alpha (gamma -> Int)
(arising from the call to 'astop')
AstOp gamma (gamma -> Int)
(arising from the recursive call to 'upcast')
</pre><p>
And we can't solve these from the given constraint <code>(AstOp alpha (alpha -> Int))</code>, because nothing forces <code>gamma</code> and <code>alpha</code> to be unified.
</p>
<p>
The problem is that when the recursive call is polymorphic, we get more unknown types (arising from instantiating the type variables of the recursive call to <code>upcast</code>). We can fix that with a type signature such as
</p>
<pre class="wiki">upcast :: forall a. AstOp a (a -> Int) => a -> Int
upcast ast = astop ast (upcast :: a -> Int)
</pre><p>
where the type signature on the RHS fixes <code>gamma</code>. (Needs <code>ScopedTypeVariables</code>.)
</p>
<p>
But that is not the point. The point is that it's very unhelpful for GHC to suggest a type that doesn't work. But
</p>
<ul><li>Even realising that the suggested type doesn't work requires re-generating the constraints from scratch, which is a major (and non-linear) pain.
</li><li>Even if we knew that the suggested type didn't work, it's not clear what complaint to give.
</li></ul><p>
So I'm a bit stuck here, and for now I propose to do nothing. Nice bug report though!
</p>
TicketsimonpjTue, 05 Jun 2012 08:04:14 GMTmilestone set
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:4
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:4
<ul>
<li><strong>milestone</strong>
set to <em>_|_</em>
</li>
</ul>
TickettvynrTue, 05 Jun 2012 12:16:45 GMTattachment set
http://ghc.haskell.org/trac/ghc/ticket/6065
http://ghc.haskell.org/trac/ghc/ticket/6065
<ul>
<li><strong>attachment</strong>
set to <em>MWE2.hs</em>
</li>
</ul>
TickettvynrTue, 05 Jun 2012 12:19:28 GMT
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:5
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:5
<p>
Unfortunately, it seems that the reduced example has lost something; applying the typecast to the upcast function in the original MWE.hs (as shown in the newly-attached MWE2.hs) does not work; the same type error is raised. Does MWE2.hs have the appropriate typecast or did I do something wrong?
</p>
TicketsimonpjTue, 05 Jun 2012 12:39:21 GMT
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:6
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:6
<p>
Type variables only scope if you have an explicit <code>forall</code>. So you need
</p>
<pre class="wiki">upcast :: forall ast1 ast2. (AstOp HomOp ast1 ((ast1 -> ast2) -> ast2)) => ast1 -> ast2
</pre><p>
That compiles fine.
</p>
TickettvynrTue, 05 Jun 2012 13:12:36 GMT
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:7
http://ghc.haskell.org/trac/ghc/ticket/6065#comment:7
<p>
Fair point; sorry about that. :) It compiles fine on my machine as well. Thanks for the workaround!
</p>
Ticket