GHC: Ticket #10141: CUSK mysteries
http://ghc.haskell.org/trac/ghc/ticket/10141
<p>
Take the following definition:
</p>
<div class="wiki-code"><div class="code"><pre><span class="kr">type</span> <span class="kr">family</span> <span class="kt">G</span> <span class="p">(</span>a <span class="ow">::</span> k<span class="p">)</span> <span class="kr">where</span>
<span class="kt">G</span> <span class="kt">Int</span> <span class="ow">=</span> <span class="kt">Bool</span>
<span class="kt">G</span> <span class="kt">Bool</span> <span class="ow">=</span> <span class="kt">Int</span>
<span class="kt">G</span> a <span class="ow">=</span> a
</pre></div></div><p>
It compiles in 7.8.3, but not in 7.10.1 RC2. This makes me sad. I will fix.
</p>
<p>
(Found by Jan Stolarek.)
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/10141
Trac 1.2.2simonpjFri, 06 Mar 2015 17:22:20 GMT
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:1
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:1
<p>
This looks bad. Release blocker? I assume so. Say if not.
</p>
TicketgoldfireSun, 08 Mar 2015 05:32:49 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:2
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:2
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>invalid</em>
</li>
</ul>
<p>
This is by design. As I discovered en route to the solution to <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/9200" title="#9200: bug: Milner-Mycroft failure at the kind level (closed: fixed)">#9200</a>, the old kind inference for closed type families was bogus. For the type family above, what should the return kind be? <code>k</code>, <code>k2</code>, and <code>*</code> are all viable options. Thus, this type family has no principal kind and should be rejected.
</p>
<p>
Another was of looking at this is that <code>G</code> does not have a CUSK. Therefore, its right-hand side must use kind variables uniformly -- which it doesn't, because the first two equations must specialize <code>k</code> to <code>*</code>.
</p>
<p>
So, closing as invalid.
</p>
TicketrwbartonSun, 08 Mar 2015 16:30:58 GMT
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:3
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:3
<p>
In this particular case, given the third equation <code>G a = a</code>, I'm pretty sure the only possible return kind is <code>k</code>, no? But there was that whole long discussion about CUSKs that I didn't really follow, so I take it that in general a closed type family may have no principal kind.
</p>
<p>
I would venture to say though that the error message GHC produces is IMHO not that helpful. In this case the fix is clearly to add a CUSK <code>type family G (a :: k) :: k where</code>; could GHC work out when it is appropriate to suggest adding a CUSK?
</p>
TicketjstolarekSun, 08 Mar 2015 17:58:26 GMTstatus changed; owner, resolution deleted
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:4
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:4
<ul>
<li><strong>owner</strong>
<em>goldfire</em> deleted
</li>
<li><strong>status</strong>
changed from <em>closed</em> to <em>new</em>
</li>
<li><strong>resolution</strong>
<em>invalid</em> deleted
</li>
</ul>
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/10141#comment:2" title="Comment 2">goldfire</a>:
</p>
<blockquote class="citation">
<p>
So, closing as invalid.
</p>
</blockquote>
<p>
I believe we should create a test case so that any accidental change of semantics does not go unnoticed (like it seems to have between 7.8.3 and 7.10.1?). Richard, I'm re-opening and assigning to you but if you don't have the time please re-assign it to me - I'll take care of that in due time.
</p>
TicketjstolarekSun, 08 Mar 2015 17:58:49 GMTowner set
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:5
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:5
<ul>
<li><strong>owner</strong>
set to <em>goldfire</em>
</li>
</ul>
TicketgoldfireMon, 09 Mar 2015 05:30:16 GMT
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:6
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:6
<p>
Responding to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/10141#comment:3" title="Comment 3">comment:3</a>:
</p>
<p>
No, the return kind could well be <code>*</code>. I'll rewrite with explicit kinds:
</p>
<pre class="wiki">type family G (a :: k) :: * where
G * Int = Bool
G * Bool = Int
G * a = a
</pre><p>
This <code>G</code> doesn't really use its kind-polymorphism, but the definition kind checks.
</p>
<p>
However, I think you're right about the suggestion for a CUSK, here and in other cases. And I think it's possible for GHC to have at least some heuristics for when a CUSK is the answer. Specifically, it could include a note about CUSKs in error messages that arise from kind mismatches in non-CUSK right-hand sides.
</p>
<p>
And, yes, this would make for a decent test case. Thanks for the suggestion.
</p>
<p>
I'm very unsure I can get to this by Friday (the next RC release), though!
</p>
TicketgoldfireMon, 09 Mar 2015 05:30:32 GMTpriority changed
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:7
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:7
<ul>
<li><strong>priority</strong>
changed from <em>highest</em> to <em>normal</em>
</li>
</ul>
TicketthoughtpoliceTue, 17 Mar 2015 16:52:27 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:8
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:8
<ul>
<li><strong>milestone</strong>
changed from <em>7.10.1</em> to <em>7.12.1</em>
</li>
</ul>
<p>
Moving to 7.12.1 milestone.
</p>
TicketgoldfireFri, 24 Apr 2015 02:16:48 GMT
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:9
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:9
<p>
I've added a (not-yet-pushed) test case, but it's hard to see how to improve error messages. The problem is that the place that generates the kind errors is far from where we know whether or not we have a CUSK. I attempted to use <code>addErrCtxt</code> to include a note about CUSKs before kind-checking, but this note got appended to lots of errors that are clearly unrelated to CUSKs -- this is the wrong approach. I think the right approach is to somehow record in <code>TcM</code> that we're kind-checking a declaration which could potentially have a CUSK but in fact does not and then look there before reporting certain errors. But this is terribly heavy.
</p>
<p>
Perhaps after my branch is merged, a way forward will present itself.
</p>
TicketRichard Eisenberg <eir@…>Fri, 24 Apr 2015 21:02:03 GMT
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:10
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:10
<p>
In <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/dc587fe7f27e2bc762d8a6cae3687ca2ebbbdb9b/ghc" title="Test case for #10141">dc587fe7f27e2bc762d8a6cae3687ca2ebbbdb9b/ghc</a>:
</p>
<pre class="message">Test case for #10141</pre>
TicketsimonpjFri, 24 Apr 2015 21:11:38 GMTtestcase set
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:11
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:11
<ul>
<li><strong>testcase</strong>
set to <em>indexed-types/should_fail/T10141</em>
</li>
</ul>
TicketthoughtpoliceFri, 11 Sep 2015 08:38:26 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:12
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:12
<ul>
<li><strong>milestone</strong>
changed from <em>7.12.1</em> to <em>8.0.1</em>
</li>
</ul>
<p>
Milestone renamed
</p>
TicketthomieSun, 24 Jan 2016 16:26:27 GMTkeywords set
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:13
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:13
<ul>
<li><strong>keywords</strong>
<em>TypeFamilies</em> added
</li>
</ul>
TicketbgamariSat, 12 Mar 2016 00:24:16 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:14
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:14
<ul>
<li><strong>milestone</strong>
changed from <em>8.0.1</em> to <em>8.2.1</em>
</li>
</ul>
<p>
This bug won't be fixed in 8.0.1; bumping to 8.2.
</p>
TicketsimonpjWed, 08 Feb 2017 17:32:34 GMTsummary changed
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:15
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:15
<ul>
<li><strong>summary</strong>
changed from <em>Kind inference regression in closed type families</em> to <em>CUSK mysteries</em>
</li>
</ul>
<p>
Here's an example that I was baffled by. This works
</p>
<pre class="wiki">type family F (a :: k)
type instance F Maybe = Char
</pre><p>
But this does not.
</p>
<pre class="wiki">type family F (a :: k) where -- = r | r -> a where
F Maybe = Char
</pre><p>
The latter is rejected with
</p>
<pre class="wiki">Foo.hs:6:5: error:
* Expecting one more argument to `Maybe'
Expected kind `k', but `Maybe' has kind `* -> *'
* In the first argument of `F', namely `Maybe'
In the type family declaration for `F'
</pre><p>
It is bizarre that one works and the other does not, and I was all ready to open a ticket when Richard said: This is correct behavior. The former has a CUSK, as all open type families have CUSKs with un-annotated kinds defaulting to Type. The latter does not have a CUSK, because the result kind is unknown. You therefore cannot specialize the k variable in the definition of the latter.
</p>
<p>
I can't help feeling that our CUSK story is a bit wonky, so I'm recording it here.
</p>
TicketsimonpjWed, 08 Feb 2017 17:35:57 GMTkeywords changed
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:16
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:16
<ul>
<li><strong>keywords</strong>
<em>TypeInType</em> added
</li>
</ul>
TicketgoldfireThu, 09 Feb 2017 02:21:49 GMT
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:17
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:17
<p>
If you want <code>TypeInType</code> to mean "Richard's bailiwick", that's perhaps convenient. But I'll note that this problem has nothing to do with <code>-XTypeInType</code> and exists in 7.10 and perhaps 7.8.
</p>
TicketbgamariWed, 05 Apr 2017 21:02:05 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:18
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:18
<ul>
<li><strong>milestone</strong>
changed from <em>8.2.1</em> to <em>8.4.1</em>
</li>
</ul>
<p>
Given that 8.2.1-rc1 is imminent, I'm bumping these off to the 8.4
</p>
TicketbgamariSun, 21 Jan 2018 16:28:11 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:19
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:19
<ul>
<li><strong>milestone</strong>
changed from <em>8.4.1</em> to <em>8.6.1</em>
</li>
</ul>
<p>
This ticket won't be resolved in 8.4; remilestoning for 8.6. Do holler if you are affected by this or would otherwise like to work on it.
</p>
TicketbgamariMon, 19 Mar 2018 22:20:56 GMTdescription changed; milestone deleted
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:20
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:20
<ul>
<li><strong>description</strong>
modified (<a href="/trac/ghc/ticket/10141?action=diff&version=20">diff</a>)
</li>
<li><strong>milestone</strong>
<em>8.6.1</em> deleted
</li>
</ul>
<p>
Removing milestone as no one is actively looking at this.
</p>
TicketRyanGlScottSun, 27 May 2018 13:36:40 GMTkeywords changed
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:21
http://ghc.haskell.org/trac/ghc/ticket/10141#comment:21
<ul>
<li><strong>keywords</strong>
<em>CUSKs</em> added
</li>
</ul>
Ticket