#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