id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc	os	architecture	failure	difficulty	testcase	blockedby	blocking	related
3765	"Rules should ""look through"" case binders too"	simonpj		"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.
"	bug	new	normal	_|_	Compiler	6.12.1				Unknown/Multiple	Unknown/Multiple	None/Unknown