[commit: ghc] master: Fix a constant folding rule (65eec9c)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/65eec9cfd4410c0e30b0ed06116c15f8ce3de49d/ghc

>---------------------------------------------------------------

commit 65eec9cfd4410c0e30b0ed06116c15f8ce3de49d
Author: Andrey Mokhov <andrey.mokhov at gmail.com>
Date:   Wed Aug 29 15:16:51 2018 +0200

    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


>---------------------------------------------------------------

65eec9cfd4410c0e30b0ed06116c15f8ce3de49d
 compiler/prelude/PrelRules.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/compiler/prelude/PrelRules.hs b/compiler/prelude/PrelRules.hs
index 695e879..80cfa20 100644
--- a/compiler/prelude/PrelRules.hs
+++ b/compiler/prelude/PrelRules.hs
@@ -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)