Commit 65eec9cf authored by Andrey Mokhov's avatar Andrey Mokhov Committed by Krzysztof Gogolewski

Fix a constant folding rule

Summary:
One of the constant folding rules introduced in D2858 is:

```
(L y :-:   v) :-: (L x :-: w) -> return $ mkL (y-x)   `add` (w `add` v)
```

Or, after removing syntactic noise: `(y - v) - (x - w) ==> (y - x) + (w + v)`.
This is incorrect, since the sign of `v` is changed from negative to positive.
As a consequence, the following program prints `3` when compiled with `-O`:

```
-- This is just subtraction in disguise
minus :: Int -> Int -> Int
minus x y = (8 - y) - (8 - x)
{-# NOINLINE minus #-}

main :: IO ()
main = print (2 `minus` 1)
```

The correct rule is: `(y - v) - (x - w) ==> (y - x) + (w - v)`.

This commit does the fix. I haven't found any other issues with the constant
folding code, but it's difficult to be certain without some automated checking.

Reviewers: bgamari, tdammers

Subscribers: hsyl20, tdammers, rwbarton, carter

GHC Trac Issues: #15569

Differential Revision: https://phabricator.haskell.org/D5109
parent 36c1431d
......@@ -1783,7 +1783,7 @@ numFoldingRules op dict = do
(v :-: L y) :-: (w :-: L x) -> return $ mkL (x-y) `add` (v `sub` w)
(v :-: L y) :-: (L x :-: w) -> return $ mkL (0-x-y) `add` (v `add` w)
(L y :-: v) :-: (w :-: L x) -> return $ mkL (x+y) `sub` (v `add` w)
(L y :-: v) :-: (L x :-: w) -> return $ mkL (y-x) `add` (w `add` v)
(L y :-: v) :-: (L x :-: w) -> return $ mkL (y-x) `add` (w `sub` v)
(x :++: w) :-: (y :++: v) -> return $ mkL (x-y) `add` (w `sub` v)
(w :-: L x) :-: (y :++: v) -> return $ mkL (0-y-x) `add` (w `sub` v)
(L x :-: w) :-: (y :++: v) -> return $ mkL (x-y) `sub` (v `add` w)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment