Note [Kinding rules for types]
Here are the key kinding rules for types
torc1 is TYPE or CONSTRAINT
torc2 is TYPE or CONSTRAINT
t1 : torc1 rep1
t2 : torc2 rep2
(FUN) ----------------
t1 -> t2 : torc2 LiftedRep
In fact the arrow varies with torc1/torc2
See Note [Function type constructors and FunTy]
in GHC.Builtin.Types.Prim
torc is TYPE or CONSTRAINT
ty : body_torc rep
ki : Type
`a` is a type variable
`a` is not free in rep
(FORALL1) -----------------------
forall (a::ki). ty : body_torc rep
torc is TYPE or CONSTRAINT
ty : body_torc rep
`c` is a coercion variable
`c` is not free in rep
`c` is free in ty -- Surprise 1!
(FORALL2) -------------------------
forall (cv::k1 ~#{N,R} k2). ty : body_torc LiftedRep
Surprise 2!
Note that:
* (FORALL1) rejects (forall (a::Maybe). blah)
* (FORALL2) Surprise 1:
See GHC.Core.TyCo.Rep Note [Unused coercion variable in ForAllTy]
* (FORALL2) Surprise 2: coercion abstractions are not erased, so
this must be LiftedRep, just like (FUN). (FORALL2) is just a
dependent form of (FUN). References 2
- Function type constructors and FunTy GHC.Builtin.Types.Prim
- Unused coercion variable in ForAllTy GHC.Core.TyCo.Rep
Referenced by 1
- Phantom type variables in kinds GHC.Core.Type