Rules should "look through" case binders too

Here's a program suggested by Roman

inc :: Int -> Int
{-# INLINE CONLIKE [1] inc #-}
inc n = n+1

dec :: Int -> Int
{-# INLINE [1] dec #-}
dec n = n-1

{-# RULES  "dec/inc" forall n. dec (inc n) = n   #-}

data T = T !Int    -- The bang here prevents the rule firing

foo :: T -> Int
{-# INLINE foo #-}
foo (T n) = dec n + n

bar :: Int -> Int
bar n = foo (T (inc n))

The rule doesn't fire with the bang in the definition of T. If I remove the bang, it fires. It should fire in both cases.

The trouble is that, with the bang, we see something like this (in the output of phase 2 of the simplifier):

Roman.bar =
  \ (n_aat :: GHC.Types.Int) ->
    case Roman.inc n_aat of tpl_X3 { GHC.Types.I# ipv_skx ->
    case Roman.dec tpl_X3 of _ { GHC.Types.I# x_ak2 ->
    GHC.Types.I# (GHC.Prim.+# x_ak2 ipv_skx)
    }

but tpl_X3 is bound to (I# ipv_skx), not to (inc n_aat). Somehow we need both unfoldings for tpl_X3. That seems like a big step, so I'm just capturing the ticket but not actually doing anything about it yet.

Trac metadata

Trac field	Value
Version	6.12.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture