See also Note [ForAllTy and type equality] in GHC.Core.TyCo.Compare.
Constructing coercions between forall-types can be a bit tricky,
because the kinds of the bound tyvars can be different.
The typing rule is:
G |- kind_co : k1 ~N k2
tv1 \not\in fv(typeKind(t1),typeKind(t2)) -- Skolem escape
G, tv1:k1 |- co : t1 ~r t2
if r=N, then vis1=vis2
G |- ForAllCo (tv1:k1) vis1 vis2 kind_co co
: forall (tv1:k1) <vis1>. t1
~r
forall (tv1:k2) <vis2>. (t2[tv1 |-> (tv1:k2) |> sym kind_co])
Several things to note here
(FC1) First, the TyCoVar stored in a ForAllCo is really just a convenience: this
field should be a Name, as its kind is redundant. Thinking of the field as a
Name is helpful in understanding what a ForAllCo means. The kind of TyCoVar
always matches the left-hand kind of the coercion.
* The idea is that kind_co gives the two kinds of the tyvar. See how, in the
conclusion, tv1 is assigned kind k1 on the left but kind k2 on the right.
* Of course, a type variable can't have different kinds at the same time.
So, in `co` itself we use (tv1 : k1); hence the premise
tv1:k1 |- co : t1 ~r t2
* The last wrinkle is that we need to fix the kinds in the conclusion. In
t2, tv1 is assumed to have kind k1, but it has kind k2 in the conclusion of
the rule. So we do a kind-fixing substitution, replacing (tv1:k1) with
(tv1:k2) |> sym kind_co. This substitution is slightly bizarre, because it
mentions the same name with different kinds, but it *is* well-kinded, noting
that `(tv1:k2) |> sym kind_co` has kind k1.
We could instead store just a Name in the ForAllCo, and it might even be
more efficient to do so. But we can't add Names to, e.g., VarSets, and
there generally is just an impedance mismatch in a bunch of places. So we
use tv1. When we need tv2, we can use setTyVarKind.
(FC2) Note that the kind coercion must be Nominal; and that the role `r` of
the final coercion is the same as that of the body coercion.
(FC3) A ForAllCo allows casting between visibilities. For example:
ForAllCo a Required Specified (SubCo (Refl ty))
: (forall a -> ty) ~R (forall a. ty)
But you can only cast between visiblities at Representational role;
Hence the premise
if r=N, then vis1=vis2
in the typing rule. See also Note [ForAllTy and type equality] in
GHC.Core.TyCo.Compare.
(FC4) See Note [Required foralls in Core].
(FC5) In a /type/, in (ForAllTy cv ty) where cv is a CoVar, we insist that
`cv` must appear free in `ty`; see Note [Unused coercion variable in ForAllTy]
in GHC.Core.TyCo.Rep for the motivation. If it does not appear free,
use FunTy.
However we do /not/ impose the same restriction on ForAllCo in /coercions/.
Instead, in coercionLKind and coercionRKind, we use mkTyCoForAllTy to perform
the check and construct a FunTy when necessary. Why?
* For a coercion, all that matters is its kind, So ForAllCo vs FunCo does not
make a difference.
* Even if cv occurs in body_co, it is possible that cv does not occur in the kind
of body_co. Therefore the check in coercionKind is inevitable.
(FC6) Invariant: in a ForAllCo where fco_tcv is a coercion variable, `cv`,
we insist that `cv` appears only in positions that are erased. In fact we use
a conservative approximation of this: we require that
(almostDevoidCoVarOfCo cv fco_body)
holds. This function checks that `cv` appers only within the type in a Refl
node and under a GRefl node (including in the Coercion stored in a GRefl).
It's possible other places are OK, too, but this is a safe approximation.
Why all this fuss? See Section 5.8.5.2 of Richard's thesis. The idea is that
we cannot prove that the type system is consistent with unrestricted use of this
cv; the consistency proof uses an untyped rewrite relation that works over types
with all coercions and casts removed. So, we can allow the cv to appear only in
positions that are erased.
Sadly, with heterogeneous equality, this restriction might be able to be
violated; Richard's thesis is unable to prove that it isn't. Specifically, the
liftCoSubst function might create an invalid coercion. Because a violation of
the restriction might lead to a program that "goes wrong", it is checked all
the time, even in a production compiler and without -dcore-lint. We *have*
proved that the problem does not occur with homogeneous equality, so this
check can be dropped once ~# is made to be homogeneous.
(FC7) Invariant: in a ForAllCo, if fco_tcv is a CoVar, then
fco_visL = fco_visR = coreTyLamForAllTyFlag
c.f. (FT2) in Note [ForAllTy]