GHC: Ticket #7220: Confusing error message in type checking related to type family, fundep, and higher-rank type
http://ghc.haskell.org/trac/ghc/ticket/7220
<p>
(This is related to, but different from, the message which I posted to glasgow-haskell-users mailing list: <a class="ext-link" href="http://www.haskell.org/pipermail/glasgow-haskell-users/2012-September/022815.html"><span class="icon"></span>http://www.haskell.org/pipermail/glasgow-haskell-users/2012-September/022815.html</a>.)
</p>
<p>
GHC 7.6.1-rc1 (7.6.0.20120810; 64-bit Windows) rejects the attached code (Test2.hs) with the following error message:
</p>
<pre class="wiki">Test2.hs:24:52:
Couldn't match expected type `Y'
with actual type `TF (forall b. (C A b, TF b ~ Y) => b)'
In the first argument of `f ::
(forall b. (C A b, TF b ~ Y) => b) -> X', namely
`u'
In the expression: (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
In an equation for `v':
v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
</pre><p>
I am not sure whether the code is supposed to be accepted or rejected, but even if it is correct to reject the code, this error message does not look right to me. If I am not mistaken, the error message is saying that the type checker expects the argument of <code>(f :: (forall b. (C A b, TF b ~ Y) => b) -> X)</code> to have type <code>Y</code>, but I cannot think of any reason why it should relate the type <code>(forall b. (C A b, TF b ~ Y) => b)</code> with <code>Y</code>.
</p>
<p>
The same code is available also at <a class="ext-link" href="https://gist.github.com/3606856"><span class="icon"></span>https://gist.github.com/3606856</a>.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/7220
Trac 1.2tsuyoshiWed, 05 Sep 2012 17:37:01 GMTattachment set
http://ghc.haskell.org/trac/ghc/ticket/7220
http://ghc.haskell.org/trac/ghc/ticket/7220
<ul>
<li><strong>attachment</strong>
set to <em>Test2.hs</em>
</li>
</ul>
TickettsuyoshiWed, 05 Sep 2012 18:46:51 GMT
http://ghc.haskell.org/trac/ghc/ticket/7220#comment:1
http://ghc.haskell.org/trac/ghc/ticket/7220#comment:1
<p>
When I posted this report, I had been overlooking <code>TF</code> in the “actual type” part of the error message. Now the error message at least makes some sense.
</p>
<p>
(Although I do not fully understand why the code is rejected in the first place, I think that I have to understand the algorithm used by the type checker to understand this.)
</p>
<p>
I am not sure whether this bug report still makes sense or not. If not, please close it. Sorry about this.
</p>
TicketiglooSat, 20 Oct 2012 22:31:05 GMTowner, difficulty, milestone set
http://ghc.haskell.org/trac/ghc/ticket/7220#comment:2
http://ghc.haskell.org/trac/ghc/ticket/7220#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, could you take a look at this please?
</p>
TicketsimonpjWed, 31 Oct 2012 17:13:34 GMTstatus changed; testcase, resolution set
http://ghc.haskell.org/trac/ghc/ticket/7220#comment:3
http://ghc.haskell.org/trac/ghc/ticket/7220#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/T7220</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
"I cannot think of any reason why it should relate the type (forall b. (C A b, TF b ~ Y) => b) with Y". Here's why:
</p>
<pre class="wiki">u :: (C A b, TF b ~ Y) => b
u = undefined
v :: X
v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
</pre><ul><li>GHC instanatiates the occurence of <code>u</code>, given type just <code>beta</code>, where <code>beta</code> is a fresh unification variable. Plus constraints <code>(C A beta, TF beta ~ Y)</code>.
</li></ul><ul><li>Now it tries to unify <code>beta</code> with the expected arugment type of the <code>(f :: sig)</code> expression. This argument type is <code>(forall b. (C A b, TF b ~ Y) => b)</code>
</li></ul><ul><li>So GHC (until today) would unify <code>beta := forall b. (C A b, TF b ~ Y) => b</code>.
</li></ul><ul><li>So the constraint <code>(TF beta ~ Y)</code> turns into (TF (forall b. (C A b, TF b ~ Y) => b) ~ Y)`, and that's the error you saw.
</li></ul><p>
But really GHC should not have taken the third step above (at least not without <code>-XImpredicativeTypes</code>). With the patch that fixes <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/6069" title="#6069: bug: Rank 2 Polymorphism Compile Error (closed: fixed)">#6069</a> and <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/7264" title="#7264: bug: Adding GHC's inferred type signatures to a working program can make it ... (closed: fixed)">#7264</a> it no longer does so, yielding instead
</p>
<pre class="wiki">T7220.hs:24:6:
Cannot instantiate unification variable `b0'
with a type involving foralls: forall b. (C A b, TF b ~ Y) => b
Perhaps you want -XImpredicativeTypes
In the expression: f :: (forall b. (C A b, TF b ~ Y) => b) -> X
In the expression: (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
In an equation for `v':
v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
</pre><p>
which isn't fantastic but is perhaps less confusing than before.
</p>
TicketsimonpjTue, 11 Nov 2014 10:36:05 GMT
http://ghc.haskell.org/trac/ghc/ticket/7220#comment:4
http://ghc.haskell.org/trac/ghc/ticket/7220#comment:4
<p>
Richard's fix for <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/9404" title="#9404: bug: tcInferRho muddies the waters (closed: fixed)">#9404</a> makes this compile. He says:
</p>
<p>
The reason this went wrong before is that the old method of inferring a type would get caught when unifying a <code>TauTv</code> (the metavariable given as the guess for <code>f</code>'s type) with a polytype, deferring to the solver. If we defer, then we don't have enough information to type-check <code>u</code> successfully, and we fail.
With the new inferring types with <code>PolyTv</code>, no deferring happens, and <code>u</code> type-checks fine.
</p>
<p>
But with the <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/9404" title="#9404: bug: tcInferRho muddies the waters (closed: fixed)">#9404</a> fix, <code>f</code> is inferred to have the type as given. Then, <code>u</code> is checked (by <code>tcPolyExprNC</code>) to have the argument type of <code>f</code>, which it does. No problems.
</p>
<p>
I actually think that success is the right behavior here, so I chalk this up to a success of this patch.
</p>
TicketSimon Peyton Jones <simonpj@…>Fri, 21 Nov 2014 13:02:51 GMT
http://ghc.haskell.org/trac/ghc/ticket/7220#comment:5
http://ghc.haskell.org/trac/ghc/ticket/7220#comment:5
<p>
In <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/7b1a8562d9b92547251d0dff23bb3a2de25d4b6f/ghc" title="Fix up tests for Trac #7220; the old test really was ambiguous">7b1a8562d9b92547251d0dff23bb3a2de25d4b6f/ghc</a>:
</p>
<pre class="message">Fix up tests for Trac #7220; the old test really was ambiguous</pre>
Ticket