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.