[GHC] #11471: Kind polymorphism and unboxed types: bad things are happening

[GHC]

#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