GHC: Ticket #7939: RHS of associated type not kind-checked
http://ghc.haskell.org/trac/ghc/ticket/7939
<p>
The following code compiles without complaint:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, PolyKinds #-}
class Foo a where
type Bar a
instance Foo Int where
type Bar Int = Maybe
instance Foo Bool where
type Bar Bool = Double
</pre><p>
We can see here that <code>Bar</code> is ill-kinded. When I try <code>:k Bar</code> in GHCi, I get an assertion failure, not unexpectedly.
</p>
<p>
I will fix in ongoing work.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/7939
Trac 1.2.2.dev0goldfireMon, 27 May 2013 09:47:23 GMT
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:1
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:1
<p>
This problem is a little worse than I thought. With just
</p>
<pre class="wiki">class Foo a where
type Bar a
</pre><p>
(with <code>-XPolyKinds</code>), I get an assertion failure in GHCi on <code>:k Bar</code>.
</p>
Ticketsimonpj@…Tue, 28 May 2013 08:25:48 GMT
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:2
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:2
<p>
commit <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/3d0d8d02b0f1359813eed00c0910cb6729460a13/ghc" title="Do not do an ambiguity check on the type in a GHCi ":kind" command
...">3d0d8d02b0f1359813eed00c0910cb6729460a13</a>
</p>
<pre class="wiki">Author: Simon Peyton Jones <simonpj@microsoft.com>
Date: Mon May 27 17:27:33 2013 +0100
Do not do an ambiguity check on the type in a GHCi ":kind" command
Otherwise we get errors for polykinded type families;
type family F a :: *
Then :k F
would give an ambiguity check trying to unify (F k1) with (F k2),
which is all a bit stupid.
I found this when investigating Trac #7939
compiler/typecheck/TcValidity.lhs | 6 ++++++
1 files changed, 6 insertions(+), 0 deletions(-)
</pre>
TicketsimonpjTue, 28 May 2013 08:47:42 GMTstatus changed; testcase, difficulty, resolution set
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:3
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:3
<ul>
<li><strong>testcase</strong>
set to <em>ghci/scripts/T7939</em>
</li>
<li><strong>difficulty</strong>
set to <em>Unknown</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>
I think the main error was fixed by my improvements to kind generalisation, late last week.
</p>
<p>
Simon
</p>
TicketmonoidalWed, 19 Jun 2013 16:22:30 GMTstatus changed; owner, resolution deleted
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:4
http://ghc.haskell.org/trac/ghc/ticket/7939#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>fixed</em> deleted
</li>
</ul>
<p>
Something is suspicious here.
</p>
<p>
GHC accepts original program
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, PolyKinds #-}
class Foo a where
type Bar a
instance Foo Int where
type Bar Int = Maybe
instance Foo Bool where
type Bar Bool = Double
</pre><p>
but rejects
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, PolyKinds #-}
type family Baz a
type instance Baz Int = Maybe
type instance Baz Bool = Double
</pre><p>
Is this really expected? Even more, you can write
</p>
<pre class="wiki">instance Foo Bool where
type Bar Bool = Double
type Bar Bool = Maybe
</pre>
TicketmonoidalWed, 19 Jun 2013 23:18:42 GMT
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:5
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:5
<p>
Aha - <code>type Bar a</code> in a typeclass declaration defaults to <code>type Bar a :: k</code>, while <code>type family Baz a</code> defaults to <code>type family Baz a :: *</code>. This is a slight inconsistency.
</p>
<p>
Meanwhile, we can also write
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, PolyKinds #-}
type family A :: k
type instance A = Double
type instance A = Maybe
</pre>
TicketsimonpjFri, 21 Jun 2013 17:13:48 GMT
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:6
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:6
<p>
Well analysed.
</p>
<ul><li>The inconsistency seems to be deliberate; look at <code>TcTyClDecls.getFamDeclInitialKind</code>. But there is no explanation of why the difference, so I think we should abolish the difference until proved otherwise.
</li></ul><ul><li>With <code>-XPolyKinds</code> we get kind polymorphism by default in data decls. Eg
<pre class="wiki">data T f a = MkT (f a)
</pre>we get <code>T :: (k -> *) -> k -> *</code>.
</li></ul><ul><li>By the same token it is perhaps reasonable that
<pre class="wiki">type family F a :: *
</pre>gives <code>F :: k -> *</code>
</li></ul><ul><li>But getting polykinded <em>result</em> kind by default (even with <code>-XPolyKinds</code>) seems odd to me:
<pre class="wiki">type family F a
</pre>Do we really want <code>F :: k1 -> k2</code>?
</li></ul><p>
My suggestion is that we adopt the current top-level story, namely that the result kind of a type family is <code>*</code> unless you explicitly use a kind variable. That's inconsistent with the argument story, but the examples you give above really are quite confusing
</p>
<p>
Comments, anyone? The fix is easy either way.
</p>
<p>
Simon
</p>
TicketgoldfireMon, 24 Jun 2013 22:43:03 GMT
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:7
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:7
<p>
I tend to agree that generalizing the result kind (without an explicit annotation) is a step too far. In general, I'm happy with the current story that type family arguments and results default to <code>*</code>. Because instances aren't provided at the same place as the family declaration, any sort of kind inference amounts to some level of spooky action at a distance. Note that the kind inference for datatypes looks only at the declaration of the constructors, not any uses of the type. Similarly, the kind inference for classes only looks at the methods/other members of the class, not any instances. For consistency with those cases, I would expect for type families either (everything defaults to <code>*</code>) or (everything defaults to fresh kind variables). The former gives better errors in the common case, so I favor that one.
</p>
TicketsimonpjTue, 25 Jun 2013 13:31:12 GMTowner set
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:8
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:8
<ul>
<li><strong>owner</strong>
set to <em>goldfire</em>
</li>
</ul>
<p>
Richard is going to implement (and document) the story I describe above, as part of adding kind inference for closed type families, in the next few days.
</p>
<p>
Simon
</p>
TicketmonoidalTue, 25 Jun 2013 15:42:42 GMT
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:9
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:9
<p>
I think it's fine to default to *. But, again, consider
</p>
<pre class="wiki">type family A :: k
type instance A = Double
type instance A = Maybe
</pre><p>
Should this really compile? I don't know, it looks suspicious but perhaps it is OK.
</p>
<p>
What makes me suspicious is this. Consider
</p>
<pre class="wiki">data D :: k -> * where
D1 :: D Bool
D2 :: D Maybe
</pre><p>
GHC gives an error:
</p>
<pre class="wiki"> Data constructor `D1' cannot be GADT-like in its *kind* arguments
D1 :: D * Bool
</pre><p>
But this seemingly equivalent code compiles:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, GADTs, PolyKinds #-}
type family A :: k
type instance A = Bool
type family B :: k
type instance B = Maybe
data D :: k -> * where
D1 :: D A
D2 :: D B
</pre>
TicketgoldfireWed, 26 Jun 2013 15:50:04 GMT
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:10
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:10
<p>
I've implemented the plan above, but there is still at least one dark corner. Consider this:
</p>
<pre class="wiki">class Foo a where
type Bar a b
</pre><p>
What should the kind of <code>Bar</code> be? Because classes are kind-polymorphic by default (which is good), the kind of <code>a</code> must be <code>k</code>. But, what about <code>b</code>? Right now, in both HEAD and my implementation with the fix for this ticket, <code>Bar</code> has the kind <code>k1 -> k2 -> *</code>. We don't generalize the result kind (as described above), but we still do generalize all arguments. It wouldn't be hard to separate out the arguments that are bound in the class head, generalize those and not generalize the others, but that seems even stranger somehow.
</p>
<p>
Thoughts?
</p>
<p>
Expect a patch soon.
</p>
TicketgoldfireWed, 26 Jun 2013 15:58:34 GMT
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:11
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:11
<p>
In response to monoidal's most recent comment:
</p>
<p>
I'm fine with your definition for <code>A</code>. It is deeply strange-looking, I agree, but if we make the kind applications explicit, it's quite normal:
</p>
<pre class="wiki">type family A (k :: BOX) :: k
type instance A * = Double
type instance A (* -> *) = Maybe
</pre><p>
As for the GADT example, I find that more interesting. Let's make everything more explicit:
</p>
<pre class="wiki">type family A (k :: BOX) :: k
type instance A * = Bool
type family B (k :: BOX) :: k
type instance B (* -> *) = Maybe
data D :: forall (k :: BOX). k -> * where
D1 :: forall (k :: BOX). D k (A k)
D2 :: forall (k :: BOX). D k (B k)
</pre><p>
Now, <code>D</code> doesn't look GADT-like in its kind parameter, which is always just <code>k</code>. The difference between the version that works and the version that doesn't is that pattern-matching on the version that works does <em>not</em> refine information about the kind <code>k</code>. In fact, you can see this easily because you can write more instances for either <code>A</code> or <code>B</code> showing that the kind argument is not really fixed by this construction.
</p>
TicketsimonpjWed, 26 Jun 2013 20:47:53 GMT
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:12
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:12
<p>
Concerning the dark corner, there is a reason that classes are by-default kind-polymorphic: there are some visible uses of the type variable to constraint it. Consider
</p>
<pre class="wiki">class C a where { opc :: a -> a }
class D f b where { opd :: f b -> f b }
</pre><p>
Then, just as in a data type declaration, we look at the uses of type variables <code>a</code>, <code>f</code>, <code>b</code>, and get these kinds:
</p>
<pre class="wiki">C :: * -> Constraint
D :: (k -> *) -> k -> Constraint
</pre><p>
This is good. It is very different for a top-level open type family
</p>
<pre class="wiki">type family F a b
</pre><p>
Here there are no uses, and hence no kind constraints, on <code>a</code> and <code>b</code>, and there can't be. But it seems over-kill to assume maximal polymorphism, so our plan is to default to *, thus
</p>
<pre class="wiki">F :: * -> * -> *
</pre><p>
Now, with the associated type you give, there's a mixture of the two:
</p>
<pre class="wiki">class Foo a where
type Bar a b
op :: a -> a
</pre><p>
Here there probably <em>are</em> some constraints on <code>a</code> (from the class methods as usual), but there can be none on <code>b</code>. So my suggestion would be to default <code>b</code> to <code>*</code>, just like for top-level ones, but to constrain <code>a</code> by the way it is used in class methods and superclasses. That's a bit more complicated in a way, but there is a principled reason:
</p>
<ul><li>If there is some "scope" for the variable, infer the kind from its uses
</li><li>If there is no "scope", use <code>*</code>, unless there's a kind annotation.
</li></ul><p>
Simon
</p>
TicketgoldfireWed, 26 Jun 2013 21:53:27 GMT
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:13
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:13
<p>
As I was looking at all of this, I wasn't sure what to do about type variables like <code>b</code> above. My decision to leave it to be polymorphic was mostly from a lack of a clearly-articulated reason why some variables are polymorphic and some aren't.
</p>
<p>
However, I don't think Simon's "scope" rule really does it.
</p>
<p>
Currently, variables are kind-polymorphic-by-default in the following places:
</p>
<ul><li>Class definitions
</li><li>Datatype definitions without a full kind signature
</li><li>Associated type declarations
</li><li>Vanilla type synonyms
</li></ul><p>
Variables are defaulted to <code>*</code> in the following places:
</p>
<ul><li>Top-level family declarations
</li><li>Datatype definitions with a full kind signature
</li></ul><p>
And, with the kind inference for closed type families that Simon and I discussed, we have a third case:
</p>
<ul><li>Type variables in closed type families are kind-polymorphic, but unconstrained type variables are defaulted to <code>*</code>.
</li></ul><p>
The "scope" rule doesn't quite describe this menagerie. Even excepting closed type families, the scope rule fails for datatype definitions. Type variables in a (GADT-style) datatype definition have no scope, but they get their constraints other ways.
</p>
<p>
It's easy enough in the implementation to make the type variable <code>b</code> from above default to <code>*</code>, and that might be sensible, but it does make for a rather complicated rule to state.
</p>
TicketmonoidalThu, 27 Jun 2013 21:40:37 GMT
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:14
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:14
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/7939#comment:11" title="Comment 11">goldfire</a>:
</p>
<blockquote class="citation">
<p>
Now, <code>D</code> doesn't look GADT-like in its kind parameter, which is always just <code>k</code>. The difference between the version that works and the version that doesn't is that pattern-matching on the version that works does <em>not</em> refine information about the kind <code>k</code>. In fact, you can see this easily because you can write more instances for either <code>A</code> or <code>B</code> showing that the kind argument is not really fixed by this construction.
</p>
</blockquote>
<p>
I see, thanks. One last question - does anything change in your comment if I use a closed type family? Like this:
</p>
<pre class="wiki">type family F :: k where
F = Maybe
x :: Maybe F
x = Nothing
</pre><p>
Should this be legal? While the type <code>F</code> has kind <code>k</code>, it works effectively as a synonym for <code>Maybe</code>, which is kind <code>* -> *</code>.
</p>
TicketgoldfireThu, 27 Jun 2013 22:16:46 GMT
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:15
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:15
<p>
This, too, is fine. <code>F</code> does have kind <code>k</code>, but it will only be a synonym to <code>Maybe</code> in contexts that expect a type of kind <code>* -> *</code>:
</p>
<pre class="wiki">Prelude> type family F :: k where F = Maybe
Prelude> :kind! F
F :: k
= forall (k :: BOX). F k
Prelude> :kind! F Int
F Int :: k
= forall (k :: BOX). F (* -> k) Int
Prelude> :kind! (F Int :: *)
(F Int :: *) :: *
= Maybe Int
</pre><p>
So, I do think that beasts like <code>F</code> are strange, but I think (hope?) that a programmer is unlikely to stumble upon an <code>F</code> without knowing what they are doing.
</p>
Ticketeir@…Fri, 28 Jun 2013 08:37:04 GMT
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:16
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:16
<p>
commit <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/8c5e7346746a870ccc2eb86747792700f2a08deb/ghc" title="Fix Trac #7939, and add kind inference to closed type families.
Now, ...">8c5e7346746a870ccc2eb86747792700f2a08deb</a>
</p>
<pre class="wiki">Author: Richard Eisenberg <eir@cis.upenn.edu>
Date: Tue Jun 25 17:42:47 2013 +0100
Fix Trac #7939, and add kind inference to closed type families.
Now, all open type families have result kinds that default to
*. Top-level type families have all arguments default to *,
and associated type families have all arguments that are not
mentioned in the class header default to *. Closed type
families perform kind inference, but generalize only over
those kind variables that are parametric in their use.
This is all a little fiddly and specific, but it seems to follow
use cases. This commit also includes a large
Note [Kind-checking strategies] in TcHsType that helps keep all
of this straight.
compiler/hsSyn/HsDecls.lhs | 12 ++
compiler/typecheck/TcHsType.lhs | 224 ++++++++++++++++++++++++++++++++--
compiler/typecheck/TcMType.lhs | 11 +--
compiler/typecheck/TcTyClsDecls.lhs | 210 +++++++++++++++++++--------------
4 files changed, 345 insertions(+), 112 deletions(-)
</pre>
TicketgoldfireFri, 28 Jun 2013 08:39:47 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:17
http://ghc.haskell.org/trac/ghc/ticket/7939#comment:17
<ul>
<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>
Most of the above commit are comments in <code>TcHsType</code> detailing the rather-subtle kind inference story.
</p>
<p>
One aspect of the code did get simpler though: associated type families are now kind-checked identically to top-level families.
</p>
Ticket