Nasty bug in RULE matching

Roman discovered a long-standing bug in RULE matching. . Suppose we have this rule:

  forall x y. f (g x) (h y) = i x y

which we match against this term:

  f (let a = 1 in g a) (let b = False in h b)

This is the result of the rewrite:

  let a = 1 in let b = False in (\x y -> i x y) a b

Fine so far. But suppose a and b have the same name (or, more precisely, unique). Now the original term looks like this:

  f (let a = 1 in g a) (let a = False in h a)

and gets rewritten to this:

  let a = 1 in let a = False in (\x y -> i x y) a a

Disaster!

Here is a concrete test case:

module RuleLetFloat where
foo :: Int -> Int
{-# INLINE foo #-}
foo x = g (bar (x,x))

bar :: (Int,Int) -> Int
{-# NOINLINE bar #-}
bar (x,y) = x

baz :: Int -> Int
{-# NOINLINE baz #-}
baz x = x

f :: Int -> Int -> Int
{-# NOINLINE f #-}
f x y = x+y

g :: Int -> Int
{-# NOINLINE g #-}
g x = x

{-# RULES

 "f/g" [1] forall x y. f (g x) (g y) = x + y

 #-}

main = print $ f (foo (baz 1)) (foo (baz 2))
-- Should print 3
-- Bug means that it prints 4

Trac metadata

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