Rewrite rules on functions on unboxed values are not supported

If I say

{-# LANGUAGE MagicHash #-}

module Bug where

import GHC.Exts

up :: Int# -> Int#
up x = x +# 1#

down :: Int# -> Int#
down x = x -# 1#

{-# RULES "up/down" forall x. up (down x) = x #-}

I get

Bug.hs:13:11: warning:
    RULE left-hand side too complicated to desugar
      Optimised lhs: case down x of wild_00 { __DEFAULT -> up wild_00 }
      Orig lhs: case down x of wild_00 { __DEFAULT -> up wild_00 }
   |
13 | {-# RULES "up/down" forall x. up (down x) = x #-}
   |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I know why this happens: GHC eagerly A-normalizes strict application, so that any strict argument is always a variable. In up (down x), the argument is not a variable, and so GHC rewrites this to case down x of y -> up y (as you can see in the error message). But this means that strict application cannot work with rewrite rules, which is unfortunate.

Yet I think we can do better, by allowing a rewrite rule to match against a case that (critically) has only a default. What do others think about this?

In searching for a related ticket, I found #10555, but the discussion there seems to focus on division and that it can throw an exception.

(The lack of ability to write such a rule has implications for Conal Elliott's work in compiling to categories.)