GHC: Ticket #5978: Type error in one function causes wrong type error report in another function in the presence of functionally dependent types
http://ghc.haskell.org/trac/ghc/ticket/5978
<p>
When trying to reduce my problem in <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/5970" title="#5970: bug: Type checker hangs (closed: wontfix)">#5970</a> to a simple program I encountered an even more obvious bug. The problem is essentially as follows: I have
</p>
<pre class="wiki">correct :: T
correct = ...
wrong :: T
wrong = f correct
</pre><p>
where 'wrong' has a type error and 'correct' is type correct. If I outcomment 'wrong' then GHC correctly confirms type-correctness of 'correct', but if 'wrong' is enabled then GHC claims a type error in both 'wrong' and 'correct'.
To me it looks like the type-checker is trying to unify types across function boundaries. This would explain both non-linear growth of type-checking time and the observed effect of incorrect type errors.
See attached program for a working example.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/5978
Trac 1.2LemmingWed, 28 Mar 2012 22:57:37 GMTattachment set
http://ghc.haskell.org/trac/ghc/ticket/5978
http://ghc.haskell.org/trac/ghc/ticket/5978
<ul>
<li><strong>attachment</strong>
set to <em>TypeCheck7_4_1.hs</em>
</li>
</ul>
TicketsimonpjThu, 29 Mar 2012 06:59:30 GMTdifficulty set
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:1
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:1
<ul>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
</ul>
<p>
Can you explain how to reproduce? Is <code>monoBar</code> the <code>correct</code>? Or <code>monoFoo</code>?
</p>
TicketLemmingThu, 29 Mar 2012 07:58:13 GMT
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:2
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:2
<p>
Sorry ... monoFoo is correct and monoBar is incorrect.
But when I compile that module GHC reports two type errors: One for monoFoo and one for monoBar.
If I remove monoBar, then monoFoo is accepted by GHC.
</p>
<p>
The result of monoBar is Double, thus fromB=Double.
The argument of polyBar in monoBar is of type Float, thus fromA=Float.
From the functional dependencies it follows toB=Bool and toA=Char.
Thus id would need type Char -> Bool, which is a type error and this one is correctly spotted by GHC.
But additionally also a type error for monoBar is reported, although monoBar is correct.
It has type Float and it follows to=Char, but the 'to' type is not used in monoBar.
</p>
TicketsimonpjThu, 29 Mar 2012 09:01:47 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:3
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:3
<ul>
<li><strong>cc</strong>
<em>dimitris@…</em> added
</li>
</ul>
<p>
OK I see what is happening. From the two definitions we get these "wanted" constraints:
</p>
<pre class="wiki">monoFoo: mf1: C Float alpha
monoBar: mb1: C Float beta,
mb2: C Double beta
</pre><p>
where <code>alpha</code> and <code>beta</code> are otherwise-unconstrained unification variables.
</p>
<p>
Now if we first do fundeps wrt the <code>instance</code> decls, we get <code>alpha = Char</code> from <code>mf1</code>, <code>beta = Char</code> from <code>mb1</code> and <code>beta = Bool</code> from <code>mb2</code>, the latter two yield an error.
</p>
<p>
But if we first do fundeps <em>between</em> the wanted constraints, we get <code>alpha = beta</code>, so that leaves us with <code>(mf1: C Float alpha, mb2: C Double alpha)</code>. Now we can solve <code>mb2</code> via the fundep with the <code>instance</code> to give <code>alpha=Bool</code>, and that leaves an error for the innocent <code>mf1</code>!
</p>
<p>
Even this isn't quite what happens. Functional dependencies are a pain.
</p>
<p>
Simon
</p>
TicketLemmingThu, 29 Mar 2012 09:18:43 GMT
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:4
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:4
<p>
Would you suggest that I convert my code to type families?
</p>
TicketsimonpjThu, 29 Mar 2012 09:36:58 GMT
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:5
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:5
<p>
I would certainly give type families a try, yes. I'd be interested to hear how it goes.
</p>
TicketLemmingThu, 26 Apr 2012 15:29:57 GMT
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:6
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:6
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/5978#comment:5" title="Comment 5">simonpj</a>:
</p>
<blockquote class="citation">
<p>
I would certainly give type families a try, yes. I'd be interested to hear how it goes.
</p>
</blockquote>
<p>
I have converted some of my code to type families. Unfortunately, since I depend on the llvm package, the code is now quite inconsistent, because llvm uses a lot of functional dependencies and it uses in turn the type-level package that requires even more functional dependencies. Thus for now I cannot get rid of the problematic code. My hope is that we can remove all of these functional dependencies when the type level naturals (<a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/4385" title="#4385: feature request: Type-level natural numbers (new)">#4385</a>) become part of GHC HEAD.
</p>
TicketsimonpjThu, 26 Apr 2012 15:40:55 GMT
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:7
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:7
<p>
OK. So the error message is a bit odd. Could be fixed, with some work. But as I undrestand it, this ticket is not standing in anyone's path. It's just a "nice to have" possible improvement, right?
</p>
TicketLemmingThu, 26 Apr 2012 15:51:21 GMT
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:8
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:8
<p>
At first I thought that the type checker is wrong, since it reports a type error where no type error is. If I understand you correctly, then GHC still correctly identifies type correct and type incorrect programs, only the error message is misleading. If so, then this bug has no high priority for me.
You may simply add "if this type error message confuses you, then better switch to type families" to every type error message concerning functional dependencies. :-)
</p>
TicketLemmingSun, 17 Jun 2012 12:40:40 GMT
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:9
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:9
<p>
Now I got the same problem with type families and without functional dependencies.
</p>
TicketLemmingMon, 18 Jun 2012 18:46:59 GMT
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:10
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:10
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/5978#comment:9" title="Comment 9">Lemming</a>:
</p>
<blockquote class="citation">
<p>
Now I got the same problem with type families and without functional dependencies.
</p>
</blockquote>
<p>
I have opened a new ticket for the issue with type families: <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/7010" title="#7010: bug: Type error in one function causes wrong type error report in another ... (closed: fixed)">#7010</a>.
</p>
TicketpcapriottiWed, 20 Jun 2012 15:33:39 GMTpriority changed; milestone set
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:11
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:11
<ul>
<li><strong>priority</strong>
changed from <em>normal</em> to <em>low</em>
</li>
<li><strong>milestone</strong>
set to <em>7.6.1</em>
</li>
</ul>
TicketsimonpjSat, 14 Jul 2012 12:51:50 GMTstatus changed; testcase, resolution set
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:12
http://ghc.haskell.org/trac/ghc/ticket/5978#comment:12
<ul>
<li><strong>testcase</strong>
set to <em>typecheck/should_fail/T5978</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>
Recent changes in the type inference engine mean that you now get just one error, and on <code>monoBar</code>. To be honest I'm not 100% certain of why this has come right, and that means I'm not certain that the solution is robust (mabye it's a fluke). But I'm sort of time, so I'm closing the ticket. But I'm adding the test as a regression test so we'll know immediately if it stops working.
</p>
<p>
Thanks for the example.
</p>
<p>
Simon
</p>
Ticket