Note [zonkEqTypes and the PKTI]

Because `zonkEqTypes` does /partial/ zonking, we need to be very careful
to maintain the Purely Kinded Type Invariant: see GHC.Tc.Gen/HsType
HsNote [The Purely Kinded Type Invariant (PKTI)].

In #26256 we try to solve this equality constraint:
   Int :-> Maybe Char ~# k0 Int (m0 Char)
where m0 and k0 are unification variables, and
   m0 :: Type -> Type
It happens that m0 was already unified
   m0 := (w0 :: kappa)
where kappa is another unification variable that is also already unified:
   kappa := Type->Type.
So the original type satisifed the PKTI, but a partially-zonked form
   k0 Int (w0 Char)
does not!! (This a bit reminiscent of Note [mkAppTyM].)

The solution I have adopted is simply to make `zonkEqTypes` bale out on `AppTy`.
After all, it's only supposed to be a quick hack to see if two types are already
equal; if we bale out we'll just get into the "proper" canonicaliser.

The only tricky thing about this approach is that it relies on /omitting/
code -- for the AppTy/AppTy case!  Hence this Note