[GHC] #7939: RHS of associated type not kind-checked
#7939: RHS of associated type not kind-checked ----------------------------------------+----------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Component: Compiler Version: 7.7 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Blockedby: Blocking: | Related: ----------------------------------------+----------------------------------- The following code compiles without complaint: {{{ {-# 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 }}} We can see here that {{{Bar}}} is ill-kinded. When I try {{{:k Bar}}} in GHCi, I get an assertion failure, not unexpectedly. I will fix in ongoing work. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked ----------------------------------------+----------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Component: Compiler Version: 7.7 | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Blockedby: Blocking: | Related: ----------------------------------------+----------------------------------- Comment(by goldfire): This problem is a little worse than I thought. With just {{{ class Foo a where type Bar a }}} (with {{{-XPolyKinds}}}), I get an assertion failure in GHCi on {{{:k Bar}}}. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Changes (by monoidal): * owner: goldfire => * status: closed => new * resolution: fixed => Comment: Something is suspicious here. GHC accepts original program {{{ {-# 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 }}} but rejects {{{ {-# LANGUAGE TypeFamilies, PolyKinds #-} type family Baz a type instance Baz Int = Maybe type instance Baz Bool = Double }}} Is this really expected? Even more, you can write {{{ instance Foo Bool where type Bar Bool = Double type Bar Bool = Maybe }}} -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Comment(by monoidal): Aha - `type Bar a` in a typeclass declaration defaults to `type Bar a :: k`, while `type family Baz a` defaults to `type family Baz a :: *`. This is a slight inconsistency. Meanwhile, we can also write {{{ {-# LANGUAGE TypeFamilies, PolyKinds #-} type family A :: k type instance A = Double type instance A = Maybe }}} -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Comment(by simonpj): Well analysed. * The inconsistency seems to be deliberate; look at `TcTyClDecls.getFamDeclInitialKind`. But there is no explanation of why the difference, so I think we should abolish the difference until proved otherwise. * With `-XPolyKinds` we get kind polymorphism by default in data decls. Eg {{{ data T f a = MkT (f a) }}} we get `T :: (k -> *) -> k -> *`. * By the same token it is perhaps reasonable that {{{ type family F a :: * }}} gives `F :: k -> *` * But getting polykinded ''result'' kind by default (even with `-XPolyKinds`) seems odd to me: {{{ type family F a }}} Do we really want `F :: k1 -> k2`? My suggestion is that we adopt the current top-level story, namely that the result kind of a type family is `*` unless you explicitly use a kind variable. That's inconsistent with the argument story, but the examples you give above really are quite confusing Comments, anyone? The fix is easy either way. Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Comment(by goldfire): 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 {{{*}}}. 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 {{{*}}}) or (everything defaults to fresh kind variables). The former gives better errors in the common case, so I favor that one. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Changes (by simonpj): * owner: => goldfire Comment: 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. Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Comment(by monoidal): I think it's fine to default to *. But, again, consider {{{ type family A :: k type instance A = Double type instance A = Maybe }}} Should this really compile? I don't know, it looks suspicious but perhaps it is OK. What makes me suspicious is this. Consider {{{ data D :: k -> * where D1 :: D Bool D2 :: D Maybe }}} GHC gives an error: {{{ Data constructor `D1' cannot be GADT-like in its *kind* arguments D1 :: D * Bool }}} But this seemingly equivalent code compiles: {{{ {-# 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 }}} -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Comment(by goldfire): I've implemented the plan above, but there is still at least one dark corner. Consider this: {{{ class Foo a where type Bar a b }}} What should the kind of {{{Bar}}} be? Because classes are kind-polymorphic by default (which is good), the kind of {{{a}}} must be {{{k}}}. But, what about {{{b}}}? Right now, in both HEAD and my implementation with the fix for this ticket, {{{Bar}}} has the kind {{{k1 -> k2 -> *}}}. 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. Thoughts? Expect a patch soon. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Comment(by goldfire): In response to monoidal's most recent comment: I'm fine with your definition for {{{A}}}. It is deeply strange-looking, I agree, but if we make the kind applications explicit, it's quite normal: {{{ type family A (k :: BOX) :: k type instance A * = Double type instance A (* -> *) = Maybe }}} As for the GADT example, I find that more interesting. Let's make everything more explicit: {{{ 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) }}} Now, {{{D}}} doesn't look GADT-like in its kind parameter, which is always just {{{k}}}. The difference between the version that works and the version that doesn't is that pattern-matching on the version that works does ''not'' refine information about the kind {{{k}}}. In fact, you can see this easily because you can write more instances for either {{{A}}} or {{{B}}} showing that the kind argument is not really fixed by this construction. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Comment(by simonpj): 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 {{{ class C a where { opc :: a -> a } class D f b where { opd :: f b -> f b } }}} Then, just as in a data type declaration, we look at the uses of type variables `a`, `f`, `b`, and get these kinds: {{{ C :: * -> Constraint D :: (k -> *) -> k -> Constraint }}} This is good. It is very different for a top-level open type family {{{ type family F a b }}} Here there are no uses, and hence no kind constraints, on `a` and `b`, and there can't be. But it seems over-kill to assume maximal polymorphism, so our plan is to default to *, thus {{{ F :: * -> * -> * }}} Now, with the associated type you give, there's a mixture of the two: {{{ class Foo a where type Bar a b op :: a -> a }}} Here there probably ''are'' some constraints on `a` (from the class methods as usual), but there can be none on `b`. So my suggestion would be to default `b` to `*`, just like for top-level ones, but to constrain `a` 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: * If there is some "scope" for the variable, infer the kind from its uses * If there is no "scope", use `*`, unless there's a kind annotation. Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Comment(by goldfire): As I was looking at all of this, I wasn't sure what to do about type variables like `b` 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. However, I don't think Simon's "scope" rule really does it. Currently, variables are kind-polymorphic-by-default in the following places: * Class definitions * Datatype definitions without a full kind signature * Associated type declarations * Vanilla type synonyms Variables are defaulted to `*` in the following places: * Top-level family declarations * Datatype definitions with a full kind signature And, with the kind inference for closed type families that Simon and I discussed, we have a third case: * Type variables in closed type families are kind-polymorphic, but unconstrained type variables are defaulted to `*`. 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. It's easy enough in the implementation to make the type variable `b` from above default to `*`, and that might be sensible, but it does make for a rather complicated rule to state. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Comment(by monoidal): Replying to [comment:11 goldfire]:
Now, {{{D}}} doesn't look GADT-like in its kind parameter, which is always just {{{k}}}. The difference between the version that works and the version that doesn't is that pattern-matching on the version that works does ''not'' refine information about the kind {{{k}}}. In fact, you can see this easily because you can write more instances for either {{{A}}} or {{{B}}} showing that the kind argument is not really fixed by this construction.
I see, thanks. One last question - does anything change in your comment if I use a closed type family? Like this: {{{ type family F :: k where F = Maybe x :: Maybe F x = Nothing }}} Should this be legal? While the type `F` has kind `k`, it works effectively as a synonym for `Maybe`, which is kind `* -> *`. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Comment(by goldfire): This, too, is fine. `F` does have kind `k`, but it will only be a synonym to `Maybe` in contexts that expect a type of kind `* -> *`: {{{ 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 }}} So, I do think that beasts like `F` are strange, but I think (hope?) that a programmer is unlikely to stumble upon an `F` without knowing what they are doing. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#7939: RHS of associated type not kind-checked
------------------------------------------+---------------------------------
Reporter: goldfire | Owner: goldfire
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.7
Resolution: | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC accepts invalid program | Difficulty: Unknown
Testcase: ghci/scripts/T7939 | Blockedby:
Blocking: | Related:
------------------------------------------+---------------------------------
Comment(by eir@…):
commit 8c5e7346746a870ccc2eb86747792700f2a08deb
{{{
Author: Richard Eisenberg
#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: fixed | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Changes (by goldfire): * status: new => closed * resolution: => fixed Comment: Most of the above commit are comments in TcHsType detailing the rather- subtle kind inference story. One aspect of the code did get simpler though: associated type families are now kind-checked identically to top-level families. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (2)
-
GHC -
GHC