`Note [Equality on AppTys]` looks wrong

This Note says

Note [Equality on AppTys]
~~~~~~~~~~~~~~~~~~~~~~~~~
In our cast-ignoring equality, we want to say that the following two
are equal:

  (Maybe |> co) (Int |> co')   ~?       Maybe Int

But the left is an AppTy while the right is a TyConApp. The solution is
to use splitAppTyNoView_maybe to break up the TyConApp into its pieces and
then continue. Easy to do, but also easy to forget to do.

But in GHC.Core.TyCo.Rep we see

Note [Respecting definitional equality]
...
  (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.

It seems that (EQ1) means that the example in Note [Equality on AppTys] isn't possible. After all:

• Maybe :: Type -> Type
• So co :: (Type->Type) ~ (k1 -> k2), for some kinds k1 and k2
• So co is decomposable
• So (EQ1) does not hold

Question: is Note [Equality on AppTys] needed? Is there another example to illustrate why we need splitAppTyNoView_maybe in tcEqType and friends?

@rae: this is a question for you!