RULE quantification over equalities is fragile

We quantify over some equality constraints arising from the LHS of rules, as explained in Note [RULE quantification over equalities]. We do so by inspecting the initial LHS Wanted constraints, before we have even attempted to canonicalise anything. This seems a bit fragile; for example, we are willing to quantify over equalities of the form A ~# F B for a type family F, but what if the constraint was of the form D A ~# D (F B) for a datatype D? We would now decide not to quantify over it because neither the LHS or RHS is headed by a type family, even though it is decomposable and decomposes to A ~# F B, which we would quantify over.

Here's a contrived example I came up with that illustrates the problem:

type I :: k -> k
type family I a where
  I a = a

f :: forall rr (a :: TYPE (I rr)). Proxy rr -> Proxy a -> Proxy a
f _ px = px
{-# NOINLINE f #-}
{-# RULES "f_id" forall (k :: Proxy LiftedRep) (x :: Proxy Int). f k x = x #-}

warning:
    Forall'd constraint `LiftedRep ~ I LiftedRep'
    is not bound in RULE lhs
      Orig bndrs: [co_aBT, k, x]
      Orig lhs: f @LiftedRep @Int k x
      optimised lhs: f @LiftedRep @Int k x
   |
16 | {-# RULES "f_id" forall (k :: Proxy LiftedRep) (x :: Proxy Int). f k x = x #-}
   |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^