Simplify the IdInfo before any RHSs
[ghc-hetmet.git] / ghc / compiler / simplCore / Simplify.lhs
index 7dc3cfc..0c857c6 100644 (file)
@@ -8,57 +8,58 @@ 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(..), 
-                         mkStop, mkBoringStop,  pushContArgs,
+                         mkRhsStop, mkBoringStop,  pushContArgs,
                          contResultType, countArgs, contIsDupable, contIsRhsOrArg,
-                         getContArgs, interestingCallContext, interestingArg, isStrictType
+                         getContArgs, interestingCallContext, interestingArg, isStrictType,
+                         preInlineUnconditionally, postInlineUnconditionally, 
+                         inlineMode, activeInline, activeRule
                        )
-import Var             ( mustHaveLocalBinding )
-import VarEnv
 import Id              ( Id, idType, idInfo, idArity, isDataConWorkId, 
                          setIdUnfolding, isDeadBinder,
-                         idNewDemandInfo, setIdInfo,
-                         setIdOccInfo, zapLamIdInfo, setOneShotLambda, 
+                         idNewDemandInfo, setIdInfo, 
+                         setIdOccInfo, zapLamIdInfo, setOneShotLambda
                        )
-import OccName         ( encodeFS )
+import MkId            ( eRROR_ID )
+import Literal         ( mkStringLit )
 import IdInfo          ( OccInfo(..), isLoopBreaker,
                          setArityInfo, zapDemandInfo,
                          setUnfoldingInfo, 
                          occInfo
                        )
 import NewDemand       ( isStrictDmd )
-import DataCon         ( dataConNumInstArgs, dataConRepStrictness )
+import Unify           ( coreRefineTys )
+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, 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 
                        )
+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 )
@@ -297,33 +298,38 @@ 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 (extendSubst env bndr (ContEx (getSubstEnv 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) ->
-    simplStrictArg AnRhs env rhs rhs_se (idType bndr1) cont_ty $ \ env1 rhs1 ->
+    simplNonRecBndr env bndr                                   `thenSmpl` \ (env, bndr2) ->
+    simplStrictArg AnRhs env rhs rhs_se (idType bndr2) cont_ty $ \ env2 rhs1 ->
 
        -- Now complete the binding and simplify the body
-    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)
-       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 
        -- fragile occurrence info in the substitution
-    simplLetBndr env bndr                              `thenSmpl` \ (env, bndr') ->
+    simplNonRecBndr env bndr                           `thenSmpl` \ (env, bndr') ->
     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
@@ -347,9 +353,10 @@ 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)])
+    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
@@ -358,7 +365,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 (DoneEx new_rhs))
 
   | otherwise
   = simplBinder env bndr       `thenSmpl` \ (env, bndr') ->
@@ -418,9 +425,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, extendSubst env bndr (ContEx (getSubstEnv 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
@@ -452,52 +459,21 @@ simplLazyBind :: SimplEnv
              -> InExpr -> SimplEnv     -- The RHS and its environment
              -> SimplM (FloatsWith SimplEnv)
 
-simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
-  = let        -- Transfer the IdInfo of the original binder to the new binder
-       -- This is crucial: we must preserve
-       --      strictness
-       --      rules
-       --      worker info
-       -- etc.  To do this we must apply the current substitution, 
-       -- which incorporates earlier substitutions in this very letrec group.
-       --
-       -- NB 1.  We do this *before* processing the RHS of the binder, so that
-       -- its substituted rules are visible in its own RHS.
-       -- This is important.  Manuel found cases where he really, really
-       -- wanted a RULE for a recursive function to apply in that function's
-       -- own right-hand side.
-       --
-       -- NB 2: We do not transfer the arity (see Subst.substIdInfo)
-       -- The arity of an Id should not be visible
-       -- in its own RHS, else we eta-reduce
-       --      f = \x -> f x
-       -- to
-       --      f = f
-       -- which isn't sound.  And it makes the arity in f's IdInfo greater than
-       -- the manifest arity, which isn't good.
-       -- The arity will get added later.
-       --
-       -- NB 3: It's important that we *do* transer the loop-breaker OccInfo,
-       -- because that's what stops the Id getting inlined infinitely, in the body
-       -- of the letrec.
-
-       -- NB 4: does no harm for non-recursive bindings
-
-       bndr2             = bndr1 `setIdInfo` simplIdInfo (getSubst env) (idInfo bndr)
-       env1              = modifyInScope env bndr2 bndr2
-       rhs_env           = setInScope rhs_se env1
+simplLazyBind env top_lvl is_rec bndr bndr2 rhs rhs_se
+  = let        
+       rhs_env           = setInScope rhs_se env
        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 bndr2)
     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) ->
 
        -- If any of the floats can't be floated, give up now
        -- (The allLifted predicate says True for empty floats.)
     if (not ok_float_unlifted && not (allLifted floats)) then
-       completeLazyBind env1 top_lvl bndr bndr2
+       completeLazyBind env top_lvl bndr bndr2
                         (wrapFloats floats rhs1)
     else       
 
@@ -508,26 +484,26 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
        -- If the result is a PAP, float the floats out, else wrap them
        -- By this time it's already been ANF-ised (if necessary)
     if isEmptyFloats floats && isNilOL aux_binds then  -- Shortcut a common case
-       completeLazyBind env1 top_lvl bndr bndr2 rhs2
+       completeLazyBind env 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.
@@ -549,12 +525,12 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
                 ppr (filter demanded_float (floatBinds floats)) )
 
        tick LetFloatFromLet                    `thenSmpl_` (
-       addFloats env1 floats                   $ \ env2 ->
+       addFloats env floats                    $ \ env2 ->
        addAtomicBinds env2 (fromOL aux_binds)  $ \ env3 ->
        completeLazyBind env3 top_lvl bndr bndr2 rhs2)
 
     else
-       completeLazyBind env1 top_lvl bndr bndr2 (wrapFloats floats rhs1)
+       completeLazyBind env top_lvl bndr bndr2 (wrapFloats floats rhs1)
 
 #ifdef DEBUG
 demanded_float (NonRec b r) = isStrictDmd (idNewDemandInfo b) && not (isUnLiftedType (idType b))
@@ -601,10 +577,10 @@ 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, 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
 
@@ -632,7 +608,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
@@ -646,6 +621,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
@@ -699,9 +675,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 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 +704,7 @@ simplExprF env (Type ty) cont
     simplType env ty                   `thenSmpl` \ ty' ->
     rebuild env (Type ty') cont
 
-simplExprF env (Case scrut bndr alts) cont
+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 +715,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 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 +739,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 env ty
 \end{code}
 
 
@@ -784,7 +761,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,7 +806,10 @@ mkLamBndrZapper fun n_args
 \begin{code}
 simplNote env (Coerce to from) body cont
   = let
-       in_scope = getInScope env 
+       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)
@@ -841,9 +821,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
@@ -862,7 +842,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 arg_env arg)
+               arg_env = setInScope arg_se env
            in
            ApplyTo dup new_arg (zapSubstEnv env) (addCoerce t2 s2 cont)
                        
@@ -908,12 +889,11 @@ simplNote env (CoreNote s) e cont
 
 \begin{code}
 simplVar env var cont
-  = case lookupIdSubst (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
+  = 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
                --      let x = e in
@@ -964,9 +944,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) -> 
@@ -998,6 +979,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
 
        ;
@@ -1024,7 +1012,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 +1096,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 +1225,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 -> 
@@ -1284,7 +1273,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
 
@@ -1299,22 +1288,35 @@ 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 ->      
 
-       -- Deal with variable scrutinee
-    simplCaseBinder env scrut case_bndr        `thenSmpl` \ (alt_env, case_bndr', zap_occ_info) ->
+    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 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   `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 +1390,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 +1412,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
          -> SimplM [OutAlt]            -- Includes the continuation
 
-simplAlts env zap_occ_info handled_cons case_bndr' alts cont'
-  = 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
+    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
-    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') ->
+    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
-               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 (Just (emptyVarEnv, (DataAlt con, vs', rhs')))
+
+  | otherwise  -- GADT case
+  = let
+       (tvs,ids) = span isTyVar vs
+    in
+    simplBinders env tvs                       `thenSmpl` \ (env1, tvs') ->
+    case coreRefineTys 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 
+               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
@@ -1466,22 +1528,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 []
+             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}
 
 
@@ -1527,25 +1596,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 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 +1714,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.
 
-
 mkDupableCont env (Select _ case_bndr alts se cont)
   =    -- e.g.         (case [...hole...] of { pi -> ei })
        --      ===>
@@ -1678,17 +1752,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.
@@ -1708,8 +1789,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 (!),
@@ -1743,7 +1829,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 
@@ -1751,7 +1837,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.
@@ -1777,5 +1863,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.