If I say ```hs {-# 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.)