Fix scoped type variables for expression type signatures
[ghc-hetmet.git] / compiler / simplCore / Simplify.lhs
index 329d326..dffdd75 100644 (file)
@@ -13,7 +13,7 @@ import DynFlags       ( dopt, DynFlag(Opt_D_dump_inlinings),
                        )
 import SimplMonad
 import SimplEnv        
-import SimplUtils      ( mkCase, mkLam,
+import SimplUtils      ( mkCase, mkLam, 
                          SimplCont(..), DupFlag(..), LetRhsFlag(..), 
                          mkRhsStop, mkBoringStop,  mkLazyArgStop, pushContArgs,
                          contResultType, countArgs, contIsDupable, contIsRhsOrArg,
@@ -26,17 +26,14 @@ import Id           ( Id, idType, idInfo, idArity, isDataConWorkId,
                          idNewDemandInfo, setIdInfo, 
                          setIdOccInfo, zapLamIdInfo, setOneShotLambda
                        )
-import MkId            ( eRROR_ID )
-import Literal         ( mkStringLit )
 import IdInfo          ( OccInfo(..), isLoopBreaker,
                          setArityInfo, zapDemandInfo,
                          setUnfoldingInfo, 
                          occInfo
                        )
 import NewDemand       ( isStrictDmd )
-import Unify           ( coreRefineTys, dataConCanMatch )
-import DataCon         ( DataCon, dataConTyCon, dataConRepStrictness, isVanillaDataCon,
-                         dataConInstArgTys, dataConTyVars )
+import TcGadt          ( dataConCanMatch )
+import DataCon         ( dataConTyCon, dataConRepStrictness )
 import TyCon           ( tyConArity, isAlgTyCon, isNewTyCon, tyConDataCons_maybe )
 import CoreSyn
 import PprCore         ( pprParendExpr, pprCoreExpr )
@@ -45,24 +42,24 @@ import CoreUtils    ( exprIsDupable, exprIsTrivial, needsCaseBinding,
                          exprIsConApp_maybe, mkPiTypes, findAlt, 
                          exprType, exprIsHNF, findDefault, mergeAlts,
                          exprOkForSpeculation, exprArity, 
-                         mkCoerce, mkCoerce2, mkSCC, mkInlineMe, applyTypeToArg
+                         mkCoerce, mkSCC, mkInlineMe, applyTypeToArg,
+                          dataConRepInstPat
                        )
 import Rules           ( lookupRule )
 import BasicTypes      ( isMarkedStrict )
 import CostCentre      ( currentCCS )
 import Type            ( TvSubstEnv, isUnLiftedType, seqType, tyConAppArgs, funArgTy,
-                         splitFunTy_maybe, splitFunTy, coreEqType, splitTyConApp_maybe,
-                         isTyVarTy, mkTyVarTys
+                         coreEqType, splitTyConApp_maybe,
+                         isTyVarTy, isFunTy, tcEqType
                        )
-import Var             ( tyVarKind, mkTyVar )
+import Coercion         ( Coercion, coercionKind,
+                          mkTransCoercion, mkSymCoercion, splitCoercionKind_maybe, decomposeCo  )
 import VarEnv          ( elemVarEnv, emptyVarEnv )
 import TysPrim         ( realWorldStatePrimTy )
 import PrelInfo                ( realWorldPrimId )
 import BasicTypes      ( TopLevelFlag(..), isTopLevel, 
                          RecFlag(..), isNonRec
                        )
-import Name            ( mkSysTvName )
-import StaticFlags     ( opt_PprStyle_Debug )
 import OrdList
 import List            ( nub )
 import Maybes          ( orElse )
@@ -320,13 +317,7 @@ simplNonRecBind' env bndr rhs rhs_se cont_ty 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
+    completeNonRecX env2 True {- strict -} bndr bndr2 rhs1 thing_inside
 
   | otherwise                                                  -- Normal, lazy case
   =    -- Don't use simplBinder because that doesn't keep 
@@ -351,7 +342,21 @@ simplNonRecX :: SimplEnv
             -> SimplM FloatsWithExpr
 
 simplNonRecX env bndr new_rhs thing_inside
-  | needsCaseBinding (idType bndr) new_rhs
+  = do { (env, bndr') <- simplBinder env bndr
+       ; completeNonRecX env False {- Non-strict; pessimistic -} 
+                         bndr bndr' new_rhs thing_inside }
+
+
+completeNonRecX :: SimplEnv
+               -> Bool                 -- Strict binding
+               -> InId                 -- Old binder
+               -> OutId                -- New binder
+               -> OutExpr              -- Simplified RHS
+               -> (SimplEnv -> SimplM FloatsWithExpr)
+               -> SimplM FloatsWithExpr
+
+completeNonRecX env is_strict old_bndr new_bndr new_rhs thing_inside
+  | needsCaseBinding (idType new_bndr) new_rhs
        -- Make this test *before* the preInlineUnconditionally
        -- Consider     case I# (quotInt# x y) of 
        --                I# v -> let w = J# v in ...
@@ -359,12 +364,24 @@ simplNonRecX env bndr new_rhs thing_inside
        -- 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')])
+  = do { (floats, body) <- thing_inside env
+       ; let body' = wrapFloats floats body
+       ; return (emptyFloats env, Case new_rhs new_bndr (exprType body) 
+                                       [(DEFAULT, [], body')]) }
 
-  | preInlineUnconditionally env NotTopLevel bndr new_rhs
+  | otherwise
+  =    -- Make the arguments atomic if necessary, 
+       -- adding suitable bindings
+    -- pprTrace "completeNonRecX" (ppr new_bndr <+> ppr new_rhs) $
+    mkAtomicArgsE env is_strict new_rhs                $ \ env new_rhs ->
+    completeLazyBind env NotTopLevel
+                    old_bndr new_bndr new_rhs  `thenSmpl` \ (floats, env) ->
+    addFloats env floats thing_inside
+
+{- No, no, no!  Do not try preInlineUnconditionally in completeNonRecX
+   Doing so risks exponential behaviour, because new_rhs has been simplified once already
+   In the cases described by the folowing commment, postInlineUnconditionally will 
+   catch many of the relevant cases.
        -- 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
@@ -373,24 +390,11 @@ 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.
+  | preInlineUnconditionally env NotTopLevel bndr new_rhs
   = thing_inside (extendIdSubst env bndr (DoneEx new_rhs))
 
-  | otherwise
-  = simplBinder env bndr       `thenSmpl` \ (env, bndr') ->
-    completeNonRecX env False {- Non-strict; pessimistic -} 
-                   bndr bndr' new_rhs thing_inside
-
-completeNonRecX env is_strict old_bndr new_bndr new_rhs thing_inside
-  = 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 (fromOL aux_binds)     $ \ env ->
-    completeLazyBind env NotTopLevel
-                    old_bndr new_bndr rhs2     `thenSmpl` \ (floats, env) ->
-    addFloats env floats thing_inside
+  -- NB: completeLazyBind uses postInlineUnconditionally; no need to do that here
+-}
 \end{code}
 
 
@@ -530,8 +534,8 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
                -- 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 warning
-        ASSERT2( is_top_level || not (any demanded_float (floatBinds floats)), 
-                ppr (filter demanded_float (floatBinds floats)) )
+        WARN( not (is_top_level || not (any demanded_float (floatBinds floats))), 
+             ppr (filter demanded_float (floatBinds floats)) )
 
        tick LetFloatFromLet                    `thenSmpl_` (
        addFloats env1 floats                   $ \ env2 ->
@@ -589,6 +593,7 @@ completeLazyBind env top_lvl old_bndr new_bndr new_rhs
   | postInlineUnconditionally env top_lvl new_bndr occ_info new_rhs unfolding
   =            -- Drop the binding
     tick (PostInlineUnconditionally old_bndr)  `thenSmpl_`
+    -- pprTrace "Inline unconditionally" (ppr old_bndr <+> ppr new_bndr <+> ppr 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
@@ -603,7 +608,6 @@ completeLazyBind env top_lvl old_bndr new_bndr new_rhs
        -- 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
@@ -627,6 +631,7 @@ completeLazyBind env top_lvl old_bndr new_bndr new_rhs
                -- These seqs forces the Id, and hence its IdInfo,
                -- and hence any inner substitutions
     final_id                                   `seq`
+    -- pprTrace "Binding" (ppr final_id <+> ppr unfolding) $
     returnSmpl (unitFloat env final_id new_rhs, env)
 
   where 
@@ -706,7 +711,9 @@ simplExprF env (Var v)              cont = simplVar env v cont
 simplExprF env (Lit lit)       cont = rebuild env (Lit lit) cont
 simplExprF env expr@(Lam _ _)   cont = simplLam env expr cont
 simplExprF env (Note note expr) cont = simplNote env note expr cont
-simplExprF env (App fun arg)    cont = simplExprF env fun (ApplyTo NoDup arg env cont)
+simplExprF env (Cast body co)   cont = simplCast env body co cont
+simplExprF env (App fun arg)    cont = simplExprF env fun 
+                                        (ApplyTo NoDup arg (Just env) cont)
 
 simplExprF env (Type ty) cont
   = ASSERT( contIsRhsOrArg cont )
@@ -759,6 +766,69 @@ simplType env ty
 %************************************************************************
 
 \begin{code}
+simplCast :: SimplEnv -> InExpr -> Coercion -> SimplCont -> SimplM FloatsWithExpr
+simplCast env body co cont
+  = let
+       addCoerce co cont 
+         | (s1, k1) <- coercionKind co
+         , s1 `tcEqType` k1 = cont
+       addCoerce co1 (CoerceIt co2 cont)
+         | (s1, k1) <- coercionKind co1
+         , (l1, t1) <- coercionKind co2
+                --     coerce T1 S1 (coerce S1 K1 e)
+               -- ==>
+               --      e,                      if T1=K1
+               --      coerce T1 K1 e,         otherwise
+               --
+               -- For example, in the initial form of a worker
+               -- 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
+         , s1 `coreEqType` t1  = cont           -- The coerces cancel out  
+         | otherwise           = CoerceIt (mkTransCoercion co1 co2) cont
+    
+       addCoerce co (ApplyTo dup arg arg_se cont)
+         | not (isTypeArg arg)    -- This whole case only works for value args
+                               -- Could upgrade to have equiv thing for type apps too  
+         , Just (s1s2, t1t2) <- splitCoercionKind_maybe co
+         , isFunTy s1s2
+                -- co : s1s2 :=: t1t2
+               --      (coerce (T1->T2) (S1->S2) F) E
+               -- ===> 
+               --      coerce T2 S2 (F (coerce S1 T1 E))
+               --
+               -- 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
+               -- with the InExpr in the argument, so we simply substitute
+               -- to make it all consistent.  It's a bit messy.
+               -- But it isn't a common case.
+         = result
+         where
+           -- we split coercion t1->t2 :=: s1->s2 into t1 :=: s1 and 
+           -- t2 :=: s2 with left and right on the curried form: 
+           --    (->) t1 t2 :=: (->) s1 s2
+           [co1, co2] = decomposeCo 2 co
+           new_arg    = mkCoerce (mkSymCoercion co1) arg'
+          arg'       = case arg_se of
+                         Nothing     -> arg
+                         Just arg_se -> substExpr (setInScope arg_se env) arg
+           result     = ApplyTo dup new_arg (Just $ zapSubstEnv env) 
+                               (addCoerce co2 cont)
+       addCoerce co cont = CoerceIt co cont
+    in
+    simplType env co           `thenSmpl` \ co' ->
+    simplExprF env body (addCoerce co' cont)
+\end{code}
+
+%************************************************************************
+%*                                                                     *
+\subsection{Lambdas}
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
 simplLam env fun cont
   = go env fun cont
   where
@@ -766,25 +836,32 @@ simplLam env fun cont
     cont_ty = contResultType cont
 
        -- Type-beta reduction
-    go env (Lam bndr body) (ApplyTo _ (Type ty_arg) arg_se body_cont)
+    go env (Lam bndr body) (ApplyTo _ (Type ty_arg) mb_arg_se body_cont)
       =        ASSERT( isTyVar bndr )
-       tick (BetaReduction bndr)                       `thenSmpl_`
-       simplType (setInScope arg_se env) ty_arg        `thenSmpl` \ ty_arg' ->
-       go (extendTvSubst env bndr ty_arg') body body_cont
+       do { tick (BetaReduction bndr)
+          ; ty_arg' <- case mb_arg_se of
+                         Just arg_se -> simplType (setInScope arg_se env) ty_arg
+                         Nothing     -> return ty_arg
+          ; go (extendTvSubst env bndr ty_arg') body body_cont }
 
        -- Ordinary beta reduction
-    go env (Lam bndr body) cont@(ApplyTo _ arg arg_se body_cont)
-      = tick (BetaReduction bndr)                              `thenSmpl_`
-       simplNonRecBind env (zap_it bndr) arg arg_se cont_ty    $ \ env -> 
-       go env body body_cont
+    go env (Lam bndr body) cont@(ApplyTo _ arg (Just arg_se) body_cont)
+      = do { tick (BetaReduction bndr) 
+          ; simplNonRecBind env (zap_it bndr) arg arg_se cont_ty       $ \ env -> 
+            go env body body_cont }
+
+    go env (Lam bndr body) cont@(ApplyTo _ arg Nothing body_cont)
+      = do { tick (BetaReduction bndr) 
+          ; simplNonRecX env (zap_it bndr) arg         $ \ env -> 
+            go env body body_cont }
 
        -- Not enough args, so there are real lambdas left to put in the result
     go env lam@(Lam _ _) cont
-      = simplLamBndrs env bndrs                `thenSmpl` \ (env, bndrs') ->
-       simplExpr env body              `thenSmpl` \ body' ->
-       mkLam env bndrs' body' cont     `thenSmpl` \ (floats, new_lam) ->
-       addFloats env floats            $ \ env -> 
-       rebuild env new_lam cont
+      = do { (env, bndrs') <- simplLamBndrs env bndrs
+          ; body' <- simplExpr env body
+          ; (floats, new_lam) <- mkLam env bndrs' body' cont
+          ; addFloats env floats               $ \ env -> 
+            rebuild env new_lam cont }
       where
        (bndrs,body) = collectBinders lam
 
@@ -813,54 +890,6 @@ mkLamBndrZapper fun n_args
 %************************************************************************
 
 \begin{code}
-simplNote env (Coerce to from) body cont
-  = let
-       addCoerce s1 k1 cont    -- Drop redundant coerces.  This can happen if a polymoprhic
-                               -- (coerce a b e) is instantiated with a=ty1 b=ty2 and the
-                               -- two are the same. This happens a lot in Happy-generated parsers
-         | s1 `coreEqType` k1 = cont
-
-       addCoerce s1 k1 (CoerceIt t1 cont)
-               --      coerce T1 S1 (coerce S1 K1 e)
-               -- ==>
-               --      e,                      if T1=K1
-               --      coerce T1 K1 e,         otherwise
-               --
-               -- For example, in the initial form of a worker
-               -- 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 `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
-                                       -- 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, because it's applied to something
-               -- but s1s2 might conceivably not be
-               --
-               -- When we build the ApplyTo we can't mix the out-types
-               -- with the InExpr in the argument, so we simply substitute
-               -- to make it all consistent.  It's a bit messy.
-               -- But it isn't a common case.
-         = let 
-               (t1,t2) = splitFunTy t1t2
-               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)
-                       
-       addCoerce to' _ cont = CoerceIt to' cont
-    in
-    simplType env to           `thenSmpl` \ to' ->
-    simplType env from         `thenSmpl` \ from' ->
-    simplExprF env body (addCoerce to' from' cont)
 
                
 -- Hack: we only distinguish subsumed cost centre stacks for the purposes of
@@ -869,9 +898,6 @@ simplNote env (SCC cc) e cont
   = simplExpr (setEnclosingCC env currentCCS) e        `thenSmpl` \ e' ->
     rebuild env (mkSCC cc e') cont
 
-simplNote env InlineCall e cont
-  = simplExprF env e (InlinePlease cont)
-
 -- See notes with SimplMonad.inlineMode
 simplNote env InlineMe e cont
   | contIsRhsOrArg cont                -- Totally boring continuation; see notes above
@@ -919,9 +945,9 @@ completeCall env var occ_info cont
   =     -- Simplify the arguments
     getDOptsSmpl                                       `thenSmpl` \ dflags ->
     let
-       chkr                           = getSwitchChecker env
-       (args, call_cont, inline_call) = getContArgs chkr var cont
-       fn_ty                          = idType var
+       chkr              = getSwitchChecker env
+       (args, call_cont) = getContArgs chkr var cont
+       fn_ty             = idType var
     in
     simplifyArgs env fn_ty (interestingArgContext var call_cont) args 
                 (contResultType call_cont)     $ \ env args ->
@@ -981,7 +1007,7 @@ completeCall env var occ_info cont
                                                  (notNull arg_infos)
                                                  call_cont
        active_inline = activeInline env var occ_info
-       maybe_inline  = callSiteInline dflags active_inline inline_call occ_info
+       maybe_inline  = callSiteInline dflags active_inline occ_info
                                       var arg_infos interesting_cont
     in
     case maybe_inline of {
@@ -994,7 +1020,7 @@ completeCall env var occ_info cont
                        text "Cont:  " <+> ppr call_cont])
                 else
                        id)             $
-             makeThatCall env var unfolding args call_cont
+             simplExprF env unfolding (pushContArgs args call_cont)
 
        ;
        Nothing ->              -- No inlining!
@@ -1002,43 +1028,7 @@ completeCall env var occ_info cont
        -- Done
     rebuild env (mkApps (Var var) args) call_cont
     }}
-
-makeThatCall :: SimplEnv
-            -> Id
-            -> InExpr          -- Inlined function rhs 
-            -> [OutExpr]       -- Arguments, already simplified
-            -> SimplCont       -- After the call
-            -> SimplM FloatsWithExpr
--- Similar to simplLam, but this time 
--- the arguments are already simplified
-makeThatCall orig_env var fun@(Lam _ _) args cont
-  = go orig_env fun args
-  where
-    zap_it = mkLamBndrZapper fun (length args)
-
-       -- Type-beta reduction
-    go env (Lam bndr body) (Type ty_arg : args)
-      =        ASSERT( isTyVar bndr )
-       tick (BetaReduction bndr)                       `thenSmpl_`
-       go (extendTvSubst env bndr ty_arg) body args
-
-       -- Ordinary beta reduction
-    go env (Lam bndr body) (arg : args)
-      = tick (BetaReduction bndr)                      `thenSmpl_`
-       simplNonRecX env (zap_it bndr) arg              $ \ env -> 
-       go env body args
-
-       -- Not enough args, so there are real lambdas left to put in the result
-    go env fun args
-      = simplExprF env fun (pushContArgs orig_env args cont)
-       -- NB: orig_env; the correct environment to capture with
-       -- the arguments.... env has been augmented with substitutions 
-       -- from the beta reductions.
-
-makeThatCall env var fun args cont
-  = simplExprF env fun (pushContArgs env args cont)
-\end{code}                
-
+\end{code}
 
 %************************************************************************
 %*                                                                     *
@@ -1053,7 +1043,7 @@ makeThatCall env var fun args cont
 simplifyArgs :: SimplEnv 
             -> OutType                         -- Type of the function
             -> Bool                            -- True if the fn has RULES
-            -> [(InExpr, SimplEnv, Bool)]      -- Details of the arguments
+            -> [(InExpr, Maybe SimplEnv, Bool)] -- Details of the arguments
             -> OutType                         -- Type of the continuation
             -> (SimplEnv -> [OutExpr] -> SimplM FloatsWithExpr)
             -> SimplM FloatsWithExpr
@@ -1091,11 +1081,14 @@ simplifyArgs env fn_ty has_rules args cont_ty thing_inside
                                           go env (applyTypeToArg fn_ty arg') args      $ \ env args' ->
                                           thing_inside env (arg':args')
 
-simplifyArg env fn_ty has_rules (Type ty_arg, se, _) cont_ty thing_inside
+simplifyArg env fn_ty has_rules (arg, Nothing, _) cont_ty thing_inside
+  = thing_inside env arg       -- Already simplified
+
+simplifyArg env fn_ty has_rules (Type ty_arg, Just se, _) cont_ty thing_inside
   = simplType (setInScope se env) ty_arg       `thenSmpl` \ new_ty_arg ->
     thing_inside env (Type new_ty_arg)
 
-simplifyArg env fn_ty has_rules (val_arg, arg_se, is_strict) cont_ty thing_inside 
+simplifyArg env fn_ty has_rules (val_arg, Just arg_se, is_strict) cont_ty thing_inside 
   | is_strict 
   = simplStrictArg AnArg env val_arg arg_se arg_ty cont_ty thing_inside
 
@@ -1175,6 +1168,38 @@ a *strict* let, then it would be a good thing to do.  Hence the
 context information.
 
 \begin{code}
+mkAtomicArgsE :: SimplEnv 
+             -> Bool   -- A strict binding
+             -> OutExpr                                                -- The rhs
+             -> (SimplEnv -> OutExpr -> SimplM FloatsWithExpr)
+             -> SimplM FloatsWithExpr
+
+mkAtomicArgsE env is_strict rhs thing_inside
+  | (Var fun, args) <- collectArgs rhs,                                -- It's an application
+    isDataConWorkId fun || valArgCount args < idArity fun      -- And it's a constructor or PAP
+  = go env (Var fun) args
+
+  | otherwise = thing_inside env rhs
+
+  where
+    go env fun [] = thing_inside env fun
+
+    go env fun (arg : args) 
+       |  exprIsTrivial arg    -- Easy case
+       || no_float_arg         -- Can't make it atomic
+       = go env (App fun arg) args
+
+       | otherwise
+       = do { arg_id <- newId FSLIT("a") arg_ty
+            ; completeNonRecX env False {- pessimistic -} arg_id arg_id arg $ \env ->
+              go env (App fun (Var arg_id)) args }
+       where
+         arg_ty = exprType arg
+         no_float_arg = not is_strict && (isUnLiftedType arg_ty) && not (exprOkForSpeculation arg)
+
+
+-- Old code: consider rewriting to be more like mkAtomicArgsE
+
 mkAtomicArgs :: Bool   -- A strict binding
             -> Bool    -- OK to float unlifted args
             -> OutExpr
@@ -1221,25 +1246,6 @@ addAtomicBinds :: SimplEnv -> [(OutId,OutExpr)]
 addAtomicBinds env []         thing_inside = thing_inside env
 addAtomicBinds env ((v,r):bs) thing_inside = addAuxiliaryBind env (NonRec v r) $ \ env -> 
                                             addAtomicBinds env bs thing_inside
-
-addAtomicBindsE :: SimplEnv -> [(OutId,OutExpr)]
-               -> (SimplEnv -> SimplM FloatsWithExpr)
-               -> SimplM FloatsWithExpr
--- Same again, but this time we're in an expression context,
--- and may need to do some case bindings
-
-addAtomicBindsE env [] thing_inside 
-  = thing_inside env
-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 )
-    (let body = wrapFloats floats expr in 
-     returnSmpl (emptyFloats env, Case r v (exprType body) [(DEFAULT,[],body)]))
-
-  | otherwise
-  = addAuxiliaryBind env (NonRec v r)  $ \ env -> 
-    addAtomicBindsE env bs thing_inside
 \end{code}
 
 
@@ -1254,14 +1260,17 @@ 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 expr) cont
-rebuild env expr (InlinePlease cont)         = rebuild env (Note InlineCall expr) cont
+rebuild env expr (CoerceIt co cont)          = rebuild env (mkCoerce co 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
+rebuild env expr (ApplyTo _ arg mb_se cont)   = rebuildApp  env expr arg mb_se cont
 
-rebuildApp env fun arg cont
-  = simplExpr env arg  `thenSmpl` \ arg' ->
-    rebuild env (App fun arg') cont
+rebuildApp env fun arg mb_se cont
+  = do { arg' <- simplArg env arg mb_se
+       ; rebuild env (App fun arg') cont }
+
+simplArg :: SimplEnv -> CoreExpr -> Maybe SimplEnv -> SimplM CoreExpr
+simplArg env arg Nothing        = return arg   -- The arg is already simplified
+simplArg env arg (Just arg_env) = simplExpr (setInScope arg_env env) arg
 
 rebuildDone env expr = returnSmpl (emptyFloats env, expr)
 \end{code}
@@ -1290,11 +1299,11 @@ rebuildCase env scrut case_bndr alts cont
   | Just (con,args) <- exprIsConApp_maybe scrut        
        -- Works when the scrutinee is a variable with a known unfolding
        -- as well as when it's an explicit constructor application
-  = knownCon env (DataAlt con) args case_bndr alts cont
+  = knownCon env scrut (DataAlt con) args case_bndr alts cont
 
   | Lit lit <- scrut   -- No need for same treatment as constructors
                        -- because literals are inlined more vigorously
-  = knownCon env (LitAlt lit) [] case_bndr alts cont
+  = knownCon env scrut (LitAlt lit) [] case_bndr alts cont
 
   | otherwise
   =    -- Prepare the continuation;
@@ -1416,17 +1425,18 @@ simplCaseBinder env (Var v) case_bndr
 -- Failed try [see Note 2 above]
 --     not (isEvaldUnfolding (idUnfolding v))
 
-  = simplBinder env (zap case_bndr)            `thenSmpl` \ (env, case_bndr') ->
+  = simplBinder env (zapOccInfo case_bndr)             `thenSmpl` \ (env, case_bndr') ->
     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 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')
+
+zapOccInfo :: InId -> InId
+zapOccInfo b = b `setIdOccInfo` NoOccInfo
 \end{code}
 
 
@@ -1506,6 +1516,7 @@ simplDefault :: SimplEnv
 
 simplDefault env case_bndr' imposs_cons cont Nothing
   = return []  -- No default branch
+
 simplDefault env case_bndr' imposs_cons cont (Just rhs)
   |    -- This branch handles the case where we are 
        -- scrutinisng an algebraic data type
@@ -1537,7 +1548,11 @@ simplDefault env case_bndr' imposs_cons cont (Just rhs)
                                -- altogether if it can't match
 
        [con] ->        -- It matches exactly one constructor, so fill it in
-                do { con_alt <- mkDataConAlt case_bndr' con inst_tys rhs
+                do { tick (FillInCaseDefault case_bndr')
+                    ; us <- getUniquesSmpl
+                    ; let (ex_tvs, co_tvs, arg_ids) =
+                              dataConRepInstPat us con inst_tys
+                    ; let con_alt = (DataAlt con, ex_tvs ++ co_tvs ++ arg_ids, rhs)
                    ; Just (_, alt') <- simplAlt env [] case_bndr' cont con_alt
                        -- The simplAlt must succeed with Just because we have
                        -- already filtered out construtors that can't match
@@ -1545,7 +1560,7 @@ simplDefault env case_bndr' imposs_cons cont (Just rhs)
 
        two_or_more -> simplify_default (map DataAlt gadt_imposs ++ imposs_cons)
 
-  | otherwise
+  | otherwise 
   = simplify_default imposs_cons
   where
     cant_match tys data_con = not (dataConCanMatch data_con tys)
@@ -1556,29 +1571,6 @@ simplDefault env case_bndr' imposs_cons cont (Just rhs)
             ; rhs' <- simplExprC env' rhs cont
             ; return [(DEFAULT, [], rhs')] }
 
-mkDataConAlt :: Id -> DataCon -> [OutType] -> InExpr -> SimplM InAlt
--- Make a data-constructor alternative to replace the DEFAULT case
--- NB: there's something a bit bogus here, because we put OutTypes into an InAlt
-mkDataConAlt case_bndr con tys rhs
-  = do         { tick (FillInCaseDefault case_bndr)
-       ; args <- mk_args con tys
-       ; return (DataAlt con, args, rhs) }
-  where
-    mk_args con inst_tys
-      = do { (tv_bndrs, inst_tys') <- mk_tv_bndrs con inst_tys
-          ; let arg_tys = dataConInstArgTys con inst_tys'
-          ; arg_ids <- mapM (newId FSLIT("a")) arg_tys
-          ; returnSmpl (tv_bndrs ++ arg_ids) }
-
-    mk_tv_bndrs con inst_tys
-      | isVanillaDataCon con
-      = return ([], inst_tys)
-      | otherwise
-      = do { tv_uniqs <- getUniquesSmpl
-          ; let new_tvs    = zipWith mk tv_uniqs (dataConTyVars con)
-                mk uniq tv = mkTyVar (mkSysTvName uniq FSLIT("t")) (tyVarKind tv)
-          ; return (new_tvs, mkTyVarTys new_tvs) }
-
 simplAlt :: SimplEnv
         -> [AltCon]    -- These constructors can't be present when
                        -- matching this alternative
@@ -1613,7 +1605,6 @@ simplAlt env handled_cons case_bndr' cont' (LitAlt lit, bndrs, rhs)
     env' = mk_rhs_env env case_bndr' (mkUnfolding False (Lit lit))
 
 simplAlt env handled_cons case_bndr' cont' (DataAlt con, vs, rhs)
-  | isVanillaDataCon con
   =    -- Deal with the pattern-bound variables
        -- Mark the ones that are in ! positions in the data constructor
        -- as certainly-evaluated.
@@ -1625,50 +1616,11 @@ simplAlt env handled_cons case_bndr' cont' (DataAlt con, vs, rhs)
                -- Bind the case-binder to (con args)
     let unf       = mkUnfolding False (mkConApp con con_args)
        inst_tys' = tyConAppArgs (idType case_bndr')
-       con_args  = map Type inst_tys' ++ map varToCoreExpr vs' 
+       con_args  = map Type inst_tys' ++ varsToCoreExprs 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
@@ -1696,8 +1648,9 @@ simplAlt env handled_cons case_bndr' cont' (DataAlt con, vs, rhs)
        -- 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
+       -- Note [Aug06] I can't see why this actually matters
     zap_occ_info | isDeadBinder case_bndr' = \id -> id
-                | otherwise               = \id -> id `setIdOccInfo` NoOccInfo
+                | otherwise               = zapOccInfo
 
 mk_rhs_env env case_bndr' case_bndr_unf
   = modifyInScope env case_bndr' (case_bndr' `setIdUnfolding` case_bndr_unf)
@@ -1724,54 +1677,66 @@ and then
 All this should happen in one sweep.
 
 \begin{code}
-knownCon :: SimplEnv -> AltCon -> [OutExpr]
+knownCon :: SimplEnv -> OutExpr -> AltCon -> [OutExpr]
         -> InId -> [InAlt] -> SimplCont
         -> SimplM FloatsWithExpr
 
-knownCon env con args bndr alts cont
-  = tick (KnownBranch bndr)    `thenSmpl_`
+knownCon env scrut con args bndr alts cont
+  = tick (KnownBranch bndr)            `thenSmpl_`
     case findAlt con alts of
        (DEFAULT, bs, rhs)     -> ASSERT( null bs )
                                  simplNonRecX env bndr scrut   $ \ env ->
-                                       -- This might give rise to a binding with non-atomic args
-                                       -- like x = Node (f x) (g x)
-                                       -- but no harm will be done
+                               -- This might give rise to a binding with non-atomic args
+                               -- like x = Node (f x) (g x)
+                               -- but simplNonRecX will atomic-ify it
                                  simplExprF env rhs cont
-                               where
-                                 scrut = case con of
-                                           LitAlt lit -> Lit lit
-                                           DataAlt dc -> mkConApp dc args
 
        (LitAlt lit, bs, rhs) ->  ASSERT( null bs )
-                                 simplNonRecX env bndr (Lit lit)       $ \ env ->
+                                 simplNonRecX env bndr scrut   $ \ env ->
                                  simplExprF env rhs cont
 
        (DataAlt dc, bs, rhs)  
-               -> ASSERT( n_drop_tys + length bs == length args )
-                  bind_args env bs (drop n_drop_tys args)      $ \ env ->
+               -> -- ASSERT( n_drop_tys + length bs == length args )
+                  bind_args env dead_bndr bs (drop n_drop_tys args)    $ \ env ->
                   let
-                       con_app  = mkConApp dc (take n_drop_tys args ++ con_args)
+                       -- It's useful to bind bndr to scrut, rather than to a fresh
+                       -- binding      x = Con arg1 .. argn
+                       -- because very often the scrut is a variable, so we avoid
+                       -- creating, and then subsequently eliminating, a let-binding
+                       -- BUT, if scrut is a not a variable, we must be careful
+                       -- about duplicating the arg redexes; in that case, make
+                       -- a new con-app from the args
+                       bndr_rhs  = case scrut of
+                                       Var v -> scrut
+                                       other -> con_app
+                       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 ->
+                  simplNonRecX env bndr bndr_rhs               $ \ 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
+                  dead_bndr  = isDeadBinder bndr
+                  n_drop_tys = tyConArity (dataConTyCon dc)
 
 -- Ugh!
-bind_args env [] _ thing_inside = thing_inside env
+bind_args env dead_bndr [] _ thing_inside = thing_inside env
 
-bind_args env (b:bs) (Type ty : args) thing_inside
+bind_args env dead_bndr (b:bs) (Type ty : args) thing_inside
   = ASSERT( isTyVar b )
-    bind_args (extendTvSubst env b ty) bs args thing_inside
+    bind_args (extendTvSubst env b ty) dead_bndr bs args thing_inside
     
-bind_args env (b:bs) (arg : args) thing_inside
+bind_args env dead_bndr (b:bs) (arg : args) thing_inside
   = ASSERT( isId b )
-    simplNonRecX env b arg     $ \ env ->
-    bind_args env bs args thing_inside
+    let
+       b' = if dead_bndr then b else zapOccInfo b
+               -- Note that the binder might be "dead", because it doesn't occur 
+               -- in the RHS; and simplNonRecX may therefore discard it via postInlineUnconditionally
+               -- Nevertheless we must keep it if the case-binder is alive, because it may
+               -- be used in teh con_app
+    in
+    simplNonRecX env b' arg    $ \ env ->
+    bind_args env dead_bndr bs args thing_inside
 \end{code}
 
 
@@ -1806,10 +1771,6 @@ 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
@@ -1838,16 +1799,85 @@ mkDupableCont env cont@(ArgOf _ arg_ty _ _)
        --              let $j = \a -> ...strict-fn...
        --              in $j [...hole...]
 
-mkDupableCont env (ApplyTo _ arg se cont)
+mkDupableCont env (ApplyTo _ arg mb_se cont)
   =    -- e.g.         [...hole...] (...arg...)
        --      ==>
        --              let a = ...arg... 
        --              in [...hole...] a
     do { (floats, (dup_cont, nondup_cont)) <- mkDupableCont env cont
        ; addFloats env floats $ \ env -> do
-       { arg1 <- simplExpr (setInScope se env) arg
+       { arg1 <- simplArg env arg mb_se
        ; (floats2, arg2) <- mkDupableArg env arg1
-       ; return (floats2, (ApplyTo OkToDup arg2 (zapSubstEnv se) dup_cont, nondup_cont)) }}
+       ; return (floats2, (ApplyTo OkToDup arg2 Nothing dup_cont, nondup_cont)) }}
+
+mkDupableCont env cont@(Select _ case_bndr [(_,bs,rhs)] se case_cont)
+--   | not (exprIsDupable rhs && contIsDupable case_cont)      -- See notes below
+--  | not (isDeadBinder case_bndr)
+  | all isDeadBinder bs
+  = returnSmpl (emptyFloats env, (mkBoringStop scrut_ty, cont))
+  where
+    scrut_ty = substTy se (idType case_bndr)
+
+{-     Note [Single-alternative cases]
+       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+This case is just like the ArgOf case.  Here's an example:
+       data T a = MkT !a
+       ...(MkT (abs x))...
+Then we get
+       case (case x of I# x' -> 
+             case x' <# 0# of
+               True  -> I# (negate# x')
+               False -> I# x') of y {
+         DEFAULT -> MkT y
+Because the (case x) has only one alternative, we'll transform to
+       case x of I# x' ->
+       case (case x' <# 0# of
+               True  -> I# (negate# x')
+               False -> I# x') of y {
+         DEFAULT -> MkT y
+But now we do *NOT* want to make a join point etc, giving 
+       case x of I# x' ->
+       let $j = \y -> MkT y
+       in case x' <# 0# of
+               True  -> $j (I# (negate# x'))
+               False -> $j (I# x')
+In this case the $j will inline again, but suppose there was a big
+strict computation enclosing the orginal call to MkT.  Then, it won't
+"see" the MkT any more, because it's big and won't get duplicated.
+And, what is worse, nothing was gained by the case-of-case transform.
+
+When should use this case of mkDupableCont?  
+However, matching on *any* single-alternative case is a *disaster*;
+  e.g. case (case ....) of (a,b) -> (# a,b #)
+  We must push the outer case into the inner one!
+Other choices:
+
+   * Match [(DEFAULT,_,_)], but in the common case of Int, 
+     the alternative-filling-in code turned the outer case into
+               case (...) of y { I# _ -> MkT y }
+
+   * Match on single alternative plus (not (isDeadBinder case_bndr))
+     Rationale: pushing the case inwards won't eliminate the construction.
+     But there's a risk of
+               case (...) of y { (a,b) -> let z=(a,b) in ... }
+     Now y looks dead, but it'll come alive again.  Still, this
+     seems like the best option at the moment.
+
+   * Match on single alternative plus (all (isDeadBinder bndrs))
+     Rationale: this is essentially  seq.
+
+   * Match when the rhs is *not* duplicable, and hence would lead to a
+     join point.  This catches the disaster-case above.  We can test
+     the *un-simplified* rhs, which is fine.  It might get bigger or
+     smaller after simplification; if it gets smaller, this case might
+     fire next time round.  NB also that we must test contIsDupable
+     case_cont *btoo, because case_cont might be big!
+
+     HOWEVER: I found that this version doesn't work well, because
+     we can get        let x = case (...) of { small } in ...case x...
+     When x is inlined into its full context, we find that it was a bad
+     idea to have pushed the outer case inside the (...) case.
+-}
 
 mkDupableCont env (Select _ case_bndr alts se cont)
   =    -- e.g.         (case [...hole...] of { pi -> ei })
@@ -1984,7 +2014,7 @@ mkDupableAlt env case_bndr' cont alt
        then newId FSLIT("w") realWorldStatePrimTy      `thenSmpl` \ rw_id ->
             returnSmpl ([rw_id], [Var realWorldPrimId])
        else 
-            returnSmpl (used_bndrs', map varToCoreExpr used_bndrs')
+            returnSmpl (used_bndrs', varsToCoreExprs used_bndrs')
     )                                                  `thenSmpl` \ (final_bndrs', final_args) ->
 
        -- See comment about "$j" name above