[project @ 2004-12-20 17:16:24 by simonpj]
[ghc-hetmet.git] / ghc / compiler / simplCore / Simplify.lhs
index 7dc3cfc..15bd612 100644 (file)
@@ -15,17 +15,17 @@ import SimplMonad
 import SimplUtils      ( mkCase, mkLam, newId, prepareAlts,
                          simplBinder, simplBinders, simplLamBndrs, simplRecBndrs, simplLetBndr,
                          SimplCont(..), DupFlag(..), LetRhsFlag(..), 
-                         mkStop, mkBoringStop,  pushContArgs,
+                         mkRhsStop, mkBoringStop,  pushContArgs,
                          contResultType, countArgs, contIsDupable, contIsRhsOrArg,
                          getContArgs, interestingCallContext, interestingArg, isStrictType
                        )
-import Var             ( mustHaveLocalBinding )
-import VarEnv
 import Id              ( Id, idType, idInfo, idArity, isDataConWorkId, 
                          setIdUnfolding, isDeadBinder,
-                         idNewDemandInfo, setIdInfo,
+                         idNewDemandInfo, setIdInfo, 
                          setIdOccInfo, zapLamIdInfo, setOneShotLambda, 
                        )
+import MkId            ( eRROR_ID )
+import Literal         ( mkStringLit )
 import OccName         ( encodeFS )
 import IdInfo          ( OccInfo(..), isLoopBreaker,
                          setArityInfo, zapDemandInfo,
@@ -33,7 +33,9 @@ import IdInfo         ( OccInfo(..), isLoopBreaker,
                          occInfo
                        )
 import NewDemand       ( isStrictDmd )
-import DataCon         ( dataConNumInstArgs, dataConRepStrictness )
+import Unify           ( coreRefineTys )
+import DataCon         ( dataConTyCon, dataConRepStrictness, isVanillaDataCon, dataConResTy )
+import TyCon           ( tyConArity )
 import CoreSyn
 import PprCore         ( pprParendExpr, pprCoreExpr )
 import CoreUnfold      ( mkOtherCon, mkUnfolding, callSiteInline )
@@ -41,17 +43,18 @@ import CoreUtils    ( exprIsDupable, exprIsTrivial, needsCaseBinding,
                          exprIsConApp_maybe, mkPiTypes, findAlt, 
                          exprType, exprIsValue, 
                          exprOkForSpeculation, exprArity, 
-                         mkCoerce, mkCoerce2, mkSCC, mkInlineMe, mkAltExpr, applyTypeToArg
+                         mkCoerce, mkCoerce2, mkSCC, mkInlineMe, applyTypeToArg
                        )
 import Rules           ( lookupRule )
 import BasicTypes      ( isMarkedStrict )
 import CostCentre      ( currentCCS )
-import Type            ( isUnLiftedType, seqType, tyConAppArgs, funArgTy,
-                         splitFunTy_maybe, splitFunTy, eqType
-                       )
-import Subst           ( mkSubst, substTy, substExpr, 
-                         isInScope, lookupIdSubst, simplIdInfo
+import Type            ( TvSubstEnv, isUnLiftedType, seqType, tyConAppArgs, funArgTy,
+                         splitFunTy_maybe, splitFunTy, coreEqType, substTy,
+                         mkTyVarTys, mkTyConApp
                        )
+import VarEnv          ( elemVarEnv )
+import Subst           ( SubstResult(..), emptySubst, substExpr, 
+                         substId, simplIdInfo )
 import TysPrim         ( realWorldStatePrimTy )
 import PrelInfo                ( realWorldPrimId )
 import BasicTypes      ( TopLevelFlag(..), isTopLevel, 
@@ -61,7 +64,7 @@ import OrdList
 import Maybe           ( Maybe )
 import Maybes          ( orElse )
 import Outputable
-import Util             ( notNull )
+import Util             ( notNull, equalLength )
 \end{code}
 
 
@@ -299,7 +302,7 @@ simplNonRecBind env bndr rhs rhs_se cont_ty thing_inside
 simplNonRecBind env bndr rhs rhs_se cont_ty thing_inside
   | preInlineUnconditionally env NotTopLevel bndr
   = tick (PreInlineUnconditionally bndr)               `thenSmpl_`
-    thing_inside (extendSubst env bndr (ContEx (getSubstEnv rhs_se) rhs))
+    thing_inside (extendIdSubst env bndr (ContEx (getSubst rhs_se) rhs))
 
 
   | isStrictDmd (idNewDemandInfo bndr) || isStrictType (idType bndr)   -- A strict let
@@ -347,7 +350,9 @@ simplNonRecX env bndr new_rhs thing_inside
        -- because quotInt# can fail.
   = simplBinder env bndr       `thenSmpl` \ (env, bndr') ->
     thing_inside env           `thenSmpl` \ (floats, body) ->
-    returnSmpl (emptyFloats env, Case new_rhs bndr' [(DEFAULT, [], wrapFloats 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
        -- This happens; for example, the case_bndr during case of
@@ -358,7 +363,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 (extendSubst env bndr (ContEx emptySubstEnv new_rhs))
+  = thing_inside (extendIdSubst env bndr (ContEx emptySubst new_rhs))
 
   | otherwise
   = simplBinder env bndr       `thenSmpl` \ (env, bndr') ->
@@ -420,7 +425,7 @@ simplRecOrTopPair :: SimplEnv
 simplRecOrTopPair env top_lvl bndr bndr' rhs
   | preInlineUnconditionally env top_lvl bndr          -- Check for unconditional inline
   = tick (PreInlineUnconditionally bndr)       `thenSmpl_`
-    returnSmpl (emptyFloats env, extendSubst env bndr (ContEx (getSubstEnv env) rhs))
+    returnSmpl (emptyFloats env, extendIdSubst env bndr (ContEx (getSubst env) rhs))
 
   | otherwise
   = simplLazyBind env top_lvl Recursive bndr bndr' rhs env
@@ -488,9 +493,9 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
        rhs_env           = setInScope rhs_se env1
        is_top_level      = isTopLevel top_lvl
        ok_float_unlifted = not is_top_level && isNonRec is_rec
-       rhs_cont          = mkStop (idType bndr1) AnRhs
+       rhs_cont          = mkRhsStop (idType bndr1)
     in
-       -- Simplify the RHS; note the mkStop, which tells 
+       -- Simplify the RHS; note the mkRhsStop, which tells 
        -- the simplifier that this is the RHS of a let.
     simplExprF rhs_env rhs rhs_cont            `thenSmpl` \ (floats, rhs1) ->
 
@@ -604,7 +609,7 @@ completeLazyBind env top_lvl old_bndr new_bndr new_rhs
   | postInlineUnconditionally env new_bndr occ_info new_rhs
   =            -- Drop the binding
     tick (PostInlineUnconditionally old_bndr)  `thenSmpl_`
-    returnSmpl (emptyFloats env, extendSubst env old_bndr (DoneEx new_rhs))
+    returnSmpl (emptyFloats env, extendIdSubst env old_bndr (DoneEx new_rhs))
                -- Use the substitution to make quite, quite sure that the substitution
                -- will happen, since we are going to discard the binding
 
@@ -699,9 +704,9 @@ might do the same again.
 
 \begin{code}
 simplExpr :: SimplEnv -> CoreExpr -> SimplM CoreExpr
-simplExpr env expr = simplExprC env expr (mkStop expr_ty' AnArg)
+simplExpr env expr = simplExprC env expr (mkBoringStop expr_ty')
                   where
-                    expr_ty' = substTy (getSubst env) (exprType expr)
+                    expr_ty' = substTy (getTvSubst 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.
@@ -728,7 +733,8 @@ simplExprF env (Type ty) cont
     simplType env ty                   `thenSmpl` \ ty' ->
     rebuild env (Type ty') cont
 
-simplExprF env (Case scrut bndr alts) cont
+-- gaw 2004
+simplExprF env (Case scrut bndr case_ty alts) cont
   | not (switchIsOn (getSwitchChecker env) NoCaseOfCase)
   =    -- Simplify the scrutinee with a Select continuation
     simplExprF env scrut (Select NoDup bndr alts env cont)
@@ -739,7 +745,8 @@ simplExprF env (Case scrut bndr alts) cont
     simplExprC env scrut case_cont     `thenSmpl` \ case_expr' ->
     rebuild env case_expr' cont
   where
-    case_cont = Select NoDup bndr alts env (mkBoringStop (contResultType cont))
+    case_cont = Select NoDup bndr alts env (mkBoringStop case_ty')
+    case_ty'  = substTy (getTvSubst env) case_ty       -- c.f. defn of simplExpr
 
 simplExprF env (Let (Rec pairs) body) cont
   = simplRecBndrs env (map fst pairs)          `thenSmpl` \ (env, bndrs') -> 
@@ -762,7 +769,7 @@ simplType :: SimplEnv -> InType -> SimplM OutType
 simplType env ty
   = seqType new_ty   `seq`   returnSmpl new_ty
   where
-    new_ty = substTy (getSubst env) ty
+    new_ty = substTy (getTvSubst env) ty
 \end{code}
 
 
@@ -784,7 +791,7 @@ simplLam env fun cont
       =        ASSERT( isTyVar bndr )
        tick (BetaReduction bndr)                       `thenSmpl_`
        simplType (setInScope arg_se env) ty_arg        `thenSmpl` \ ty_arg' ->
-       go (extendSubst env bndr (DoneTy ty_arg')) body body_cont
+       go (extendTvSubst env bndr ty_arg') body body_cont
 
        -- Ordinary beta reduction
     go env (Lam bndr body) cont@(ApplyTo _ arg arg_se body_cont)
@@ -829,8 +836,6 @@ mkLamBndrZapper fun n_args
 \begin{code}
 simplNote env (Coerce to from) body cont
   = let
-       in_scope = getInScope env 
-
        addCoerce s1 k1 (CoerceIt t1 cont)
                --      coerce T1 S1 (coerce S1 K1 e)
                -- ==>
@@ -841,7 +846,7 @@ 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
+         | t1 `coreEqType` k1  = cont          -- The coerces cancel out
          | otherwise       = CoerceIt t1 cont  -- They don't cancel, but 
                                                -- the inner one is redundant
 
@@ -862,7 +867,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 (mkSubst in_scope (getSubstEnv arg_se)) arg)
+               new_arg = mkCoerce2 s1 t1 (substExpr subst arg)
+               subst   = getSubst (setInScope arg_se env)
            in
            ApplyTo dup new_arg (zapSubstEnv env) (addCoerce t2 s2 cont)
                        
@@ -908,12 +914,11 @@ simplNote env (CoreNote s) e cont
 
 \begin{code}
 simplVar env var cont
-  = case lookupIdSubst (getSubst env) var of
+  = 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 -> WARN( not (isInScope var1 (getSubst env)) && mustHaveLocalBinding var1,
-                                text "simplVar:" <+> ppr var )
-                          completeCall (zapSubstEnv env) var1 occ 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
                --      let x = e in
@@ -1024,7 +1029,7 @@ makeThatCall orig_env var fun@(Lam _ _) args cont
     go env (Lam bndr body) (Type ty_arg : args)
       =        ASSERT( isTyVar bndr )
        tick (BetaReduction bndr)                       `thenSmpl_`
-       go (extendSubst env bndr (DoneTy ty_arg)) body args
+       go (extendTvSubst env bndr ty_arg) body args
 
        -- Ordinary beta reduction
     go env (Lam bndr body) (arg : args)
@@ -1108,7 +1113,7 @@ simplifyArg env fn_ty (val_arg, arg_se, is_strict) cont_ty thing_inside
                -- have to be very careful about bogus strictness through 
                -- floating a demanded let.
   = simplExprC (setInScope arg_se env) val_arg
-              (mkStop arg_ty AnArg)            `thenSmpl` \ arg1 ->
+              (mkBoringStop arg_ty)            `thenSmpl` \ arg1 ->
    thing_inside env arg1
   where
     arg_ty = funArgTy fn_ty
@@ -1237,7 +1242,8 @@ addAtomicBindsE env ((v,r):bs) thing_inside
   | needsCaseBinding (idType v) r
   = addAtomicBindsE (addNewInScopeIds env [v]) bs thing_inside `thenSmpl` \ (floats, expr) ->
     WARN( exprIsTrivial expr, ppr v <+> pprCoreExpr expr )
-    returnSmpl (emptyFloats env, Case r v [(DEFAULT,[], wrapFloats floats expr)])
+    (let body = wrapFloats floats expr in 
+     returnSmpl (emptyFloats env, Case r v (exprType body) [(DEFAULT,[],body)]))
 
   | otherwise
   = addAuxiliaryBind env (NonRec v r)  $ \ env -> 
@@ -1306,15 +1312,27 @@ rebuildCase env scrut case_bndr alts cont
     prepareCaseCont env better_alts cont       `thenSmpl` \ (floats, (dup_cont, nondup_cont)) ->
     addFloats env floats                       $ \ env ->      
 
+    let
+       -- The case expression is annotated with the result type of the continuation
+       -- This may differ from the type originally on the case.  For example
+       --      case(T) (case(Int#) a of { True -> 1#; False -> 0# }) of
+       --         a# -> <blob>
+       -- ===>
+       --      let j a# = <blob>
+       --      in case(T) a of { True -> j 1#; False -> j 0# }
+       -- Note that the case that scrutinises a now returns a T not an Int#
+       res_ty' = contResultType dup_cont
+    in
+
        -- Deal with variable scrutinee
-    simplCaseBinder env scrut case_bndr        `thenSmpl` \ (alt_env, case_bndr', zap_occ_info) ->
+    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   `thenSmpl` \ alts' ->
+    simplAlts alt_env handled_cons
+             case_bndr' better_alts dup_cont   `thenSmpl` \ alts' ->
 
        -- Put the case back together
-    mkCase scrut case_bndr' alts'              `thenSmpl` \ case_expr ->
+    mkCase scrut case_bndr' res_ty' alts'      `thenSmpl` \ case_expr ->
 
        -- Notice that rebuildDone returns the in-scope set from env, not alt_env
        -- The case binder *not* scope over the whole returned case-expression
@@ -1388,10 +1406,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
@@ -1401,63 +1428,111 @@ 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
          -> SimplM [OutAlt]            -- Includes the continuation
 
-simplAlts env zap_occ_info handled_cons case_bndr' alts cont'
+simplAlts env handled_cons case_bndr' alts cont'
   = mapSmpl simpl_alt alts
   where
-    inst_tys' = tyConAppArgs (idType case_bndr')
-
-    simpl_alt (DEFAULT, _, rhs)
-       = let
-               -- In the default case we record the constructors that the
-               -- case-binder *can't* be.
-               -- We take advantage of any OtherCon info in the case scrutinee
-               case_bndr_w_unf = case_bndr' `setIdUnfolding` mkOtherCon handled_cons
-               env_with_unf    = modifyInScope env case_bndr' case_bndr_w_unf 
-         in
-         simplExprC env_with_unf rhs cont'     `thenSmpl` \ rhs' ->
-         returnSmpl (DEFAULT, [], rhs')
-
-    simpl_alt (con, vs, rhs)
-       =       -- 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'     `thenSmpl` \ (_, alt') ->
+                   returnSmpl alt'
+
+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
+
+simplAlt env handled_cons case_bndr' (DEFAULT, bndrs, rhs) cont'
+  = ASSERT( null bndrs )
+    simplExprC env' rhs cont'  `thenSmpl` \ rhs' ->
+    returnSmpl (Nothing, (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 (Nothing, (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
-               unfolding    = mkUnfolding False (mkAltExpr con vs' inst_tys')
-               env_with_unf = modifyInScope env case_bndr' (case_bndr' `setIdUnfolding` unfolding)
-         in
-         simplExprC env_with_unf rhs cont'             `thenSmpl` \ rhs' ->
-         returnSmpl (con, vs', 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 (Nothing, (DataAlt con, vs', rhs'))
 
+  | otherwise  -- GADT case
+  = let
+       (tvs,ids) = span isTyVar vs
+    in
+    simplBinders env tvs                       `thenSmpl` \ (env1, tvs') ->
+    let
+       pat_res_ty = dataConResTy con (mkTyVarTys tvs')
+       tv_subst   = getTvSubst env1
+    in
+    case coreRefineTys tvs' tv_subst pat_res_ty (idType case_bndr') of {
+       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)),
+                                Lit (mkStringLit "Impossible alternative (GADT)")]
+               in 
+               simplBinders env1 ids           `thenSmpl` \ (env2, ids') -> 
+               returnSmpl (Nothing, (DataAlt con, tvs' ++ ids', rhs')) ;
+
+       Just tv_subst_env ->    -- The normal case
 
+    let 
+       env2  = setTvSubstEnv env1 tv_subst_env
+       -- 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
+    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
@@ -1466,22 +1541,29 @@ simplAlts env zap_occ_info handled_cons case_bndr' alts cont'
        --
        -- 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 (DataAlt dc) vs = cat_evals dc vs (dataConRepStrictness dc)
-    add_evals other_con    vs = vs
+    add_evals dc vs = cat_evals dc vs (dataConRepStrictness dc)
 
     cat_evals dc vs strs
        = go vs strs
        where
          go [] [] = []
+         go (v:vs) strs | isTyVar v = v : go vs strs
          go (v:vs) (str:strs)
-           | isTyVar v          = v        : go vs (str:strs)
            | isMarkedStrict str = evald_v  : go vs strs
            | otherwise          = zapped_v : go vs strs
            where
              zapped_v = zap_occ_info v
              evald_v  = zapped_v `setIdUnfolding` mkOtherCon []
          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}
 
 
@@ -1527,25 +1609,31 @@ knownCon env con args bndr alts cont
                                  simplNonRecX env bndr (Lit lit)       $ \ env ->
                                  simplExprF env rhs cont
 
-       (DataAlt dc, bs, rhs)  -> ASSERT( length bs + n_tys == length args )
-                                 bind_args env bs (drop n_tys args)    $ \ env ->
-                                 let
-                                   con_app  = mkConApp dc (take n_tys args ++ con_args)
-                                   con_args = [substExpr (getSubst env) (varToCoreExpr b) | b <- bs]
+       (DataAlt dc, bs, rhs)  
+               -> ASSERT( n_drop_tys + length bs == length args )
+                  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]
                                        -- args are aready OutExprs, but bs are InIds
-                                 in
-                                 simplNonRecX env bndr con_app         $ \ env ->
-                                 simplExprF env rhs cont
-                              where
-                                 n_tys = dataConNumInstArgs dc -- Non-existential type args
+                  in
+                  simplNonRecX env bndr con_app                $ \ env ->
+                  simplExprF env rhs cont
+               where
+                  n_drop_tys | isVanillaDataCon dc = tyConArity (dataConTyCon dc)
+                             | otherwise           = 0
+                       -- Vanilla data constructors lack type arguments in the pattern
+
 -- Ugh!
 bind_args env [] _ thing_inside = thing_inside env
 
 bind_args env (b:bs) (Type ty : args) thing_inside
-  = bind_args (extendSubst env b (DoneTy ty)) bs args thing_inside
+  = ASSERT( isTyVar b )
+    bind_args (extendTvSubst env b ty) bs args thing_inside
     
 bind_args env (b:bs) (arg : args) thing_inside
-  = simplNonRecX env b arg     $ \ env ->
+  = ASSERT( isId b )
+    simplNonRecX env b arg     $ \ env ->
     bind_args env bs args thing_inside
 \end{code}
 
@@ -1639,7 +1727,7 @@ 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 })
        --      ===>
@@ -1683,9 +1771,9 @@ mkDupableAlts env case_bndr' alts dupable_cont
          go env alts                                   `thenSmpl` \ (floats2, alts') ->
          returnSmpl (floats2, alt' : 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_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'))
@@ -1708,8 +1796,15 @@ 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 (mb_reft `refines` bndr)
+               -- Don't abstract over tyvar binders which are refined away
+         | otherwise    = not (isDeadBinder bndr)
+               -- The deadness info on the new Ids is preserved by simplBinders
+       refines Nothing         bndr = False
+       refines (Just tv_subst) bndr = bndr `elemVarEnv` tv_subst       
+               -- See Note [Refinement] below
     in
        -- If we try to lift a primitive-typed something out
        -- for let-binding-purposes, we will *caseify* it (!),
@@ -1743,7 +1838,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 
@@ -1779,3 +1874,26 @@ mkDupableAlt env case_bndr' cont alt@(con, bndrs, rhs)
     in
     returnSmpl (unitFloat env join_bndr join_rhs, (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.