[project @ 2006-01-06 16:30:17 by simonmar]
[ghc-hetmet.git] / ghc / compiler / simplCore / Simplify.lhs
index 997423d..17a7969 100644 (file)
@@ -8,25 +8,26 @@ module Simplify ( simplTopBinds, simplExpr ) where
 
 #include "HsVersions.h"
 
-import CmdLineOpts     ( dopt, DynFlag(Opt_D_dump_inlinings),
+import DynFlags        ( dopt, DynFlag(Opt_D_dump_inlinings),
                          SimplifierSwitch(..)
                        )
 import SimplMonad
-import SimplUtils      ( mkCase, mkLam, newId, prepareAlts,
-                         simplBinder, simplBinders, simplLamBndrs, simplRecBndrs, simplLetBndr,
+import SimplEnv        
+import SimplUtils      ( mkCase, mkLam, prepareAlts,
                          SimplCont(..), DupFlag(..), LetRhsFlag(..), 
                          mkRhsStop, mkBoringStop,  pushContArgs,
                          contResultType, countArgs, contIsDupable, contIsRhsOrArg,
-                         getContArgs, interestingCallContext, interestingArg, isStrictType
+                         getContArgs, interestingCallContext, interestingArg, isStrictType,
+                         preInlineUnconditionally, postInlineUnconditionally, 
+                         inlineMode, activeInline, activeRule
                        )
 import Id              ( Id, idType, idInfo, idArity, isDataConWorkId, 
                          setIdUnfolding, isDeadBinder,
                          idNewDemandInfo, setIdInfo, 
-                         setIdOccInfo, zapLamIdInfo, setOneShotLambda, 
+                         setIdOccInfo, zapLamIdInfo, setOneShotLambda
                        )
 import MkId            ( eRROR_ID )
 import Literal         ( mkStringLit )
-import OccName         ( encodeFS )
 import IdInfo          ( OccInfo(..), isLoopBreaker,
                          setArityInfo, zapDemandInfo,
                          setUnfoldingInfo, 
@@ -38,28 +39,27 @@ import DataCon              ( dataConTyCon, dataConRepStrictness, isVanillaDataCon )
 import TyCon           ( tyConArity )
 import CoreSyn
 import PprCore         ( pprParendExpr, pprCoreExpr )
-import CoreUnfold      ( mkOtherCon, mkUnfolding, callSiteInline )
+import CoreUnfold      ( mkUnfolding, callSiteInline )
 import CoreUtils       ( exprIsDupable, exprIsTrivial, needsCaseBinding,
                          exprIsConApp_maybe, mkPiTypes, findAlt, 
-                         exprType, exprIsValue, 
+                         exprType, exprIsHNF, 
                          exprOkForSpeculation, exprArity, 
                          mkCoerce, mkCoerce2, mkSCC, mkInlineMe, applyTypeToArg
                        )
 import Rules           ( lookupRule )
 import BasicTypes      ( isMarkedStrict )
 import CostCentre      ( currentCCS )
-import Type            ( isUnLiftedType, seqType, tyConAppArgs, funArgTy,
-                         splitFunTy_maybe, splitFunTy, eqType, substTy
+import Type            ( TvSubstEnv, isUnLiftedType, seqType, tyConAppArgs, funArgTy,
+                         splitFunTy_maybe, splitFunTy, coreEqType 
                        )
-import Subst           ( SubstResult(..), emptySubst, substExpr, 
-                         substId, simplIdInfo )
+import VarEnv          ( elemVarEnv, emptyVarEnv )
 import TysPrim         ( realWorldStatePrimTy )
 import PrelInfo                ( realWorldPrimId )
 import BasicTypes      ( TopLevelFlag(..), isTopLevel, 
                          RecFlag(..), isNonRec
                        )
+import StaticFlags     ( opt_PprStyle_Debug )
 import OrdList
-import Maybe           ( Maybe )
 import Maybes          ( orElse )
 import Outputable
 import Util             ( notNull )
@@ -233,7 +233,7 @@ simplTopBinds env binds
        -- so that if a transformation rule has unexpectedly brought
        -- anything into scope, then we don't get a complaint about that.
        -- It's rather as if the top-level binders were imported.
-    simplRecBndrs env (bindersOfBinds binds)   `thenSmpl` \ (env, bndrs') -> 
+    simplLetBndrs env (bindersOfBinds binds)   `thenSmpl` \ (env, bndrs') -> 
     simpl_binds env binds bndrs'               `thenSmpl` \ (floats, _) ->
     freeTick SimplifierDone                    `thenSmpl_`
     returnSmpl (floatBinds floats)
@@ -298,12 +298,14 @@ simplNonRecBind env bndr rhs rhs_se cont_ty thing_inside
 #endif
 
 simplNonRecBind env bndr rhs rhs_se cont_ty thing_inside
-  | preInlineUnconditionally env NotTopLevel bndr
-  = tick (PreInlineUnconditionally bndr)               `thenSmpl_`
-    thing_inside (extendIdSubst env bndr (ContEx (getSubst rhs_se) rhs))
+  = simplNonRecBind' env bndr rhs rhs_se cont_ty thing_inside
 
+simplNonRecBind' env bndr rhs rhs_se cont_ty thing_inside
+  | preInlineUnconditionally env NotTopLevel bndr rhs
+  = tick (PreInlineUnconditionally bndr)               `thenSmpl_`
+    thing_inside (extendIdSubst env bndr (mkContEx rhs_se rhs))
 
-  | isStrictDmd (idNewDemandInfo bndr) || isStrictType (idType bndr)   -- A strict let
+  | isStrictDmd (idNewDemandInfo bndr) || isStrictType bndr_ty -- A strict let
   =    -- Don't use simplBinder because that doesn't keep 
        -- fragile occurrence info in the substitution
     simplLetBndr env bndr                                      `thenSmpl` \ (env, bndr1) ->
@@ -313,10 +315,16 @@ simplNonRecBind env bndr rhs rhs_se cont_ty thing_inside
     let
        -- simplLetBndr doesn't deal with the IdInfo, so we must
        -- do so here (c.f. simplLazyBind)
-       bndr2  = bndr1 `setIdInfo` simplIdInfo (getSubst env) (idInfo bndr)
+       bndr2  = bndr1 `setIdInfo` simplIdInfo env (idInfo bndr)
        env2   = modifyInScope env1 bndr2 bndr2
     in
-    completeNonRecX env2 True {- strict -} bndr bndr2 rhs1 thing_inside
+    if needsCaseBinding bndr_ty rhs1
+    then
+      thing_inside env2                                        `thenSmpl` \ (floats, body) ->
+      returnSmpl (emptyFloats env2, Case rhs1 bndr2 (exprType body) 
+                                       [(DEFAULT, [], wrapFloats floats body)])
+    else
+      completeNonRecX env2 True {- strict -} bndr bndr2 rhs1 thing_inside
 
   | otherwise                                                  -- Normal, lazy case
   =    -- Don't use simplBinder because that doesn't keep 
@@ -325,6 +333,9 @@ simplNonRecBind env bndr rhs rhs_se cont_ty thing_inside
     simplLazyBind env NotTopLevel NonRecursive
                  bndr bndr' rhs rhs_se                 `thenSmpl` \ (floats, env) ->
     addFloats env floats thing_inside
+
+  where
+    bndr_ty = idType bndr
 \end{code}
 
 A specialised variant of simplNonRec used when the RHS is already simplified, notably
@@ -348,11 +359,10 @@ simplNonRecX env bndr new_rhs thing_inside
        -- because quotInt# can fail.
   = simplBinder env bndr       `thenSmpl` \ (env, bndr') ->
     thing_inside env           `thenSmpl` \ (floats, body) ->
--- gaw 2004
     let body' = wrapFloats floats body in 
     returnSmpl (emptyFloats env, Case new_rhs bndr' (exprType body') [(DEFAULT, [], body')])
 
-  | preInlineUnconditionally env NotTopLevel  bndr
+  | preInlineUnconditionally env NotTopLevel bndr new_rhs
        -- This happens; for example, the case_bndr during case of
        -- known constructor:  case (a,b) of x { (p,q) -> ... }
        -- Here x isn't mentioned in the RHS, so we don't want to
@@ -361,7 +371,7 @@ simplNonRecX env bndr new_rhs thing_inside
        -- Similarly, single occurrences can be inlined vigourously
        -- e.g.  case (f x, g y) of (a,b) -> ....
        -- If a,b occur once we can avoid constructing the let binding for them.
-  = thing_inside (extendIdSubst env bndr (ContEx emptySubst new_rhs))
+  = thing_inside (extendIdSubst env bndr (DoneEx new_rhs))
 
   | otherwise
   = simplBinder env bndr       `thenSmpl` \ (env, bndr') ->
@@ -421,9 +431,9 @@ simplRecOrTopPair :: SimplEnv
                  -> SimplM (FloatsWith SimplEnv)
 
 simplRecOrTopPair env top_lvl bndr bndr' rhs
-  | preInlineUnconditionally env top_lvl bndr          -- Check for unconditional inline
-  = tick (PreInlineUnconditionally bndr)       `thenSmpl_`
-    returnSmpl (emptyFloats env, extendIdSubst env bndr (ContEx (getSubst env) rhs))
+  | preInlineUnconditionally env top_lvl bndr rhs      -- Check for unconditional inline
+  = tick (PreInlineUnconditionally bndr)               `thenSmpl_`
+    returnSmpl (emptyFloats env, extendIdSubst env bndr (mkContEx env rhs))
 
   | otherwise
   = simplLazyBind env top_lvl Recursive bndr bndr' rhs env
@@ -486,7 +496,7 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
 
        -- NB 4: does no harm for non-recursive bindings
 
-       bndr2             = bndr1 `setIdInfo` simplIdInfo (getSubst env) (idInfo bndr)
+       bndr2             = bndr1 `setIdInfo` simplIdInfo env (idInfo bndr)
        env1              = modifyInScope env bndr2 bndr2
        rhs_env           = setInScope rhs_se env1
        is_top_level      = isTopLevel top_lvl
@@ -513,24 +523,24 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
     if isEmptyFloats floats && isNilOL aux_binds then  -- Shortcut a common case
        completeLazyBind env1 top_lvl bndr bndr2 rhs2
 
-    else if is_top_level || exprIsTrivial rhs2 || exprIsValue rhs2 then
+    else if is_top_level || exprIsTrivial rhs2 || exprIsHNF rhs2 then
        --      WARNING: long dodgy argument coming up
        --      WANTED: a better way to do this
        --              
-       -- We can't use "exprIsCheap" instead of exprIsValue, 
+       -- We can't use "exprIsCheap" instead of exprIsHNF, 
        -- because that causes a strictness bug.
        --         x = let y* = E in case (scc y) of { T -> F; F -> T}
        -- The case expression is 'cheap', but it's wrong to transform to
        --         y* = E; x = case (scc y) of {...}
        -- Either we must be careful not to float demanded non-values, or
-       -- we must use exprIsValue for the test, which ensures that the
-       -- thing is non-strict.  So exprIsValue => bindings are non-strict
+       -- we must use exprIsHNF for the test, which ensures that the
+       -- thing is non-strict.  So exprIsHNF => bindings are non-strict
        -- I think.  The WARN below tests for this.
        --
        -- We use exprIsTrivial here because we want to reveal lone variables.  
        -- E.g.  let { x = letrec { y = E } in y } in ...
        -- Here we definitely want to float the y=E defn. 
-       -- exprIsValue definitely isn't right for that.
+       -- exprIsHNF definitely isn't right for that.
        --
        -- Again, the floated binding can't be strict; if it's recursive it'll
        -- be non-strict; if it's non-recursive it'd be inlined.
@@ -604,7 +614,7 @@ completeLazyBind :: SimplEnv
 --     (as usual) use the in-scope-env from the floats
 
 completeLazyBind env top_lvl old_bndr new_bndr new_rhs
-  | postInlineUnconditionally env new_bndr occ_info new_rhs
+  | postInlineUnconditionally env top_lvl new_bndr occ_info new_rhs unfolding
   =            -- Drop the binding
     tick (PostInlineUnconditionally old_bndr)  `thenSmpl_`
     returnSmpl (emptyFloats env, extendIdSubst env old_bndr (DoneEx new_rhs))
@@ -635,7 +645,6 @@ completeLazyBind env top_lvl old_bndr new_bndr new_rhs
        -- After inling f at some of its call sites the original binding may
        -- (for example) be no longer strictly demanded.
        -- The solution here is a bit ad hoc...
-       unfolding  = mkUnfolding (isTopLevel top_lvl) new_rhs
        info_w_unf = new_bndr_info `setUnfoldingInfo` unfolding
         final_info | loop_breaker              = new_bndr_info
                   | isEvaldUnfolding unfolding = zapDemandInfo info_w_unf `orElse` info_w_unf
@@ -649,6 +658,7 @@ completeLazyBind env top_lvl old_bndr new_bndr new_rhs
     returnSmpl (unitFloat env final_id new_rhs, env)
 
   where 
+    unfolding    = mkUnfolding (isTopLevel top_lvl) new_rhs
     loop_breaker = isLoopBreaker occ_info
     old_info     = idInfo old_bndr
     occ_info     = occInfo old_info
@@ -704,7 +714,7 @@ might do the same again.
 simplExpr :: SimplEnv -> CoreExpr -> SimplM CoreExpr
 simplExpr env expr = simplExprC env expr (mkBoringStop expr_ty')
                   where
-                    expr_ty' = substTy (getTvSubst env) (exprType expr)
+                    expr_ty' = substTy env (exprType expr)
        -- The type in the Stop continuation, expr_ty', is usually not used
        -- It's only needed when discarding continuations after finding
        -- a function that returns bottom.
@@ -731,7 +741,6 @@ simplExprF env (Type ty) cont
     simplType env ty                   `thenSmpl` \ ty' ->
     rebuild env (Type ty') cont
 
--- gaw 2004
 simplExprF env (Case scrut bndr case_ty alts) cont
   | not (switchIsOn (getSwitchChecker env) NoCaseOfCase)
   =    -- Simplify the scrutinee with a Select continuation
@@ -744,10 +753,10 @@ simplExprF env (Case scrut bndr case_ty alts) cont
     rebuild env case_expr' cont
   where
     case_cont = Select NoDup bndr alts env (mkBoringStop case_ty')
-    case_ty'  = substTy (getTvSubst env) case_ty       -- c.f. defn of simplExpr
+    case_ty'  = substTy env case_ty    -- c.f. defn of simplExpr
 
 simplExprF env (Let (Rec pairs) body) cont
-  = simplRecBndrs env (map fst pairs)          `thenSmpl` \ (env, bndrs') -> 
+  = simplLetBndrs env (map fst pairs)          `thenSmpl` \ (env, bndrs') -> 
        -- NB: bndrs' don't have unfoldings or rules
        -- We add them as we go down
 
@@ -767,7 +776,7 @@ simplType :: SimplEnv -> InType -> SimplM OutType
 simplType env ty
   = seqType new_ty   `seq`   returnSmpl new_ty
   where
-    new_ty = substTy (getTvSubst env) ty
+    new_ty = substTy env ty
 \end{code}
 
 
@@ -834,6 +843,11 @@ mkLamBndrZapper fun n_args
 \begin{code}
 simplNote env (Coerce to from) body cont
   = let
+       addCoerce s1 k1 cont    -- Drop redundant coerces.  This can happen if a polymoprhic
+                               -- (coerce a b e) is instantiated with a=ty1 b=ty2 and the
+                               -- two are the same. This happens a lot in Happy-generated parsers
+         | s1 `coreEqType` k1 = cont
+
        addCoerce s1 k1 (CoerceIt t1 cont)
                --      coerce T1 S1 (coerce S1 K1 e)
                -- ==>
@@ -844,9 +858,9 @@ simplNote env (Coerce to from) body cont
                -- we may find  (coerce T (coerce S (\x.e))) y
                -- and we'd like it to simplify to e[y/x] in one round 
                -- of simplification
-         | t1 `eqType` k1  = cont              -- The coerces cancel out
-         | otherwise       = CoerceIt t1 cont  -- They don't cancel, but 
-                                               -- the inner one is redundant
+         | t1 `coreEqType` k1  = cont                  -- The coerces cancel out
+         | otherwise           = CoerceIt t1 cont      -- They don't cancel, but 
+                                                       -- the inner one is redundant
 
        addCoerce t1t2 s1s2 (ApplyTo dup arg arg_se cont)
          | not (isTypeArg arg),        -- This whole case only works for value args
@@ -865,8 +879,8 @@ simplNote env (Coerce to from) body cont
                -- But it isn't a common case.
          = let 
                (t1,t2) = splitFunTy t1t2
-               new_arg = mkCoerce2 s1 t1 (substExpr subst arg)
-               subst   = getSubst (setInScope arg_se env)
+               new_arg = mkCoerce2 s1 t1 (substExpr arg_env arg)
+               arg_env = setInScope arg_se env
            in
            ApplyTo dup new_arg (zapSubstEnv env) (addCoerce t2 s2 cont)
                        
@@ -912,10 +926,10 @@ simplNote env (CoreNote s) e cont
 
 \begin{code}
 simplVar env var cont
-  = case substId (getSubst env) var of
-       DoneEx e        -> simplExprF (zapSubstEnv env) e cont
-       ContEx se e     -> simplExprF (setSubstEnv env se) e cont
-       DoneId var1 occ -> completeCall (zapSubstEnv env) var1 occ cont
+  = case substId env var of
+       DoneEx e         -> simplExprF (zapSubstEnv env) e cont
+       ContEx tvs ids e -> simplExprF (setSubstEnv env tvs ids) e cont
+       DoneId var1 occ  -> completeCall (zapSubstEnv env) var1 occ cont
                -- Note [zapSubstEnv]
                -- The template is already simplified, so don't re-substitute.
                -- This is VITAL.  Consider
@@ -967,9 +981,10 @@ completeCall env var occ_info cont
 
     let
        in_scope   = getInScope env
+       rules      = getRules env
        maybe_rule = case activeRule env of
                        Nothing     -> Nothing  -- No rules apply
-                       Just act_fn -> lookupRule act_fn in_scope var args 
+                       Just act_fn -> lookupRule act_fn in_scope rules var args 
     in
     case maybe_rule of {
        Just (rule_name, rule_rhs) -> 
@@ -1001,6 +1016,13 @@ completeCall env var occ_info cont
     case maybe_inline of {
        Just unfolding          -- There is an inlining!
          ->  tick (UnfoldingDone var)          `thenSmpl_`
+               (if dopt Opt_D_dump_inlinings dflags then
+                  pprTrace "Inlining done" (vcat [
+                       text "Before:" <+> ppr var <+> sep (map pprParendExpr args),
+                       text "Inlined fn: " <+> ppr unfolding,
+                       text "Cont:  " <+> ppr call_cont])
+                else
+                       id)             $
              makeThatCall env var unfolding args call_cont
 
        ;
@@ -1288,7 +1310,7 @@ Blob of helper functions for the "case-of-something-else" situation.
 rebuildCase :: SimplEnv
            -> OutExpr          -- Scrutinee
            -> InId             -- Case binder
-           -> [InAlt]          -- Alternatives
+           -> [InAlt]          -- Alternatives (inceasing order)
            -> SimplCont
            -> SimplM FloatsWithExpr
 
@@ -1303,9 +1325,10 @@ rebuildCase env scrut case_bndr alts cont
   = knownCon env (LitAlt lit) [] case_bndr alts cont
 
   | otherwise
-  = prepareAlts scrut case_bndr alts           `thenSmpl` \ (better_alts, handled_cons) -> 
+  =    -- Prepare the alternatives.
+    prepareAlts scrut case_bndr alts           `thenSmpl` \ (better_alts, handled_cons) -> 
        
-       -- Deal with the case binder, and prepare the continuation;
+       -- Prepare the continuation;
        -- The new subst_env is in place
     prepareCaseCont env better_alts cont       `thenSmpl` \ (floats, (dup_cont, nondup_cont)) ->
     addFloats env floats                       $ \ env ->      
@@ -1322,12 +1345,12 @@ rebuildCase env scrut case_bndr alts cont
        res_ty' = contResultType dup_cont
     in
 
-       -- Deal with variable scrutinee
-    simplCaseBinder env scrut case_bndr        `thenSmpl` \ (alt_env, case_bndr', zap_occ_info) ->
+       -- Deal with case binder
+    simplCaseBinder env scrut case_bndr        `thenSmpl` \ (alt_env, case_bndr') ->
 
        -- Deal with the case alternatives
-    simplAlts alt_env zap_occ_info handled_cons
-             case_bndr' better_alts dup_cont res_ty'   `thenSmpl` \ alts' ->
+    simplAlts alt_env handled_cons
+             case_bndr' better_alts dup_cont   `thenSmpl` \ alts' ->
 
        -- Put the case back together
     mkCase scrut case_bndr' res_ty' alts'      `thenSmpl` \ case_expr ->
@@ -1404,10 +1427,19 @@ the same for the pattern-bound variables!  Example:
 Here, b and p are dead.  But when we move the argment inside the first
 case RHS, and eliminate the second case, we get
 
-       case x or { (a,b) -> a b }
+       case x of { (a,b) -> a b }
 
 Urk! b is alive!  Reason: the scrutinee was a variable, and case elimination
-happened.  Hence the zap_occ_info function returned by simplCaseBinder
+happened.  
+
+Indeed, this can happen anytime the case binder isn't dead:
+       case <any> of x { (a,b) -> 
+        case x of { (p,q) -> p } }
+Here (a,b) both look dead, but come alive after the inner case is eliminated.
+The point is that we bring into the envt a binding
+       let x = (a,b) 
+after the outer case, and that makes (a,b) alive.  At least we do unless
+the case binder is guaranteed dead.
 
 \begin{code}
 simplCaseBinder env (Var v) case_bndr
@@ -1417,87 +1449,114 @@ simplCaseBinder env (Var v) case_bndr
 --     not (isEvaldUnfolding (idUnfolding v))
 
   = simplBinder env (zap case_bndr)            `thenSmpl` \ (env, case_bndr') ->
-    returnSmpl (modifyInScope env v case_bndr', case_bndr', zap)
+    returnSmpl (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 just just as well.
+       -- any more (v is an OutId).  And this does just as well.
   where
     zap b = b `setIdOccInfo` NoOccInfo
            
 simplCaseBinder env other_scrut case_bndr 
   = simplBinder env case_bndr          `thenSmpl` \ (env, case_bndr') ->
-    returnSmpl (env, case_bndr', \ bndr -> bndr)       -- NoOp on bndr
+    returnSmpl (env, case_bndr')
 \end{code}
 
 
 
 \begin{code}
 simplAlts :: SimplEnv 
-         -> (InId -> InId)             -- Occ-info zapper
          -> [AltCon]                   -- Alternatives the scrutinee can't be
                                        -- in the default case
          -> OutId                      -- Case binder
          -> [InAlt] -> SimplCont
-         -> OutType                    -- Result type
          -> SimplM [OutAlt]            -- Includes the continuation
 
-simplAlts env zap_occ_info handled_cons case_bndr' alts cont' res_ty'
-  = mapSmpl simpl_alt alts
+simplAlts env handled_cons case_bndr' alts cont'
+  = do { mb_alts <- mapSmpl simpl_alt alts
+       ; return [alt' | Just (_, alt') <- mb_alts] }
+       -- Filter out the alternatives that are inaccessible
   where
-    mk_rhs_env env case_bndr_unf
-       = modifyInScope env case_bndr' (case_bndr' `setIdUnfolding` case_bndr_unf)
-
-    simpl_alt (DEFAULT, _, rhs)
-       = let unf = mkOtherCon handled_cons in
-               -- Record the constructors that the case-binder *can't* be.
-         simplExprC (mk_rhs_env env unf) rhs cont'     `thenSmpl` \ rhs' ->
-         returnSmpl (DEFAULT, [], rhs')
-
-    simpl_alt (LitAlt lit, _, rhs)
-       = let unf = mkUnfolding False (Lit lit) in
-         simplExprC (mk_rhs_env env unf) rhs cont'     `thenSmpl` \ rhs' ->
-         returnSmpl (LitAlt lit, [], rhs')
-
-    simpl_alt (DataAlt con, vs, rhs)
-       | isVanillaDataCon con
-       =       -- 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
-         simplBinders env (add_evals con vs)           `thenSmpl` \ (env, vs') ->
+    simpl_alt alt = simplAlt env handled_cons case_bndr' alt cont'
+
+simplAlt :: SimplEnv -> [AltCon] -> OutId -> InAlt -> SimplCont
+        -> SimplM (Maybe (TvSubstEnv, OutAlt))
+-- Simplify an alternative, returning the type refinement for the 
+-- alternative, if the alternative does any refinement at all
+-- Nothing => the alternative is inaccessible
+
+simplAlt env handled_cons case_bndr' (DEFAULT, bndrs, rhs) cont'
+  = ASSERT( null bndrs )
+    simplExprC env' rhs cont'  `thenSmpl` \ rhs' ->
+    returnSmpl (Just (emptyVarEnv, (DEFAULT, [], rhs')))
+  where
+    env' = mk_rhs_env env case_bndr' (mkOtherCon handled_cons)
+       -- Record the constructors that the case-binder *can't* be.
+
+simplAlt env handled_cons case_bndr' (LitAlt lit, bndrs, rhs) cont'
+  = ASSERT( null bndrs )
+    simplExprC env' rhs cont'  `thenSmpl` \ rhs' ->
+    returnSmpl (Just (emptyVarEnv, (LitAlt lit, [], rhs')))
+  where
+    env' = mk_rhs_env env case_bndr' (mkUnfolding False (Lit lit))
+
+simplAlt env handled_cons case_bndr' (DataAlt con, vs, rhs) cont'
+  | isVanillaDataCon con
+  =    -- 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
+    simplBinders env (add_evals con vs)                `thenSmpl` \ (env, vs') ->
 
                -- Bind the case-binder to (con args)
-         let unf = mkUnfolding False (mkConApp con con_args)
-             inst_tys' = tyConAppArgs (idType case_bndr')
-             con_args  = map Type inst_tys' ++ map varToCoreExpr vs' 
-         in
-         simplExprC (mk_rhs_env env unf) rhs cont'     `thenSmpl` \ rhs' ->
-         returnSmpl (DataAlt con, vs', rhs')
-
-
-       | otherwise     -- GADT case
-       = simplBinders env (add_evals con vs)           `thenSmpl` \ (env, vs') ->
-         let unf         = mkUnfolding False con_app
-             con_app    = mkConApp con con_args
-             con_args   = map varToCoreExpr vs'        -- NB: no inst_tys'
-             pat_res_ty = exprType con_app
-             env_w_unf  = mk_rhs_env env unf
-             tv_subst   = getTvSubst env
-         in
-         case coreRefineTys vs' tv_subst pat_res_ty (idType case_bndr') of
-            Just tv_subst_env -> 
-               simplExprC (setTvSubstEnv env_w_unf tv_subst_env) rhs cont'     `thenSmpl` \ rhs' ->
-               returnSmpl (DataAlt con, vs', rhs')
-            Nothing ->         -- Dead code; for now, I'm just going to put in an
-                               -- error case so I can see them
-               let rhs' = mkApps (Var eRROR_ID) 
-                               [Type (substTy tv_subst (exprType rhs)),
+    let unf       = mkUnfolding False (mkConApp con con_args)
+       inst_tys' = tyConAppArgs (idType case_bndr')
+       con_args  = map Type inst_tys' ++ map varToCoreExpr vs' 
+       env'      = mk_rhs_env env case_bndr' unf
+    in
+    simplExprC env' rhs cont'  `thenSmpl` \ rhs' ->
+    returnSmpl (Just (emptyVarEnv, (DataAlt con, vs', rhs')))
+
+  | otherwise  -- GADT case
+  = let
+       (tvs,ids) = span isTyVar vs
+    in
+    simplBinders env tvs                       `thenSmpl` \ (env1, tvs') ->
+    case coreRefineTys (getInScope env1) con tvs' (idType case_bndr') of {
+       Nothing         -- Inaccessible
+           | opt_PprStyle_Debug        -- Hack: if debugging is on, generate an error case 
+                                       --       so we can see it
+           ->  let rhs' = mkApps (Var eRROR_ID) 
+                               [Type (substTy env (exprType rhs)),
                                 Lit (mkStringLit "Impossible alternative (GADT)")]
                in 
-               returnSmpl (DataAlt con, vs', rhs')
+               simplBinders env1 ids           `thenSmpl` \ (env2, ids') -> 
+               returnSmpl (Just (emptyVarEnv, (DataAlt con, tvs' ++ ids', rhs'))) 
+
+           | otherwise -- Filter out the inaccessible branch
+           -> return Nothing ; 
+
+       Just refine@(tv_subst_env, _) ->        -- The normal case
+
+    let 
+       env2 = refineSimplEnv env1 refine
+       -- Simplify the Ids in the refined environment, so their types
+       -- reflect the refinement.  Usually this doesn't matter, but it helps
+       -- in mkDupableAlt, when we want to float a lambda that uses these binders
+       -- Furthermore, it means the binders contain maximal type information
+    in
+    simplBinders env2 (add_evals con ids)      `thenSmpl` \ (env3, ids') ->
+    let unf        = mkUnfolding False con_app
+       con_app    = mkConApp con con_args
+       con_args   = map varToCoreExpr vs'      -- NB: no inst_tys'
+       env_w_unf  = mk_rhs_env env3 case_bndr' unf
+       vs'        = tvs' ++ ids'
+    in
+    simplExprC env_w_unf rhs cont'     `thenSmpl` \ rhs' ->
+    returnSmpl (Just (tv_subst_env, (DataAlt con, vs', rhs'))) }
 
+  where
        -- add_evals records the evaluated-ness of the bound variables of
        -- a case pattern.  This is *important*.  Consider
        --      data T = T !Int !Int
@@ -1506,7 +1565,6 @@ simplAlts env zap_occ_info handled_cons case_bndr' alts cont' res_ty'
        --
        -- We really must record that b is already evaluated so that we don't
        -- go and re-evaluate it when constructing the result.
-
     add_evals dc vs = cat_evals dc vs (dataConRepStrictness dc)
 
     cat_evals dc vs strs
@@ -1519,8 +1577,17 @@ simplAlts env zap_occ_info handled_cons case_bndr' alts cont' res_ty'
            | otherwise          = zapped_v : go vs strs
            where
              zapped_v = zap_occ_info v
-             evald_v  = zapped_v `setIdUnfolding` mkOtherCon []
+             evald_v  = zapped_v `setIdUnfolding` evaldUnfolding
          go _ _ = pprPanic "cat_evals" (ppr dc $$ ppr vs $$ ppr strs)
+
+       -- 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
+    zap_occ_info | isDeadBinder case_bndr' = \id -> id
+                | otherwise               = \id -> id `setIdOccInfo` NoOccInfo
+
+mk_rhs_env env case_bndr' case_bndr_unf
+  = modifyInScope env case_bndr' (case_bndr' `setIdUnfolding` case_bndr_unf)
 \end{code}
 
 
@@ -1571,7 +1638,7 @@ knownCon env con args bndr alts cont
                   bind_args env bs (drop n_drop_tys args)      $ \ env ->
                   let
                        con_app  = mkConApp dc (take n_drop_tys args ++ con_args)
-                       con_args = [substExpr (getSubst env) (varToCoreExpr b) | b <- bs]
+                       con_args = [substExpr env (varToCoreExpr b) | b <- bs]
                                        -- args are aready OutExprs, but bs are InIds
                   in
                   simplNonRecX env bndr con_app                $ \ env ->
@@ -1684,7 +1751,6 @@ mkDupableCont env (ApplyTo _ arg se cont)
        -- This has been this way for a long time, so I'll leave it,
        -- but I can't convince myself that it's right.
 
--- gaw 2004
 mkDupableCont env (Select _ case_bndr alts se cont)
   =    -- e.g.         (case [...hole...] of { pi -> ei })
        --      ===>
@@ -1723,17 +1789,24 @@ mkDupableAlts env case_bndr' alts dupable_cont
   where
     go env [] = returnSmpl (emptyFloats env, [])
     go env (alt:alts)
-       = mkDupableAlt env case_bndr' dupable_cont alt  `thenSmpl` \ (floats1, alt') ->
-         addFloats env floats1                         $ \ env ->
-         go env alts                                   `thenSmpl` \ (floats2, alts') ->
-         returnSmpl (floats2, alt' : alts')
+       = do { (floats1, mb_alt') <- mkDupableAlt env case_bndr' dupable_cont alt
+            ; addFloats env floats1    $ \ env -> do
+            { (floats2, alts') <- go env alts
+            ; returnSmpl (floats2, case mb_alt' of
+                                       Just alt' -> alt' : alts'
+                                       Nothing   -> alts'
+                         )}}
                                        
-mkDupableAlt env case_bndr' cont alt@(con, bndrs, rhs)
-  = simplBinders env bndrs                             `thenSmpl` \ (env, bndrs') ->
-    simplExprC env rhs cont                            `thenSmpl` \ rhs' ->
+mkDupableAlt env case_bndr' cont alt
+  = simplAlt env [] case_bndr' alt cont                `thenSmpl` \ mb_stuff ->
+    case mb_stuff of {
+       Nothing -> returnSmpl (emptyFloats env, Nothing) ;
+
+       Just (reft, (con, bndrs', rhs')) ->
+       -- Safe to say that there are no handled-cons for the DEFAULT case
 
     if exprIsDupable rhs' then
-       returnSmpl (emptyFloats env, (con, bndrs', rhs'))
+       returnSmpl (emptyFloats env, Just (con, bndrs', rhs'))
        -- It is worth checking for a small RHS because otherwise we
        -- get extra let bindings that may cause an extra iteration of the simplifier to
        -- inline back in place.  Quite often the rhs is just a variable or constructor.
@@ -1753,8 +1826,13 @@ mkDupableAlt env case_bndr' cont alt@(con, bndrs, rhs)
     else
     let
        rhs_ty'     = exprType rhs'
-        used_bndrs' = filter (not . isDeadBinder) (case_bndr' : bndrs')
-               -- The deadness info on the new binders is unscathed
+        used_bndrs' = filter abstract_over (case_bndr' : bndrs')
+       abstract_over bndr
+         | isTyVar bndr = not (bndr `elemVarEnv` reft)
+               -- Don't abstract over tyvar binders which are refined away
+               -- See Note [Refinement] below
+         | otherwise    = not (isDeadBinder bndr)
+               -- The deadness info on the new Ids is preserved by simplBinders
     in
        -- If we try to lift a primitive-typed something out
        -- for let-binding-purposes, we will *caseify* it (!),
@@ -1788,7 +1866,7 @@ mkDupableAlt env case_bndr' cont alt@(con, bndrs, rhs)
        --         True -> $j s
        -- (the \v alone is enough to make CPR happy) but I think it's rare
 
-    ( if null used_bndrs' 
+    ( if not (any isId used_bndrs')
        then newId FSLIT("w") realWorldStatePrimTy      `thenSmpl` \ rw_id ->
             returnSmpl ([rw_id], [Var realWorldPrimId])
        else 
@@ -1796,7 +1874,7 @@ mkDupableAlt env case_bndr' cont alt@(con, bndrs, rhs)
     )                                                  `thenSmpl` \ (final_bndrs', final_args) ->
 
        -- See comment about "$j" name above
-    newId (encodeFS FSLIT("$j")) (mkPiTypes final_bndrs' rhs_ty')      `thenSmpl` \ join_bndr ->
+    newId FSLIT("$j") (mkPiTypes final_bndrs' rhs_ty') `thenSmpl` \ join_bndr ->
        -- Notice the funky mkPiTypes.  If the contructor has existentials
        -- it's possible that the join point will be abstracted over
        -- type varaibles as well as term variables.
@@ -1822,5 +1900,28 @@ mkDupableAlt env case_bndr' cont alt@(con, bndrs, rhs)
        join_rhs  = mkLams really_final_bndrs rhs'
        join_call = mkApps (Var join_bndr) final_args
     in
-    returnSmpl (unitFloat env join_bndr join_rhs, (con, bndrs', join_call))
+    returnSmpl (unitFloat env join_bndr join_rhs, Just (con, bndrs', join_call)) }
 \end{code}
+
+Note [Refinement]
+~~~~~~~~~~~~~~~~~
+Consider
+       data T a where
+         MkT :: a -> b -> T a
+
+       f = /\a. \(w::a).
+          case (case ...) of
+                 MkT a' b (p::a') (q::b) -> [p,w]
+
+The danger is that we'll make a join point
+       
+       j a' p = [p,w]
+
+and that's ill-typed, because (p::a') but (w::a).  
+
+Solution so far: don't abstract over a', because the type refinement
+maps [a' -> a] .  Ultimately that won't work when real refinement goes on.
+
+Then we must abstract over any refined free variables.  Hmm.  Maybe we 
+could just abstract over *all* free variables, thereby lambda-lifting
+the join point?   We should try this.