Note [Phantom type variables in kinds]
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
- Kinding rules for types GHC.Core.Type
Referenced by 3
- GHC.Core.Lint call site
- GHC.Core.Type call site
- GHC.Tc.Validity call site