[GHC] #11471: Note [The kind invariant] in TyCoRep needs to be updated

[GHC]

#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