Rewrite rule can trigger Lint

Consider this program (produced by Michael Sperber)

{-# LANGUAGE MagicHash #-}
module ConCatRules where

import GHC.Prim
import GHC.Int

unboxI :: Int -> Int#
unboxI (I# i#) = i#

plus :: Int -> Int -> Int
plus x y = plus x y
{-# NOINLINE plus #-}

{-# RULES
"reboxa" forall u# v# . (+#) u# v# = unboxI (plus (I# u#) (I# v#))
#-}

foo = I# (10# +# 1#)

Compile with -O and you get

*** Core Lint errors : in result of Simplifier ***
Bar.hs:25:1: warning:
    This argument does not satisfy the let/app invariant:
      case plus (I# 10#) (I# 1#) of { I# i#_aBa -> i#_aBa }
    In the RHS of foo :: Int
    Substitution: [TCvSubst
                     In scope: InScope {}
                     Type env: []
                     Co env: []]

There is a good reason for this. The RULE rewrites

• an expression that is okForSpeculation (namely 10# +# 1#)
• into an expression that is not okForSpeculation (namely case plus (I# 10#) (I# 1#) of { I# i#_aBa -> i#_aBa })

The former is allowed as an argument of I# (as it appears in foo); but the latter is not, by the let/app invariant.

GHC never itself rewrites an expression that is okForSpeculation into one that isn't. But this RULE does. And that triggers Lint.

Is this a bug in GHC, or a bug in the RULE?

We could make the simplifier test for this situation, without much difficulty, but doing so would impose a small extra overhead on every compilation.