Record evaluated-ness information correctly for strict constructors
[ghc-hetmet.git] / compiler / simplCore / Simplify.lhs
index efd1b78..baf2a30 100644 (file)
@@ -4,24 +4,30 @@
 \section[Simplify]{The main module of the simplifier}
 
 \begin{code}
 \section[Simplify]{The main module of the simplifier}
 
 \begin{code}
+{-# OPTIONS -w #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+
 module Simplify ( simplTopBinds, simplExpr ) where
 
 #include "HsVersions.h"
 
 module Simplify ( simplTopBinds, simplExpr ) where
 
 #include "HsVersions.h"
 
-import DynFlags        ( dopt, DynFlag(Opt_D_dump_inlinings),
-                         SimplifierSwitch(..)
-                       )
+import DynFlags
 import SimplMonad
 import Type hiding     ( substTy, extendTvSubst )
 import SimplEnv        
 import SimplUtils
 import Id
 import SimplMonad
 import Type hiding     ( substTy, extendTvSubst )
 import SimplEnv        
 import SimplUtils
 import Id
+import Var
 import IdInfo
 import Coercion
 import IdInfo
 import Coercion
-import TcGadt          ( dataConCanMatch )
-import DataCon         ( dataConTyCon, dataConRepStrictness )
-import TyCon           ( tyConArity, isAlgTyCon, isNewTyCon, tyConDataCons_maybe )
+import FamInstEnv      ( topNormaliseType )
+import DataCon         ( dataConRepStrictness, dataConUnivTyVars )
 import CoreSyn
 import CoreSyn
+import NewDemand       ( isStrictDmd )
 import PprCore         ( pprParendExpr, pprCoreExpr )
 import CoreUnfold      ( mkUnfolding, callSiteInline )
 import CoreUtils
 import PprCore         ( pprParendExpr, pprCoreExpr )
 import CoreUnfold      ( mkUnfolding, callSiteInline )
 import CoreUtils
@@ -32,8 +38,8 @@ import TysPrim                ( realWorldStatePrimTy )
 import PrelInfo                ( realWorldPrimId )
 import BasicTypes      ( TopLevelFlag(..), isTopLevel, 
                          RecFlag(..), isNonRuleLoopBreaker )
 import PrelInfo                ( realWorldPrimId )
 import BasicTypes      ( TopLevelFlag(..), isTopLevel, 
                          RecFlag(..), isNonRuleLoopBreaker )
-import List            ( nub )
 import Maybes          ( orElse )
 import Maybes          ( orElse )
+import Data.List       ( mapAccumL )
 import Outputable
 import Util
 \end{code}
 import Outputable
 import Util
 \end{code}
@@ -208,7 +214,8 @@ simplTopBinds env binds
                -- It's rather as if the top-level binders were imported.
        ; env <- simplRecBndrs env (bindersOfBinds binds)
        ; dflags <- getDOptsSmpl
                -- It's rather as if the top-level binders were imported.
        ; env <- simplRecBndrs env (bindersOfBinds binds)
        ; dflags <- getDOptsSmpl
-       ; let dump_flag = dopt Opt_D_dump_inlinings dflags
+       ; let dump_flag = dopt Opt_D_dump_inlinings dflags || 
+                         dopt Opt_D_dump_rule_firings dflags
        ; env' <- simpl_binds dump_flag env binds
        ; freeTick SimplifierDone
        ; return (getFloats env') }
        ; env' <- simpl_binds dump_flag env binds
        ; freeTick SimplifierDone
        ; return (getFloats env') }
@@ -216,6 +223,9 @@ simplTopBinds env binds
        -- We need to track the zapped top-level binders, because
        -- they should have their fragile IdInfo zapped (notably occurrence info)
        -- That's why we run down binds and bndrs' simultaneously.
        -- We need to track the zapped top-level binders, because
        -- they should have their fragile IdInfo zapped (notably occurrence info)
        -- That's why we run down binds and bndrs' simultaneously.
+       --
+       -- The dump-flag emits a trace for each top-level binding, which
+       -- helps to locate the tracing for inlining and rule firing
     simpl_binds :: Bool -> SimplEnv -> [InBind] -> SimplM SimplEnv
     simpl_binds dump env []          = return env
     simpl_binds dump env (bind:binds) = do { env' <- trace dump bind $
     simpl_binds :: Bool -> SimplEnv -> [InBind] -> SimplM SimplEnv
     simpl_binds dump env []          = return env
     simpl_binds dump env (bind:binds) = do { env' <- trace dump bind $
@@ -225,8 +235,10 @@ simplTopBinds env binds
     trace True  bind = pprTrace "SimplBind" (ppr (bindersOf bind))
     trace False bind = \x -> x
 
     trace True  bind = pprTrace "SimplBind" (ppr (bindersOf bind))
     trace False bind = \x -> x
 
-    simpl_bind env (NonRec b r) = simplRecOrTopPair env TopLevel b r
-    simpl_bind env (Rec pairs)  = simplRecBind      env TopLevel pairs
+    simpl_bind env (Rec pairs)  = simplRecBind      env  TopLevel pairs
+    simpl_bind env (NonRec b r) = simplRecOrTopPair env' TopLevel b b' r
+       where
+         (env', b') = addBndrRules env b (lookupRecBndr env b)
 \end{code}
 
 
 \end{code}
 
 
@@ -244,15 +256,22 @@ simplRecBind :: SimplEnv -> TopLevelFlag
             -> [(InId, InExpr)]
             -> SimplM SimplEnv
 simplRecBind env top_lvl pairs
             -> [(InId, InExpr)]
             -> SimplM SimplEnv
 simplRecBind env top_lvl pairs
-  = do { env' <- go (zapFloats env) pairs
+  = do { let (env_with_info, triples) = mapAccumL add_rules env pairs
+       ; env' <- go (zapFloats env_with_info) triples
        ; return (env `addRecFloats` env') }
        -- addFloats adds the floats from env', 
        -- *and* updates env with the in-scope set from env'
   where
        ; return (env `addRecFloats` env') }
        -- addFloats adds the floats from env', 
        -- *and* updates env with the in-scope set from env'
   where
+    add_rules :: SimplEnv -> (InBndr,InExpr) -> (SimplEnv, (InBndr, OutBndr, InExpr))
+       -- Add the (substituted) rules to the binder
+    add_rules env (bndr, rhs) = (env', (bndr, bndr', rhs))
+       where
+         (env', bndr') = addBndrRules env bndr (lookupRecBndr env bndr)
+
     go env [] = return env
        
     go env [] = return env
        
-    go env ((bndr, rhs) : pairs)
-       = do { env <- simplRecOrTopPair env top_lvl bndr rhs
+    go env ((old_bndr, new_bndr, rhs) : pairs)
+       = do { env <- simplRecOrTopPair env top_lvl old_bndr new_bndr rhs
             ; go env pairs }
 \end{code}
 
             ; go env pairs }
 \end{code}
 
@@ -265,18 +284,16 @@ It assumes the binder has already been simplified, but not its IdInfo.
 \begin{code}
 simplRecOrTopPair :: SimplEnv
                  -> TopLevelFlag
 \begin{code}
 simplRecOrTopPair :: SimplEnv
                  -> TopLevelFlag
-                 -> InId -> InExpr     -- Binder and rhs
+                 -> InId -> OutBndr -> InExpr  -- Binder and rhs
                  -> SimplM SimplEnv    -- Returns an env that includes the binding
 
                  -> SimplM SimplEnv    -- Returns an env that includes the binding
 
-simplRecOrTopPair env top_lvl bndr rhs
-  | preInlineUnconditionally env top_lvl bndr rhs      -- Check for unconditional inline
-  = do { tick (PreInlineUnconditionally bndr)
-       ; return (extendIdSubst env bndr (mkContEx env rhs)) }
+simplRecOrTopPair env top_lvl old_bndr new_bndr rhs
+  | preInlineUnconditionally env top_lvl old_bndr rhs          -- Check for unconditional inline
+  = do { tick (PreInlineUnconditionally old_bndr)
+       ; return (extendIdSubst env old_bndr (mkContEx env rhs)) }
 
   | otherwise
 
   | otherwise
-  = do { let bndr' = lookupRecBndr env bndr
-             (env', bndr'') = addLetIdInfo env bndr bndr'
-       ; simplLazyBind env' top_lvl Recursive bndr bndr'' rhs env' }
+  = simplLazyBind env top_lvl Recursive old_bndr new_bndr rhs env 
        -- May not actually be recursive, but it doesn't matter
 \end{code}
 
        -- May not actually be recursive, but it doesn't matter
 \end{code}
 
@@ -304,46 +321,38 @@ simplLazyBind :: SimplEnv
              -> SimplM SimplEnv
 
 simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
              -> SimplM SimplEnv
 
 simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
-  = do { let   rhs_env  = rhs_se `setInScope` env
-               rhs_cont = mkRhsStop (idType bndr1)
+  = do { let   rhs_env     = rhs_se `setInScope` env
+               (tvs, body) = collectTyBinders rhs
+       ; (body_env, tvs') <- simplBinders rhs_env tvs
+               -- See Note [Floating and type abstraction]
+               -- in SimplUtils
 
        -- Simplify the RHS; note the mkRhsStop, which tells 
        -- the simplifier that this is the RHS of a let.
 
        -- Simplify the RHS; note the mkRhsStop, which tells 
        -- the simplifier that this is the RHS of a let.
-       ; (rhs_env1, rhs1) <- simplExprF rhs_env rhs rhs_cont
-
-       -- If any of the floats can't be floated, give up now
-       -- (The canFloat predicate says True for empty floats.)
-       ; if (not (canFloat top_lvl is_rec False rhs_env1))
-         then  completeBind env top_lvl bndr bndr1
-                                (wrapFloats rhs_env1 rhs1)
-         else do
+       ; let rhs_cont = mkRhsStop (applyTys (idType bndr1) (mkTyVarTys tvs'))
+       ; (body_env1, body1) <- simplExprF body_env body rhs_cont
+
        -- ANF-ise a constructor or PAP rhs
        -- ANF-ise a constructor or PAP rhs
-       { (rhs_env2, rhs2) <- prepareRhs rhs_env1 rhs1
-       ; (env', rhs3) <- chooseRhsFloats top_lvl is_rec False env rhs_env2 rhs2
-       ; completeBind env' top_lvl bndr bndr1 rhs3 } }
-
-chooseRhsFloats :: TopLevelFlag -> RecFlag -> Bool
-               -> SimplEnv     -- Env for the let
-               -> SimplEnv     -- Env for the RHS, with RHS floats in it
-               -> OutExpr              -- ..and the RHS itself
-               -> SimplM (SimplEnv, OutExpr)   -- New env for let, and RHS
-
-chooseRhsFloats top_lvl is_rec is_strict env rhs_env rhs
-  | not (isEmptyFloats rhs_env)                -- Something to float
-  , canFloat top_lvl is_rec is_strict rhs_env  -- ...that can float
-  , (isTopLevel top_lvl  || exprIsCheap rhs)   -- ...and we want to float      
-  = do { tick LetFloatFromLet  -- Float
-       ; return (addFloats env rhs_env, rhs) } -- Add the floats to the main env
-  | otherwise                  -- Don't float
-  = return (env, wrapFloats rhs_env rhs)       -- Wrap the floats around the RHS
-\end{code}
+       ; (body_env2, body2) <- prepareRhs body_env1 body1
 
 
+       ; (env', rhs')
+           <-  if not (doFloatFromRhs top_lvl is_rec False body2 body_env2)
+               then                            -- No floating, just wrap up!
+                    do { rhs' <- mkLam tvs' (wrapFloats body_env2 body2)
+                       ; return (env, rhs') }
 
 
-%************************************************************************
-%*                                                                     *
-\subsection{simplNonRec}
-%*                                                                     *
-%************************************************************************
+               else if null tvs then           -- Simple floating
+                    do { tick LetFloatFromLet
+                       ; return (addFloats env body_env2, body2) }
+
+               else                            -- Do type-abstraction first
+                    do { tick LetFloatFromLet
+                       ; (poly_binds, body3) <- abstractFloats tvs' body_env2 body2
+                       ; rhs' <- mkLam tvs' body3
+                       ; return (extendFloats env poly_binds, rhs') }
+
+       ; completeBind env' top_lvl bndr bndr1 rhs' }
+\end{code}
 
 A specialised variant of simplNonRec used when the RHS is already simplified, 
 notably in knownCon.  It uses case-binding where necessary.
 
 A specialised variant of simplNonRec used when the RHS is already simplified, 
 notably in knownCon.  It uses case-binding where necessary.
@@ -357,7 +366,7 @@ simplNonRecX :: SimplEnv
 simplNonRecX env bndr new_rhs
   = do { (env, bndr') <- simplBinder env bndr
        ; completeNonRecX env NotTopLevel NonRecursive
 simplNonRecX env bndr new_rhs
   = do { (env, bndr') <- simplBinder env bndr
        ; completeNonRecX env NotTopLevel NonRecursive
-                         (isStrictBndr bndr) bndr bndr' new_rhs }
+                         (isStrictId bndr) bndr bndr' new_rhs }
 
 completeNonRecX :: SimplEnv
                -> TopLevelFlag -> RecFlag -> Bool
 
 completeNonRecX :: SimplEnv
                -> TopLevelFlag -> RecFlag -> Bool
@@ -368,7 +377,11 @@ completeNonRecX :: SimplEnv
 
 completeNonRecX env top_lvl is_rec is_strict old_bndr new_bndr new_rhs
   = do         { (env1, rhs1) <- prepareRhs (zapFloats env) new_rhs
 
 completeNonRecX env top_lvl is_rec is_strict old_bndr new_bndr new_rhs
   = do         { (env1, rhs1) <- prepareRhs (zapFloats env) new_rhs
-       ; (env2, rhs2) <- chooseRhsFloats top_lvl is_rec is_strict env env1 rhs1
+       ; (env2, rhs2) <- 
+               if doFloatFromRhs top_lvl is_rec is_strict rhs1 env1
+               then do { tick LetFloatFromLet
+                       ; return (addFloats env env1, rhs1) }   -- Add the floats to the main env
+               else return (env, wrapFloats env1 rhs1)         -- Wrap the floats around the RHS
        ; completeBind env2 NotTopLevel old_bndr new_bndr rhs2 }
 \end{code}
 
        ; completeBind env2 NotTopLevel old_bndr new_bndr rhs2 }
 \end{code}
 
@@ -397,6 +410,7 @@ completeNonRecX env top_lvl is_rec is_strict old_bndr new_bndr new_rhs
   = thing_inside (extendIdSubst env bndr (DoneEx new_rhs))
 -}
 
   = thing_inside (extendIdSubst env bndr (DoneEx new_rhs))
 -}
 
+----------------------------------
 prepareRhs takes a putative RHS, checks whether it's a PAP or
 constructor application and, if so, converts it to ANF, so that the 
 resulting thing can be inlined more easily.  Thus
 prepareRhs takes a putative RHS, checks whether it's a PAP or
 constructor application and, if so, converts it to ANF, so that the 
 resulting thing can be inlined more easily.  Thus
@@ -406,29 +420,48 @@ becomes
        t2 = g b
        x = (t1,t2)
 
        t2 = g b
        x = (t1,t2)
 
+We also want to deal well cases like this
+       v = (f e1 `cast` co) e2
+Here we want to make e1,e2 trivial and get
+       x1 = e1; x2 = e2; v = (f x1 `cast` co) v2
+That's what the 'go' loop in prepareRhs does
+
 \begin{code}
 prepareRhs :: SimplEnv -> OutExpr -> SimplM (SimplEnv, OutExpr)
 -- Adds new floats to the env iff that allows us to return a good RHS
 \begin{code}
 prepareRhs :: SimplEnv -> OutExpr -> SimplM (SimplEnv, OutExpr)
 -- Adds new floats to the env iff that allows us to return a good RHS
-
-prepareRhs env (Cast rhs co)   -- Note [Float coersions]
+prepareRhs env (Cast rhs co)   -- Note [Float coercions]
+  | (ty1, ty2) <- coercionKind co      -- Do *not* do this if rhs has an unlifted type
+  , not (isUnLiftedType ty1)           -- see Note [Float coercions (unlifted)]
   = do { (env', rhs') <- makeTrivial env rhs
        ; return (env', Cast rhs' co) }
 
 prepareRhs env rhs
   = do { (env', rhs') <- makeTrivial env rhs
        ; return (env', Cast rhs' co) }
 
 prepareRhs env rhs
-  | (Var fun, args) <- collectArgs rhs         -- It's an application
-  , let n_args = valArgCount args      
-  , n_args > 0                                 -- ...but not a trivial one     
-  , isDataConWorkId fun || n_args < idArity fun        -- ...and it's a constructor or PAP
-  = go env (Var fun) args
+  = do { (is_val, env', rhs') <- go 0 env rhs 
+       ; return (env', rhs') }
   where
   where
-    go env fun []          = return (env, fun)
-    go env fun (arg : args) = do { (env', arg') <- makeTrivial env arg
-                                ; go env' (App fun arg') args }
-
-prepareRhs env rhs             -- The default case
-  = return (env, rhs)
+    go n_val_args env (Cast rhs co)
+       = do { (is_val, env', rhs') <- go n_val_args env rhs
+            ; return (is_val, env', Cast rhs' co) }
+    go n_val_args env (App fun (Type ty))
+       = do { (is_val, env', rhs') <- go n_val_args env fun
+            ; return (is_val, env', App rhs' (Type ty)) }
+    go n_val_args env (App fun arg)
+       = do { (is_val, env', fun') <- go (n_val_args+1) env fun
+            ; case is_val of
+               True -> do { (env'', arg') <- makeTrivial env' arg
+                          ; return (True, env'', App fun' arg') }
+               False -> return (False, env, App fun arg) }
+    go n_val_args env (Var fun)
+       = return (is_val, env, Var fun)
+       where
+         is_val = n_val_args > 0       -- There is at least one arg
+                                       -- ...and the fun a constructor or PAP
+                && (isDataConWorkId fun || n_val_args < idArity fun)
+    go n_val_args env other
+       = return (False, env, other)
 \end{code}
 
 \end{code}
 
+
 Note [Float coercions]
 ~~~~~~~~~~~~~~~~~~~~~~
 When we find the binding
 Note [Float coercions]
 ~~~~~~~~~~~~~~~~~~~~~~
 When we find the binding
@@ -451,6 +484,22 @@ and lead to further optimisation.  Example:
           go n = case x of { T m -> go (n-m) }
                -- This case should optimise
 
           go n = case x of { T m -> go (n-m) }
                -- This case should optimise
 
+Note [Float coercions (unlifted)]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+BUT don't do [Float coercions] if 'e' has an unlifted type. 
+This *can* happen:
+
+     foo :: Int = (error (# Int,Int #) "urk") 
+                 `cast` CoUnsafe (# Int,Int #) Int
+
+If do the makeTrivial thing to the error call, we'll get
+    foo = case error (# Int,Int #) "urk" of v -> v `cast` ...
+But 'v' isn't in scope!  
+
+These strange casts can happen as a result of case-of-case
+       bar = case (case x of { T -> (# 2,3 #); F -> error "urk" }) of
+               (# p,q #) -> p+q
+
 
 \begin{code}
 makeTrivial :: SimplEnv -> OutExpr -> SimplM (SimplEnv, OutExpr)
 
 \begin{code}
 makeTrivial :: SimplEnv -> OutExpr -> SimplM (SimplEnv, OutExpr)
@@ -537,6 +586,8 @@ completeBind env top_lvl old_bndr new_bndr new_rhs
        -- (for example) be no longer strictly demanded.
        -- The solution here is a bit ad hoc...
        info_w_unf = new_bndr_info `setUnfoldingInfo` unfolding
        -- (for example) be no longer strictly demanded.
        -- The solution here is a bit ad hoc...
        info_w_unf = new_bndr_info `setUnfoldingInfo` unfolding
+                                  `setWorkerInfo`    worker_info
+
         final_info | loop_breaker              = new_bndr_info
                   | isEvaldUnfolding unfolding = zapDemandInfo info_w_unf `orElse` info_w_unf
                   | otherwise                  = info_w_unf
         final_info | loop_breaker              = new_bndr_info
                   | isEvaldUnfolding unfolding = zapDemandInfo info_w_unf `orElse` info_w_unf
                   | otherwise                  = info_w_unf
@@ -550,6 +601,7 @@ completeBind env top_lvl old_bndr new_bndr new_rhs
     return (addNonRec env final_id new_rhs)
   where 
     unfolding    = mkUnfolding (isTopLevel top_lvl) new_rhs
     return (addNonRec env final_id new_rhs)
   where 
     unfolding    = mkUnfolding (isTopLevel top_lvl) new_rhs
+    worker_info  = substWorker env (workerInfo old_info)
     loop_breaker = isNonRuleLoopBreaker occ_info
     old_info     = idInfo old_bndr
     occ_info     = occInfo old_info
     loop_breaker = isNonRuleLoopBreaker occ_info
     old_info     = idInfo old_bndr
     occ_info     = occInfo old_info
@@ -735,8 +787,9 @@ simplCast env body co cont
   where
        addCoerce co cont = add_coerce co (coercionKind co) cont
 
   where
        addCoerce co cont = add_coerce co (coercionKind co) cont
 
-       add_coerce co (s1, k1) cont 
-         | s1 `coreEqType` k1 = cont
+       add_coerce co (s1, k1) cont     -- co :: ty~ty
+         | s1 `coreEqType` k1 = cont   -- is a no-op
+
        add_coerce co1 (s1, k2) (CoerceIt co2 cont)
          | (l1, t1) <- coercionKind co2
                 --     coerce T1 S1 (coerce S1 K1 e)
        add_coerce co1 (s1, k2) (CoerceIt co2 cont)
          | (l1, t1) <- coercionKind co2
                 --     coerce T1 S1 (coerce S1 K1 e)
@@ -751,9 +804,19 @@ simplCast env body co cont
          , s1 `coreEqType` t1  = cont           -- The coerces cancel out  
          | otherwise           = CoerceIt (mkTransCoercion co1 co2) cont
     
          , s1 `coreEqType` t1  = cont           -- The coerces cancel out  
          | otherwise           = CoerceIt (mkTransCoercion co1 co2) cont
     
+       add_coerce co (s1s2, t1t2) (ApplyTo dup (Type arg_ty) arg_se cont)
+               -- (f `cast` g) ty  --->   (f ty) `cast` (g @ ty)
+               -- This implements the PushT rule from the paper
+        | Just (tyvar,_) <- splitForAllTy_maybe s1s2
+        , not (isCoVar tyvar)
+        = ApplyTo dup (Type ty') (zapSubstEnv env) (addCoerce (mkInstCoercion co ty') cont)
+        where
+          ty' = substTy arg_se arg_ty
+
+       -- ToDo: the PushC rule is not implemented at all
+
        add_coerce co (s1s2, t1t2) (ApplyTo dup arg arg_se cont)
        add_coerce co (s1s2, t1t2) (ApplyTo dup arg arg_se cont)
-         | not (isTypeArg arg)  -- This whole case only works for value args
-                               -- Could upgrade to have equiv thing for type apps too  
+         | not (isTypeArg arg)  -- This implements the Push rule from the paper
          , isFunTy s1s2          -- t1t2 must be a function type, becuase it's applied
                 -- co : s1s2 :=: t1t2
                --      (coerce (T1->T2) (S1->S2) F) E
          , isFunTy s1s2          -- t1t2 must be a function type, becuase it's applied
                 -- co : s1s2 :=: t1t2
                --      (coerce (T1->T2) (S1->S2) F) E
@@ -839,14 +902,15 @@ simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
   = do { tick (PreInlineUnconditionally bndr)
        ; simplLam (extendIdSubst env bndr (mkContEx rhs_se rhs)) bndrs body cont }
 
   = do { tick (PreInlineUnconditionally bndr)
        ; simplLam (extendIdSubst env bndr (mkContEx rhs_se rhs)) bndrs body cont }
 
-  | isStrictBndr bndr
+  | isStrictId bndr
   = do { simplExprF (rhs_se `setFloats` env) rhs 
                     (StrictBind bndr bndrs body env cont) }
 
   | otherwise
   = do { simplExprF (rhs_se `setFloats` env) rhs 
                     (StrictBind bndr bndrs body env cont) }
 
   | otherwise
-  = do { (env, bndr') <- simplBinder env bndr
-       ; env <- simplLazyBind env NotTopLevel NonRecursive bndr bndr' rhs rhs_se
-       ; simplLam env bndrs body cont }
+  = do { (env1, bndr1) <- simplNonRecBndr env bndr
+       ; let (env2, bndr2) = addBndrRules env1 bndr bndr1
+       ; env3 <- simplLazyBind env2 NotTopLevel NonRecursive bndr bndr2 rhs rhs_se
+       ; simplLam env3 bndrs body cont }
 \end{code}
 
 
 \end{code}
 
 
@@ -865,10 +929,10 @@ simplNote env (SCC cc) e cont
 
 -- See notes with SimplMonad.inlineMode
 simplNote env InlineMe e cont
 
 -- See notes with SimplMonad.inlineMode
 simplNote env InlineMe e cont
-  | contIsRhsOrArg cont                -- Totally boring continuation; see notes above
+  | Just (inside, outside) <- splitInlineCont cont  -- Boring boring continuation; see notes above
   = do {                       -- Don't inline inside an INLINE expression
   = do {                       -- Don't inline inside an INLINE expression
-         e' <- simplExpr (setMode inlineMode env) e
-       ; rebuild env (mkInlineMe e') cont }
+         e' <- simplExprC (setMode inlineMode env) e inside
+       ; rebuild env (mkInlineMe e') outside }
 
   | otherwise          -- Dissolve the InlineMe note if there's
                -- an interesting context of any kind to combine with
 
   | otherwise          -- Dissolve the InlineMe note if there's
                -- an interesting context of any kind to combine with
@@ -925,6 +989,8 @@ completeCall env var cont
        -- the wrapper didn't occur for things that have specialisations till a 
        -- later phase, so but now we just try RULES first
        --
        -- the wrapper didn't occur for things that have specialisations till a 
        -- later phase, so but now we just try RULES first
        --
+       -- Note [Rules for recursive functions]
+       -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
        -- You might think that we shouldn't apply rules for a loop breaker: 
        -- doing so might give rise to an infinite loop, because a RULE is
        -- rather like an extra equation for the function:
        -- You might think that we shouldn't apply rules for a loop breaker: 
        -- doing so might give rise to an infinite loop, because a RULE is
        -- rather like an extra equation for the function:
@@ -936,16 +1002,16 @@ completeCall env var cont
        -- is recursive, and hence a loop breaker:
        --      foldr k z (build g) = g k z
        -- So it's up to the programmer: rules can cause divergence
        -- is recursive, and hence a loop breaker:
        --      foldr k z (build g) = g k z
        -- So it's up to the programmer: rules can cause divergence
+       ; rules <- getRules
        ; let   in_scope   = getInScope env
        ; let   in_scope   = getInScope env
-               rules      = getRules env
-               maybe_rule = case activeRule env of
+               maybe_rule = case activeRule dflags env of
                                Nothing     -> Nothing  -- No rules apply
                                Just act_fn -> lookupRule act_fn in_scope 
                                                          rules var args 
        ; case maybe_rule of {
            Just (rule, rule_rhs) -> 
                tick (RuleFired (ru_name rule))                 `thenSmpl_`
                                Nothing     -> Nothing  -- No rules apply
                                Just act_fn -> lookupRule act_fn in_scope 
                                                          rules var args 
        ; case maybe_rule of {
            Just (rule, rule_rhs) -> 
                tick (RuleFired (ru_name rule))                 `thenSmpl_`
-               (if dopt Opt_D_dump_inlinings dflags then
+               (if dopt Opt_D_dump_rule_firings dflags then
                   pprTrace "Rule fired" (vcat [
                        text "Rule:" <+> ftext (ru_name rule),
                        text "Before:" <+> ppr var <+> sep (map pprParendExpr args),
                   pprTrace "Rule fired" (vcat [
                        text "Rule:" <+> ftext (ru_name rule),
                        text "Before:" <+> ppr var <+> sep (map pprParendExpr args),
@@ -961,17 +1027,15 @@ completeCall env var cont
        ------------- Next try inlining ----------------
        { let   arg_infos = [interestingArg arg | arg <- args, isValArg arg]
                n_val_args = length arg_infos
        ------------- Next try inlining ----------------
        { let   arg_infos = [interestingArg arg | arg <- args, isValArg arg]
                n_val_args = length arg_infos
-               interesting_cont = interestingCallContext (notNull args)
-                                                         (notNull arg_infos)
-                                                         call_cont
+               interesting_cont = interestingCallContext call_cont
                active_inline = activeInline env var
                active_inline = activeInline env var
-               maybe_inline  = callSiteInline dflags active_inline
-                                      var arg_infos interesting_cont
+               maybe_inline  = callSiteInline dflags active_inline var
+                                              (null args) arg_infos interesting_cont
        ; case maybe_inline of {
            Just unfolding      -- There is an inlining!
              ->  do { tick (UnfoldingDone var)
                     ; (if dopt Opt_D_dump_inlinings dflags then
        ; case maybe_inline of {
            Just unfolding      -- There is an inlining!
              ->  do { tick (UnfoldingDone var)
                     ; (if dopt Opt_D_dump_inlinings dflags then
-                          pprTrace "Inlining done" (vcat [
+                          pprTrace ("Inlining done" ++ showSDoc (ppr var)) (vcat [
                                text "Before:" <+> ppr var <+> sep (map pprParendExpr args),
                                text "Inlined fn: " <+> nest 2 (ppr unfolding),
                                text "Cont:  " <+> ppr call_cont])
                                text "Before:" <+> ppr var <+> sep (map pprParendExpr args),
                                text "Inlined fn: " <+> nest 2 (ppr unfolding),
                                text "Cont:  " <+> ppr call_cont])
@@ -1004,7 +1068,7 @@ rebuildCall env fun fun_ty (has_rules, []) cont
   -- Then, especially in the first of these cases, we'd like to discard
   -- the continuation, leaving just the bottoming expression.  But the
   -- type might not be right, so we may have to add a coerce.
   -- Then, especially in the first of these cases, we'd like to discard
   -- the continuation, leaving just the bottoming expression.  But the
   -- type might not be right, so we may have to add a coerce.
-  | not (contIsTrivial cont)    -- Only do thia if there is a non-trivial
+  | not (contIsTrivial cont)    -- Only do this if there is a non-trivial
   = return (env, mk_coerce fun)  -- contination to discard, else we do it
   where                                 -- again and again!
     cont_ty = contResultType cont
   = return (env, mk_coerce fun)  -- contination to discard, else we do it
   where                                 -- again and again!
     cont_ty = contResultType cont
@@ -1081,6 +1145,10 @@ rebuildCase :: SimplEnv
            -> SimplCont
            -> SimplM (SimplEnv, OutExpr)
 
            -> SimplCont
            -> SimplM (SimplEnv, OutExpr)
 
+--------------------------------------------------
+--     1. Eliminate the case if there's a known constructor
+--------------------------------------------------
+
 rebuildCase env scrut case_bndr alts cont
   | Just (con,args) <- exprIsConApp_maybe scrut        
        -- Works when the scrutinee is a variable with a known unfolding
 rebuildCase env scrut case_bndr alts cont
   | Just (con,args) <- exprIsConApp_maybe scrut        
        -- Works when the scrutinee is a variable with a known unfolding
@@ -1091,15 +1159,65 @@ rebuildCase env scrut case_bndr alts cont
                        -- because literals are inlined more vigorously
   = knownCon env scrut (LitAlt lit) [] case_bndr alts cont
 
                        -- because literals are inlined more vigorously
   = knownCon env scrut (LitAlt lit) [] case_bndr alts cont
 
-  | otherwise
+
+--------------------------------------------------
+--     2. Eliminate the case if scrutinee is evaluated
+--------------------------------------------------
+
+rebuildCase env scrut case_bndr [(con,bndrs,rhs)] cont
+  -- See if we can get rid of the case altogether
+  -- See the extensive notes on case-elimination above
+  -- mkCase made sure that if all the alternatives are equal, 
+  -- then there is now only one (DEFAULT) rhs
+ | all isDeadBinder bndrs      -- bndrs are [InId]
+
+       -- Check that the scrutinee can be let-bound instead of case-bound
+ , exprOkForSpeculation scrut
+               -- OK not to evaluate it
+               -- This includes things like (==# a# b#)::Bool
+               -- so that we simplify 
+               --      case ==# a# b# of { True -> x; False -> x }
+               -- to just
+               --      x
+               -- This particular example shows up in default methods for
+               -- comparision operations (e.g. in (>=) for Int.Int32)
+       || exprIsHNF scrut                      -- It's already evaluated
+       || var_demanded_later scrut             -- It'll be demanded later
+
+--      || not opt_SimplPedanticBottoms)       -- Or we don't care!
+--     We used to allow improving termination by discarding cases, unless -fpedantic-bottoms was on,
+--     but that breaks badly for the dataToTag# primop, which relies on a case to evaluate
+--     its argument:  case x of { y -> dataToTag# y }
+--     Here we must *not* discard the case, because dataToTag# just fetches the tag from
+--     the info pointer.  So we'll be pedantic all the time, and see if that gives any
+--     other problems
+--     Also we don't want to discard 'seq's
+  = do { tick (CaseElim case_bndr)
+       ; env <- simplNonRecX env case_bndr scrut
+       ; simplExprF env rhs cont }
+  where
+       -- The case binder is going to be evaluated later, 
+       -- and the scrutinee is a simple variable
+    var_demanded_later (Var v) = isStrictDmd (idNewDemandInfo case_bndr)
+                                && not (isTickBoxOp v) 
+                                   -- ugly hack; covering this case is what 
+                                   -- exprOkForSpeculation was intended for.
+    var_demanded_later other   = False
+
+
+--------------------------------------------------
+--     3. Catch-all case
+--------------------------------------------------
+
+rebuildCase env scrut case_bndr alts cont
   = do {       -- Prepare the continuation;
                -- The new subst_env is in place
          (env, dup_cont, nodup_cont) <- prepareCaseCont env alts cont
 
        -- Simplify the alternatives
   = do {       -- Prepare the continuation;
                -- The new subst_env is in place
          (env, dup_cont, nodup_cont) <- prepareCaseCont env alts cont
 
        -- Simplify the alternatives
-       ; (case_bndr', alts') <- simplAlts env scrut case_bndr alts dup_cont
+       ; (scrut', case_bndr', alts') <- simplAlts env scrut case_bndr alts dup_cont
        ; let res_ty' = contResultType dup_cont
        ; let res_ty' = contResultType dup_cont
-       ; case_expr <- mkCase scrut case_bndr' res_ty' alts'
+       ; case_expr <- mkCase scrut' case_bndr' res_ty' alts'
 
        -- Notice that rebuildDone returns the in-scope set from env, not alt_env
        -- The case binder *not* scope over the whole returned case-expression
 
        -- Notice that rebuildDone returns the in-scope set from env, not alt_env
        -- The case binder *not* scope over the whole returned case-expression
@@ -1123,18 +1241,10 @@ in action in spectral/cichelli/Prog.hs:
         [(m,n) | m <- [1..max], n <- [1..max]]
 Hence the check for NoCaseOfCase.
 
         [(m,n) | m <- [1..max], n <- [1..max]]
 Hence the check for NoCaseOfCase.
 
-Note [Case of cast]
-~~~~~~~~~~~~~~~~~~~
-Consider       case (v `cast` co) of x { I# ->
-               ... (case (v `cast` co) of {...}) ...
-We'd like to eliminate the inner case.  We can get this neatly by 
-arranging that inside the outer case we add the unfolding
-       v |-> x `cast` (sym co)
-to v.  Then we should inline v at the inner case, cancel the casts, and away we go
-       
-Note 2
-~~~~~~
-There is another situation when we don't want to do it.  If we have
+Note [Suppressing the case binder-swap]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There is another situation when it might make sense to suppress the
+case-expression binde-swap. If we have
 
     case x of w1 { DEFAULT -> case x of w2 { A -> e1; B -> e2 }
                   ...other cases .... }
 
     case x of w1 { DEFAULT -> case x of w2 { A -> e1; B -> e2 }
                   ...other cases .... }
@@ -1196,31 +1306,183 @@ The point is that we bring into the envt a binding
 after the outer case, and that makes (a,b) alive.  At least we do unless
 the case binder is guaranteed dead.
 
 after the outer case, and that makes (a,b) alive.  At least we do unless
 the case binder is guaranteed dead.
 
+Note [Case of cast]
+~~~~~~~~~~~~~~~~~~~
+Consider       case (v `cast` co) of x { I# ->
+               ... (case (v `cast` co) of {...}) ...
+We'd like to eliminate the inner case.  We can get this neatly by 
+arranging that inside the outer case we add the unfolding
+       v |-> x `cast` (sym co)
+to v.  Then we should inline v at the inner case, cancel the casts, and away we go
+       
+Note [Improving seq]
+~~~~~~~~~~~~~~~~~~~
+Consider
+       type family F :: * -> *
+       type instance F Int = Int
+
+       ... case e of x { DEFAULT -> rhs } ...
+
+where x::F Int.  Then we'd like to rewrite (F Int) to Int, getting
+
+       case e `cast` co of x'::Int
+          I# x# -> let x = x' `cast` sym co 
+                   in rhs
+
+so that 'rhs' can take advantage of the form of x'.  Notice that Note
+[Case of cast] may then apply to the result.
+
+This showed up in Roman's experiments.  Example:
+  foo :: F Int -> Int -> Int
+  foo t n = t `seq` bar n
+     where
+       bar 0 = 0
+       bar n = bar (n - case t of TI i -> i)
+Here we'd like to avoid repeated evaluating t inside the loop, by 
+taking advantage of the `seq`.
+
+At one point I did transformation in LiberateCase, but it's more robust here.
+(Otherwise, there's a danger that we'll simply drop the 'seq' altogether, before
+LiberateCase gets to see it.)
+
+Note [Case elimination]
+~~~~~~~~~~~~~~~~~~~~~~~
+The case-elimination transformation discards redundant case expressions.
+Start with a simple situation:
+
+       case x# of      ===>   e[x#/y#]
+         y# -> e
+
+(when x#, y# are of primitive type, of course).  We can't (in general)
+do this for algebraic cases, because we might turn bottom into
+non-bottom!
+
+The code in SimplUtils.prepareAlts has the effect of generalise this
+idea to look for a case where we're scrutinising a variable, and we
+know that only the default case can match.  For example:
+
+       case x of
+         0#      -> ...
+         DEFAULT -> ...(case x of
+                        0#      -> ...
+                        DEFAULT -> ...) ...
+
+Here the inner case is first trimmed to have only one alternative, the
+DEFAULT, after which it's an instance of the previous case.  This
+really only shows up in eliminating error-checking code.
+
+We also make sure that we deal with this very common case:
+
+       case e of 
+         x -> ...x...
+
+Here we are using the case as a strict let; if x is used only once
+then we want to inline it.  We have to be careful that this doesn't 
+make the program terminate when it would have diverged before, so we
+check that 
+       - e is already evaluated (it may so if e is a variable)
+       - x is used strictly, or
+
+Lastly, the code in SimplUtils.mkCase combines identical RHSs.  So
+
+       case e of       ===> case e of DEFAULT -> r
+          True  -> r
+          False -> r
+
+Now again the case may be elminated by the CaseElim transformation.
+
+
+Further notes about case elimination
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider:      test :: Integer -> IO ()
+               test = print
+
+Turns out that this compiles to:
+    Print.test
+      = \ eta :: Integer
+         eta1 :: State# RealWorld ->
+         case PrelNum.< eta PrelNum.zeroInteger of wild { __DEFAULT ->
+         case hPutStr stdout
+                (PrelNum.jtos eta ($w[] @ Char))
+                eta1
+         of wild1 { (# new_s, a4 #) -> PrelIO.lvl23 new_s  }}
+
+Notice the strange '<' which has no effect at all. This is a funny one.  
+It started like this:
+
+f x y = if x < 0 then jtos x
+          else if y==0 then "" else jtos x
+
+At a particular call site we have (f v 1).  So we inline to get
+
+       if v < 0 then jtos x 
+       else if 1==0 then "" else jtos x
+
+Now simplify the 1==0 conditional:
+
+       if v<0 then jtos v else jtos v
+
+Now common-up the two branches of the case:
+
+       case (v<0) of DEFAULT -> jtos v
+
+Why don't we drop the case?  Because it's strict in v.  It's technically
+wrong to drop even unnecessary evaluations, and in practice they
+may be a result of 'seq' so we *definitely* don't want to drop those.
+I don't really know how to improve this situation.
+
+
 \begin{code}
 \begin{code}
-simplCaseBinder :: SimplEnv -> OutExpr -> InId -> SimplM (SimplEnv, OutId)
-simplCaseBinder env scrut case_bndr
-  | switchIsOn (getSwitchChecker env) NoCaseOfCase
-       -- See Note [no-case-of-case]
-  = do { (env, case_bndr') <- simplBinder env case_bndr
-       ; return (env, case_bndr') }
-
-simplCaseBinder env (Var v) case_bndr
--- Failed try [see Note 2 above]
---     not (isEvaldUnfolding (idUnfolding v))
-  = do { (env, case_bndr') <- simplBinder env (zapOccInfo case_bndr)
-       ; return (modifyInScope env v case_bndr', case_bndr') }
-       -- We could extend the substitution instead, but it would be
-       -- a hack because then the substitution wouldn't be idempotent
-       -- any more (v is an OutId).  And this does just as well.
-           
-simplCaseBinder env (Cast (Var v) co) case_bndr                -- Note [Case of cast]
-  = do { (env, case_bndr') <- simplBinder env (zapOccInfo case_bndr)
-       ; let rhs = Cast (Var case_bndr') (mkSymCoercion co)
-       ; return (addBinderUnfolding env v rhs, case_bndr') }
-
-simplCaseBinder env other_scrut case_bndr 
-  = do { (env, case_bndr') <- simplBinder env case_bndr
-       ; return (env, case_bndr') }
+simplCaseBinder :: SimplEnv -> OutExpr -> OutId -> [InAlt]
+               -> SimplM (SimplEnv, OutExpr, OutId)
+simplCaseBinder env scrut case_bndr alts
+  = do { (env1, case_bndr1) <- simplBinder env case_bndr
+
+       ; fam_envs <- getFamEnvs
+       ; (env2, scrut2, case_bndr2) <- improve_seq fam_envs env1 scrut 
+                                               case_bndr case_bndr1 alts
+                       -- Note [Improving seq]
+
+       ; let (env3, case_bndr3) = improve_case_bndr env2 scrut2 case_bndr2
+                       -- Note [Case of cast]
+
+       ; return (env3, scrut2, case_bndr3) }
+  where
+
+    improve_seq fam_envs env1 scrut case_bndr case_bndr1 [(DEFAULT,_,_)] 
+       | Just (co, ty2) <- topNormaliseType fam_envs (idType case_bndr1)
+       =  do { case_bndr2 <- newId FSLIT("nt") ty2
+             ; let rhs  = DoneEx (Var case_bndr2 `Cast` mkSymCoercion co)
+                   env2 = extendIdSubst env1 case_bndr rhs
+             ; return (env2, scrut `Cast` co, case_bndr2) }
+
+    improve_seq fam_envs env1 scrut case_bndr case_bndr1 alts
+       = return (env1, scrut, case_bndr1)
+
+
+    improve_case_bndr env scrut case_bndr
+       | switchIsOn (getSwitchChecker env) NoCaseOfCase
+               -- See Note [no-case-of-case]
+       = (env, case_bndr)
+
+       | otherwise     -- Failed try; see Note [Suppressing the case binder-swap]
+                       --     not (isEvaldUnfolding (idUnfolding v))
+       = case scrut of
+           Var v -> (modifyInScope env1 v case_bndr', case_bndr')
+               -- Note about using modifyInScope for v here
+               -- We could extend the substitution instead, but it would be
+               -- a hack because then the substitution wouldn't be idempotent
+               -- any more (v is an OutId).  And this does just as well.
+
+           Cast (Var v) co -> (addBinderUnfolding env1 v rhs, case_bndr')
+                           where
+                               rhs = Cast (Var case_bndr') (mkSymCoercion co)
+
+           other -> (env, case_bndr)
+       where
+         case_bndr' = zapOccInfo case_bndr
+         env1       = modifyInScope env case_bndr case_bndr'
+
 
 zapOccInfo :: InId -> InId     -- See Note [zapOccInfo]
 zapOccInfo b = b `setIdOccInfo` NoOccInfo
 
 zapOccInfo :: InId -> InId     -- See Note [zapOccInfo]
 zapOccInfo b = b `setIdOccInfo` NoOccInfo
@@ -1272,126 +1534,49 @@ simplAlts :: SimplEnv
          -> OutExpr
          -> InId                       -- Case binder
          -> [InAlt] -> SimplCont
          -> OutExpr
          -> InId                       -- Case binder
          -> [InAlt] -> SimplCont
-         -> SimplM (OutId, [OutAlt])   -- Includes the continuation
+         -> SimplM (OutExpr, OutId, [OutAlt])  -- Includes the continuation
 -- Like simplExpr, this just returns the simplified alternatives;
 -- it not return an environment
 
 simplAlts env scrut case_bndr alts cont'
   = -- pprTrace "simplAlts" (ppr alts $$ ppr (seIdSubst env)) $
     do { let alt_env = zapFloats env
 -- Like simplExpr, this just returns the simplified alternatives;
 -- it not return an environment
 
 simplAlts env scrut case_bndr alts cont'
   = -- pprTrace "simplAlts" (ppr alts $$ ppr (seIdSubst env)) $
     do { let alt_env = zapFloats env
-       ; (alt_env, case_bndr') <- simplCaseBinder alt_env scrut case_bndr
-
-       ; default_alts <- prepareDefault alt_env case_bndr' imposs_deflt_cons cont' maybe_deflt
-
-       ; let inst_tys = tyConAppArgs (idType case_bndr')
-             trimmed_alts = filter (is_possible inst_tys) alts_wo_default
-             in_alts      = mergeAlts default_alts trimmed_alts
-               -- We need the mergeAlts in case the new default_alt 
-               -- has turned into a constructor alternative.
+       ; (alt_env, scrut', case_bndr') <- simplCaseBinder alt_env scrut case_bndr alts
 
 
-       ; alts' <- mapM (simplAlt alt_env imposs_cons case_bndr' cont') in_alts
-       ; return (case_bndr', alts') }
-  where
-    (alts_wo_default, maybe_deflt) = findDefault alts
-    imposs_cons = case scrut of
-                   Var v -> otherCons (idUnfolding v)
-                   other -> []
-
-       -- "imposs_deflt_cons" are handled either by the context, 
-       -- OR by a branch in this case expression. (Don't include DEFAULT!!)
-    imposs_deflt_cons = nub (imposs_cons ++ [con | (con,_,_) <- alts_wo_default])
+       ; (imposs_deflt_cons, in_alts) <- prepareAlts alt_env scrut case_bndr' alts
 
 
-    is_possible :: [Type] -> CoreAlt -> Bool
-    is_possible tys (con, _, _) | con `elem` imposs_cons = False
-    is_possible tys (DataAlt con, _, _) = dataConCanMatch tys con
-    is_possible tys alt                        = True
-
-------------------------------------
-prepareDefault :: SimplEnv
-              -> OutId         -- Case binder; need just for its type. Note that as an
-                               --   OutId, it has maximum information; this is important.
-                               --   Test simpl013 is an example
-            -> [AltCon]        -- These cons can't happen when matching the default
-            -> SimplCont
-            -> Maybe InExpr
-            -> SimplM [InAlt]  -- One branch or none; still unsimplified
-                               -- We use a list because it's what mergeAlts expects
-
-prepareDefault env case_bndr' imposs_cons cont Nothing
-  = return []  -- No default branch
-
-prepareDefault env case_bndr' imposs_cons cont (Just rhs)
-  |    -- This branch handles the case where we are 
-       -- scrutinisng an algebraic data type
-    Just (tycon, inst_tys) <- splitTyConApp_maybe (idType case_bndr'),
-    isAlgTyCon tycon,          -- It's a data type, tuple, or unboxed tuples.  
-    not (isNewTyCon tycon),    -- We can have a newtype, if we are just doing an eval:
-                               --      case x of { DEFAULT -> e }
-                               -- and we don't want to fill in a default for them!
-    Just all_cons <- tyConDataCons_maybe tycon,
-    not (null all_cons),       -- This is a tricky corner case.  If the data type has no constructors,
-                               -- which GHC allows, then the case expression will have at most a default
-                               -- alternative.  We don't want to eliminate that alternative, because the
-                               -- invariant is that there's always one alternative.  It's more convenient
-                               -- to leave     
-                               --      case x of { DEFAULT -> e }     
-                               -- as it is, rather than transform it to
-                               --      error "case cant match"
-                               -- which would be quite legitmate.  But it's a really obscure corner, and
-                               -- not worth wasting code on.
-
-    let imposs_data_cons = [con | DataAlt con <- imposs_cons]  -- We now know it's a data type 
-       is_possible con  = not (con `elem` imposs_data_cons)
-                          && dataConCanMatch inst_tys con
-  = case filter is_possible all_cons of
-       []    -> return []      -- Eliminate the default alternative
-                               -- altogether if it can't match
-
-       [con] ->        -- It matches exactly one constructor, so fill it in
-                do { tick (FillInCaseDefault case_bndr')
-                    ; us <- getUniquesSmpl
-                    ; let (ex_tvs, co_tvs, arg_ids) =
-                              dataConRepInstPat us con inst_tys
-                    ; return [(DataAlt con, ex_tvs ++ co_tvs ++ arg_ids, rhs)] }
-
-       two_or_more -> return [(DEFAULT, [], rhs)]
-
-  | otherwise 
-  = return [(DEFAULT, [], rhs)]
+       ; alts' <- mapM (simplAlt alt_env imposs_deflt_cons case_bndr' cont') in_alts
+       ; return (scrut', case_bndr', alts') }
 
 ------------------------------------
 simplAlt :: SimplEnv
         -> [AltCon]    -- These constructors can't be present when
 
 ------------------------------------
 simplAlt :: SimplEnv
         -> [AltCon]    -- These constructors can't be present when
-                       -- matching this alternative
+                       -- matching the DEFAULT alternative
         -> OutId       -- The case binder
         -> SimplCont
         -> InAlt
         -> OutId       -- The case binder
         -> SimplCont
         -> InAlt
-        -> SimplM (OutAlt)
-
--- Simplify an alternative, returning the type refinement for the 
--- alternative, if the alternative does any refinement at all
+        -> SimplM OutAlt
 
 
-simplAlt env handled_cons case_bndr' cont' (DEFAULT, bndrs, rhs)
+simplAlt env imposs_deflt_cons case_bndr' cont' (DEFAULT, bndrs, rhs)
   = ASSERT( null bndrs )
   = ASSERT( null bndrs )
-    do { let env' = addBinderOtherCon env case_bndr' handled_cons
+    do { let env' = addBinderOtherCon env case_bndr' imposs_deflt_cons
                -- Record the constructors that the case-binder *can't* be.
        ; rhs' <- simplExprC env' rhs cont'
        ; return (DEFAULT, [], rhs') }
 
                -- Record the constructors that the case-binder *can't* be.
        ; rhs' <- simplExprC env' rhs cont'
        ; return (DEFAULT, [], rhs') }
 
-simplAlt env handled_cons case_bndr' cont' (LitAlt lit, bndrs, rhs)
+simplAlt env imposs_deflt_cons case_bndr' cont' (LitAlt lit, bndrs, rhs)
   = ASSERT( null bndrs )
     do { let env' = addBinderUnfolding env case_bndr' (Lit lit)
        ; rhs' <- simplExprC env' rhs cont'
        ; return (LitAlt lit, [], rhs') }
 
   = ASSERT( null bndrs )
     do { let env' = addBinderUnfolding env case_bndr' (Lit lit)
        ; rhs' <- simplExprC env' rhs cont'
        ; return (LitAlt lit, [], rhs') }
 
-simplAlt env handled_cons case_bndr' cont' (DataAlt con, vs, rhs)
+simplAlt env imposs_deflt_cons case_bndr' cont' (DataAlt con, vs, rhs)
   = do {       -- Deal with the pattern-bound variables
   = do {       -- Deal with the pattern-bound variables
-               -- Mark the ones that are in ! positions in the data constructor
-               -- as certainly-evaluated.
-               -- NB: it happens that simplBinders does *not* erase the OtherCon
-               --     form of unfolding, so it's ok to add this info before 
-               --     doing simplBinders
-         (env, vs') <- simplBinders env (add_evals con vs)
+               -- Mark the ones that are in ! positions in the
+               -- data constructor as certainly-evaluated.
+               -- NB: simplLamBinders preserves this eval info
+         let vs_with_evals = add_evals vs (dataConRepStrictness con)
+       ; (env, vs') <- simplLamBndrs env vs_with_evals
 
                -- Bind the case-binder to (con args)
        ; let inst_tys' = tyConAppArgs (idType case_bndr')
 
                -- Bind the case-binder to (con args)
        ; let inst_tys' = tyConAppArgs (idType case_bndr')
@@ -1410,9 +1595,7 @@ simplAlt env handled_cons case_bndr' cont' (DataAlt con, vs, rhs)
        -- We really must record that b is already evaluated so that we don't
        -- go and re-evaluate it when constructing the result.
        -- See Note [Data-con worker strictness] in MkId.lhs
        -- We really must record that b is already evaluated so that we don't
        -- go and re-evaluate it when constructing the result.
        -- See Note [Data-con worker strictness] in MkId.lhs
-    add_evals dc vs = cat_evals dc vs (dataConRepStrictness dc)
-
-    cat_evals dc vs strs
+    add_evals vs strs
        = go vs strs
        where
          go [] [] = []
        = go vs strs
        where
          go [] [] = []
@@ -1423,12 +1606,15 @@ simplAlt env handled_cons case_bndr' cont' (DataAlt con, vs, rhs)
            where
              zapped_v = zap_occ_info v
              evald_v  = zapped_v `setIdUnfolding` evaldUnfolding
            where
              zapped_v = zap_occ_info v
              evald_v  = zapped_v `setIdUnfolding` evaldUnfolding
-         go _ _ = pprPanic "cat_evals" (ppr dc $$ ppr vs $$ ppr strs)
+         go _ _ = pprPanic "cat_evals" (ppr con $$ ppr vs $$ ppr strs)
 
 
-       -- If the case binder is alive, then we add the unfolding
+       -- zap_occ_info: if the case binder is alive, then we add the unfolding
        --      case_bndr = C vs
        -- to the envt; so vs are now very much alive
        --      case_bndr = C vs
        -- to the envt; so vs are now very much alive
-       -- Note [Aug06] I can't see why this actually matters
+       -- Note [Aug06] I can't see why this actually matters, but it's neater
+       --        case e of t { (a,b) -> ...(case t of (p,q) -> p)... }
+       --   ==>  case e of t { (a,b) -> ...(a)... }
+       -- Look, Ma, a is alive now.
     zap_occ_info | isDeadBinder case_bndr' = \id -> id
                 | otherwise               = zapOccInfo
 
     zap_occ_info | isDeadBinder case_bndr' = \id -> id
                 | otherwise               = zapOccInfo
 
@@ -1484,8 +1670,8 @@ knownAlt env scrut args bndr (LitAlt lit, bs, rhs) cont
        ; simplExprF env rhs cont }
 
 knownAlt env scrut args bndr (DataAlt dc, bs, rhs) cont
        ; simplExprF env rhs cont }
 
 knownAlt env scrut args bndr (DataAlt dc, bs, rhs) cont
-  = do { let dead_bndr  = isDeadBinder bndr
-             n_drop_tys = tyConArity (dataConTyCon dc)
+  = do { let dead_bndr  = isDeadBinder bndr    -- bndr is an InId
+             n_drop_tys = length (dataConUnivTyVars dc)
        ; env <- bind_args env dead_bndr bs (drop n_drop_tys args)
        ; let
                -- It's useful to bind bndr to scrut, rather than to a fresh
        ; env <- bind_args env dead_bndr bs (drop n_drop_tys args)
        ; let
                -- It's useful to bind bndr to scrut, rather than to a fresh
@@ -1505,25 +1691,27 @@ knownAlt env scrut args bndr (DataAlt dc, bs, rhs) cont
        ; env <- simplNonRecX env bndr bndr_rhs
        ; -- pprTrace "knownCon2" (ppr bs $$ ppr rhs $$ ppr (seIdSubst env)) $
          simplExprF env rhs cont }
        ; env <- simplNonRecX env bndr bndr_rhs
        ; -- pprTrace "knownCon2" (ppr bs $$ ppr rhs $$ ppr (seIdSubst env)) $
          simplExprF env rhs cont }
-
--- Ugh!
-bind_args env dead_bndr [] _  = return env
-
-bind_args env dead_bndr (b:bs) (Type ty : args)
-  = ASSERT( isTyVar b )
-    bind_args (extendTvSubst env b ty) dead_bndr bs args
-    
-bind_args env dead_bndr (b:bs) (arg : args)
-  = ASSERT( isId b )
-    do { let b' = if dead_bndr then b else zapOccInfo b
-               -- Note that the binder might be "dead", because it doesn't occur 
-               -- in the RHS; and simplNonRecX may therefore discard it via postInlineUnconditionally
-               -- Nevertheless we must keep it if the case-binder is alive, because it may
-               -- be used in the con_app.  See Note [zapOccInfo]
-       ; env <- simplNonRecX env b' arg
-       ; bind_args env dead_bndr bs args }
-
-bind_args _ _ _ _ = panic "bind_args"
+  where
+    -- Ugh!
+    bind_args env dead_bndr [] _  = return env
+
+    bind_args env dead_bndr (b:bs) (Type ty : args)
+      = ASSERT( isTyVar b )
+        bind_args (extendTvSubst env b ty) dead_bndr bs args
+
+    bind_args env dead_bndr (b:bs) (arg : args)
+      = ASSERT( isId b )
+        do     { let b' = if dead_bndr then b else zapOccInfo b
+                    -- Note that the binder might be "dead", because it doesn't occur 
+                    -- in the RHS; and simplNonRecX may therefore discard it via postInlineUnconditionally
+                    -- Nevertheless we must keep it if the case-binder is alive, because it may
+                    -- be used in the con_app.  See Note [zapOccInfo]
+            ; env <- simplNonRecX env b' arg
+            ; bind_args env dead_bndr bs args }
+
+    bind_args _ _ _ _ = 
+      pprPanic "bind_args" $ ppr dc $$ ppr bs $$ ppr args $$ 
+                             text "scrut:" <+> ppr scrut
 \end{code}
 
 
 \end{code}
 
 
@@ -1583,7 +1771,7 @@ mkDupableCont env cont@(Select _ case_bndr [(_,bs,rhs)] se case_cont)
 --  See Note [Single-alternative case]
 --  | not (exprIsDupable rhs && contIsDupable case_cont)
 --  | not (isDeadBinder case_bndr)
 --  See Note [Single-alternative case]
 --  | not (exprIsDupable rhs && contIsDupable case_cont)
 --  | not (isDeadBinder case_bndr)
-  | all isDeadBinder bs
+  | all isDeadBinder bs                -- InIds
   = return (env, mkBoringStop scrut_ty, cont)
   where
     scrut_ty = substTy se (idType case_bndr)
   = return (env, mkBoringStop scrut_ty, cont)
   where
     scrut_ty = substTy se (idType case_bndr)
@@ -1606,8 +1794,8 @@ mkDupableCont env (Select _ case_bndr alts se cont)
                -- NB: simplBinder does not zap deadness occ-info, so
                -- a dead case_bndr' will still advertise its deadness
                -- This is really important because in
                -- NB: simplBinder does not zap deadness occ-info, so
                -- a dead case_bndr' will still advertise its deadness
                -- This is really important because in
-               --      case e of b { (# a,b #) -> ... }
-               -- b is always dead, and indeed we are not allowed to bind b to (# a,b #),
+               --      case e of b { (# p,q #) -> ... }
+               -- b is always dead, and indeed we are not allowed to bind b to (# p,q #),
                -- which might happen if e was an explicit unboxed pair and b wasn't marked dead.
                -- In the new alts we build, we have the new case binder, so it must retain
                -- its deadness.
                -- which might happen if e was an explicit unboxed pair and b wasn't marked dead.
                -- In the new alts we build, we have the new case binder, so it must retain
                -- its deadness.