Note [Respecting definitional equality] introduces invariant EQ1:
(EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable cast is one that relates either a FunTy to a FunTy or a ForAllTy to a ForAllTy.
This invariant is a small pain to uphold. And perhaps we don't need to. If, instead, we modified
eqType to look at the kind of arguments to
AppTys, then we wouldn't need EQ1, significantly simplifying
mkAppTy. (Actually, it will just remove 2 lines. But it removes two calls to
decomposePiCos. This will allow the one remaining call to this function to have more sway in the design of
decomposePiCos, simplifying that bit of code, as well.)