Improve Note [Respecting definitional equality]
Note about (EQ1)
(t1 t2) |> co =? (t1 |> (<k>->co)) t2
These are both well kinded, and are eqType. But they reply differently to splitAppTy
This applies whether t1 is TyVar, AppTy, TyConApp, anything. So it subsumes the longer comment about TyConApps.
All the work is in mkAppTy.
"Accordingly, by eliminating reflexive casts, splitTyConApp need not worry about outermost casts to uphold (EQ). Eliminating reflexive casts is done in mkCastTy."
Mention EQ2 here.
Lastly, in order to detect reflexive casts reliably, we must make sure not
to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 TransCo
co2)).
Mention EQ3.
Motivate EQ4.
Note [Weird typing rule for ForAllTy]
does not exist. It is referred to in many places.
It's in commit 03d48526. Re-add it. (in TyCoRep)
"three invariants"!
Second way to improve the note
Consider
t1 = t |> (cv1 :: Int ~ T)
t2 = t |> (cv2 :: Int ~ T)
where cv1 and cv2 are two different, locally bound, coercion variables. So two types that are eqType may have different free coercion variables.
If two types are eqType, then their relevant free vars must be the same. (See above for why their coercion variables, and indeed tyvars occurrence in coercions may not be the same.)
"Relevant" means shallow free vars ignoring coercions.