remove empty dir
[ghc-hetmet.git] / ghc / compiler / simplCore / Simplify.lhs
index 09b8cb0..5ea0a91 100644 (file)
@@ -8,58 +8,61 @@ 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,
-                         simplBinder, simplBinders, simplLamBndrs, simplRecBndrs, simplLetBndr,
-                         simplTopBndrs, SimplCont(..), DupFlag(..), LetRhsFlag(..), 
-                         mkStop, mkBoringStop,  pushContArgs,
+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 Var             ( mustHaveLocalBinding )
-import VarEnv
-import Id              ( Id, idType, idInfo, idArity, isDataConId, 
-                         idUnfolding, setIdUnfolding, isDeadBinder,
-                         idNewDemandInfo, setIdInfo,
-                         setIdOccInfo, isLocalId,
-                         zapLamIdInfo, setOneShotLambda, 
+import Id              ( Id, idType, idInfo, idArity, isDataConWorkId, 
+                         setIdUnfolding, isDeadBinder,
+                         idNewDemandInfo, setIdInfo, 
+                         setIdOccInfo, zapLamIdInfo, setOneShotLambda
                        )
+import MkId            ( eRROR_ID )
+import Literal         ( mkStringLit )
 import IdInfo          ( OccInfo(..), isLoopBreaker,
-                         setArityInfo, 
+                         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, otherCons, callSiteInline )
+import CoreUnfold      ( mkUnfolding, callSiteInline )
 import CoreUtils       ( exprIsDupable, exprIsTrivial, needsCaseBinding,
-                         exprIsConApp_maybe, mkPiType, findAlt, findDefault,
-                         exprType, coreAltsType, exprIsValue, 
+                         exprIsConApp_maybe, mkPiTypes, findAlt, 
+                         exprType, exprIsHNF, 
                          exprOkForSpeculation, exprArity, 
-                         mkCoerce, mkSCC, mkInlineMe, mkAltExpr
+                         mkCoerce, mkCoerce2, mkSCC, mkInlineMe, applyTypeToArg
                        )
 import Rules           ( lookupRule )
 import BasicTypes      ( isMarkedStrict )
 import CostCentre      ( currentCCS )
-import Type            ( isUnLiftedType, seqType, mkFunTy, tyConAppArgs,
-                         funResultTy, 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, isNotTopLevel,
+import BasicTypes      ( TopLevelFlag(..), isTopLevel, 
                          RecFlag(..), isNonRec
                        )
+import StaticFlags     ( opt_PprStyle_Debug )
 import OrdList
-import Maybe           ( Maybe )
+import Maybes          ( orElse )
 import Outputable
+import Util             ( notNull )
 \end{code}
 
 
@@ -230,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.
-    simplTopBndrs env (bindersOfBinds binds)   `thenSmpl` \ (env, bndrs') -> 
+    simplRecBndrs env (bindersOfBinds binds)   `thenSmpl` \ (env, bndrs') -> 
     simpl_binds env binds bndrs'               `thenSmpl` \ (floats, _) ->
     freeTick SimplifierDone                    `thenSmpl_`
     returnSmpl (floatBinds floats)
@@ -247,8 +250,15 @@ simplTopBinds env binds
     drop_bs (NonRec _ _) (_ : bs) = bs
     drop_bs (Rec prs)    bs      = drop (length prs) bs
 
-    simpl_bind env (NonRec b r) (b':_) = simplRecOrTopPair env TopLevel b b' r
-    simpl_bind env (Rec pairs)  bs'    = simplRecBind      env TopLevel pairs bs'
+    simpl_bind env bind bs 
+      = getDOptsSmpl                           `thenSmpl` \ dflags ->
+        if dopt Opt_D_dump_inlinings dflags then
+          pprTrace "SimplBind" (ppr (bindersOf bind)) $ simpl_bind1 env bind bs
+       else
+          simpl_bind1 env bind bs
+
+    simpl_bind1 env (NonRec b r) (b':_) = simplRecOrTopPair env TopLevel b b' r
+    simpl_bind1 env (Rec pairs)  bs'    = simplRecBind      env TopLevel pairs bs'
 \end{code}
 
 
@@ -288,27 +298,41 @@ 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 in the substitution
-    simplLetBndr env bndr                              `thenSmpl` \ (env, bndr') ->
-    simplStrictArg env AnRhs rhs rhs_se cont_ty        $ \ env rhs1 ->
+       -- fragile occurrence info in the substitution
+    simplNonRecBndr env bndr                                   `thenSmpl` \ (env, bndr1) ->
+    simplStrictArg AnRhs env rhs rhs_se (idType bndr1) cont_ty $ \ env1 rhs1 ->
 
        -- Now complete the binding and simplify the body
-    completeNonRecX env True {- strict -} bndr bndr' rhs1 thing_inside
+    let
+       (env2,bndr2) = addLetIdInfo env1 bndr bndr1
+    in
+    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 in the substitution
-    simplLetBndr env bndr                              `thenSmpl` \ (env, bndr') ->
+       -- fragile occurrence info in the substitution
+    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
@@ -322,7 +346,20 @@ simplNonRecX :: SimplEnv
             -> SimplM FloatsWithExpr
 
 simplNonRecX env bndr new_rhs thing_inside
-  | preInlineUnconditionally env NotTopLevel  bndr
+  | needsCaseBinding (idType bndr) new_rhs
+       -- Make this test *before* the preInlineUnconditionally
+       -- Consider     case I# (quotInt# x y) of 
+       --                I# v -> let w = J# v in ...
+       -- If we gaily inline (quotInt# x y) for v, we end up building an
+       -- extra thunk:
+       --                let w = J# (quotInt# x y) in ...
+       -- because quotInt# can fail.
+  = simplBinder env bndr       `thenSmpl` \ (env, bndr') ->
+    thing_inside env           `thenSmpl` \ (floats, body) ->
+    let body' = wrapFloats floats body in 
+    returnSmpl (emptyFloats env, Case new_rhs bndr' (exprType body') [(DEFAULT, [], body')])
+
+  | 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
@@ -331,7 +368,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') ->
@@ -339,18 +376,13 @@ simplNonRecX env bndr new_rhs thing_inside
                    bndr bndr' new_rhs thing_inside
 
 completeNonRecX env is_strict old_bndr new_bndr new_rhs thing_inside
-  | needsCaseBinding (idType new_bndr) new_rhs
-  = thing_inside env                   `thenSmpl` \ (floats, body) ->
-    returnSmpl (emptyFloats env, Case new_rhs new_bndr [(DEFAULT, [], wrapFloats floats body)])
-
-  | otherwise
   = mkAtomicArgs is_strict 
                 True {- OK to float unlifted -} 
                 new_rhs                        `thenSmpl` \ (aux_binds, rhs2) ->
 
        -- Make the arguments atomic if necessary, 
        -- adding suitable bindings
-    addAtomicBindsE env aux_binds              $ \ env ->
+    addAtomicBindsE env (fromOL aux_binds)     $ \ env ->
     completeLazyBind env NotTopLevel
                     old_bndr new_bndr rhs2     `thenSmpl` \ (floats, env) ->
     addFloats env floats thing_inside
@@ -396,9 +428,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
@@ -430,33 +462,22 @@ simplLazyBind :: SimplEnv
              -> InExpr -> SimplEnv     -- The RHS and its environment
              -> SimplM (FloatsWith SimplEnv)
 
-simplLazyBind env top_lvl is_rec bndr bndr' rhs rhs_se
-  =    -- Substitute IdInfo on binder, in the light of earlier
-       -- substitutions in this very letrec, and extend the 
-       -- in-scope env, so that the IdInfo for this binder extends 
-       -- over the RHS for the binder itself.
-       --
-       -- 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: does no harm for non-recursive bindings
-    let
-       bndr_ty'          = idType bndr'
-       bndr''            = simplIdInfo (getSubst rhs_se) (idInfo bndr) bndr'
-       env1              = modifyInScope env bndr'' bndr''
+simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
+  = let        
+       (env1,bndr2)      = addLetIdInfo env bndr bndr1
        rhs_env           = setInScope rhs_se env1
-       ok_float_unlifted = isNotTopLevel top_lvl && isNonRec is_rec
-       rhs_cont          = mkStop bndr_ty' AnRhs
+       is_top_level      = isTopLevel top_lvl
+       ok_float_unlifted = not is_top_level && isNonRec is_rec
+       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 bndr''
+       completeLazyBind env1 top_lvl bndr bndr2
                         (wrapFloats floats rhs1)
     else       
 
@@ -466,38 +487,54 @@ simplLazyBind env top_lvl is_rec bndr bndr' 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 && null aux_binds then     -- Shortcut a common case
-       completeLazyBind env1 top_lvl bndr bndr'' rhs2
-
-       -- 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.
-       --
-       -- BUT we can't use "exprIsCheap", because that causes a strictness bug.
+    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 || exprIsHNF rhs2 then
+       --      WARNING: long dodgy argument coming up
+       --      WANTED: a better way to do this
+       --              
+       -- 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.  I think.  The WARN below tests for this.
-    else if exprIsTrivial rhs2 || exprIsValue rhs2 then
+       -- 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. 
+       -- 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.
+       --
+       -- Note [SCC-and-exprIsTrivial]
+       -- If we have
+       --      y = let { x* = E } in scc "foo" x
+       -- then we do *not* want to float out the x binding, because
+       -- it's strict!  Fortunately, exprIsTrivial replies False to
+       -- (scc "foo" x).
+
                -- There's a subtlety here.  There may be a binding (x* = e) in the
                -- floats, where the '*' means 'will be demanded'.  So is it safe
                -- to float it out?  Answer no, but it won't matter because
-               -- we only float if arg' is a WHNF,
+               -- we only float if (a) arg' is a WHNF, or (b) it's going to top level
                -- and so there can't be any 'will be demanded' bindings in the floats.
-               -- Hence the assert
-        WARN( any demanded_float (floatBinds floats), 
-             ppr (filter demanded_float (floatBinds floats)) )
+               -- Hence the warning
+        ASSERT2( is_top_level || not (any demanded_float (floatBinds floats)), 
+                ppr (filter demanded_float (floatBinds floats)) )
 
        tick LetFloatFromLet                    `thenSmpl_` (
        addFloats env1 floats                   $ \ env2 ->
-       addAtomicBinds env2 aux_binds           $ \ env3 ->
-       completeLazyBind env3 top_lvl bndr bndr'' rhs2)
+       addAtomicBinds env2 (fromOL aux_binds)  $ \ env3 ->
+       completeLazyBind env3 top_lvl bndr bndr2 rhs2)
 
     else
-       completeLazyBind env1 top_lvl bndr bndr'' (wrapFloats floats rhs1)
+       completeLazyBind env1 top_lvl bndr bndr2 (wrapFloats floats rhs1)
 
 #ifdef DEBUG
 demanded_float (NonRec b r) = isStrictDmd (idNewDemandInfo b) && not (isUnLiftedType (idType b))
@@ -544,10 +581,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 loop_breaker 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
 
@@ -556,16 +593,31 @@ completeLazyBind env top_lvl old_bndr new_bndr new_rhs
                -- Add arity info
        new_bndr_info = idInfo new_bndr `setArityInfo` exprArity new_rhs
 
-               -- Add the unfolding *only* for non-loop-breakers
-               -- Making loop breakers not have an unfolding at all 
-               -- means that we can avoid tests in exprIsConApp, for example.
-               -- This is important: if exprIsConApp says 'yes' for a recursive
-               -- thing, then we can get into an infinite loop
-        info_w_unf | loop_breaker = new_bndr_info
-                  | otherwise    = new_bndr_info `setUnfoldingInfo` unfolding
-       unfolding = mkUnfolding (isTopLevel top_lvl) new_rhs
-
-       final_id = new_bndr `setIdInfo` info_w_unf
+       -- Add the unfolding *only* for non-loop-breakers
+       -- Making loop breakers not have an unfolding at all 
+       -- means that we can avoid tests in exprIsConApp, for example.
+       -- This is important: if exprIsConApp says 'yes' for a recursive
+       -- thing, then we can get into an infinite loop
+
+       -- If the unfolding is a value, the demand info may
+       -- go pear-shaped, so we nuke it.  Example:
+       --      let x = (a,b) in
+       --      case x of (p,q) -> h p q x
+       -- Here x is certainly demanded. But after we've nuked
+       -- the case, we'll get just
+       --      let x = (a,b) in h a b x
+       -- and now x is not demanded (I'm assuming h is lazy)
+       -- This really happens.  Similarly
+       --      let f = \x -> e in ...f..f...
+       -- 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...
+       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
+                  | otherwise                  = info_w_unf
+
+       final_id = new_bndr `setIdInfo` final_info
     in
                -- These seqs forces the Id, and hence its IdInfo,
                -- and hence any inner substitutions
@@ -573,6 +625,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
@@ -628,7 +681,7 @@ might do the same again.
 simplExpr :: SimplEnv -> CoreExpr -> SimplM CoreExpr
 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.
@@ -655,7 +708,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)
@@ -666,12 +719,13 @@ 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') -> 
-       -- NB: bndrs' don't have unfoldings or spec-envs
-       -- We add them as we go down, using simplPrags
+       -- NB: bndrs' don't have unfoldings or rules
+       -- We add them as we go down
 
     simplRecBind env NotTopLevel pairs bndrs'  `thenSmpl` \ (floats, env) ->
     addFloats env floats                       $ \ env ->
@@ -689,7 +743,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}
 
 
@@ -711,7 +765,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)
@@ -756,7 +810,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)
@@ -768,17 +825,19 @@ 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)
-         | Just (s1, s2) <- splitFunTy_maybe s1s2
+         | not (isTypeArg arg),        -- This whole case only works for value args
+                                       -- Could upgrade to have equiv thing for type apps too  
+           Just (s1, s2) <- splitFunTy_maybe s1s2
                --      (coerce (T1->T2) (S1->S2) F) E
                -- ===> 
                --      coerce T2 S2 (F (coerce S1 T1 E))
                --
-               -- t1t2 must be a function type, T1->T2
+               -- t1t2 must be a function type, T1->T2, because it's applied to something
                -- but s1s2 might conceivably not be
                --
                -- When we build the ApplyTo we can't mix the out-types
@@ -787,7 +846,8 @@ simplNote env (Coerce to from) body cont
                -- But it isn't a common case.
          = let 
                (t1,t2) = splitFunTy t1t2
-               new_arg = mkCoerce 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)
                        
@@ -818,6 +878,10 @@ simplNote env InlineMe e cont
                -- an interesting context of any kind to combine with
                -- (even a type application -- anything except Stop)
   = simplExprF env e cont
+
+simplNote env (CoreNote s) e cont
+  = simplExpr env e    `thenSmpl` \ e' ->
+    rebuild env (Note (CoreNote s) e') cont
 \end{code}
 
 
@@ -829,12 +893,11 @@ simplNote env InlineMe 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
@@ -853,8 +916,9 @@ completeCall env var occ_info cont
     let
        chkr                           = getSwitchChecker env
        (args, call_cont, inline_call) = getContArgs chkr var cont
+       fn_ty                          = idType var
     in
-    simplifyArgs env args (contResultType call_cont)   $ \ env args ->
+    simplifyArgs env fn_ty args (contResultType call_cont)     $ \ env args ->
 
        -- Next, look for rules or specialisations that match
        --
@@ -884,18 +948,20 @@ 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) -> 
                tick (RuleFired rule_name)                      `thenSmpl_`
                (if dopt Opt_D_dump_inlinings dflags then
                   pprTrace "Rule fired" (vcat [
-                       text "Rule:" <+> ptext rule_name,
+                       text "Rule:" <+> ftext rule_name,
                        text "Before:" <+> ppr var <+> sep (map pprParendExpr args),
-                       text "After: " <+> pprCoreExpr rule_rhs])
+                       text "After: " <+> pprCoreExpr rule_rhs,
+                       text "Cont:  " <+> ppr call_cont])
                 else
                        id)             $
                simplExprF env rule_rhs call_cont ;
@@ -906,17 +972,24 @@ completeCall env var occ_info cont
     let
        arg_infos = [ interestingArg arg | arg <- args, isValArg arg]
 
-       interesting_cont = interestingCallContext (not (null args)) 
-                                                 (not (null arg_infos))
+       interesting_cont = interestingCallContext (notNull args)
+                                                 (notNull arg_infos)
                                                  call_cont
 
-       active_inline = activeInline env var
+       active_inline = activeInline env var occ_info
        maybe_inline  = callSiteInline dflags active_inline inline_call occ_info
                                       var arg_infos interesting_cont
     in
     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
 
        ;
@@ -943,7 +1016,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)
@@ -974,6 +1047,7 @@ makeThatCall env var fun args cont
 --     Simplifying the arguments of a call
 
 simplifyArgs :: SimplEnv 
+            -> OutType                         -- Type of the function
             -> [(InExpr, SimplEnv, Bool)]      -- Details of the arguments
             -> OutType                         -- Type of the continuation
             -> (SimplEnv -> [OutExpr] -> SimplM FloatsWithExpr)
@@ -1004,35 +1078,38 @@ simplifyArgs :: SimplEnv
 -- discard the entire application and replace it with (error "foo").  Getting
 -- all this at once is TOO HARD!
 
-simplifyArgs env args cont_ty thing_inside
-  = go env args thing_inside
+simplifyArgs env fn_ty args cont_ty thing_inside
+  = go env fn_ty args thing_inside
   where
-    go env []        thing_inside = thing_inside env []
-    go env (arg:args) thing_inside = simplifyArg env arg cont_ty       $ \ env arg' ->
-                                    go env args                        $ \ env args' ->
-                                    thing_inside env (arg':args')
+    go env fn_ty []        thing_inside = thing_inside env []
+    go env fn_ty (arg:args) thing_inside = simplifyArg env fn_ty arg cont_ty           $ \ env arg' ->
+                                          go env (applyTypeToArg fn_ty arg') args      $ \ env args' ->
+                                          thing_inside env (arg':args')
 
-simplifyArg env (Type ty_arg, se, _) cont_ty thing_inside
+simplifyArg env fn_ty (Type ty_arg, se, _) cont_ty thing_inside
   = simplType (setInScope se env) ty_arg       `thenSmpl` \ new_ty_arg ->
     thing_inside env (Type new_ty_arg)
 
-simplifyArg env (val_arg, arg_se, is_strict) cont_ty thing_inside 
+simplifyArg env fn_ty (val_arg, arg_se, is_strict) cont_ty thing_inside 
   | is_strict 
-  = simplStrictArg env AnArg val_arg arg_se cont_ty thing_inside
-
-  | otherwise
-  = let
-       arg_env = setInScope arg_se env
-    in
-    simplType arg_env (exprType val_arg)               `thenSmpl` \ arg_ty ->
-    simplExprF arg_env val_arg (mkStop arg_ty AnArg)   `thenSmpl` \ (floats, arg1) ->
-    addFloats env floats                               $ \ env ->
-    thing_inside env arg1
+  = simplStrictArg AnArg env val_arg arg_se arg_ty cont_ty thing_inside
+
+  | otherwise  -- Lazy argument
+               -- DO NOT float anything outside, hence simplExprC
+               -- There is no benefit (unlike in a let-binding), and we'd
+               -- have to be very careful about bogus strictness through 
+               -- floating a demanded let.
+  = simplExprC (setInScope arg_se env) val_arg
+              (mkBoringStop arg_ty)            `thenSmpl` \ arg1 ->
+   thing_inside env arg1
+  where
+    arg_ty = funArgTy fn_ty
 
 
-simplStrictArg :: SimplEnv             -- The env of the call
-               -> LetRhsFlag
-               -> InExpr -> SimplEnv   -- The arg plus its env
+simplStrictArg ::  LetRhsFlag
+               -> SimplEnv             -- The env of the call
+               -> InExpr -> SimplEnv   -- The arg plus its env
+               -> OutType              -- arg_ty: type of the argument
                -> OutType              -- cont_ty: Type of thing computed by the context
                -> (SimplEnv -> OutExpr -> SimplM FloatsWithExpr)       
                                        -- Takes an expression of type rhs_ty, 
@@ -1041,9 +1118,9 @@ simplStrictArg :: SimplEnv                -- The env of the call
                                        -- env of the call, plus any new in-scope variables
                -> SimplM FloatsWithExpr        -- An expression of type cont_ty
 
-simplStrictArg call_env is_rhs arg arg_env cont_ty thing_inside
+simplStrictArg is_rhs call_env arg arg_env arg_ty cont_ty thing_inside
   = simplExprF (setInScope arg_env call_env) arg
-              (ArgOf NoDup is_rhs cont_ty (\ new_env -> thing_inside (setInScope call_env new_env)))
+              (ArgOf is_rhs arg_ty cont_ty (\ new_env -> thing_inside (setInScope call_env new_env)))
   -- Notice the way we use arg_env (augmented with in-scope vars from call_env) 
   --   to simplify the argument
   -- and call-env (augmented with in-scope vars from the arg) to pass to the continuation
@@ -1096,57 +1173,43 @@ context information.
 mkAtomicArgs :: Bool   -- A strict binding
             -> Bool    -- OK to float unlifted args
             -> OutExpr
-            -> SimplM ([(OutId,OutExpr)],      -- The floats (unusually) may include
-                       OutExpr)                -- things that need case-binding,
-                                               -- if the strict-binding flag is on
+            -> SimplM (OrdList (OutId,OutExpr),  -- The floats (unusually) may include
+                       OutExpr)                  -- things that need case-binding,
+                                                 -- if the strict-binding flag is on
 
 mkAtomicArgs is_strict ok_float_unlifted rhs
-  = mk_atomic_args rhs         `thenSmpl` \ maybe_stuff ->
-    case maybe_stuff of
-       Nothing               -> returnSmpl ([],              rhs) 
-       Just (ol_binds, rhs') -> returnSmpl (fromOL ol_binds, rhs')
+  | (Var fun, args) <- collectArgs rhs,                                -- It's an application
+    isDataConWorkId fun || valArgCount args < idArity fun      -- And it's a constructor or PAP
+  = go fun nilOL [] args       -- Have a go
+
+  | otherwise = bale_out       -- Give up
 
   where
-    mk_atomic_args :: OutExpr -> SimplM (Maybe (OrdList (Id,OutExpr), OutExpr))
-       -- Nothing => no change
-    mk_atomic_args rhs
-      | (Var fun, args) <- collectArgs rhs,                    -- It's an application
-        isDataConId fun || valArgCount args < idArity fun      -- And it's a constructor or PAP
-      =        -- Worth a try
-        go nilOL [] args       `thenSmpl` \ maybe_stuff ->
-       case maybe_stuff of
-         Nothing                 -> returnSmpl Nothing
-         Just (aux_binds, args') -> returnSmpl (Just (aux_binds, mkApps (Var fun) args'))
-    
-     | otherwise
-     = returnSmpl Nothing
+    bale_out = returnSmpl (nilOL, rhs)
+
+    go fun binds rev_args [] 
+       = returnSmpl (binds, mkApps (Var fun) (reverse rev_args))
 
-    go binds rev_args [] 
-       = returnSmpl (Just (binds, reverse rev_args))
-    go binds rev_args (arg : args) 
-       |  exprIsTrivial arg    -- Easy case
-       = go binds (arg:rev_args) args
+    go fun binds rev_args (arg : args) 
+       | exprIsTrivial arg     -- Easy case
+       = go fun binds (arg:rev_args) args
 
        | not can_float_arg     -- Can't make this arg atomic
-       = returnSmpl Nothing    -- ... so give up
+       = bale_out              -- ... so give up
 
        | otherwise     -- Don't forget to do it recursively
                        -- E.g.  x = a:b:c:[]
-       =  mk_atomic_args arg                                   `thenSmpl` \ maybe_anf ->
-          case maybe_anf of {
-            Nothing -> returnSmpl Nothing ;
-            Just (arg_binds,arg') ->
-
-          newId SLIT("a") arg_ty                               `thenSmpl` \ arg_id ->
-          go ((arg_binds `snocOL` (arg_id,arg')) `appOL` binds) 
+       =  mkAtomicArgs is_strict ok_float_unlifted arg `thenSmpl` \ (arg_binds, arg') ->
+          newId FSLIT("a") arg_ty                      `thenSmpl` \ arg_id ->
+          go fun ((arg_binds `snocOL` (arg_id,arg')) `appOL` binds) 
              (Var arg_id : rev_args) args
-          }
        where
          arg_ty        = exprType arg
          can_float_arg =  is_strict 
                        || not (isUnLiftedType arg_ty)
                        || (ok_float_unlifted && exprOkForSpeculation arg)
 
+
 addAtomicBinds :: SimplEnv -> [(OutId,OutExpr)]
               -> (SimplEnv -> SimplM (FloatsWith a))
               -> SimplM (FloatsWith a)
@@ -1166,7 +1229,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 -> 
@@ -1185,7 +1249,7 @@ rebuild :: SimplEnv -> OutExpr -> SimplCont -> SimplM FloatsWithExpr
 
 rebuild env expr (Stop _ _ _)                = rebuildDone env expr
 rebuild env expr (ArgOf _ _ _ cont_fn)       = cont_fn env expr
-rebuild env expr (CoerceIt to_ty cont)       = rebuild env (mkCoerce to_ty (exprType expr) expr) cont
+rebuild env expr (CoerceIt to_ty cont)       = rebuild env (mkCoerce to_ty expr) cont
 rebuild env expr (InlinePlease cont)         = rebuild env (Note InlineCall expr) cont
 rebuild env expr (Select _ bndr alts se cont) = rebuildCase (setInScope se env) expr bndr alts cont
 rebuild env expr (ApplyTo _ arg se cont)      = rebuildApp  (setInScope se env) expr arg cont
@@ -1213,7 +1277,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
 
@@ -1228,42 +1292,39 @@ rebuildCase env scrut case_bndr alts cont
   = knownCon env (LitAlt lit) [] case_bndr alts cont
 
   | otherwise
-  =    -- Prepare case alternatives
-       -- Filter out alternatives that can't possibly match
+  =    -- Prepare the alternatives.
+    prepareAlts scrut case_bndr alts           `thenSmpl` \ (better_alts, handled_cons) -> 
+       
+       -- 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 ->      
+
     let
-        impossible_cons = case scrut of
-                           Var v -> otherCons (idUnfolding v)
-                           other -> []
-       better_alts = case impossible_cons of
-                       []    -> alts
-                       other -> [alt | alt@(con,_,_) <- alts, 
-                                       not (con `elem` impossible_cons)]
-
-       -- "handled_cons" are handled either by the context, 
-       -- or by a branch in this case expression
-       -- Don't add DEFAULT to the handled_cons!!
-       (alts_wo_default, _) = findDefault better_alts
-       handled_cons = impossible_cons ++ [con | (con,_,_) <- alts_wo_default]
+       -- 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 the case binder, and prepare the continuation;
-       -- The new subst_env is in place
-    prepareCaseCont env better_alts cont               `thenSmpl` \ (floats, cont') ->
-    addFloats env floats                               $ \ env ->      
-
-       -- 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 cont'              `thenSmpl` \ alts' ->
+    simplAlts alt_env handled_cons
+             case_bndr' better_alts dup_cont   `thenSmpl` \ alts' ->
 
        -- Put the case back together
-    mkCase scrut handled_cons 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
-    rebuildDone env case_expr
+    rebuild env case_expr nondup_cont
 \end{code}
 
 simplCaseBinder checks whether the scrutinee is a variable, v.  If so,
@@ -1295,10 +1356,10 @@ We'll perform the binder-swap for the outer case, giving
     case x of w1 { DEFAULT -> case w1 of w2 { A -> e1; B -> e2 } 
                   ...other cases .... }
 
-But there is no point in doing it for the inner case,
-because w1 can't be inlined anyway.   Furthermore, doing the case-swapping
-involves zapping w2's occurrence info (see paragraphs that follow),
-and that forces us to bind w2 when doing case merging.  So we get
+But there is no point in doing it for the inner case, because w1 can't
+be inlined anyway.  Furthermore, doing the case-swapping involves
+zapping w2's occurrence info (see paragraphs that follow), and that
+forces us to bind w2 when doing case merging.  So we get
 
     case x of w1 { A -> let w2 = w1 in e1
                   B -> let w2 = w1 in e2
@@ -1333,10 +1394,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
@@ -1346,63 +1416,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
-    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'
+
+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
-               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
@@ -1411,18 +1532,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 dc vs = cat_evals dc vs (dataConRepStrictness dc)
 
-    add_evals (DataAlt dc) vs = cat_evals vs (dataConRepStrictness dc)
-    add_evals other_con    vs = vs
-
-    cat_evals [] [] = []
-    cat_evals (v:vs) (str:strs)
-       | isTyVar v          = v        : cat_evals vs (str:strs)
-       | isMarkedStrict str = evald_v  : cat_evals vs strs
-       | otherwise          = zapped_v : cat_evals vs strs
+    cat_evals dc vs strs
+       = go vs strs
        where
-         zapped_v = zap_occ_info v
-         evald_v  = zapped_v `setIdUnfolding` mkOtherCon []
+         go [] [] = []
+         go (v:vs) strs | isTyVar v = v : go vs strs
+         go (v: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` 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}
 
 
@@ -1468,25 +1600,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}
 
@@ -1500,79 +1638,73 @@ bind_args env (b:bs) (arg : args) thing_inside
 \begin{code}
 prepareCaseCont :: SimplEnv
                -> [InAlt] -> SimplCont
-               -> SimplM (FloatsWith SimplCont)        -- Return a duplicatable continuation,
-                                                       -- plus some extra bindings
+               -> SimplM (FloatsWith (SimplCont,SimplCont))    
+                       -- Return a duplicatable continuation, a non-duplicable part 
+                       -- plus some extra bindings
 
-prepareCaseCont env [alt] cont = returnSmpl (emptyFloats env, cont)
        -- No need to make it duplicatable if there's only one alternative
-
-prepareCaseCont env alts  cont = simplType env (coreAltsType alts)     `thenSmpl` \ alts_ty ->
-                                mkDupableCont env alts_ty cont
-       -- At one time I passed in the un-simplified type, and simplified
-       -- it only if we needed to construct a join binder, but that    
-       -- didn't work because we have to decompse function types
-       -- (using funResultTy) in mkDupableCont.
+prepareCaseCont env [alt] cont = returnSmpl (emptyFloats env, (cont, mkBoringStop (contResultType cont)))
+prepareCaseCont env alts  cont = mkDupableCont env cont
 \end{code}
 
 \begin{code}
-mkDupableCont :: SimplEnv
-             -> OutType                -- Type of the thing to be given to the continuation
-             -> SimplCont 
-             -> SimplM (FloatsWith SimplCont)  -- Return a duplicatable continuation,
-                                               -- plus some extra bindings
+mkDupableCont :: SimplEnv -> SimplCont 
+             -> SimplM (FloatsWith (SimplCont, SimplCont))
 
-mkDupableCont env ty cont
+mkDupableCont env cont
   | contIsDupable cont
-  = returnSmpl (emptyFloats env, cont)
-
-mkDupableCont env _ (CoerceIt ty cont)
-  = mkDupableCont env ty cont          `thenSmpl` \ (floats, cont') ->
-    returnSmpl (floats, CoerceIt ty cont')
-
-mkDupableCont env ty (InlinePlease cont)
-  = mkDupableCont env ty cont          `thenSmpl` \ (floats, cont') ->
-    returnSmpl (floats, InlinePlease cont')
-
-mkDupableCont env join_arg_ty (ArgOf _ is_rhs cont_ty cont_fn)
-  =    -- e.g.         (...strict-fn...) [...hole...]
+  = returnSmpl (emptyFloats env, (cont, mkBoringStop (contResultType cont)))
+
+mkDupableCont env (CoerceIt ty cont)
+  = mkDupableCont env cont             `thenSmpl` \ (floats, (dup_cont, nondup_cont)) ->
+    returnSmpl (floats, (CoerceIt ty dup_cont, nondup_cont))
+
+mkDupableCont env (InlinePlease cont)
+  = mkDupableCont env cont             `thenSmpl` \ (floats, (dup_cont, nondup_cont)) ->
+    returnSmpl (floats, (InlinePlease dup_cont, nondup_cont))
+
+mkDupableCont env cont@(ArgOf _ arg_ty _ _)
+  =  returnSmpl (emptyFloats env, (mkBoringStop arg_ty, cont))
+       -- Do *not* duplicate an ArgOf continuation
+       -- Because ArgOf continuations are opaque, we gain nothing by
+       -- propagating them into the expressions, and we do lose a lot.
+       -- Here's an example:
+       --      && (case x of { T -> F; F -> T }) E
+       -- Now, && is strict so we end up simplifying the case with
+       -- an ArgOf continuation.  If we let-bind it, we get
+       --
+       --      let $j = \v -> && v E
+       --      in simplExpr (case x of { T -> F; F -> T })
+       --                   (ArgOf (\r -> $j r)
+       -- And after simplifying more we get
+       --
+       --      let $j = \v -> && v E
+       --      in case of { T -> $j F; F -> $j T }
+       -- Which is a Very Bad Thing
+       --
+       -- The desire not to duplicate is the entire reason that
+       -- mkDupableCont returns a pair of continuations.
+       --
+       -- The original plan had:
+       -- e.g.         (...strict-fn...) [...hole...]
        --      ==>
        --              let $j = \a -> ...strict-fn...
        --              in $j [...hole...]
 
-       -- Build the join Id and continuation
-       -- We give it a "$j" name just so that for later amusement
-       -- we can identify any join points that don't end up as let-no-escapes
-       -- [NOTE: the type used to be exprType join_rhs, but this seems more elegant.]
-    newId SLIT("$j") (mkFunTy join_arg_ty cont_ty)             `thenSmpl` \ join_id ->
-    newId SLIT("a") join_arg_ty                                        `thenSmpl` \ arg_id ->
-
-    cont_fn (addNewInScopeIds env [arg_id]) (Var arg_id)       `thenSmpl` \ (floats, rhs) ->
-    let
-       cont_fn env arg' = rebuildDone env (App (Var join_id) arg')
-       join_rhs         = Lam (setOneShotLambda arg_id) (wrapFloats floats rhs)
-    in
-
-    tick (CaseOfCase join_id)                                          `thenSmpl_`
-       -- Want to tick here so that we go round again,
-       -- and maybe copy or inline the code;
-       -- not strictly CaseOf Case
-
-    returnSmpl (unitFloat env join_id join_rhs, 
-               ArgOf OkToDup is_rhs cont_ty cont_fn)
-
-mkDupableCont env ty (ApplyTo _ arg se cont)
+mkDupableCont env (ApplyTo _ arg se cont)
   =    -- e.g.         [...hole...] (...arg...)
        --      ==>
        --              let a = ...arg... 
        --              in [...hole...] a
-    mkDupableCont env (funResultTy ty) cont            `thenSmpl` \ (floats, cont') ->
+    simplExpr (setInScope se env) arg                  `thenSmpl` \ arg' ->
+
+    mkDupableCont env cont                             `thenSmpl` \ (floats, (dup_cont, nondup_cont)) ->
     addFloats env floats                               $ \ env ->
 
-    simplExpr (setInScope se env) arg                  `thenSmpl` \ arg' ->
     if exprIsDupable arg' then
-       returnSmpl (emptyFloats env, ApplyTo OkToDup arg' (zapSubstEnv se) cont')
+       returnSmpl (emptyFloats env, (ApplyTo OkToDup arg' (zapSubstEnv se) dup_cont, nondup_cont))
     else
-    newId SLIT("a") (exprType arg')                    `thenSmpl` \ arg_id ->
+    newId FSLIT("a") (exprType arg')                   `thenSmpl` \ arg_id ->
 
     tick (CaseOfCase arg_id)                           `thenSmpl_`
        -- Want to tick here so that we go round again,
@@ -1580,13 +1712,13 @@ mkDupableCont env ty (ApplyTo _ arg se cont)
        -- Not strictly CaseOfCase, but never mind
 
     returnSmpl (unitFloat env arg_id arg', 
-               ApplyTo OkToDup (Var arg_id) (zapSubstEnv se) cont')
+               (ApplyTo OkToDup (Var arg_id) (zapSubstEnv se) dup_cont,
+                nondup_cont))
        -- But what if the arg should be case-bound? 
        -- 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 ty (Select _ case_bndr alts se cont)
+mkDupableCont env (Select _ case_bndr alts se cont)
   =    -- e.g.         (case [...hole...] of { pi -> ei })
        --      ===>
        --              let ji = \xij -> ei 
@@ -1595,7 +1727,7 @@ mkDupableCont env ty (Select _ case_bndr alts se cont)
     let
        alt_env = setInScope se env
     in
-    prepareCaseCont alt_env alts cont                          `thenSmpl` \ (floats1, dupable_cont) ->
+    prepareCaseCont alt_env alts cont                          `thenSmpl` \ (floats1, (dup_cont, nondup_cont)) ->
     addFloats alt_env floats1                                  $ \ alt_env ->
 
     simplBinder alt_env case_bndr                              `thenSmpl` \ (alt_env, case_bndr') ->
@@ -1608,10 +1740,12 @@ mkDupableCont env ty (Select _ case_bndr alts se cont)
        -- In the new alts we build, we have the new case binder, so it must retain
        -- its deadness.
 
-    mkDupableAlts alt_env case_bndr' alts dupable_cont `thenSmpl` \ (floats2, alts') ->
+    mkDupableAlts alt_env case_bndr' alts dup_cont     `thenSmpl` \ (floats2, alts') ->
     addFloats alt_env floats2                          $ \ alt_env ->
-    returnSmpl (emptyFloats alt_env, Select OkToDup case_bndr' alts' (zapSubstEnv se) 
-                                           (mkBoringStop (contResultType cont)))
+    returnSmpl (emptyFloats alt_env, 
+               (Select OkToDup case_bndr' alts' (zapSubstEnv se) 
+                       (mkBoringStop (contResultType dup_cont)),
+                nondup_cont))
 
 mkDupableAlts :: SimplEnv -> OutId -> [InAlt] -> SimplCont
              -> SimplM (FloatsWith [InAlt])
@@ -1622,17 +1756,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.
@@ -1652,8 +1793,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 (!),
@@ -1687,16 +1833,16 @@ 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' 
-       then newId SLIT("w") realWorldStatePrimTy       `thenSmpl` \ rw_id ->
+    ( if not (any isId used_bndrs')
+       then newId FSLIT("w") realWorldStatePrimTy      `thenSmpl` \ rw_id ->
             returnSmpl ([rw_id], [Var realWorldPrimId])
        else 
             returnSmpl (used_bndrs', map varToCoreExpr used_bndrs')
     )                                                  `thenSmpl` \ (final_bndrs', final_args) ->
 
        -- See comment about "$j" name above
-    newId SLIT("$j") (foldr mkPiType rhs_ty' final_bndrs')     `thenSmpl` \ join_bndr ->
-       -- Notice the funky mkPiType.  If the contructor has existentials
+    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.
        --  Example:  Suppose we have
@@ -1721,5 +1867,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.