Rules: "Forall'd constraint ‘Num Int’ is not bound in RULE lhs"

Consider

foo :: (forall a. [a] -> Int) -> Int
foo len = len [1,2,3] + len "abc"
{-# RULES "foo" forall (f :: forall a. [a] -> Int). foo (\xs -> 1 + f xs) = 2 + foo f #-}
{-# NOINLINE foo #-}

bar :: Int
bar = foo f
  where
    f xs = 1 + length xs

Apart from the fact that the RULE does not fire today (I came up with the example as a motivation for !9343 (closed)), GHC emits the following warning:

test.hs:12:11: warning: [GHC-40548]
    Forall'd constraint ‘Num Int’ is not bound in RULE lhs
      Orig bndrs: [$dNum_aQO, $dNum_aQQ, f]
      Orig lhs: foo
                  (\ (@a) (xs :: [a]) ->
                     + @Int $dNum_aQO (GHC.Types.I# 1#) (f @a xs))
      optimised lhs: foo
                       (\ (@a) (xs :: [a]) ->
                          + @Int $dNum_aQO (GHC.Types.I# 1#) (f @a xs))
   |
12 | {-# RULES "foo" forall (f :: forall a. [a] -> Int). foo (\xs -> 1 + f xs) = 2 + foo f #-}
   |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I think that warning is wrong: The Num Int dictionaries should not actually need to be quantified over but rather solved directly. I'm not sure what's going on here.