Fix two bugs in caes-floating (fixes Trac #5453)

The problem is documented in the ticket.  The patch
does two things

1. Make exprOkForSpeculation return False for a non-exhaustive case

2. In SetLevels.lvlExpr, look at the *result* scrutinee, not the
   *input* scrutinee, when testing for evaluated-ness

compiler/coreSyn/CoreUtils.lhs

@@ -688,7 +688,9 @@ it's applied only to dictionaries.
 -- 
 -- We can only do this if the @y + 1@ is ok for speculation: it has no
 -- side effects, and can't diverge or raise an exception.
-exprOkForSpeculation :: CoreExpr -> Bool
+exprOkForSpeculation :: Expr b -> Bool
+  -- Polymorphic in binder type
+  -- There is one call at a non-Id binder type, in SetLevels
 exprOkForSpeculation (Lit _)      = True
 exprOkForSpeculation (Type _)     = True
 exprOkForSpeculation (Coercion _) = True
@@ -706,6 +708,7 @@ exprOkForSpeculation (Cast e _)  = exprOkForSpeculation e
 exprOkForSpeculation (Case e _ _ alts) 
   =  exprOkForSpeculation e  -- Note [exprOkForSpeculation: case expressions]
   && all (\(_,_,rhs) -> exprOkForSpeculation rhs) alts
+  && altsAreExhaustive alts	-- Note [exprOkForSpeculation: exhaustive alts]
 
 exprOkForSpeculation other_expr
   = case collectArgs other_expr of
@@ -740,6 +743,21 @@ exprOkForSpeculation other_expr
 
     spec_ok _ _ = False
 
+altsAreExhaustive :: [Alt b] -> Bool
+-- True  <=> the case alterantives are definiely exhaustive
+-- False <=> they may or may not be
+altsAreExhaustive []
+  = False    -- Should not happen
+altsAreExhaustive ((con1,_,_) : alts)
+  = case con1 of
+      DEFAULT   -> True
+      LitAlt {} -> False
+      DataAlt c -> 1 + length alts == tyConFamilySize (dataConTyCon c)
+      -- It is possible to have an exhaustive case that does not
+      -- enumerate all constructors, notably in a GADT match, but
+      -- we behave conservatively here -- I don't think it's important
+      -- enough to deserve special treatment
+
 -- | True of dyadic operators that can fail only if the second arg is zero!
 isDivOp :: PrimOp -> Bool
 -- This function probably belongs in PrimOp, or even in 
@@ -782,6 +800,28 @@ If exprOkForSpeculation doesn't look through case expressions, you get this:
 
 The inner case is redundant, and should be nuked.
 
+Note [exprOkForSpeculation: exhaustive alts]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We might have something like
+  case x of { 
+    A -> ...
+    _ -> ...(case x of { B -> ...; C -> ... })...
+Here, the inner case is fine, becuase the A alternative 
+can't happen, but it's not ok to float the inner case outside 
+the outer one (even if we know x is evaluated outside), because
+then it would be non-exhaustive. See Trac #5453.
+
+Similarly, this is a valid program (albeit a slightly dodgy one)
+   let v = case x of { B -> ...; C -> ... }
+   in case x of 
+         A -> ...
+         _ ->  ...v...v....
+But we don't want to speculate the v binding.
+
+One could try to be clever, but the easy fix is simpy to regard
+a non-exhaustive case as *not* okForSpeculation.
+
+
 Note [dataToTag speculation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Is this OK?

compiler/simplCore/FloatOut.lhs

@@ -440,7 +440,10 @@ partitionByMajorLevel.
 \begin{code}
 data FloatBind 
   = FloatLet FloatLet  
-  | FloatCase CoreExpr Id DataCon [Var]       -- case e of y { C ys -> ... }
+
+  | FloatCase CoreExpr Id DataCon [Var]       
+      -- case e of y { C ys -> ... }
+      -- See Note [Floating cases] in SetLevels
 
 type FloatLet = CoreBind	-- INVARIANT: a FloatLet is always lifted
 type MajorEnv = M.IntMap MinorEnv	  -- Keyed by major level

compiler/simplCore/SetLevels.lhs

@@ -341,13 +341,25 @@ lvlExpr ctxt_lvl env (_, AnnLet bind body) = do
     return (Let bind' body')
 
 lvlExpr ctxt_lvl env (_, AnnCase scrut@(scrut_fvs,_) case_bndr ty alts)
+  = do { scrut' <- lvlMFE True ctxt_lvl env scrut
+       ; lvlCase ctxt_lvl env scrut_fvs scrut' case_bndr ty alts }
+
+-------------------------------------------
+lvlCase :: Level		-- ctxt_lvl: Level of enclosing expression
+	-> LevelEnv		-- Level of in-scope names/tyvars
+        -> VarSet		-- Free vars of input scrutinee
+        -> LevelledExpr		-- Processed scrutinee
+	-> Id -> Type		-- Case binder and result type
+	-> [AnnAlt Id VarSet]	-- Input alternatives
+	-> LvlM LevelledExpr	-- Result expression
+lvlCase ctxt_lvl env scrut_fvs scrut' case_bndr ty alts
   | [(con@(DataAlt {}), bs, rhs)] <- alts
-  , exprOkForSpeculation (deAnnotate scrut)
-  , not (isTopLvl dest_lvl)	-- Can't have top-level cases
-  = 	-- Always float the case if possible
+  , exprOkForSpeculation scrut'	  -- See Note [Check the output scrutinee for okForSpec]
+  , not (isTopLvl dest_lvl)	  -- Can't have top-level cases
+  =     -- See Note [Case floating]
+    	-- Always float the case if possible
   	-- Unlike lets we don't insist that it escapes a value lambda
-    do { scrut' <- lvlMFE True ctxt_lvl env scrut
-       ; (rhs_env, (case_bndr':bs')) <- cloneVars env (case_bndr:bs) dest_lvl
+    do { (rhs_env, (case_bndr':bs')) <- cloneVars env (case_bndr:bs) dest_lvl
        	 	   -- We don't need to use extendCaseBndrLvlEnv here
 		   -- because we are floating the case outwards so
 		   -- no need to do the binder-swap thing
@@ -356,8 +368,7 @@ lvlExpr ctxt_lvl env (_, AnnCase scrut@(scrut_fvs,_) case_bndr ty alts)
        ; return (Case scrut' (TB case_bndr' (FloatMe dest_lvl)) ty [alt']) }
 
   | otherwise	  -- Stays put
-  = do { scrut' <- lvlMFE True ctxt_lvl env scrut
-       ; let case_bndr' = TB case_bndr bndr_spec
+  = do { let case_bndr' = TB case_bndr bndr_spec
              alts_env   = extendCaseBndrLvlEnv env scrut' case_bndr'
        ; alts' <- mapM (lvl_alt alts_env) alts
        ; return (Case scrut' case_bndr' ty alts') }
@@ -375,51 +386,46 @@ lvlExpr ctxt_lvl env (_, AnnCase scrut@(scrut_fvs,_) case_bndr ty alts)
           new_env = extendLvlEnv alts_env bs'
 \end{code}
 
-@lvlMFE@ is just like @lvlExpr@, except that it might let-bind
-the expression, so that it can itself be floated.
-
-Note [Unlifted MFEs]
-~~~~~~~~~~~~~~~~~~~~
-We don't float unlifted MFEs, which potentially loses big opportunites.
-For example:
-	\x -> f (h y)
-where h :: Int -> Int# is expensive. We'd like to float the (h y) outside
-the \x, but we don't because it's unboxed.  Possible solution: box it.
-
-Note [Bottoming floats]
-~~~~~~~~~~~~~~~~~~~~~~~
-If we see
-	f = \x. g (error "urk")
-we'd like to float the call to error, to get
-	lvl = error "urk"
-	f = \x. g lvl
-Furthermore, we want to float a bottoming expression even if it has free
-variables:
-	f = \x. g (let v = h x in error ("urk" ++ v))
-Then we'd like to abstact over 'x' can float the whole arg of g:
-	lvl = \x. let v = h x in error ("urk" ++ v)
-	f = \x. g (lvl x)
-See Maessen's paper 1999 "Bottom extraction: factoring error handling out
-of functional programs" (unpublished I think).
-
-When we do this, we set the strictness and arity of the new bottoming 
-Id, so that it's properly exposed as such in the interface file, even if
-this is all happening after strictness analysis.  
-
-Note [Bottoming floats: eta expansion] c.f Note [Bottoming floats]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Tiresomely, though, the simplifier has an invariant that the manifest
-arity of the RHS should be the same as the arity; but we can't call
-etaExpand during SetLevels because it works over a decorated form of
-CoreExpr.  So we do the eta expansion later, in FloatOut.
-
-Note [Case MFEs]
-~~~~~~~~~~~~~~~~
-We don't float a case expression as an MFE from a strict context.  Why not?
-Because in doing so we share a tiny bit of computation (the switch) but
-in exchange we build a thunk, which is bad.  This case reduces allocation 
-by 7% in spectral/puzzle (a rather strange benchmark) and 1.2% in real/fem.
-Doesn't change any other allocation at all.
+Note [Floating cases]
+~~~~~~~~~~~~~~~~~~~~~
+Consider this:
+  data T a = MkT !a
+  f :: T Int -> blah
+  f x vs = case x of { MkT y -> 
+             let f vs = ...(case y of I# w -> e)...f..
+             in f vs
+Here we can float the (case y ...) out , because y is sure
+to be evaluated, to give
+  f x vs = case x of { MkT y -> 
+           caes y of I# w ->
+             let f vs = ...(e)...f..
+             in f vs
+
+That saves unboxing it every time round the loop.  It's important in
+some DPH stuff where we really want to avoid that repeated unboxing in
+the inner loop.
+
+Things to note
+ * We can't float a case to top level
+ * It's worth doing this float even if we don't float
+   the case outside a value lambda
+ * We only do this with a single-alternative case
+
+Note [Check the output scrutinee for okForSpec]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this:
+  case x of y { 
+    A -> ....(case y of alts)....
+  }
+Because of the binder-swap, the inner case will get substituted to
+(case x of ..).  So when testing whether the scrutinee is
+okForSpecuation we must be careful to test the *result* scrutinee ('x'
+in this case), not the *input* one 'y'.  The latter *is* ok for
+speculation here, but the former is not -- and ideed we can't float
+the inner case out, at least not unless x is also evaluated at its
+binding site.
+
+That's why we apply exprOkForSpeculation to scrut' and not to scrut.
 
 \begin{code}
 lvlMFE ::  Bool			-- True <=> strict context [body of case or let]
@@ -427,6 +433,8 @@ lvlMFE ::  Bool			-- True <=> strict context [body of case or let]
 	-> LevelEnv		-- Level of in-scope names/tyvars
 	-> CoreExprWithFVs	-- input expression
 	-> LvlM LevelledExpr	-- Result expression
+-- lvlMFE is just like lvlExpr, except that it might let-bind
+-- the expression, so that it can itself be floated.
 
 lvlMFE _ _ _ (_, AnnType ty)
   = return (Type ty)
@@ -492,7 +500,52 @@ lvlMFE strict_ctxt ctxt_lvl env ann_expr@(fvs, _)
 	  -- 
 	  -- Also a strict contxt includes uboxed values, and they
 	  -- can't be bound at top level
+\end{code}
+
+Note [Unlifted MFEs]
+~~~~~~~~~~~~~~~~~~~~
+We don't float unlifted MFEs, which potentially loses big opportunites.
+For example:
+	\x -> f (h y)
+where h :: Int -> Int# is expensive. We'd like to float the (h y) outside
+the \x, but we don't because it's unboxed.  Possible solution: box it.
+
+Note [Bottoming floats]
+~~~~~~~~~~~~~~~~~~~~~~~
+If we see
+	f = \x. g (error "urk")
+we'd like to float the call to error, to get
+	lvl = error "urk"
+	f = \x. g lvl
+Furthermore, we want to float a bottoming expression even if it has free
+variables:
+	f = \x. g (let v = h x in error ("urk" ++ v))
+Then we'd like to abstact over 'x' can float the whole arg of g:
+	lvl = \x. let v = h x in error ("urk" ++ v)
+	f = \x. g (lvl x)
+See Maessen's paper 1999 "Bottom extraction: factoring error handling out
+of functional programs" (unpublished I think).
+
+When we do this, we set the strictness and arity of the new bottoming 
+Id, so that it's properly exposed as such in the interface file, even if
+this is all happening after strictness analysis.  
 
+Note [Bottoming floats: eta expansion] c.f Note [Bottoming floats]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Tiresomely, though, the simplifier has an invariant that the manifest
+arity of the RHS should be the same as the arity; but we can't call
+etaExpand during SetLevels because it works over a decorated form of
+CoreExpr.  So we do the eta expansion later, in FloatOut.
+
+Note [Case MFEs]
+~~~~~~~~~~~~~~~~
+We don't float a case expression as an MFE from a strict context.  Why not?
+Because in doing so we share a tiny bit of computation (the switch) but
+in exchange we build a thunk, which is bad.  This case reduces allocation 
+by 7% in spectral/puzzle (a rather strange benchmark) and 1.2% in real/fem.
+Doesn't change any other allocation at all.
+
+\begin{code}
 annotateBotStr :: Id -> Maybe (Arity, StrictSig) -> Id
 annotateBotStr id Nothing            = id
 annotateBotStr id (Just (arity,sig)) = id `setIdArity` arity