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 |