#11471: Note [The kind invariant] in TyCoRep needs to be updated -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Bother. There are worms under this stone. Is this OK? {{{ type family F a :: k type instance F Int = Int# type instance F Bool = Int }}} This looks very bad to me. Now the runtime representation of `(F a)` might be boxed or unboxed. Eeek. And indeed `Type.typePrimRep` assumes that any `AppTy` is a boxed pointer; and any `TyConApp` whose tycon is not primitive is also a boxed pointer. So if we can have type families with a poly-kinded result, then we can't allow kind variables to be instantiated with `TYPE Unlifted` (or anything levity polymorphic). Sigh. And if we have type constructors like `State# :: TYPE Lifted -> TYPE Unlifted`, which we do, then similar problems occur if we have {{{ type instance F Char = State# }}} because now `(F Char Int)` has a zero-width representation. So we can't allow that kind variable to be instantiated with `* -> #` either. This is what `Note [The kind invariant]` was all about, and we have been quietly ignoring it. I think we must allow type families to have a poly-kinded result. So do we have to impose (painful to specify, painful to implement) restrictions on how kind variables can be instantiated. Ironically, we have just loosened this up; see #11120 comment:19, first bullet, and #11465. I'm really not sure what to do here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: TypeInType => TypeInType, LevityPolymorphism * type: task => bug Comment: Replying to [comment:4 bgamari]:

You also might be interested in [[https://phabricator.haskell.org/D1807#53426]]. I was quite surprised to find that nothing blew up here.

Eeek. See #11473. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: => goldfire Comment: Richard and I developed a plan this afternoon. '''Principle''': the kind of a type tells you its runtime representation (both width and pointer-hood). Currently we have {{{ data Levity = Lifted | Unlifted }}} With this new principle we would have {{{ data Levity = L -- Lifted, boxed, represented by a pointer | UB -- Unlifted, boxed, represented by a pointer | UV -- Unboxed, zero width | UW32 -- Unboxed, represented by a 32 bit word | UW64 -- Unboxed, represented by a 64 bit word | UF32 -- Unboxed, represented by a 32 bit float | UF64 -- Unboxed, represented by a 64 bit float ...etc... }}} Pretty much one case for each constructor in `PrimRep`. And that's it really. Now `typePrimRep` just takes the kind, and converts it to a `PrimRep`. This is a nice generalisation, and (we think) solves the problem. We need a Levity wiki page!! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): By the way, I know the name of the extension is `TypeInType`, but might it not make more sense to have a separate `Levity` constructor for kinds? Say `* :: TYPE T`. While the values of `Int` are things like `1 :: Int`, and they are lifted and boxed, the "values" of `*` are things like `Int :: *`, and... `Int` is not really represented by anything at runtime. But if it was, it wouldn't necessarily be a lifted, boxed pointer. Maybe you want lazy evaluation on the value level, but strict evaluation on the type level, along with a totally different runtime representation for types. I don't know of any reason why you would want to abstract over specifically (regular types of kind `*` + kinds). It seems to me that in such cases it would make just as much sense to allow unboxed types as well. On the other hand, I do realize that the name `*` is a lot more convenient than writing `forall (a :: RuntimeRep). ... (TYPE a)`, and maybe that is the real issue...? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm afraid I don't understand the idea of comment:9. I'm happy that Richard says he likes it, but what precisely is the suggestion? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): So under comment:7 as I understand it `*` is a synonym for `TYPE L`. We can make a table {{{ 1 :: Int and Int :: * = TYPE L 2# :: Int# and Int# :: TYPE UW64 3.0# :: Double# and Double# :: TYPE UF64 Int :: * and * :: * = TYPE L }}} The last line is given to us by TypeInType. But to me the thing `Int` seems at least as different from the thing `1` as the things `1`, `2#` and `3.0#` are from each other. So, the suggestion is to add another constructor `T` to `RuntimeRep` and replace the last line with {{{ Int :: * and * :: TYPE T }}} We could define a synonym `type Kind = TYPE T` and then `* :: Kind`. The motivation is basically: By merging the type and kind levels, TypeInType means that we no longer ''need'' to distinguish types and kinds. That is great for implementing, say, kind coercions because we don't need to duplicate the language of coercions to the kind level any more. (Feel free to substitute your own, better examples.) However, now that this RuntimeRep story has emerged, it seems we could get the best of both worlds, by defining `* = TYPE L`, and `Kind = TYPE T`. Now we can abstract over the difference between types and kinds when we want to, by working with `TYPE t`. Or we can distinguish between types and kinds when that makes sense, by using `*` and `Kind`. I don't have any great examples for the latter. Maybe if you define a type family whose result is intended to be a kind (since you use it to classify a type elsewhere) you would want to be able to enforce that on clients who may define their own instances. Or maybe the typing rule for a coercion should be that the type `s ~ t` of coercions is well-formed only if `s :: TYPE r` and `t :: TYPE r` for the same `r`, and you don't want to allow coercing between values and types. (But see the end of this comment.) ---- Note that one could perhaps retain even more of the type/kind/sort/etc. hierarchy by adding a parameter to `T`. The parameter `r` would contain information about the representation of the "values" (types) classified by types of kind `TYPE (T r)`. Or in symbols, {{{ if C :: K = TYPE r, (i.e., the type C has representation r) then K :: TYPE (T r), }}} or in short `TYPE r :: TYPE (T r)`. I'm not sure how this would interact with type constructors though (with kinds built from `(->)`). This probably has something to do with the indexed TypeRep story also, which I haven't been paying any attention to. ---- These suggestions apply to an unspecified extension of Haskell that might want to treat the type level in an arbitrary way. If there's a specific plan for "GHC Haskell" to identify types with their TypeReps as mentioned in comment:10 (I guess this means there is some way to refer to a type at the value level, so now it really makes sense to write functions of type `* -> *`, etc.) then there is probably not much reason to take this route, indeed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1891 Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * differential: => Phab:D1891 Comment: As the differential states, there are still some performance issues to be worked out. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1891 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"d8c64e86361f6766ebe26a262bb229fb8301a42a/ghc" d8c64e86/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="d8c64e86361f6766ebe26a262bb229fb8301a42a" Address #11471 by putting RuntimeRep in kinds. See Note [TYPE] in TysPrim. There are still some outstanding pieces in #11471 though, so this doesn't actually nail the bug. This commit also contains a few performance improvements: * Short-cut equality checking of nullary type syns * Compare types before kinds in eqType * INLINE coreViewOneStarKind * Store tycon binders separately from kinds. This resulted in a ~10% performance improvement in compiling the Cabal package. No change in functionality other than performance. (This affects the interface file format, though.) This commit updates the haddock submodule. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1891 Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): Sure. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1891 Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * owner: bgamari => goldfire Comment: I'm still on this, actually. The `RuntimeRep` stuff was just a necessary stop along the way. The actual fix should be quite simple to put in on top of this all. Ben, if you want to add tests, I won't stop you, but I don't imagine they will pass. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1891 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"f602f4a6fbf40d1a3c3c02294e90fcb2d5866d04/ghc" f602f4a6/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="f602f4a6fbf40d1a3c3c02294e90fcb2d5866d04" Fix printing of "kind" vs. "type" This is as reported in #11471, though it's not the focus of that ticket. test case: polykinds/KindVType }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | dependent/should_fail/T11471 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1891 Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => merge * testcase: => dependent/should_fail/T11471 Comment: In the end, there wasn't much to do here other than the `RuntimeRep` stuff. Still worth merging that last commit, but it's not all that important. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: fixed | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | dependent/should_fail/T11471 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1891 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed * milestone: => 8.0.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11471: Kind polymorphism and unboxed types: bad things are happening -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeInType, Resolution: fixed | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | dependent/should_fail/T11471 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1891 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): comment:28 introduces two new, mostly-unrelated bugs. I've spun them off into #11722 and #11723. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11471#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler