Note [Phantom type variables in kinds]

GHC/Core/Type.hs:2642 compiler 1 ticket

Consider

  type K (r :: RuntimeRep) = Type   -- Note 'r' is unused
  data T r :: K r                   -- T :: forall r -> K r
  foo :: forall r. T r

The body of the forall in foo's type has kind (K r), and
normally it would make no sense to have
   forall r. (ty :: K r)
because the kind of the forall would escape the binding
of 'r'.  But in this case it's fine because (K r) expands
to Type, so we explicitly /permit/ the type
   forall r. T r

To accommodate such a type, in typeKind (forall a.ty) we use
occCheckExpand to expand any type synonyms in the kind of 'ty'
to eliminate 'a'.  See kinding rule (FORALL) in
Note [Kinding rules for types]


See also
 * GHC.Core.Type.occCheckExpand
 * GHC.Core.Utils.coreAltsType
 * GHC.Tc.Validity.checkEscapingKind
all of which grapple with the same problem.

See #14939.

References 1

Referenced by 3