RULES involving newtypes don't fire

In the following program, the RULE involving the newtype constructor MkN does not fire:

{-# NOINLINE f #-}
f :: a -> a
f x = x

newtype N = MkN { runN :: Int }

{-# RULES
     "f/N" forall i. f (MkN i) = MkN (1000 * i)
 #-}

main = print $ runN (f (MkN 17))

We get a result of 17, instead of the expected 17000.

This is because of the logic in GHC.Core.Rules.match_co which only allows coercions which are reflexive or coercion variables, whereas in this example the coercion is Sym (N:N[0]).

Note that this observation does not jeopardise the map/coerce rule, which does function as intended. That is, map MkN is indeed simplified away to a cast, and this happens AFTER the compulsory unfolding of MkN into \ x -> x |> Sym N[0] is inlined, as explained in Note [Getting the map/coerce RULE to work] in GHC.Core.SimpleOpt.

One concern I have about these RULES involving newtypes is that firing the rule whenever we see x |> Sym N[0] (or any coercion relating the same types as Sym N[0], to account for proof irrelevance) seems dodgy: the typechecker can insert coercions at will, in places which might not correspond to user-written applications of the newtype constructor MkN. So we would end up firing the RULE in unexpected circumstances.