[GHC] #10114: Kind mismatches with AnyK in rank-2 types
#10114: Kind mismatches with AnyK in rank-2 types -------------------------------------+------------------------------------- Reporter: cam | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- The following module: {{{#!hs {-# LANGUAGE Rank2Types #-} module KindBug where type T = forall f a. f a foo :: T foo = undefined bar :: forall f a. f a bar = foo }}} ...produces the following error: {{{ [1 of 1] Compiling KindBug ( KindBug.hs, KindBug.o ) KindBug.hs:10:7: Kind incompatibility when matching types: f0 :: AnyK -> * f :: * -> * Expected type: f a Actual type: f0 a0 Relevant bindings include bar :: f a (bound at KindBug.hs:10:1) In the expression: foo In an equation for ‘bar’: bar = foo }}} Note that no extensions are enabled other than rank-2 types. Enabling and using kind annotations fixes the error, as does replacing the type synonym with its definition in the type signature of foo. Similar errors can also be generated with PolyKinds enabled and less plausible code, e.g. {{{ (return undefined :: forall f a. f a) :: f a }}}. The non-PolyKinds example is simplified from some actual code, where the type synonym was similar to the ones used in lens, and is the simplest example I could find (with help from Shachaf on IRC) that resembled real code. I searched for existing tickets and the closest I could find are #7916 and #5935, both of which are already fixed. Also, according to glguy (Eric Mertens) just now in #haskell-lens, the same error occurs in the 7.10 branch and in 7.11.20150120. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10114 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10114: Kind mismatches with AnyK in rank-2 types -------------------------------------+------------------------------------- Reporter: cam | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Some notes for myself (work in progress). At the moment, for type `T` above we get {{{ -- Without PolyKinds type T = forall (f :: AnyK -> *) (a :: AnyK). f a -- With PolyKinds type T k = forall (f :: AnyK -> k) (a :: AnyK). f a }}} Trouble is that we are not generalising over the kind of `a`. I think we want: {{{ -- Without PolyKinds type T = forall (f :: * -> *) (a :: *). f a -- With PolyKinds type T k1 k2 = forall (f :: k1 -> k2) (a :: k1). f a }}} But note the strange kind of `T` in `PolyKinds` case: `T :: forall k1 k2. k2`. I'm pretty sure we do NOT want to kind-generalise "inside", thus: {{{ type T = forall k1 k2 (f :: k1->k2) (a::k1). f a }}} Reasons: * see `Note [Kind generalisation]` in `TcHsType` * what kind would `T` have? `T :: k2` ??? * more operationally, kind foralls must be implicitly instantiated, during kind inference using only `T`'s kind -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10114#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10114: Kind mismatches with AnyK in rank-2 types -------------------------------------+------------------------------------- Reporter: cam | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): What about {{{ type T k2 = forall k1 (f :: k1 -> k2) (a :: k1). f a }}} That makes `T :: forall k2. k2`. That's a well-formed kind, but it looks awfully like the type of `undefined`... but I don't know if that's a problem. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10114#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10114: Kind mismatches with AnyK in rank-2 types -------------------------------------+------------------------------------- Reporter: cam | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Re comment:2, I don't think so: how does `k1` get instantiated when you have occurrences of `T`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10114#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10114: Kind mismatches with AnyK in rank-2 types -------------------------------------+------------------------------------- Reporter: cam | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): I'm not sure I understand comment:3. What are you worried about? I will also say that it's possible the right answer is {{{ type T = forall k1. (f :: k1 -> *) (a :: k1). f a }}} so that `T :: *`. My understanding is that it's generally more common to restrict the body of a forall to have kind `*`. GHC doesn't do this, but all the papers about System FC do. In other work, I changed the typing rule for forall accordingly, and something broke horribly (eta-reducing newtypes, maybe?), but perhaps we don't have to infer a type that has a non-`*` kind as the body of a forall. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10114#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10114: Kind mismatches with AnyK in rank-2 types -------------------------------------+------------------------------------- Reporter: cam | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): In comment:3 I think I was confusing these two things: {{{ T = forall k. blah T :: forall k. blah -- Uses of T must be applied to a kind }}} So I think I retract my claim in comment:1. Perhaps we do want to generalise "inside". Can anyone say why it is "generally more common to restrict the body of a forall to have kind `*`"? I can't articulate a clear argument. In GHC's case, a good reason not to do this was types like `forall a. a -> (# a, a #)`, but levity polymorpism will help here. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10114#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10114: Kind mismatches with AnyK in rank-2 types -------------------------------------+------------------------------------- Reporter: cam | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by goldfire): * cc: sweirich@… (added) Comment: Replying to [comment:5 simonpj]:
So I think I retract my claim in comment:1. Perhaps we do want to generalise "inside". I agree with your (now retracted) claim.
If `T = forall k1 k2 (f :: k1 -> k2) (a :: k1). f a`, then I think `T`'s type would have to be `k2`, which is nonsense. As I understand it, the kind of a forall-type is the kind of the body of the forall-type.
Can anyone say why it is "generally more common to restrict the body of
a forall to have kind `*`"? I can't articulate a clear argument. This claim of mine is direct from Stephanie. Stephanie, do you know why this is?
In GHC's case, a good reason not to do this was types like `forall a. a
-> (# a, a #)`, but levity polymorpism will help here. I don't think that's quite what you want to say, because the kind of the body of that forall is `*`! Maybe `forall a. (# a, a #)`? I don't see how levity polymorphism fixes this problem. Even with levity polymorphism, the kind of the body of that last forall is still `#`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10114#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10114: Kind mismatches with AnyK in rank-2 types -------------------------------------+------------------------------------- Reporter: cam | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): It's amazing how easily I can be confused by this stuff! To the question of why restricting foralls to have result of kind `*`, maybe I can attempt to answer my own question, thus: in what context could you could use such a type? Obviously not in a type signature, since that must have kind `*`. Where else? Would it make sense to say `T (forall a. Either a)`? But if `T` expected an arg of kind `* -> *`, does it make sense to instantiate it with `(forall a. Either a)`? Does the type `(forall a. Either a) Int` make sense? Maybe not. Re unboxed tuples, maybe you are right. Perhaps it only matters in very special cases like `forall a. (# a, a #)` which may not be very important. In short, maybe we should explore * `forall` always has kind `*` * Kind-generalise the RHS of type synonyms, so we get the kind in comment:4 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10114#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10114: Kind mismatches with AnyK in rank-2 types -------------------------------------+------------------------------------- Reporter: cam | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): When someone (possibly me, but not before April) explores this, a good way forward is to just change !CoreLint around this issue and then to recompile GHC, the libraries, and the test suite, all with `-dcore-lint` enabled. I'm 99% sure that the usage of `forall` with a non-`*` body will show up. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10114#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10114: Kind mismatches with AnyK in rank-2 types -------------------------------------+------------------------------------- Reporter: cam | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): NB the [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide /kind-polymorphism.html rule for kind generalisation in 7.8.2 of the user manual]. {{{ f1 :: (forall a. Proxy a) -> Int -- Means f :: forall k. (forall (a:k). Proxy k a) -> Int f2 :: (forall (a::k). Proxy a) -> Int -- Means f :: (forall k. forall (a:k). Proxy k a) -> Int }}} (Richard's new branch, which collapses types and kinds, allows explicit kind quantification, so we can then control this more explicitly.) So maybe the same should be true for `T`: {{{ type T = forall f a. f a -- Means type T k = forall (f::k->*) (a::k). f a type T = forall f (a::k). f a -- Means type T = forall k (f::k->*) (a::k). f a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10114#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10114: Kind mismatches with AnyK in rank-2 types -------------------------------------+------------------------------------- Reporter: cam | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Current BUG (HEAD, 7.10) {{{ type T = forall (f :: k -> k2) (a::k). f a }}} Compile with `-fprint-explicit-kinds -ddump-types -XRankNTypes -XPolyKinds` {{{ TYPE CONSTRUCTORS type T (k2 :: BOX) = forall (k :: BOX) (k1 :: BOX) (f :: k -> k1) (a :: k). f a }}} But this elaborated `T` simply doesn't have a sensible kind. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10114#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC