Propagate evaluated-ness a bit more faithfully

This was provoked by Trac #13027.

The fix in Simplify actually cures the reported bug; see
Note [Case binder evaluated-ness] in Simplify.

The fix in CoreTidy looks like an omission that I fixed while I
was at it.

4 files changed, 54 insertions, 3 deletions

diff --git a/compiler/coreSyn/CoreTidy.hs b/compiler/coreSyn/CoreTidy.hs
index 000a8c5d88..7f82bece17 100644
--- a/compiler/coreSyn/CoreTidy.hs
+++ b/compiler/coreSyn/CoreTidy.hs
@@ -205,6 +205,8 @@ tidyLetBndr rec_tidy_env env@(tidy_env, var_env) (id,rhs)
                     `setUnfoldingInfo`  new_unf
 
         new_unf | isStableUnfolding old_unf = tidyUnfolding rec_tidy_env old_unf old_unf
+                | isEvaldUnfolding  old_unf = evaldUnfolding
+                                              -- See Note [Preserve evaluatedness]
                 | otherwise                 = noUnfolding
         old_unf = unfoldingInfo old_info
     in
diff --git a/compiler/simplCore/Simplify.hs b/compiler/simplCore/Simplify.hs
index 18abb2c8d9..e51ef054a4 100644
--- a/compiler/simplCore/Simplify.hs
+++ b/compiler/simplCore/Simplify.hs
@@ -2065,10 +2065,13 @@ simplAlts env scrut case_bndr alts cont'
   = do  { let env0 = zapFloats env
 
         ; (env1, case_bndr1) <- simplBinder env0 case_bndr
+        ; let case_bndr2 = case_bndr1 `setIdUnfolding` evaldUnfolding
+              env2       = modifyInScope env1 case_bndr2
+              -- See Note [Case-binder evaluated-ness]
 
         ; fam_envs <- getFamEnvs
-        ; (alt_env', scrut', case_bndr') <- improveSeq fam_envs env1 scrut
-                                                       case_bndr case_bndr1 alts
+        ; (alt_env', scrut', case_bndr') <- improveSeq fam_envs env2 scrut
+                                                       case_bndr case_bndr2 alts
 
         ; (imposs_deflt_cons, in_alts) <- prepareAlts scrut' case_bndr' alts
           -- NB: it's possible that the returned in_alts is empty: this is handled
@@ -2203,7 +2206,22 @@ zapBndrOccInfo keep_occ_info pat_id
   | keep_occ_info = pat_id
   | otherwise     = zapIdOccInfo pat_id
 
-{-
+{- Note [Case binder evaluated-ness]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We pin on a (OtherCon []) unfolding to the case-binder of a Case,
+even though it'll be over-ridden in every case alternative with a more
+informative unfolding.  Why?  Because suppose a later, less clever, pass
+simply replaces all occurrences of the case binder with the binder itself;
+then Lint may complain about the let/app invariant.  Example
+    case e of b { DEFAULT -> let v = reallyUnsafePtrEq# b y in ....
+                ; K       -> blah }
+
+The let/app invariant requires that y is evaluated in the call to
+reallyUnsafePtrEq#, which it is.  But we still want that to be true if we
+propagate binders to occurrences.
+
+This showed up in Trac #13027.
+
 Note [Add unfolding for scrutinee]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In general it's unlikely that a variable scrutinee will appear
diff --git a/testsuite/tests/simplCore/should_compile/T13027.hs b/testsuite/tests/simplCore/should_compile/T13027.hs
new file mode 100644
index 0000000000..727dfc5859
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T13027.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE MagicHash #-}
+module T13027 (insert) where
+
+import GHC.Exts (isTrue#, reallyUnsafePtrEquality#)
+
+data Set a = Bin {-# UNPACK #-} !Size !a !(Set a) !(Set a)
+           | Tip
+
+type Size = Int
+
+insert :: Ord a => a -> Set a -> Set a
+insert = go
+  where
+    go :: Ord a => a -> Set a -> Set a
+    go !x Tip = Bin 1 x Tip Tip
+    go !x t@(Bin sz y l r) = case compare x y of
+        LT | l' `ptrEq` l -> t
+           | otherwise -> undefined -- balanceL y l' r
+           where !l' = go x l
+        GT | r' `ptrEq` r -> t
+           | otherwise -> undefined -- balanceR y l r'
+           where !r' = go x r
+        EQ | x `ptrEq` y -> t
+           | otherwise -> Bin sz x l r
+{-# INLINABLE insert #-}
+
+ptrEq :: a -> a -> Bool
+ptrEq x y = isTrue# (reallyUnsafePtrEquality# x y)
+{-# INLINE ptrEq #-}
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index 6b852fc77c..c5666c4a6c 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -254,4 +254,5 @@ test('T12603',
      normal,
      run_command,
      ['$MAKE -s --no-print-directory T12603'])
+test('T13027', normal, compile, [''])