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.)

Another nice benefit: by removing this invariant, we have an opportunity to explore different solutions to #17644, which hit a dead end in EQ1. See #17644 (comment 245757).