Remove very dead Java backend code.
[ghc-hetmet.git] / compiler / coreSyn / CoreUtils.lhs
index 1bd0acd..4146b62 100644 (file)
@@ -1,93 +1,80 @@
 %
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
-\section[CoreUtils]{Utility functions on @Core@ syntax}
+
+Utility functions on @Core@ syntax
 
 \begin{code}
+{-# OPTIONS -fno-warn-incomplete-patterns #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+
+-- | Commonly useful utilites for manipulating the Core language
 module CoreUtils (
-       -- Construction
-       mkInlineMe, mkSCC, mkCoerce, 
+       -- * Constructing expressions
+       mkSCC, mkCoerce,
        bindNonRec, needsCaseBinding,
-       mkIfThenElse, mkAltExpr, mkPiType, mkPiTypes,
-
-       -- Taking expressions apart
-       findDefault, findAlt, isDefaultAlt, mergeAlts,
+       mkAltExpr, mkPiType, mkPiTypes,
 
-       -- Properties of expressions
-       exprType, coreAltType,
-       exprIsDupable, exprIsTrivial, exprIsCheap, 
-       exprIsHNF,exprOkForSpeculation, exprIsBig, 
-       exprIsConApp_maybe, exprIsBottom,
-       rhsIsStatic,
+       -- * Taking expressions apart
+       findDefault, findAlt, isDefaultAlt, mergeAlts, trimConArgs,
 
-       -- Arity and eta expansion
-       manifestArity, exprArity, 
-       exprEtaExpandArity, etaExpand, 
+       -- * Properties of expressions
+       exprType, coreAltType, coreAltsType,
+       exprIsDupable, exprIsTrivial, exprIsBottom,
+        exprIsCheap, exprIsExpandable, exprIsCheap', CheapAppFun,
+       exprIsHNF, exprOkForSpeculation, exprIsBig, exprIsConLike,
+       rhsIsStatic, isCheapApp, isExpandableApp,
 
-       -- Size
-       coreBindsSize,
+       -- * Expression and bindings size
+       coreBindsSize, exprSize,
+        CoreStats(..), coreBindsStats, 
 
-       -- Hashing
+       -- * Hashing
        hashExpr,
 
-       -- Equality
-       cheapEqExpr, tcEqExpr, tcEqExprX, applyTypeToArgs, applyTypeToArg,
+       -- * Equality
+       cheapEqExpr, eqExpr, eqExprX,
 
-        dataConInstPat, dataConOccInstPat
+       -- * Eta reduction
+       tryEtaReduce,
+
+       -- * Manipulating data constructors and types
+       applyTypeToArgs, applyTypeToArg,
+        dataConRepInstPat, dataConRepFSInstPat
     ) where
 
 #include "HsVersions.h"
 
-
-import GLAEXTS         -- For `xori` 
-
 import CoreSyn
-import CoreFVs         ( exprFreeVars )
-import PprCore         ( pprCoreExpr )
-import Var             ( Var, TyVar, CoVar, isCoVar, tyVarKind, setVarUnique,
-                          mkCoVar, mkTyVar, mkCoVar )
-import OccName          ( OccName, occNameFS, mkVarOcc )
-import VarSet          ( unionVarSet )
+import PprCore
+import Var
+import SrcLoc
 import VarEnv
-import Name            ( hashName, mkSysTvName )
-#if mingw32_TARGET_OS
-import Packages                ( isDllName )
-#endif
-import Literal         ( hashLiteral, literalType, litIsDupable, 
-                         litIsTrivial, isZeroLit, Literal( MachLabel ) )
-import DataCon         ( DataCon, dataConRepArity, 
-                         isVanillaDataCon, dataConTyCon, dataConRepArgTys,
-                          dataConUnivTyVars, dataConExTyVars, dataConEqSpec )
-import PrimOp          ( PrimOp(..), primOpOkForSpeculation, primOpIsCheap )
-import Id              ( Id, idType, globalIdDetails, idNewStrictness, 
-                         mkWildId, idArity, idName, idUnfolding, idInfo,
-                         isOneShotBndr, isStateHackType, isDataConWorkId_maybe, mkSysLocal,
-                         isDataConWorkId, isBottomingId, isDictId
-                       )
-import IdInfo          ( GlobalIdDetails(..), megaSeqIdInfo )
-import NewDemand       ( appIsBottom )
-import Type            ( Type, mkFunTy, mkForAllTy, splitFunTy_maybe,
-                         splitFunTy, tcEqTypeX,
-                         applyTys, isUnLiftedType, seqType, mkTyVarTy,
-                         splitForAllTy_maybe, isForAllTy, splitRecNewType_maybe, 
-                         splitTyConApp_maybe, coreEqType, funResultTy, applyTy,
-                          substTyWith, mkPredTy
-                       )
-import Coercion         ( Coercion, mkTransCoercion, coercionKind,
-                          splitNewTypeRepCo_maybe, mkSymCoercion, mkLeftCoercion,
-                          mkRightCoercion, decomposeCo, coercionKindPredTy,
-                          splitCoercionKind, mkEqPred )
-import TyCon           ( tyConArity )
-import TysWiredIn      ( boolTy, trueDataCon, falseDataCon )
-import CostCentre      ( CostCentre )
-import BasicTypes      ( Arity )
-import PackageConfig   ( PackageId )
-import Unique          ( Unique )
+import VarSet
+import Name
+import Literal
+import DataCon
+import PrimOp
+import Id
+import IdInfo
+import Type
+import Coercion
+import TyCon
+import CostCentre
+import Unique
 import Outputable
-import DynFlags                ( DynFlags, DynFlag(Opt_DictsCheap), dopt )
-import TysPrim         ( alphaTy )     -- Debugging only
-import Util             ( equalLength, lengthAtLeast, foldl2 )
-import FastString       ( mkFastString )
+import TysPrim
+import FastString
+import Maybes
+import Util
+import Pair
+import Data.Word
+import Data.Bits
 \end{code}
 
 
@@ -99,15 +86,17 @@ import FastString       ( mkFastString )
 
 \begin{code}
 exprType :: CoreExpr -> Type
-
-exprType (Var var)             = idType var
-exprType (Lit lit)             = literalType lit
-exprType (Let _ body)          = exprType body
-exprType (Case _ _ ty alts)     = ty
-exprType (Cast e co) 
-  = let (_, ty) = coercionKind co in ty
-exprType (Note other_note e)    = exprType e
-exprType (Lam binder expr)      = mkPiType binder (exprType expr)
+-- ^ Recover the type of a well-typed Core expression. Fails when
+-- applied to the actual 'CoreSyn.Type' expression as it cannot
+-- really be said to have a type
+exprType (Var var)          = idType var
+exprType (Lit lit)          = literalType lit
+exprType (Coercion co)      = coercionType co
+exprType (Let _ body)       = exprType body
+exprType (Case _ _ ty _)     = ty
+exprType (Cast _ co)         = pSnd (coercionKind co)
+exprType (Note _ e)          = exprType e
+exprType (Lam binder expr)   = mkPiType binder (exprType expr)
 exprType e@(App _ _)
   = case collectArgs e of
        (fun, args) -> applyTypeToArgs e (exprType fun) args
@@ -115,52 +104,89 @@ exprType e@(App _ _)
 exprType other = pprTrace "exprType" (pprCoreExpr other) alphaTy
 
 coreAltType :: CoreAlt -> Type
-coreAltType (_,_,rhs) = exprType rhs
+-- ^ Returns the type of the alternatives right hand side
+coreAltType (_,bs,rhs) 
+  | any bad_binder bs = expandTypeSynonyms ty
+  | otherwise         = ty    -- Note [Existential variables and silly type synonyms]
+  where
+    ty           = exprType rhs
+    free_tvs     = tyVarsOfType ty
+    bad_binder b = isTyVar b && b `elemVarSet` free_tvs
+
+coreAltsType :: [CoreAlt] -> Type
+-- ^ Returns the type of the first alternative, which should be the same as for all alternatives
+coreAltsType (alt:_) = coreAltType alt
+coreAltsType []             = panic "corAltsType"
 \end{code}
 
-@mkPiType@ makes a (->) type or a forall type, depending on whether
-it is given a type variable or a term variable.  We cleverly use the
-lbvarinfo field to figure out the right annotation for the arrove in
-case of a term variable.
+Note [Existential variables and silly type synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+       data T = forall a. T (Funny a)
+       type Funny a = Bool
+       f :: T -> Bool
+       f (T x) = x
 
-\begin{code}
-mkPiType  :: Var   -> Type -> Type     -- The more polymorphic version
-mkPiTypes :: [Var] -> Type -> Type     --    doesn't work...
+Now, the type of 'x' is (Funny a), where 'a' is existentially quantified.
+That means that 'exprType' and 'coreAltsType' may give a result that *appears*
+to mention an out-of-scope type variable.  See Trac #3409 for a more real-world
+example.
 
-mkPiTypes vs ty = foldr mkPiType ty vs
+Various possibilities suggest themselves:
+
+ - Ignore the problem, and make Lint not complain about such variables
+
+ - Expand all type synonyms (or at least all those that discard arguments)
+      This is tricky, because at least for top-level things we want to
+      retain the type the user originally specified.
+
+ - Expand synonyms on the fly, when the problem arises. That is what
+   we are doing here.  It's not too expensive, I think.
+
+\begin{code}
+mkPiType  :: Var -> Type -> Type
+-- ^ Makes a @(->)@ type or a forall type, depending
+-- on whether it is given a type variable or a term variable.
+mkPiTypes :: [Var] -> Type -> Type
+-- ^ 'mkPiType' for multiple type or value arguments
 
 mkPiType v ty
    | isId v    = mkFunTy (idType v) ty
    | otherwise = mkForAllTy v ty
+
+mkPiTypes vs ty = foldr mkPiType ty vs
 \end{code}
 
 \begin{code}
 applyTypeToArg :: Type -> CoreExpr -> Type
+-- ^ Determines the type resulting from applying an expression to a function with the given type
 applyTypeToArg fun_ty (Type arg_ty) = applyTy fun_ty arg_ty
-applyTypeToArg fun_ty other_arg     = funResultTy fun_ty
+applyTypeToArg fun_ty _             = funResultTy fun_ty
 
 applyTypeToArgs :: CoreExpr -> Type -> [CoreExpr] -> Type
--- A more efficient version of applyTypeToArg 
--- when we have several args
--- The first argument is just for debugging
-applyTypeToArgs e op_ty [] = op_ty
+-- ^ A more efficient version of 'applyTypeToArg' when we have several arguments.
+-- The first argument is just for debugging, and gives some context
+applyTypeToArgs _ op_ty [] = op_ty
 
 applyTypeToArgs e op_ty (Type ty : args)
   =    -- Accumulate type arguments so we can instantiate all at once
     go [ty] args
   where
     go rev_tys (Type ty : args) = go (ty:rev_tys) args
-    go rev_tys rest_args        = applyTypeToArgs e op_ty' rest_args
-                               where
-                                 op_ty' = applyTys op_ty (reverse rev_tys)
+    go rev_tys rest_args         = applyTypeToArgs e op_ty' rest_args
+                                where
+                                  op_ty' = applyTysD msg op_ty (reverse rev_tys)
+                                  msg = ptext (sLit "applyTypeToArgs") <+> 
+                                        panic_msg e op_ty
 
-applyTypeToArgs e op_ty (other_arg : args)
+applyTypeToArgs e op_ty (_ : args)
   = case (splitFunTy_maybe op_ty) of
        Just (_, res_ty) -> applyTypeToArgs e res_ty args
-       Nothing -> pprPanic "applyTypeToArgs" (pprCoreExpr e $$ ppr op_ty)
-\end{code}
-
+       Nothing -> pprPanic "applyTypeToArgs" (panic_msg e op_ty)
 
+panic_msg :: CoreExpr -> Type -> SDoc
+panic_msg e op_ty = pprCoreExpr e $$ ppr op_ty
+\end{code}
 
 %************************************************************************
 %*                                                                     *
@@ -168,67 +194,33 @@ applyTypeToArgs e op_ty (other_arg : args)
 %*                                                                     *
 %************************************************************************
 
-mkNote removes redundant coercions, and SCCs where possible
-
-\begin{code}
-#ifdef UNUSED
-mkNote :: Note -> CoreExpr -> CoreExpr
-mkNote (SCC cc)        expr               = mkSCC cc expr
-mkNote InlineMe expr              = mkInlineMe expr
-mkNote note     expr              = Note note expr
-#endif
-\end{code}
-
-Drop trivial InlineMe's.  This is somewhat important, because if we have an unfolding
-that looks like        (Note InlineMe (Var v)), the InlineMe doesn't go away because it may
-not be *applied* to anything.
-
-We don't use exprIsTrivial here, though, because we sometimes generate worker/wrapper
-bindings like
-       fw = ...
-       f  = inline_me (coerce t fw)
-As usual, the inline_me prevents the worker from getting inlined back into the wrapper.
-We want the split, so that the coerces can cancel at the call site.  
-
-However, we can get left with tiresome type applications.  Notably, consider
-       f = /\ a -> let t = e in (t, w)
-Then lifting the let out of the big lambda gives
-       t' = /\a -> e
-       f = /\ a -> let t = inline_me (t' a) in (t, w)
-The inline_me is to stop the simplifier inlining t' right back
-into t's RHS.  In the next phase we'll substitute for t (since
-its rhs is trivial) and *then* we could get rid of the inline_me.
-But it hardly seems worth it, so I don't bother.
-
-\begin{code}
-mkInlineMe (Var v) = Var v
-mkInlineMe e      = Note InlineMe e
-\end{code}
-
-
-
 \begin{code}
+-- | Wrap the given expression in the coercion safely, dropping
+-- identity coercions and coalescing nested coercions
 mkCoerce :: Coercion -> CoreExpr -> CoreExpr
+mkCoerce co e | isReflCo co = e
 mkCoerce co (Cast expr co2)
-  = ASSERT(let { (from_ty, to_ty) = coercionKind co; 
-                 (from_ty2, to_ty2) = coercionKind co2} in
-           from_ty `coreEqType` to_ty2 )
-    mkCoerce (mkTransCoercion co2 co) expr
+  = ASSERT(let { Pair  from_ty  _to_ty  = coercionKind co; 
+                 Pair _from_ty2  to_ty2 = coercionKind co2} in
+           from_ty `eqType` to_ty2 )
+    mkCoerce (mkTransCo co2 co) expr
 
 mkCoerce co expr 
-  = let (from_ty, to_ty) = coercionKind co in
---    if to_ty `coreEqType` from_ty
+  = let Pair from_ty _to_ty = coercionKind co in
+--    if to_ty `eqType` from_ty
 --    then expr
 --    else 
-        ASSERT2(from_ty `coreEqType` (exprType expr), text "Trying to coerce" <+> text "(" <> ppr expr $$ text "::" <+> ppr (exprType expr) <> text ")" $$ ppr co $$ ppr (coercionKindPredTy co))
+        WARN(not (from_ty `eqType` exprType expr), text "Trying to coerce" <+> text "(" <> ppr expr $$ text "::" <+> ppr (exprType expr) <> text ")" $$ ppr co $$ pprEqPred (coercionKind co))
          (Cast expr co)
 \end{code}
 
 \begin{code}
+-- | Wraps the given expression in the cost centre unless
+-- in a way that maximises their utility to the user
 mkSCC :: CostCentre -> Expr b -> Expr b
        -- Note: Nested SCC's *are* preserved for the benefit of
        --       cost centre stack profiling
-mkSCC cc (Lit lit)         = Lit lit
+mkSCC _  (Lit lit)          = Lit lit
 mkSCC cc (Lam x e)         = Lam x (mkSCC cc e)  -- Move _scc_ inside lambda
 mkSCC cc (Note (SCC cc') e) = Note (SCC cc) (Note (SCC cc') e)
 mkSCC cc (Note n e)        = Note n (mkSCC cc e) -- Move _scc_ inside notes
@@ -245,20 +237,27 @@ mkSCC cc expr                 = Note (SCC cc) expr
 
 \begin{code}
 bindNonRec :: Id -> CoreExpr -> CoreExpr -> CoreExpr
--- (bindNonRec x r b) produces either
---     let x = r in b
--- or
---     case r of x { _DEFAULT_ -> b }
+-- ^ @bindNonRec x r b@ produces either:
+--
+-- > let x = r in b
+--
+-- or:
+--
+-- > case r of x { _DEFAULT_ -> b }
 --
--- depending on whether x is unlifted or not
+-- depending on whether we have to use a @case@ or @let@
+-- binding for the expression (see 'needsCaseBinding').
 -- It's used by the desugarer to avoid building bindings
--- that give Core Lint a heart attack.  Actually the simplifier
--- deals with them perfectly well.
-
+-- that give Core Lint a heart attack, although actually
+-- the simplifier deals with them perfectly well. See
+-- also 'MkCore.mkCoreLet'
 bindNonRec bndr rhs body 
-  | needsCaseBinding (idType bndr) rhs = Case rhs bndr (exprType body) [(DEFAULT,[],body)]
+  | needsCaseBinding (idType bndr) rhs = Case rhs bndr (exprType body) [(DEFAULT, [], body)]
   | otherwise                         = Let (NonRec bndr rhs) body
 
+-- | Tests whether we have to use a @case@ rather than @let@ binding for this expression
+-- as per the invariants of 'CoreExpr': see "CoreSyn#let_app_invariant"
+needsCaseBinding :: Type -> CoreExpr -> Bool
 needsCaseBinding ty rhs = isUnLiftedType ty && not (exprOkForSpeculation rhs)
        -- Make a case expression instead of a let
        -- These can arise either from the desugarer,
@@ -266,20 +265,18 @@ needsCaseBinding ty rhs = isUnLiftedType ty && not (exprOkForSpeculation rhs)
 \end{code}
 
 \begin{code}
-mkAltExpr :: AltCon -> [CoreBndr] -> [Type] -> CoreExpr
-       -- This guy constructs the value that the scrutinee must have
-       -- when you are in one particular branch of a case
+mkAltExpr :: AltCon     -- ^ Case alternative constructor
+          -> [CoreBndr] -- ^ Things bound by the pattern match
+          -> [Type]     -- ^ The type arguments to the case alternative
+          -> CoreExpr
+-- ^ This guy constructs the value that the scrutinee must have
+-- given that you are in one particular branch of a case
 mkAltExpr (DataAlt con) args inst_tys
   = mkConApp con (map Type inst_tys ++ varsToCoreExprs args)
 mkAltExpr (LitAlt lit) [] []
   = Lit lit
-
-mkIfThenElse :: CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
-mkIfThenElse guard then_expr else_expr
--- Not going to be refining, so okay to take the type of the "then" clause
-  = Case guard (mkWildId boolTy) (exprType then_expr) 
-        [ (DataAlt falseDataCon, [], else_expr),       -- Increasing order of tag!
-          (DataAlt trueDataCon,  [], then_expr) ]
+mkAltExpr (LitAlt _) _ _ = panic "mkAltExpr LitAlt"
+mkAltExpr DEFAULT _ _ = panic "mkAltExpr DEFAULT"
 \end{code}
 
 
@@ -293,33 +290,37 @@ The default alternative must be first, if it exists at all.
 This makes it easy to find, though it makes matching marginally harder.
 
 \begin{code}
+-- | Extract the default case alternative
 findDefault :: [CoreAlt] -> ([CoreAlt], Maybe CoreExpr)
 findDefault ((DEFAULT,args,rhs) : alts) = ASSERT( null args ) (alts, Just rhs)
 findDefault alts                       =                     (alts, Nothing)
 
-findAlt :: AltCon -> [CoreAlt] -> CoreAlt
+isDefaultAlt :: CoreAlt -> Bool
+isDefaultAlt (DEFAULT, _, _) = True
+isDefaultAlt _               = False
+
+
+-- | Find the case alternative corresponding to a particular 
+-- constructor: panics if no such constructor exists
+findAlt :: AltCon -> [CoreAlt] -> Maybe CoreAlt
+    -- A "Nothing" result *is* legitmiate
+    -- See Note [Unreachable code]
 findAlt con alts
   = case alts of
-       (deflt@(DEFAULT,_,_):alts) -> go alts deflt
-       other                      -> go alts panic_deflt
+       (deflt@(DEFAULT,_,_):alts) -> go alts (Just deflt)
+        _                          -> go alts Nothing
   where
-    panic_deflt = pprPanic "Missing alternative" (ppr con $$ vcat (map ppr alts))
-
-    go []                     deflt = deflt
+    go []                    deflt = deflt
     go (alt@(con1,_,_) : alts) deflt
       =        case con `cmpAltCon` con1 of
          LT -> deflt   -- Missed it already; the alts are in increasing order
-         EQ -> alt
+         EQ -> Just alt
          GT -> ASSERT( not (con1 == DEFAULT) ) go alts deflt
 
-isDefaultAlt :: CoreAlt -> Bool
-isDefaultAlt (DEFAULT, _, _) = True
-isDefaultAlt other          = False
-
 ---------------------------------
 mergeAlts :: [CoreAlt] -> [CoreAlt] -> [CoreAlt]
--- Merge preserving order; alternatives in the first arg
--- shadow ones in the second
+-- ^ Merge alternatives preserving order; alternatives in
+-- the first argument shadow ones in the second
 mergeAlts [] as2 = as2
 mergeAlts as1 [] = as1
 mergeAlts (a1:as1) (a2:as2)
@@ -327,52 +328,129 @@ mergeAlts (a1:as1) (a2:as2)
        LT -> a1 : mergeAlts as1      (a2:as2)
        EQ -> a1 : mergeAlts as1      as2       -- Discard a2
        GT -> a2 : mergeAlts (a1:as1) as2
+
+
+---------------------------------
+trimConArgs :: AltCon -> [CoreArg] -> [CoreArg]
+-- ^ Given:
+--
+-- > case (C a b x y) of
+-- >        C b x y -> ...
+--
+-- We want to drop the leading type argument of the scrutinee
+-- leaving the arguments to match agains the pattern
+
+trimConArgs DEFAULT      args = ASSERT( null args ) []
+trimConArgs (LitAlt _)   args = ASSERT( null args ) []
+trimConArgs (DataAlt dc) args = dropList (dataConUnivTyVars dc) args
 \end{code}
 
+Note [Unreachable code]
+~~~~~~~~~~~~~~~~~~~~~~~
+It is possible (although unusual) for GHC to find a case expression
+that cannot match.  For example: 
+
+     data Col = Red | Green | Blue
+     x = Red
+     f v = case x of 
+              Red -> ...
+             _ -> ...(case x of { Green -> e1; Blue -> e2 })...
+
+Suppose that for some silly reason, x isn't substituted in the case
+expression.  (Perhaps there's a NOINLINE on it, or profiling SCC stuff
+gets in the way; cf Trac #3118.)  Then the full-lazines pass might produce
+this
+
+     x = Red
+     lvl = case x of { Green -> e1; Blue -> e2 })
+     f v = case x of 
+             Red -> ...
+            _ -> ...lvl...
+
+Now if x gets inlined, we won't be able to find a matching alternative
+for 'Red'.  That's because 'lvl' is unreachable.  So rather than crashing
+we generate (error "Inaccessible alternative").
+
+Similar things can happen (augmented by GADTs) when the Simplifier
+filters down the matching alternatives in Simplify.rebuildCase.
+
 
 %************************************************************************
 %*                                                                     *
-\subsection{Figuring out things about expressions}
+             exprIsTrivial
 %*                                                                     *
 %************************************************************************
 
+Note [exprIsTrivial]
+~~~~~~~~~~~~~~~~~~~~
 @exprIsTrivial@ is true of expressions we are unconditionally happy to
                duplicate; simple variables and constants, and type
                applications.  Note that primop Ids aren't considered
                trivial unless 
 
-@exprIsBottom@ is true of expressions that are guaranteed to diverge
-
-
+Note [Variable are trivial]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
 There used to be a gruesome test for (hasNoBinding v) in the
 Var case:
        exprIsTrivial (Var v) | hasNoBinding v = idArity v == 0
-The idea here is that a constructor worker, like $wJust, is
-really short for (\x -> $wJust x), becuase $wJust has no binding.
+The idea here is that a constructor worker, like \$wJust, is
+really short for (\x -> \$wJust x), becuase \$wJust has no binding.
 So it should be treated like a lambda.  Ditto unsaturated primops.
 But now constructor workers are not "have-no-binding" Ids.  And
 completely un-applied primops and foreign-call Ids are sufficiently
 rare that I plan to allow them to be duplicated and put up with
 saturating them.
 
-SCC notes.  We do not treat (_scc_ "foo" x) as trivial, because 
-  a) it really generates code, (and a heap object when it's 
-     a function arg) to capture the cost centre
-  b) see the note [SCC-and-exprIsTrivial] in Simplify.simplLazyBind
+Note [SCCs are trivial]
+~~~~~~~~~~~~~~~~~~~~~~~
+We used not to treat (_scc_ "foo" x) as trivial, because it really
+generates code, (and a heap object when it's a function arg) to
+capture the cost centre.  However, the profiling system discounts the
+allocation costs for such "boxing thunks" whereas the extra costs of
+*not* inlining otherwise-trivial bindings can be high, and are hard to
+discount.
 
 \begin{code}
-exprIsTrivial (Var v)     = True       -- See notes above
-exprIsTrivial (Type _)    = True
-exprIsTrivial (Lit lit)    = litIsTrivial lit
-exprIsTrivial (App e arg)  = not (isRuntimeArg arg) && exprIsTrivial e
-exprIsTrivial (Note (SCC _) e) = False         -- See notes above
-exprIsTrivial (Note _       e) = exprIsTrivial e
-exprIsTrivial (Cast e co)  = exprIsTrivial e
-exprIsTrivial (Lam b body) = not (isRuntimeVar b) && exprIsTrivial body
-exprIsTrivial other       = False
+exprIsTrivial :: CoreExpr -> Bool
+exprIsTrivial (Var _)          = True        -- See Note [Variables are trivial]
+exprIsTrivial (Type _)        = True
+exprIsTrivial (Coercion _)     = True
+exprIsTrivial (Lit lit)        = litIsTrivial lit
+exprIsTrivial (App e arg)      = not (isRuntimeArg arg) && exprIsTrivial e
+exprIsTrivial (Note _       e) = exprIsTrivial e  -- See Note [SCCs are trivial]
+exprIsTrivial (Cast e _)       = exprIsTrivial e
+exprIsTrivial (Lam b body)     = not (isRuntimeVar b) && exprIsTrivial body
+exprIsTrivial _                = False
 \end{code}
 
+exprIsBottom is a very cheap and cheerful function; it may return
+False for bottoming expressions, but it never costs much to ask.
+See also CoreArity.exprBotStrictness_maybe, but that's a bit more 
+expensive.
 
+\begin{code}
+exprIsBottom :: CoreExpr -> Bool
+exprIsBottom e 
+  = go 0 e
+  where
+    go n (Var v) = isBottomingId v &&  n >= idArity v 
+    go n (App e a) | isTypeArg a = go n e 
+                   | otherwise   = go (n+1) e 
+    go n (Note _ e)             = go n e     
+    go n (Cast e _)             = go n e
+    go n (Let _ e)              = go n e
+    go _ _                      = False
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+             exprIsDupable
+%*                                                                     *
+%************************************************************************
+
+Note [exprIsDupable]
+~~~~~~~~~~~~~~~~~~~~
 @exprIsDupable@        is true of expressions that can be duplicated at a modest
                cost in code size.  This will only happen in different case
                branches, so there's no issue about duplicating work.
@@ -385,25 +463,39 @@ exprIsTrivial other          = False
 
 
 \begin{code}
-exprIsDupable (Type _)         = True
-exprIsDupable (Var v)          = True
-exprIsDupable (Lit lit)        = litIsDupable lit
-exprIsDupable (Note InlineMe e) = True
-exprIsDupable (Note _ e)        = exprIsDupable e
-exprIsDupable (Cast e co)       = exprIsDupable e
-exprIsDupable expr          
-  = go expr 0
+exprIsDupable :: CoreExpr -> Bool
+exprIsDupable e
+  = isJust (go dupAppSize e)
   where
-    go (Var v)   n_args = True
-    go (App f a) n_args =  n_args < dupAppSize
-                       && exprIsDupable a
-                       && go f (n_args+1)
-    go other n_args    = False
+    go :: Int -> CoreExpr -> Maybe Int
+    go n (Type {})     = Just n
+    go n (Coercion {}) = Just n
+    go n (Var {})      = decrement n
+    go n (Note _ e)    = go n e
+    go n (Cast e _)    = go n e
+    go n (App f a) | Just n' <- go n a = go n' f
+    go n (Lit lit) | litIsDupable lit = decrement n
+    go _ _ = Nothing
+
+    decrement :: Int -> Maybe Int
+    decrement 0 = Nothing
+    decrement n = Just (n-1)
 
 dupAppSize :: Int
-dupAppSize = 4         -- Size of application we are prepared to duplicate
+dupAppSize = 8  -- Size of term we are prepared to duplicate
+                -- This is *just* big enough to make test MethSharing
+                -- inline enough join points.  Really it should be
+                -- smaller, and could be if we fixed Trac #4960.
 \end{code}
 
+%************************************************************************
+%*                                                                     *
+             exprIsCheap, exprIsExpandable
+%*                                                                     *
+%************************************************************************
+
+Note [exprIsCheap]   See also Note [Interaction of exprIsCheap and lone variables]
+~~~~~~~~~~~~~~~~~~   in CoreUnfold.lhs
 @exprIsCheap@ looks at a Core expression and returns \tr{True} if
 it is obviously in weak head normal form, or is cheap to get to WHNF.
 [Note that that's not the same as exprIsDupable; an expression might be
@@ -432,116 +524,190 @@ shared.  The main examples of things which aren't WHNF but are
 Notice that a variable is considered 'cheap': we can push it inside a lambda,
 because sharing will make sure it is only evaluated once.
 
+Note [exprIsCheap and exprIsHNF]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note that exprIsHNF does not imply exprIsCheap.  Eg
+       let x = fac 20 in Just x
+This responds True to exprIsHNF (you can discard a seq), but
+False to exprIsCheap.
+
 \begin{code}
 exprIsCheap :: CoreExpr -> Bool
-exprIsCheap (Lit lit)        = True
-exprIsCheap (Type _)          = True
-exprIsCheap (Var _)           = True
-exprIsCheap (Note InlineMe e) = True
-exprIsCheap (Note _ e)        = exprIsCheap e
-exprIsCheap (Cast e co)       = exprIsCheap e
-exprIsCheap (Lam x e)         = isRuntimeVar x || exprIsCheap e
-exprIsCheap (Case e _ _ alts) = exprIsCheap e && 
-                               and [exprIsCheap rhs | (_,_,rhs) <- alts]
+exprIsCheap = exprIsCheap' isCheapApp
+
+exprIsExpandable :: CoreExpr -> Bool
+exprIsExpandable = exprIsCheap' isExpandableApp        -- See Note [CONLIKE pragma] in BasicTypes
+
+type CheapAppFun = Id -> Int -> Bool
+exprIsCheap' :: CheapAppFun -> CoreExpr -> Bool
+exprIsCheap' _        (Lit _)      = True
+exprIsCheap' _        (Type _)    = True
+exprIsCheap' _        (Coercion _) = True
+exprIsCheap' _        (Var _)      = True
+exprIsCheap' good_app (Note _ e)   = exprIsCheap' good_app e
+exprIsCheap' good_app (Cast e _)   = exprIsCheap' good_app e
+exprIsCheap' good_app (Lam x e)    = isRuntimeVar x
+                                  || exprIsCheap' good_app e
+
+exprIsCheap' good_app (Case e _ _ alts) = exprIsCheap' good_app e && 
+                                         and [exprIsCheap' good_app rhs | (_,_,rhs) <- alts]
        -- Experimentally, treat (case x of ...) as cheap
        -- (and case __coerce x etc.)
        -- This improves arities of overloaded functions where
        -- there is only dictionary selection (no construction) involved
-exprIsCheap (Let (NonRec x _) e)  
-      | isUnLiftedType (idType x) = exprIsCheap e
-      | otherwise                = False
-       -- strict lets always have cheap right hand sides,
-       -- and do no allocation.
 
-exprIsCheap other_expr         -- Applications and variables
+exprIsCheap' good_app (Let (NonRec x _) e)  
+  | isUnLiftedType (idType x) = exprIsCheap' good_app e
+  | otherwise                = False
+       -- Strict lets always have cheap right hand sides,
+       -- and do no allocation, so just look at the body
+       -- Non-strict lets do allocation so we don't treat them as cheap
+       -- See also 
+
+exprIsCheap' good_app other_expr       -- Applications and variables
   = go other_expr []
   where
        -- Accumulate value arguments, then decide
+    go (Cast e _) val_args                 = go e val_args
     go (App f a) val_args | isRuntimeArg a = go f (a:val_args)
                          | otherwise      = go f val_args
 
-    go (Var f) [] = True       -- Just a type application of a variable
+    go (Var _) [] = True       -- Just a type application of a variable
                                -- (f t1 t2 t3) counts as WHNF
     go (Var f) args
-       = case globalIdDetails f of
-               RecordSelId {} -> go_sel args
-               ClassOpId _    -> go_sel args
-               PrimOpId op    -> go_primop op args
-
-               DataConWorkId _ -> go_pap args
-               other | length args < idArity f -> go_pap args
-
-               other -> isBottomingId f
+        = case idDetails f of
+               RecSelId {}                  -> go_sel args
+               ClassOpId {}                 -> go_sel args
+               PrimOpId op                  -> go_primop op args
+               _ | good_app f (length args) -> go_pap args
+                  | isBottomingId f         -> True
+                  | otherwise               -> False
                        -- Application of a function which
                        -- always gives bottom; we treat this as cheap
                        -- because it certainly doesn't need to be shared!
        
-    go other args = False
+    go _ _ = False
  
     --------------
-    go_pap args = all exprIsTrivial args
-       -- For constructor applications and primops, check that all
-       -- the args are trivial.  We don't want to treat as cheap, say,
-       --      (1:2:3:4:5:[])
-       -- We'll put up with one constructor application, but not dozens
-       
+    go_pap args = all (exprIsCheap' good_app) args
+        -- Used to be "all exprIsTrivial args" due to concerns about
+        -- duplicating nested constructor applications, but see #4978.
+
     --------------
-    go_primop op args = primOpIsCheap op && all exprIsCheap args
+    go_primop op args = primOpIsCheap op && all (exprIsCheap' good_app) args
        -- In principle we should worry about primops
        -- that return a type variable, since the result
        -- might be applied to something, but I'm not going
        -- to bother to check the number of args
  
     --------------
-    go_sel [arg] = exprIsCheap arg     -- I'm experimenting with making record selection
-    go_sel other = False               -- look cheap, so we will substitute it inside a
+    go_sel [arg] = exprIsCheap' good_app arg   -- I'm experimenting with making record selection
+    go_sel _     = False               -- look cheap, so we will substitute it inside a
                                        -- lambda.  Particularly for dictionary field selection.
                -- BUT: Take care with (sel d x)!  The (sel d) might be cheap, but
                --      there's no guarantee that (sel d x) will be too.  Hence (n_val_args == 1)
-\end{code}
-
-exprOkForSpeculation returns True of an expression that it is
-
-       * safe to evaluate even if normal order eval might not 
-         evaluate the expression at all, or
 
-       * safe *not* to evaluate even if normal order would do so
+isCheapApp :: CheapAppFun
+isCheapApp fn n_val_args
+  = isDataConWorkId fn 
+  || n_val_args < idArity fn
 
-It returns True iff
-
-       the expression guarantees to terminate, 
-       soon, 
-       without raising an exception,
-       without causing a side effect (e.g. writing a mutable variable)
+isExpandableApp :: CheapAppFun
+isExpandableApp fn n_val_args
+  =  isConLikeId fn
+  || n_val_args < idArity fn
+  || go n_val_args (idType fn)
+  where
+  -- See if all the arguments are PredTys (implicit params or classes)
+  -- If so we'll regard it as expandable; see Note [Expandable overloadings]
+     go 0 _ = True
+     go n_val_args ty 
+       | Just (_, ty) <- splitForAllTy_maybe ty   = go n_val_args ty
+       | Just (arg, ty) <- splitFunTy_maybe ty
+       , isPredTy arg                             = go (n_val_args-1) ty
+       | otherwise                                = False
+\end{code}
 
-NB: if exprIsHNF e, then exprOkForSpecuation e
+Note [Expandable overloadings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose the user wrote this
+   {-# RULE  forall x. foo (negate x) = h x #-}
+   f x = ....(foo (negate x))....
+He'd expect the rule to fire. But since negate is overloaded, we might
+get this:
+    f = \d -> let n = negate d in \x -> ...foo (n x)...
+So we treat the application of a function (negate in this case) to a
+*dictionary* as expandable.  In effect, every function is CONLIKE when
+it's applied only to dictionaries.
 
-E.G.
-       let x = case y# +# 1# of { r# -> I# r# }
-       in E
-==>
-       case y# +# 1# of { r# -> 
-       let x = I# r#
-       in E 
-       }
 
-We can only do this if the (y+1) is ok for speculation: it has no
-side effects, and can't diverge or raise an exception.
+%************************************************************************
+%*                                                                     *
+             exprOkForSpeculation
+%*                                                                     *
+%************************************************************************
 
 \begin{code}
+-- | 'exprOkForSpeculation' returns True of an expression that is:
+--
+--  * Safe to evaluate even if normal order eval might not 
+--    evaluate the expression at all, or
+--
+--  * Safe /not/ to evaluate even if normal order would do so
+--
+-- It is usually called on arguments of unlifted type, but not always
+-- In particular, Simplify.rebuildCase calls it on lifted types
+-- when a 'case' is a plain 'seq'. See the example in 
+-- Note [exprOkForSpeculation: case expressions] below
+--
+-- Precisely, it returns @True@ iff:
+--
+--  * The expression guarantees to terminate, 
+--  * soon, 
+--  * without raising an exception,
+--  * without causing a side effect (e.g. writing a mutable variable)
+--
+-- Note that if @exprIsHNF e@, then @exprOkForSpecuation e@.
+-- As an example of the considerations in this test, consider:
+--
+-- > let x = case y# +# 1# of { r# -> I# r# }
+-- > in E
+--
+-- being translated to:
+--
+-- > case y# +# 1# of { r# -> 
+-- >    let x = I# r#
+-- >    in E 
+-- > }
+-- 
+-- We can only do this if the @y + 1@ is ok for speculation: it has no
+-- side effects, and can't diverge or raise an exception.
 exprOkForSpeculation :: CoreExpr -> Bool
-exprOkForSpeculation (Lit _)     = True
-exprOkForSpeculation (Type _)    = True
-exprOkForSpeculation (Var v)     = isUnLiftedType (idType v)
+exprOkForSpeculation (Lit _)      = True
+exprOkForSpeculation (Type _)     = True
+exprOkForSpeculation (Coercion _) = True
+
+exprOkForSpeculation (Var v)     
+  | isTickBoxOp v = False     -- Tick boxes are *not* suitable for speculation
+  | otherwise     =  isUnLiftedType (idType v) -- c.f. the Var case of exprIsHNF
+                 || isDataConWorkId v          -- Nullary constructors
+                 || idArity v > 0              -- Functions
+                 || isEvaldUnfolding (idUnfolding v)   -- Let-bound values
+
 exprOkForSpeculation (Note _ e)  = exprOkForSpeculation e
-exprOkForSpeculation (Cast e co) = exprOkForSpeculation e
+exprOkForSpeculation (Cast e _)  = exprOkForSpeculation e
+
+exprOkForSpeculation (Case e _ _ alts) 
+  =  exprOkForSpeculation e  -- Note [exprOkForSpeculation: case expressions]
+  && all (\(_,_,rhs) -> exprOkForSpeculation rhs) alts
+
 exprOkForSpeculation other_expr
   = case collectArgs other_expr of
-       (Var f, args) -> spec_ok (globalIdDetails f) args
-       other         -> False
+       (Var f, args) -> spec_ok (idDetails f) args
+        _             -> False
  
   where
-    spec_ok (DataConWorkId _) args
+    spec_ok (DataConWorkId _) _
       = True   -- The strictness of the constructor has already
                -- been expressed by its "wrapper", so we don't need
                -- to take the arguments into account
@@ -553,17 +719,23 @@ exprOkForSpeculation other_expr
                -- Often there is a literal divisor, and this 
                -- can get rid of a thunk in an inner looop
 
+      | DataToTagOp <- op      -- See Note [dataToTag speculation]
+      = True
+
       | otherwise
       = primOpOkForSpeculation op && 
        all exprOkForSpeculation args
                                -- A bit conservative: we don't really need
                                -- to care about lazy arguments, but this is easy
 
-    spec_ok other args = False
+    spec_ok (DFunId _ new_type) _ = not new_type
+         -- DFuns terminate, unless the dict is implemented with a newtype
+        -- in which case they may not
+
+    spec_ok _ _ = False
 
+-- | True of dyadic operators that can fail only if the second arg is zero!
 isDivOp :: PrimOp -> Bool
--- True of dyadic operators that can fail 
--- only if the second arg is zero
 -- This function probably belongs in PrimOp, or even in 
 -- an automagically generated file.. but it's such a 
 -- special case I thought I'd leave it here for now.
@@ -571,128 +743,181 @@ isDivOp IntQuotOp        = True
 isDivOp IntRemOp        = True
 isDivOp WordQuotOp      = True
 isDivOp WordRemOp       = True
-isDivOp IntegerQuotRemOp = True
-isDivOp IntegerDivModOp  = True
 isDivOp FloatDivOp       = True
 isDivOp DoubleDivOp      = True
-isDivOp other           = False
-\end{code}
-
-
-\begin{code}
-exprIsBottom :: CoreExpr -> Bool       -- True => definitely bottom
-exprIsBottom e = go 0 e
-              where
-               -- n is the number of args
-                go n (Note _ e)     = go n e
-                 go n (Cast e co)    = go n e
-                go n (Let _ e)      = go n e
-                go n (Case e _ _ _) = go 0 e   -- Just check the scrut
-                go n (App e _)      = go (n+1) e
-                go n (Var v)        = idAppIsBottom v n
-                go n (Lit _)        = False
-                go n (Lam _ _)      = False
-                go n (Type _)       = False
-
-idAppIsBottom :: Id -> Int -> Bool
-idAppIsBottom id n_val_args = appIsBottom (idNewStrictness id) n_val_args
+isDivOp _                = False
 \end{code}
 
-@exprIsHNF@ returns true for expressions that are certainly *already* 
-evaluated to *head* normal form.  This is used to decide whether it's ok 
-to change
-
-       case x of _ -> e   ===>   e
-
-and to decide whether it's safe to discard a `seq`
-
-So, it does *not* treat variables as evaluated, unless they say they are.
+Note [exprOkForSpeculation: case expressions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+It's always sound for exprOkForSpeculation to return False, and we
+don't want it to take too long, so it bales out on complicated-looking
+terms.  Notably lets, which can be stacked very deeply; and in any 
+case the argument of exprOkForSpeculation is usually in a strict context,
+so any lets will have been floated away.
+
+However, we keep going on case-expressions.  An example like this one
+showed up in DPH code (Trac #3717):
+    foo :: Int -> Int
+    foo 0 = 0
+    foo n = (if n < 5 then 1 else 2) `seq` foo (n-1)
+
+If exprOkForSpeculation doesn't look through case expressions, you get this:
+    T.$wfoo =
+      \ (ww :: GHC.Prim.Int#) ->
+        case ww of ds {
+          __DEFAULT -> case (case <# ds 5 of _ {
+                          GHC.Types.False -> lvl1;
+                          GHC.Types.True -> lvl})
+                       of _ { __DEFAULT ->
+                       T.$wfoo (GHC.Prim.-# ds_XkE 1) };
+          0 -> 0
+        }
+
+The inner case is redundant, and should be nuked.
+
+Note [dataToTag speculation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Is this OK?
+   f x = let v::Int# = dataToTag# x
+         in ...
+We say "yes", even though 'x' may not be evaluated.  Reasons
+
+  * dataToTag#'s strictness means that its argument often will be
+    evaluated, but FloatOut makes that temporarily untrue
+         case x of y -> let v = dataToTag# y in ...
+    -->
+         case x of y -> let v = dataToTag# x in ...
+    Note that we look at 'x' instead of 'y' (this is to improve
+    floating in FloatOut).  So Lint complains.    
+    Moreover, it really *might* improve floating to let the
+    v-binding float out
+         
+  * CorePrep makes sure dataToTag#'s argument is evaluated, just
+    before code gen.  Until then, it's not guaranteed
 
-But it *does* treat partial applications and constructor applications
-as values, even if their arguments are non-trivial, provided the argument
-type is lifted; 
-       e.g.  (:) (f x) (map f xs)      is a value
-             map (...redex...)         is a value
-Because `seq` on such things completes immediately
 
-For unlifted argument types, we have to be careful:
-               C (f x :: Int#)
-Suppose (f x) diverges; then C (f x) is not a value.  True, but
-this form is illegal (see the invariants in CoreSyn).  Args of unboxed
-type must be ok-for-speculation (or trivial).
+%************************************************************************
+%*                                                                     *
+             exprIsHNF, exprIsConLike
+%*                                                                     *
+%************************************************************************
 
 \begin{code}
+-- Note [exprIsHNF]            See also Note [exprIsCheap and exprIsHNF]
+-- ~~~~~~~~~~~~~~~~
+-- | exprIsHNF returns true for expressions that are certainly /already/ 
+-- evaluated to /head/ normal form.  This is used to decide whether it's ok 
+-- to change:
+--
+-- > case x of _ -> e
+--
+--    into:
+--
+-- > e
+--
+-- and to decide whether it's safe to discard a 'seq'.
+-- 
+-- So, it does /not/ treat variables as evaluated, unless they say they are.
+-- However, it /does/ treat partial applications and constructor applications
+-- as values, even if their arguments are non-trivial, provided the argument
+-- type is lifted. For example, both of these are values:
+--
+-- > (:) (f x) (map f xs)
+-- > map (...redex...)
+--
+-- because 'seq' on such things completes immediately.
+--
+-- For unlifted argument types, we have to be careful:
+--
+-- > C (f x :: Int#)
+--
+-- Suppose @f x@ diverges; then @C (f x)@ is not a value. However this can't 
+-- happen: see "CoreSyn#let_app_invariant". This invariant states that arguments of
+-- unboxed type must be ok-for-speculation (or trivial).
 exprIsHNF :: CoreExpr -> Bool          -- True => Value-lambda, constructor, PAP
-exprIsHNF (Var v)      -- NB: There are no value args at this point
-  =  isDataConWorkId v         -- Catches nullary constructors, 
+exprIsHNF = exprIsHNFlike isDataConWorkId isEvaldUnfolding
+\end{code}
+
+\begin{code}
+-- | Similar to 'exprIsHNF' but includes CONLIKE functions as well as
+-- data constructors. Conlike arguments are considered interesting by the
+-- inliner.
+exprIsConLike :: CoreExpr -> Bool      -- True => lambda, conlike, PAP
+exprIsConLike = exprIsHNFlike isConLikeId isConLikeUnfolding
+
+-- | Returns true for values or value-like expressions. These are lambdas,
+-- constructors / CONLIKE functions (as determined by the function argument)
+-- or PAPs.
+--
+exprIsHNFlike :: (Var -> Bool) -> (Unfolding -> Bool) -> CoreExpr -> Bool
+exprIsHNFlike is_con is_con_unf = is_hnf_like
+  where
+    is_hnf_like (Var v) -- NB: There are no value args at this point
+      =  is_con v      -- Catches nullary constructors, 
                        --      so that [] and () are values, for example
-  || idArity v > 0     -- Catches (e.g.) primops that don't have unfoldings
-  || isEvaldUnfolding (idUnfolding v)
+      || idArity v > 0         -- Catches (e.g.) primops that don't have unfoldings
+      || is_con_unf (idUnfolding v)
        -- Check the thing's unfolding; it might be bound to a value
-       -- A worry: what if an Id's unfolding is just itself: 
-       -- then we could get an infinite loop...
-
-exprIsHNF (Lit l)           = True
-exprIsHNF (Type ty)         = True     -- Types are honorary Values; 
-                                       -- we don't mind copying them
-exprIsHNF (Lam b e)         = isRuntimeVar b || exprIsHNF e
-exprIsHNF (Note _ e)        = exprIsHNF e
-exprIsHNF (Cast e co)        = exprIsHNF e
-exprIsHNF (App e (Type _)) = exprIsHNF e
-exprIsHNF (App e a)        = app_is_value e [a]
-exprIsHNF other             = False
-
--- There is at least one value argument
-app_is_value (Var fun) args
-  |  isDataConWorkId fun               -- Constructor apps are values
-  || idArity fun > valArgCount args    -- Under-applied function
-  = check_args (idType fun) args
-app_is_value (App f a) as = app_is_value f (a:as)
-app_is_value other     as = False
-
-       -- 'check_args' checks that unlifted-type args
-       -- are in fact guaranteed non-divergent
-check_args fun_ty []             = True
-check_args fun_ty (Type _ : args) = case splitForAllTy_maybe fun_ty of
-                                     Just (_, ty) -> check_args ty args
-check_args fun_ty (arg : args)
-  | isUnLiftedType arg_ty = exprOkForSpeculation arg
-  | otherwise            = check_args res_ty args
-  where
-    (arg_ty, res_ty) = splitFunTy fun_ty
+       -- We don't look through loop breakers here, which is a bit conservative
+       -- but otherwise I worry that if an Id's unfolding is just itself, 
+       -- we could get an infinite loop
+
+    is_hnf_like (Lit _)          = True
+    is_hnf_like (Type _)        = True       -- Types are honorary Values;
+                                              -- we don't mind copying them
+    is_hnf_like (Coercion _)     = True       -- Same for coercions
+    is_hnf_like (Lam b e)        = isRuntimeVar b || is_hnf_like e
+    is_hnf_like (Note _ e)       = is_hnf_like e
+    is_hnf_like (Cast e _)       = is_hnf_like e
+    is_hnf_like (App e (Type _))    = is_hnf_like e
+    is_hnf_like (App e (Coercion _)) = is_hnf_like e
+    is_hnf_like (App e a)        = app_is_value e [a]
+    is_hnf_like (Let _ e)        = is_hnf_like e  -- Lazy let(rec)s don't affect us
+    is_hnf_like _                = False
+
+    -- There is at least one value argument
+    app_is_value :: CoreExpr -> [CoreArg] -> Bool
+    app_is_value (Var fun) args
+      = idArity fun > valArgCount args   -- Under-applied function
+        || is_con fun                    --  or constructor-like
+    app_is_value (Note _ f) as = app_is_value f as
+    app_is_value (Cast f _) as = app_is_value f as
+    app_is_value (App f a)  as = app_is_value f (a:as)
+    app_is_value _          _  = False
 \end{code}
 
+
+%************************************************************************
+%*                                                                     *
+             Instantiating data constructors
+%*                                                                     *
+%************************************************************************
+
+These InstPat functions go here to avoid circularity between DataCon and Id
+
 \begin{code}
--- deep applies a TyConApp coercion as a substitution to a reflexive coercion
--- deepCast t [a1,...,an] co corresponds to deep(t, [a1,...,an], co) from
--- FC paper
-deepCast :: Type -> [TyVar] -> Coercion -> Coercion
-deepCast ty tyVars co 
-  = ASSERT( let {(lty, rty) = coercionKind co;
-                 Just (tc1, lArgs) = splitTyConApp_maybe lty;
-                Just (tc2, rArgs) = splitTyConApp_maybe rty} 
-            in
-              tc1 == tc2 && length lArgs == length rArgs &&
-              length lArgs == length tyVars )
-    substTyWith tyVars coArgs ty
-  where
-    -- coArgs = [right (left (left co)), right (left co), right co]
-    coArgs = decomposeCo (length tyVars) co
+dataConRepInstPat   ::                 [Unique] -> DataCon -> [Type] -> ([TyVar], [Id])
+dataConRepFSInstPat :: [FastString] -> [Unique] -> DataCon -> [Type] -> ([TyVar], [Id])
 
--- This goes here to avoid circularity between DataCon and Id
-dataConInstPat :: [Unique]                  -- A long enough list of uniques, at least one for each binder
+dataConRepInstPat   = dataConInstPat (repeat ((fsLit "ipv")))
+dataConRepFSInstPat = dataConInstPat 
+
+dataConInstPat :: [FastString]          -- A long enough list of FSs to use for names
+               -> [Unique]              -- An equally long list of uniques, at least one for each binder
                -> DataCon
-              -> [Type]                    -- Types to instantiate the universally quantified tyvars
-              -> ([TyVar], [CoVar], [Id])  -- Return instantiated variables
--- dataConInstPat us con inst_tys returns a triple (ex_tvs, co_tvs, arg_ids),
+              -> [Type]                -- Types to instantiate the universally quantified tyvars
+              -> ([TyVar], [Id])          -- Return instantiated variables
+-- dataConInstPat arg_fun fss us con inst_tys returns a triple 
+-- (ex_tvs, arg_ids),
 --
 --   ex_tvs are intended to be used as binders for existential type args
 --
---   co_tvs are intended to be used as binders for coercion args and the kinds
---     of these vars have been instantiated by the inst_tys and the ex_tys
---
---   arg_ids are indended to be used as binders for value arguments, including
---     dicts, and have their types instantiated with inst_tys and ex_tys
+--   arg_ids are indended to be used as binders for value arguments, 
+--     and their types have been instantiated with inst_tys and ex_tys
+--     The arg_ids include both evidence and
+--     programmer-specified arguments (both after rep-ing)
 --
 -- Example.
 --  The following constructor T1
@@ -702,615 +927,164 @@ dataConInstPat :: [Unique]                  -- A long enough list of uniques, at
 --    ...
 --
 --  has representation type 
---   forall a. forall a1. forall a2. forall b. (a :=: (a1,a2)) => 
+--   forall a. forall a1. forall b. (a ~ (a1,b)) => 
 --     Int -> b -> T a
 --
---  dataConInstPat us T1 (a1',a2') will return
+--  dataConInstPat fss us T1 (a1',b') will return
 --
---  ([a1'', a2'', b''],[c :: (a1',a2'):=:(a1'',a2'')],[x :: Int,y :: b''])
+--  ([a1'', b''], [c :: (a1', b')~(a1'', b''), x :: Int, y :: b''])
 --
---  where the double-primed variables are created from the unique list input
-dataConInstPat uniqs con inst_tys 
-  = dataConOccInstPat uniqs occs con inst_tys
-  where
-     -- dataConOccInstPat doesn't actually make use of the OccName directly for
-     -- existential and coercion variable binders, so it is right to just
-     -- use the VarName namespace for all of the OccNames
-    occs      = mk_occs 1
-    mk_occs n = mkVarOcc ("ipv" ++ show n) : mk_occs (n+1)
-
-dataConOccInstPat :: [Unique]                  -- A long enough list of uniques, at least one for each binder
-                  -> [OccName]                 -- An equally long list of OccNames to use
-                  -> DataCon
-                 -> [Type]                    -- Types to instantiate the universally quantified tyvars
-              -> ([TyVar], [CoVar], [Id])  -- Return instantiated variables
--- This function actually does the job specified in the comment for 
--- dataConInstPat, but uses the specified list of OccNames.  This is 
--- is necessary for use in e.g. tcIfaceDataAlt
-dataConOccInstPat uniqs occs con inst_tys 
-  = (ex_bndrs, co_bndrs, id_bndrs)
+--  where the double-primed variables are created with the FastStrings and
+--  Uniques given as fss and us
+dataConInstPat fss uniqs con inst_tys 
+  = (ex_bndrs, arg_ids)
   where 
     univ_tvs = dataConUnivTyVars con
     ex_tvs   = dataConExTyVars con
     arg_tys  = dataConRepArgTys con
-    eq_spec  = dataConEqSpec con
-    eq_preds = [ mkEqPred (mkTyVarTy tv, ty) | (tv,ty) <- eq_spec ]
 
     n_ex = length ex_tvs
-    n_co = length eq_spec
-    n_id = length arg_tys
-
-      -- split the Uniques and OccNames
-    (ex_uniqs, uniqs')   = splitAt n_ex uniqs
-    (co_uniqs, id_uniqs) = splitAt n_co uniqs'
 
-    (ex_occs, occs')     = splitAt n_ex occs
-    (co_occs, id_occs)   = splitAt n_co occs'
+      -- split the Uniques and FastStrings
+    (ex_uniqs, id_uniqs) = splitAt n_ex uniqs
+    (ex_fss,   id_fss)   = splitAt n_ex fss
 
-      -- make existential type variables
-    mk_ex_var uniq occ var = mkTyVar new_name kind
+      -- Make existential type variables
+    ex_bndrs = zipWith3 mk_ex_var ex_uniqs ex_fss ex_tvs
+    mk_ex_var uniq fs var = mkTyVar new_name kind
       where
-        new_name = mkSysTvName uniq (occNameFS occ)
+        new_name = mkSysTvName uniq fs
         kind     = tyVarKind var
 
-    ex_bndrs = zipWith3 mk_ex_var ex_uniqs ex_occs ex_tvs
-
-      -- make the instantiation substitution
-    inst_subst = substTyWith (univ_tvs ++ ex_tvs) (inst_tys ++ map mkTyVarTy ex_bndrs)
-
-      -- make new coercion vars, instantiating kind
-    mk_co_var uniq occ eq_pred = mkCoVar new_name (inst_subst (mkPredTy eq_pred))
-       where
-         new_name = mkSysTvName uniq (occNameFS occ)
-
-    co_bndrs               = zipWith3 mk_co_var co_uniqs co_occs eq_preds
-
-      -- make value vars, instantiating types
-    mk_id_var uniq occ ty = mkUserLocal occ uniq (inst_subst ty) noSrcLoc
-    id_bndrs = zipWith3 mk_id_var id_uniqs id_occs arg_tys
-
-exprIsConApp_maybe :: CoreExpr -> Maybe (DataCon, [CoreExpr])
--- Returns (Just (dc, [x1..xn])) if the argument expression is 
--- a constructor application of the form (dc x1 .. xn)
-
-exprIsConApp_maybe (Cast expr co)
-  =    -- Maybe this is over the top, but here we try to turn
-       --      coerce (S,T) ( x, y )
-       -- effectively into 
-       --      ( coerce S x, coerce T y )
-       -- This happens in anger in PrelArrExts which has a coerce
-       --      case coerce memcpy a b of
-       --        (# r, s #) -> ...
-       -- where the memcpy is in the IO monad, but the call is in
-       -- the (ST s) monad
-    case exprIsConApp_maybe expr of {
-       Nothing           -> Nothing ;
-       Just (dc, args)   -> 
-
-    let (from_ty, to_ty) = coercionKind co in
-  
-    case splitTyConApp_maybe to_ty of {
-       Nothing -> Nothing ;
-       Just (tc, tc_arg_tys) | tc /= dataConTyCon dc     -> Nothing
-                           --  | not (isVanillaDataCon dc) -> Nothing
-                             | otherwise                 ->
-               -- Type constructor must match datacon
-
-    case splitTyConApp_maybe from_ty of {
-        Nothing -> Nothing ;
-        Just (tc', tc_arg_tys') | tc /= tc' -> Nothing 
-                -- Both sides of coercion must have the same type constructor
-                               | otherwise ->
-
-    let
-        -- here we do the PushC reduction rule as described in the FC paper
-       arity               = tyConArity tc
-        n_ex_tvs            = length dc_ex_tyvars
-
-        (univ_args, rest)   = splitAt arity args
-        (ex_args, val_args) = splitAt n_ex_tvs rest
-
-        arg_tys            = dataConRepArgTys dc
-       dc_tyvars           = dataConUnivTyVars dc
-        dc_ex_tyvars        = dataConExTyVars dc
-
-        deep arg_ty         = deepCast arg_ty dc_tyvars co
-
-          -- first we appropriately cast the value arguments
-        arg_cos             = map deep arg_tys 
-       new_val_args        = zipWith mkCoerce (map deep arg_tys) val_args
-
-          -- then we cast the existential coercion arguments
-        orig_tvs            = dc_tyvars ++ dc_ex_tyvars
-        gammas              = decomposeCo arity co
-        new_tys             = gammas ++ (map (\ (Type t) -> t) ex_args)
-        theta               = substTyWith orig_tvs new_tys
-        cast_ty tv (Type ty) 
-          | isCoVar tv
-          , (ty1, ty2) <- splitCoercionKind (tyVarKind tv)
-          = Type $ mkTransCoercion (mkSymCoercion (theta ty1)) 
-            (mkTransCoercion ty (theta ty2))
-          | otherwise       
-          = Type ty
-        new_ex_args         = zipWith cast_ty dc_ex_tyvars ex_args
-  
-    in
-    ASSERT( all isTypeArg (take arity args) )
-    ASSERT( equalLength val_args arg_tys )
-    Just (dc, map Type tc_arg_tys ++ new_ex_args ++ new_val_args)
-    }}}
-
-exprIsConApp_maybe (Note _ expr)
-  = exprIsConApp_maybe expr
-    -- We ignore InlineMe notes in case we have
-    -- x = __inline_me__ (a,b)
-    -- All part of making sure that INLINE pragmas never hurt
-    -- Marcin tripped on this one when making dictionaries more inlinable
-    --
-    -- In fact, we ignore all notes.  For example,
-    --         case _scc_ "foo" (C a b) of
-    --                 C a b -> e
-    -- should be optimised away, but it will be only if we look
-    -- through the SCC note.
-
-exprIsConApp_maybe expr = analyse (collectArgs expr)
-  where
-    analyse (Var fun, args)
-       | Just con <- isDataConWorkId_maybe fun,
-         args `lengthAtLeast` dataConRepArity con
-               -- Might be > because the arity excludes type args
-       = Just (con,args)
-
-       -- Look through unfoldings, but only cheap ones, because
-       -- we are effectively duplicating the unfolding
-    analyse (Var fun, [])
-       | let unf = idUnfolding fun,
-         isCheapUnfolding unf
-       = exprIsConApp_maybe (unfoldingTemplate unf)
-
-    analyse other = Nothing
-\end{code}
-
+      -- Make the instantiating substitution
+    subst = zipOpenTvSubst (univ_tvs ++ ex_tvs) (inst_tys ++ map mkTyVarTy ex_bndrs)
 
+      -- Make value vars, instantiating types
+    mk_id_var uniq fs ty = mkUserLocal (mkVarOccFS fs) uniq (Type.substTy subst ty) noSrcSpan
+    arg_ids = zipWith3 mk_id_var id_uniqs id_fss arg_tys
+\end{code}
 
 %************************************************************************
 %*                                                                     *
-\subsection{Eta reduction and expansion}
+         Equality
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
-exprEtaExpandArity :: DynFlags -> CoreExpr -> Arity
-{- The Arity returned is the number of value args the 
-   thing can be applied to without doing much work
-
-exprEtaExpandArity is used when eta expanding
-       e  ==>  \xy -> e x y
-
-It returns 1 (or more) to:
-       case x of p -> \s -> ...
-because for I/O ish things we really want to get that \s to the top.
-We are prepared to evaluate x each time round the loop in order to get that
-
-It's all a bit more subtle than it looks:
-
-1.  One-shot lambdas
-
-Consider one-shot lambdas
-               let x = expensive in \y z -> E
-We want this to have arity 2 if the \y-abstraction is a 1-shot lambda
-Hence the ArityType returned by arityType
-
-2.  The state-transformer hack
-
-The one-shot lambda special cause is particularly important/useful for
-IO state transformers, where we often get
-       let x = E in \ s -> ...
-
-and the \s is a real-world state token abstraction.  Such abstractions
-are almost invariably 1-shot, so we want to pull the \s out, past the
-let x=E, even if E is expensive.  So we treat state-token lambdas as 
-one-shot even if they aren't really.  The hack is in Id.isOneShotBndr.
-
-3.  Dealing with bottom
-
-Consider also 
-       f = \x -> error "foo"
-Here, arity 1 is fine.  But if it is
-       f = \x -> case x of 
-                       True  -> error "foo"
-                       False -> \y -> x+y
-then we want to get arity 2.  Tecnically, this isn't quite right, because
-       (f True) `seq` 1
-should diverge, but it'll converge if we eta-expand f.  Nevertheless, we
-do so; it improves some programs significantly, and increasing convergence
-isn't a bad thing.  Hence the ABot/ATop in ArityType.
-
-Actually, the situation is worse.  Consider
-       f = \x -> case x of
-                       True  -> \y -> x+y
-                       False -> \y -> x-y
-Can we eta-expand here?  At first the answer looks like "yes of course", but
-consider
-       (f bot) `seq` 1
-This should diverge!  But if we eta-expand, it won't.   Again, we ignore this
-"problem", because being scrupulous would lose an important transformation for
-many programs.
-
-
-4. Newtypes
-
-Non-recursive newtypes are transparent, and should not get in the way.
-We do (currently) eta-expand recursive newtypes too.  So if we have, say
-
-       newtype T = MkT ([T] -> Int)
-
-Suppose we have
-       e = coerce T f
-where f has arity 1.  Then: etaExpandArity e = 1; 
-that is, etaExpandArity looks through the coerce.
-
-When we eta-expand e to arity 1: eta_expand 1 e T
-we want to get:                 coerce T (\x::[T] -> (coerce ([T]->Int) e) x)
-
-HOWEVER, note that if you use coerce bogusly you can ge
-       coerce Int negate
-And since negate has arity 2, you might try to eta expand.  But you can't
-decopose Int to a function type.   Hence the final case in eta_expand.
--}
-
-
-exprEtaExpandArity dflags e = arityDepth (arityType dflags e)
-
--- A limited sort of function type
-data ArityType = AFun Bool ArityType   -- True <=> one-shot
-              | ATop                   -- Know nothing
-              | ABot                   -- Diverges
-
-arityDepth :: ArityType -> Arity
-arityDepth (AFun _ ty) = 1 + arityDepth ty
-arityDepth ty         = 0
-
-andArityType ABot          at2           = at2
-andArityType ATop          at2           = ATop
-andArityType (AFun t1 at1)  (AFun t2 at2) = AFun (t1 && t2) (andArityType at1 at2)
-andArityType at1           at2           = andArityType at2 at1
+-- | A cheap equality test which bales out fast!
+--      If it returns @True@ the arguments are definitely equal,
+--      otherwise, they may or may not be equal.
+--
+-- See also 'exprIsBig'
+cheapEqExpr :: Expr b -> Expr b -> Bool
 
-arityType :: DynFlags -> CoreExpr -> ArityType
-       -- (go1 e) = [b1,..,bn]
-       -- means expression can be rewritten \x_b1 -> ... \x_bn -> body
-       -- where bi is True <=> the lambda is one-shot
+cheapEqExpr (Var v1)   (Var v2)   = v1==v2
+cheapEqExpr (Lit lit1) (Lit lit2) = lit1 == lit2
+cheapEqExpr (Type t1) (Type t2) = t1 `eqType` t2
+cheapEqExpr (Coercion c1) (Coercion c2) = c1 `coreEqCoercion` c2
 
-arityType dflags (Note n e) = arityType dflags e
---     Not needed any more: etaExpand is cleverer
---  | ok_note n = arityType dflags e
---  | otherwise = ATop
+cheapEqExpr (App f1 a1) (App f2 a2)
+  = f1 `cheapEqExpr` f2 && a1 `cheapEqExpr` a2
 
-arityType dflags (Cast e co) = arityType dflags e
+cheapEqExpr (Cast e1 t1) (Cast e2 t2)
+  = e1 `cheapEqExpr` e2 && t1 `coreEqCoercion` t2
 
-arityType dflags (Var v) 
-  = mk (idArity v) (arg_tys (idType v))
-  where
-    mk :: Arity -> [Type] -> ArityType
-       -- The argument types are only to steer the "state hack"
-       -- Consider case x of
-       --              True  -> foo
-       --              False -> \(s:RealWorld) -> e
-       -- where foo has arity 1.  Then we want the state hack to
-       -- apply to foo too, so we can eta expand the case.
-    mk 0 tys | isBottomingId v                    = ABot
-             | (ty:tys) <- tys, isStateHackType ty = AFun True ATop
-            | otherwise                           = ATop
-    mk n (ty:tys) = AFun (isStateHackType ty) (mk (n-1) tys)
-    mk n []       = AFun False               (mk (n-1) [])
-
-    arg_tys :: Type -> [Type]  -- Ignore for-alls
-    arg_tys ty 
-       | Just (_, ty')  <- splitForAllTy_maybe ty = arg_tys ty'
-       | Just (arg,res) <- splitFunTy_maybe ty    = arg : arg_tys res
-       | otherwise                                = []
-
-       -- Lambdas; increase arity
-arityType dflags (Lam x e)
-  | isId x    = AFun (isOneShotBndr x) (arityType dflags e)
-  | otherwise = arityType dflags e
-
-       -- Applications; decrease arity
-arityType dflags (App f (Type _)) = arityType dflags f
-arityType dflags (App f a)       = case arityType dflags f of
-                                       AFun one_shot xs | exprIsCheap a -> xs
-                                       other                            -> ATop
-                                                          
-       -- Case/Let; keep arity if either the expression is cheap
-       -- or it's a 1-shot lambda
-       -- The former is not really right for Haskell
-       --      f x = case x of { (a,b) -> \y. e }
-       --  ===>
-       --      f x y = case x of { (a,b) -> e }
-       -- The difference is observable using 'seq'
-arityType dflags (Case scrut _ _ alts)
-  = case foldr1 andArityType [arityType dflags rhs | (_,_,rhs) <- alts] of
-       xs | exprIsCheap scrut          -> xs
-       xs@(AFun one_shot _) | one_shot -> AFun True ATop
-       other                           -> ATop
-
-arityType dflags (Let b e) 
-  = case arityType dflags e of
-       xs                   | cheap_bind b -> xs
-       xs@(AFun one_shot _) | one_shot     -> AFun True ATop
-       other                               -> ATop
-  where
-    cheap_bind (NonRec b e) = is_cheap (b,e)
-    cheap_bind (Rec prs)    = all is_cheap prs
-    is_cheap (b,e) = (dopt Opt_DictsCheap dflags && isDictId b)
-                  || exprIsCheap e
-       -- If the experimental -fdicts-cheap flag is on, we eta-expand through
-       -- dictionary bindings.  This improves arities. Thereby, it also
-       -- means that full laziness is less prone to floating out the
-       -- application of a function to its dictionary arguments, which
-       -- can thereby lose opportunities for fusion.  Example:
-       --      foo :: Ord a => a -> ...
-       --      foo = /\a \(d:Ord a). let d' = ...d... in \(x:a). ....
-       --              -- So foo has arity 1
-       --
-       --      f = \x. foo dInt $ bar x
-       --
-       -- The (foo DInt) is floated out, and makes ineffective a RULE 
-       --      foo (bar x) = ...
-       --
-       -- One could go further and make exprIsCheap reply True to any
-       -- dictionary-typed expression, but that's more work.
-
-arityType dflags other = ATop
-
-{- NOT NEEDED ANY MORE: etaExpand is cleverer
-ok_note InlineMe = False
-ok_note other    = True
-    -- Notice that we do not look through __inline_me__
-    -- This may seem surprising, but consider
-    --         f = _inline_me (\x -> e)
-    -- We DO NOT want to eta expand this to
-    --         f = \x -> (_inline_me (\x -> e)) x
-    -- because the _inline_me gets dropped now it is applied, 
-    -- giving just
-    --         f = \x -> e
-    -- A Bad Idea
--}
+cheapEqExpr _ _ = False
 \end{code}
 
-
 \begin{code}
-etaExpand :: Arity             -- Result should have this number of value args
-         -> [Unique]
-         -> CoreExpr -> Type   -- Expression and its type
-         -> CoreExpr
--- (etaExpand n us e ty) returns an expression with 
--- the same meaning as 'e', but with arity 'n'.  
---
--- Given e' = etaExpand n us e ty
--- We should have
---     ty = exprType e = exprType e'
---
--- Note that SCCs are not treated specially.  If we have
---     etaExpand 2 (\x -> scc "foo" e)
---     = (\xy -> (scc "foo" e) y)
--- So the costs of evaluating 'e' (not 'e y') are attributed to "foo"
-
-etaExpand n us expr ty
-  | manifestArity expr >= n = expr             -- The no-op case
-  | otherwise              
-  = eta_expand n us expr ty
-  where
-
--- manifestArity sees how many leading value lambdas there are
-manifestArity :: CoreExpr -> Arity
-manifestArity (Lam v e) | isId v    = 1 + manifestArity e
-                       | otherwise = manifestArity e
-manifestArity (Note _ e)           = manifestArity e
-manifestArity (Cast e _)            = manifestArity e
-manifestArity e                            = 0
-
--- etaExpand deals with for-alls. For example:
---             etaExpand 1 E
--- where  E :: forall a. a -> a
--- would return
---     (/\b. \y::a -> E b y)
---
--- It deals with coerces too, though they are now rare
--- so perhaps the extra code isn't worth it
-
-eta_expand n us expr ty
-  | n == 0 && 
-    -- The ILX code generator requires eta expansion for type arguments
-    -- too, but alas the 'n' doesn't tell us how many of them there 
-    -- may be.  So we eagerly eta expand any big lambdas, and just
-    -- cross our fingers about possible loss of sharing in the ILX case. 
-    -- The Right Thing is probably to make 'arity' include
-    -- type variables throughout the compiler.  (ToDo.)
-    not (isForAllTy ty)        
-    -- Saturated, so nothing to do
-  = expr
-
-       -- Short cut for the case where there already
-       -- is a lambda; no point in gratuitously adding more
-eta_expand n us (Lam v body) ty
-  | isTyVar v
-  = Lam v (eta_expand n us body (applyTy ty (mkTyVarTy v)))
-
-  | otherwise
-  = Lam v (eta_expand (n-1) us body (funResultTy ty))
-
--- We used to have a special case that stepped inside Coerces here,
--- thus:  eta_expand n us (Note note@(Coerce _ ty) e) _  
---             = Note note (eta_expand n us e ty)
--- BUT this led to an infinite loop
--- Example:    newtype T = MkT (Int -> Int)
---     eta_expand 1 (coerce (Int->Int) e)
---     --> coerce (Int->Int) (eta_expand 1 T e)
---             by the bogus eqn
---     --> coerce (Int->Int) (coerce T 
---             (\x::Int -> eta_expand 1 (coerce (Int->Int) e)))
---             by the splitNewType_maybe case below
---     and round we go
-
-eta_expand n us expr ty
-  = ASSERT2 (exprType expr `coreEqType` ty, ppr (exprType expr) $$ ppr ty)
-    case splitForAllTy_maybe ty of { 
-         Just (tv,ty') -> 
-
-              Lam lam_tv (eta_expand n us2 (App expr (Type (mkTyVarTy lam_tv))) (substTyWith [tv] [mkTyVarTy lam_tv] ty'))
-                  where 
-                    lam_tv = mkTyVar (mkSysTvName uniq FSLIT("etaT")) (tyVarKind tv)
-                    (uniq:us2) = us
-
-       ; Nothing ->
-  
-       case splitFunTy_maybe ty of {
-         Just (arg_ty, res_ty) -> Lam arg1 (eta_expand (n-1) us2 (App expr (Var arg1)) res_ty)
-                               where
-                                  arg1       = mkSysLocal FSLIT("eta") uniq arg_ty
-                                  (uniq:us2) = us
-                                  
-       ; Nothing ->
-
-               -- Given this:
-               --      newtype T = MkT ([T] -> Int)
-               -- Consider eta-expanding this
-               --      eta_expand 1 e T
-               -- We want to get
-               --      coerce T (\x::[T] -> (coerce ([T]->Int) e) x)
-
-       case splitNewTypeRepCo_maybe ty of {
-         Just(ty1,co) -> 
-              mkCoerce co (eta_expand n us (mkCoerce (mkSymCoercion co) expr) ty1) ;
-         Nothing  -> 
-
-       -- We have an expression of arity > 0, but its type isn't a function
-       -- This *can* legitmately happen: e.g.  coerce Int (\x. x)
-       -- Essentially the programmer is playing fast and loose with types
-       -- (Happy does this a lot).  So we simply decline to eta-expand.
-       expr
-       }}}
+exprIsBig :: Expr b -> Bool
+-- ^ Returns @True@ of expressions that are too big to be compared by 'cheapEqExpr'
+exprIsBig (Lit _)      = False
+exprIsBig (Var _)      = False
+exprIsBig (Type _)    = False
+exprIsBig (Coercion _) = False
+exprIsBig (Lam _ e)    = exprIsBig e
+exprIsBig (App f a)    = exprIsBig f || exprIsBig a
+exprIsBig (Cast e _)   = exprIsBig e   -- Hopefully coercions are not too big!
+exprIsBig _            = True
 \end{code}
 
-exprArity is a cheap-and-cheerful version of exprEtaExpandArity.
-It tells how many things the expression can be applied to before doing
-any work.  It doesn't look inside cases, lets, etc.  The idea is that
-exprEtaExpandArity will do the hard work, leaving something that's easy
-for exprArity to grapple with.  In particular, Simplify uses exprArity to
-compute the ArityInfo for the Id. 
-
-Originally I thought that it was enough just to look for top-level lambdas, but
-it isn't.  I've seen this
-
-       foo = PrelBase.timesInt
-
-We want foo to get arity 2 even though the eta-expander will leave it
-unchanged, in the expectation that it'll be inlined.  But occasionally it
-isn't, because foo is blacklisted (used in a rule).  
-
-Similarly, see the ok_note check in exprEtaExpandArity.  So 
-       f = __inline_me (\x -> e)
-won't be eta-expanded.
-
-And in any case it seems more robust to have exprArity be a bit more intelligent.
-But note that  (\x y z -> f x y z)
-should have arity 3, regardless of f's arity.
-
 \begin{code}
-exprArity :: CoreExpr -> Arity
-exprArity e = go e
-           where
-             go (Var v)                   = idArity v
-             go (Lam x e) | isId x        = go e + 1
-                          | otherwise     = go e
-             go (Note n e)                = go e
-              go (Cast e _)                = go e
-             go (App e (Type t))          = go e
-             go (App f a) | exprIsCheap a = (go f - 1) `max` 0
-               -- NB: exprIsCheap a!  
-               --      f (fac x) does not have arity 2, 
-               --      even if f has arity 3!
-               -- NB: `max 0`!  (\x y -> f x) has arity 2, even if f is
-               --               unknown, hence arity 0
-             go _                         = 0
+eqExpr :: InScopeSet -> CoreExpr -> CoreExpr -> Bool
+-- Compares for equality, modulo alpha
+eqExpr in_scope e1 e2
+  = eqExprX id_unf (mkRnEnv2 in_scope) e1 e2
+  where
+    id_unf _ = noUnfolding     -- Don't expand
 \end{code}
-
-%************************************************************************
-%*                                                                     *
-\subsection{Equality}
-%*                                                                     *
-%************************************************************************
-
-@cheapEqExpr@ is a cheap equality test which bales out fast!
-       True  => definitely equal
-       False => may or may not be equal
-
+    
 \begin{code}
-cheapEqExpr :: Expr b -> Expr b -> Bool
+eqExprX :: IdUnfoldingFun -> RnEnv2 -> CoreExpr -> CoreExpr -> Bool
+-- ^ Compares expressions for equality, modulo alpha.
+-- Does /not/ look through newtypes or predicate types
+-- Used in rule matching, and also CSE
 
-cheapEqExpr (Var v1)   (Var v2)   = v1==v2
-cheapEqExpr (Lit lit1) (Lit lit2) = lit1 == lit2
-cheapEqExpr (Type t1)  (Type t2)  = t1 `coreEqType` t2
+eqExprX id_unfolding_fun env e1 e2
+  = go env e1 e2
+  where
+    go env (Var v1) (Var v2)
+      | rnOccL env v1 == rnOccR env v2
+      = True
+
+    -- The next two rules expand non-local variables
+    -- C.f. Note [Expanding variables] in Rules.lhs
+    -- and  Note [Do not expand locally-bound variables] in Rules.lhs
+    go env (Var v1) e2
+      | not (locallyBoundL env v1)
+      , Just e1' <- expandUnfolding_maybe (id_unfolding_fun (lookupRnInScope env v1))
+      = go (nukeRnEnvL env) e1' e2
+
+    go env e1 (Var v2)
+      | not (locallyBoundR env v2)
+      , Just e2' <- expandUnfolding_maybe (id_unfolding_fun (lookupRnInScope env v2))
+      = go (nukeRnEnvR env) e1 e2'
+
+    go _   (Lit lit1)    (Lit lit2)      = lit1 == lit2
+    go env (Type t1)    (Type t2)        = eqTypeX env t1 t2
+    go env (Coercion co1) (Coercion co2) = coreEqCoercion2 env co1 co2
+    go env (Cast e1 co1) (Cast e2 co2) = coreEqCoercion2 env co1 co2 && go env e1 e2
+    go env (App f1 a1)   (App f2 a2)   = go env f1 f2 && go env a1 a2
+    go env (Note n1 e1)  (Note n2 e2)  = go_note n1 n2 && go env e1 e2
+
+    go env (Lam b1 e1)  (Lam b2 e2)  
+      =  eqTypeX env (varType b1) (varType b2)   -- False for Id/TyVar combination
+      && go (rnBndr2 env b1 b2) e1 e2
+
+    go env (Let (NonRec v1 r1) e1) (Let (NonRec v2 r2) e2) 
+      =  go env r1 r2  -- No need to check binder types, since RHSs match
+      && go (rnBndr2 env v1 v2) e1 e2
+
+    go env (Let (Rec ps1) e1) (Let (Rec ps2) e2) 
+      = all2 (go env') rs1 rs2 && go env' e1 e2
+      where
+        (bs1,rs1) = unzip ps1     
+        (bs2,rs2) = unzip ps2
+        env' = rnBndrs2 env bs1 bs2
 
-cheapEqExpr (App f1 a1) (App f2 a2)
-  = f1 `cheapEqExpr` f2 && a1 `cheapEqExpr` a2
+    go env (Case e1 b1 _ a1) (Case e2 b2 _ a2)
+      =  go env e1 e2
+      && eqTypeX env (idType b1) (idType b2)
+      && all2 (go_alt (rnBndr2 env b1 b2)) a1 a2
 
-cheapEqExpr _ _ = False
+    go _ _ _ = False
 
-exprIsBig :: Expr b -> Bool
--- Returns True of expressions that are too big to be compared by cheapEqExpr
-exprIsBig (Lit _)      = False
-exprIsBig (Var v)      = False
-exprIsBig (Type t)     = False
-exprIsBig (App f a)    = exprIsBig f || exprIsBig a
-exprIsBig other               = True
+    -----------
+    go_alt env (c1, bs1, e1) (c2, bs2, e2)
+      = c1 == c2 && go (rnBndrs2 env bs1 bs2) e1 e2
+
+    -----------
+    go_note (SCC cc1)     (SCC cc2)      = cc1 == cc2
+    go_note (CoreNote s1) (CoreNote s2)  = s1 == s2
+    go_note _             _              = False
 \end{code}
 
+Auxiliary functions
 
 \begin{code}
-tcEqExpr :: CoreExpr -> CoreExpr -> Bool
--- Used in rule matching, so does *not* look through 
--- newtypes, predicate types; hence tcEqExpr
-
-tcEqExpr e1 e2 = tcEqExprX rn_env e1 e2
-  where
-    rn_env = mkRnEnv2 (mkInScopeSet (exprFreeVars e1 `unionVarSet` exprFreeVars e2))
-
-tcEqExprX :: RnEnv2 -> CoreExpr -> CoreExpr -> Bool
-tcEqExprX env (Var v1)    (Var v2)     = rnOccL env v1 == rnOccR env v2
-tcEqExprX env (Lit lit1)   (Lit lit2)   = lit1 == lit2
-tcEqExprX env (App f1 a1)  (App f2 a2)  = tcEqExprX env f1 f2 && tcEqExprX env a1 a2
-tcEqExprX env (Lam v1 e1)  (Lam v2 e2)  = tcEqExprX (rnBndr2 env v1 v2) e1 e2
-tcEqExprX env (Let (NonRec v1 r1) e1)
-             (Let (NonRec v2 r2) e2)   = tcEqExprX env r1 r2 
-                                      && tcEqExprX (rnBndr2 env v1 v2) e1 e2
-tcEqExprX env (Let (Rec ps1) e1)
-             (Let (Rec ps2) e2)        =  equalLength ps1 ps2
-                                       && and (zipWith eq_rhs ps1 ps2)
-                                       && tcEqExprX env' e1 e2
-                                    where
-                                      env' = foldl2 rn_bndr2 env ps2 ps2
-                                      rn_bndr2 env (b1,_) (b2,_) = rnBndr2 env b1 b2
-                                      eq_rhs       (_,r1) (_,r2) = tcEqExprX env' r1 r2
-tcEqExprX env (Case e1 v1 t1 a1)
-             (Case e2 v2 t2 a2)     =  tcEqExprX env e1 e2
-                                     && tcEqTypeX env t1 t2                      
-                                    && equalLength a1 a2
-                                    && and (zipWith (eq_alt env') a1 a2)
-                                    where
-                                      env' = rnBndr2 env v1 v2
-
-tcEqExprX env (Note n1 e1) (Note n2 e2) = eq_note env n1 n2 && tcEqExprX env e1 e2
-tcEqExprX env (Cast e1 co1) (Cast e2 co2) = tcEqTypeX env co1 co2 && tcEqExprX env e1 e2
-tcEqExprX env (Type t1)    (Type t2)    = tcEqTypeX env t1 t2
-tcEqExprX env e1               e2      = False
-                                        
-eq_alt env (c1,vs1,r1) (c2,vs2,r2) = c1==c2 && tcEqExprX (rnBndrs2 env vs1  vs2) r1 r2
-
-eq_note env (SCC cc1)      (SCC cc2)      = cc1 == cc2
-eq_note env (CoreNote s1)  (CoreNote s2)  = s1 == s2
-eq_note env other1            other2     = False
+locallyBoundL, locallyBoundR :: RnEnv2 -> Var -> Bool
+locallyBoundL rn_env v = inRnEnvL rn_env v
+locallyBoundR rn_env v = inRnEnvR rn_env v
 \end{code}
 
 
@@ -1325,38 +1099,93 @@ coreBindsSize :: [CoreBind] -> Int
 coreBindsSize bs = foldr ((+) . bindSize) 0 bs
 
 exprSize :: CoreExpr -> Int
-       -- A measure of the size of the expressions
-       -- It also forces the expression pretty drastically as a side effect
+-- ^ A measure of the size of the expressions, strictly greater than 0
+-- It also forces the expression pretty drastically as a side effect
+-- Counts *leaves*, not internal nodes. Types and coercions are not counted.
 exprSize (Var v)         = v `seq` 1
 exprSize (Lit lit)       = lit `seq` 1
 exprSize (App f a)       = exprSize f + exprSize a
 exprSize (Lam b e)       = varSize b + exprSize e
 exprSize (Let b e)       = bindSize b + exprSize e
 exprSize (Case e b t as) = seqType t `seq` exprSize e + varSize b + 1 + foldr ((+) . altSize) 0 as
-exprSize (Cast e co)     = (seqType co `seq` 1) + exprSize e
+exprSize (Cast e co)     = (seqCo co `seq` 1) + exprSize e
 exprSize (Note n e)      = noteSize n + exprSize e
-exprSize (Type t)        = seqType t `seq` 1
+exprSize (Type t)       = seqType t `seq` 1
+exprSize (Coercion co)   = seqCo co `seq` 1
 
+noteSize :: Note -> Int
 noteSize (SCC cc)       = cc `seq` 1
-noteSize InlineMe       = 1
 noteSize (CoreNote s)   = s `seq` 1  -- hdaume: core annotations
-
 varSize :: Var -> Int
 varSize b  | isTyVar b = 1
           | otherwise = seqType (idType b)             `seq`
                         megaSeqIdInfo (idInfo b)       `seq`
                         1
 
-varsSize = foldr ((+) . varSize) 0
+varsSize :: [Var] -> Int
+varsSize = sum . map varSize
 
+bindSize :: CoreBind -> Int
 bindSize (NonRec b e) = varSize b + exprSize e
 bindSize (Rec prs)    = foldr ((+) . pairSize) 0 prs
 
+pairSize :: (Var, CoreExpr) -> Int
 pairSize (b,e) = varSize b + exprSize e
 
+altSize :: CoreAlt -> Int
 altSize (c,bs,e) = c `seq` varsSize bs + exprSize e
 \end{code}
 
+\begin{code}
+data CoreStats = CS { cs_tm, cs_ty, cs_co :: Int }
+
+plusCS :: CoreStats -> CoreStats -> CoreStats
+plusCS (CS { cs_tm = p1, cs_ty = q1, cs_co = r1 })
+       (CS { cs_tm = p2, cs_ty = q2, cs_co = r2 })
+  = CS { cs_tm = p1+p2, cs_ty = q1+q2, cs_co = r1+r2 }
+  
+zeroCS, oneTM :: CoreStats
+zeroCS = CS { cs_tm = 0, cs_ty = 0, cs_co = 0 }
+oneTM  = zeroCS { cs_tm = 1 }
+
+sumCS :: (a -> CoreStats) -> [a] -> CoreStats
+sumCS f = foldr (plusCS . f) zeroCS 
+coreBindsStats :: [CoreBind] -> CoreStats
+coreBindsStats = sumCS bindStats
+
+bindStats :: CoreBind -> CoreStats
+bindStats (NonRec v r) = bindingStats v r
+bindStats (Rec prs)    = sumCS (\(v,r) -> bindingStats v r) prs
+
+bindingStats :: Var -> CoreExpr -> CoreStats
+bindingStats v r = bndrStats v `plusCS` exprStats r
+
+bndrStats :: Var -> CoreStats
+bndrStats v = oneTM `plusCS` tyStats (varType v)
+
+exprStats :: CoreExpr -> CoreStats
+exprStats (Var {})        = oneTM
+exprStats (Lit {})        = oneTM
+exprStats (Type t)        = tyStats t
+exprStats (Coercion c)    = coStats c
+exprStats (App f a)       = exprStats f `plusCS` exprStats a 
+exprStats (Lam b e)       = bndrStats b `plusCS` exprStats e 
+exprStats (Let b e)       = bindStats b `plusCS` exprStats e 
+exprStats (Case e b _ as) = exprStats e `plusCS` bndrStats b `plusCS` sumCS altStats as
+exprStats (Cast e co)     = coStats co `plusCS` exprStats e
+exprStats (Note _ e)      = exprStats e
+
+altStats :: CoreAlt -> CoreStats
+altStats (_, bs, r) = sumCS bndrStats bs `plusCS` exprStats r
+
+tyStats :: Type -> CoreStats
+tyStats ty = zeroCS { cs_ty = typeSize ty }
+
+coStats :: Coercion -> CoreStats
+coStats co = zeroCS { cs_co = coercionSize co }
+\end{code}
 
 %************************************************************************
 %*                                                                     *
@@ -1366,41 +1195,222 @@ altSize (c,bs,e) = c `seq` varsSize bs + exprSize e
 
 \begin{code}
 hashExpr :: CoreExpr -> Int
--- Two expressions that hash to the same Int may be equal (but may not be)
--- Two expressions that hash to the different Ints are definitely unequal
+-- ^ Two expressions that hash to the same @Int@ may be equal (but may not be)
+-- Two expressions that hash to the different Ints are definitely unequal.
+--
+-- The emphasis is on a crude, fast hash, rather than on high precision.
 -- 
--- But "unequal" here means "not identical"; two alpha-equivalent 
--- expressions may hash to the different Ints
+-- But unequal here means \"not identical\"; two alpha-equivalent 
+-- expressions may hash to the different Ints.
 --
--- The emphasis is on a crude, fast hash, rather than on high precision
-
-hashExpr e | hash < 0  = 77    -- Just in case we hit -maxInt
-          | otherwise = hash
-          where
-            hash = abs (hash_expr e)   -- Negative numbers kill UniqFM
-
-hash_expr (Note _ e)                     = hash_expr e
-hash_expr (Cast e co)             = hash_expr e
-hash_expr (Let (NonRec b r) e)    = hashId b
-hash_expr (Let (Rec ((b,r):_)) e) = hashId b
-hash_expr (Case _ b _ _)         = hashId b
-hash_expr (App f e)              = hash_expr f * fast_hash_expr e
-hash_expr (Var v)                = hashId v
-hash_expr (Lit lit)              = hashLiteral lit
-hash_expr (Lam b _)              = hashId b
-hash_expr (Type t)               = trace "hash_expr: type" 1           -- Shouldn't happen
-
-fast_hash_expr (Var v)         = hashId v
-fast_hash_expr (Lit lit)       = hashLiteral lit
-fast_hash_expr (App f (Type _)) = fast_hash_expr f
-fast_hash_expr (App f a)        = fast_hash_expr a
-fast_hash_expr (Lam b _)        = hashId b
-fast_hash_expr other           = 1
-
-hashId :: Id -> Int
-hashId id = hashName (idName id)
+-- We must be careful that @\\x.x@ and @\\y.y@ map to the same hash code,
+-- (at least if we want the above invariant to be true).
+
+hashExpr e = fromIntegral (hash_expr (1,emptyVarEnv) e .&. 0x7fffffff)
+             -- UniqFM doesn't like negative Ints
+
+type HashEnv = (Int, VarEnv Int)  -- Hash code for bound variables
+
+hash_expr :: HashEnv -> CoreExpr -> Word32
+-- Word32, because we're expecting overflows here, and overflowing
+-- signed types just isn't cool.  In C it's even undefined.
+hash_expr env (Note _ e)             = hash_expr env e
+hash_expr env (Cast e _)              = hash_expr env e
+hash_expr env (Var v)                = hashVar env v
+hash_expr _   (Lit lit)               = fromIntegral (hashLiteral lit)
+hash_expr env (App f e)              = hash_expr env f * fast_hash_expr env e
+hash_expr env (Let (NonRec b r) e)    = hash_expr (extend_env env b) e * fast_hash_expr env r
+hash_expr env (Let (Rec ((b,_):_)) e) = hash_expr (extend_env env b) e
+hash_expr env (Case e _ _ _)         = hash_expr env e
+hash_expr env (Lam b e)                      = hash_expr (extend_env env b) e
+hash_expr _   (Type _)                = WARN(True, text "hash_expr: type") 1
+-- Shouldn't happen.  Better to use WARN than trace, because trace
+-- prevents the CPR optimisation kicking in for hash_expr.
+hash_expr _   (Coercion _)            = WARN(True, text "hash_expr: coercion") 1
+
+fast_hash_expr :: HashEnv -> CoreExpr -> Word32
+fast_hash_expr env (Var v)              = hashVar env v
+fast_hash_expr env (Type t)     = fast_hash_type env t
+fast_hash_expr env (Coercion co) = fast_hash_co env co
+fast_hash_expr _   (Lit lit)     = fromIntegral (hashLiteral lit)
+fast_hash_expr env (Cast e _)    = fast_hash_expr env e
+fast_hash_expr env (Note _ e)    = fast_hash_expr env e
+fast_hash_expr env (App _ a)     = fast_hash_expr env a        -- A bit idiosyncratic ('a' not 'f')!
+fast_hash_expr _   _             = 1
+
+fast_hash_type :: HashEnv -> Type -> Word32
+fast_hash_type env ty 
+  | Just tv <- getTyVar_maybe ty            = hashVar env tv
+  | Just (tc,tys) <- splitTyConApp_maybe ty = let hash_tc = fromIntegral (hashName (tyConName tc))
+                                             in foldr (\t n -> fast_hash_type env t + n) hash_tc tys
+  | otherwise                              = 1
+
+fast_hash_co :: HashEnv -> Coercion -> Word32
+fast_hash_co env co
+  | Just cv <- getCoVar_maybe co              = hashVar env cv
+  | Just (tc,cos) <- splitTyConAppCo_maybe co = let hash_tc = fromIntegral (hashName (tyConName tc))
+                                                in foldr (\c n -> fast_hash_co env c + n) hash_tc cos
+  | otherwise                                 = 1
+
+extend_env :: HashEnv -> Var -> (Int, VarEnv Int)
+extend_env (n,env) b = (n+1, extendVarEnv env b n)
+
+hashVar :: HashEnv -> Var -> Word32
+hashVar (_,env) v
+ = fromIntegral (lookupVarEnv env v `orElse` hashName (idName v))
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+               Eta reduction
+%*                                                                     *
+%************************************************************************
+
+Note [Eta reduction conditions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We try for eta reduction here, but *only* if we get all the way to an
+trivial expression.  We don't want to remove extra lambdas unless we
+are going to avoid allocating this thing altogether.
+
+There are some particularly delicate points here:
+
+* Eta reduction is not valid in general:  
+       \x. bot  /=  bot
+  This matters, partly for old-fashioned correctness reasons but,
+  worse, getting it wrong can yield a seg fault. Consider
+       f = \x.f x
+       h y = case (case y of { True -> f `seq` True; False -> False }) of
+               True -> ...; False -> ...
+
+  If we (unsoundly) eta-reduce f to get f=f, the strictness analyser
+  says f=bottom, and replaces the (f `seq` True) with just
+  (f `cast` unsafe-co).  BUT, as thing stand, 'f' got arity 1, and it
+  *keeps* arity 1 (perhaps also wrongly).  So CorePrep eta-expands 
+  the definition again, so that it does not termninate after all.
+  Result: seg-fault because the boolean case actually gets a function value.
+  See Trac #1947.
+
+  So it's important to to the right thing.
+
+* Note [Arity care]: we need to be careful if we just look at f's
+  arity. Currently (Dec07), f's arity is visible in its own RHS (see
+  Note [Arity robustness] in SimplEnv) so we must *not* trust the
+  arity when checking that 'f' is a value.  Otherwise we will
+  eta-reduce
+      f = \x. f x
+  to
+      f = f
+  Which might change a terminiating program (think (f `seq` e)) to a 
+  non-terminating one.  So we check for being a loop breaker first.
+
+  However for GlobalIds we can look at the arity; and for primops we
+  must, since they have no unfolding.  
+
+* Regardless of whether 'f' is a value, we always want to 
+  reduce (/\a -> f a) to f
+  This came up in a RULE: foldr (build (/\a -> g a))
+  did not match          foldr (build (/\b -> ...something complex...))
+  The type checker can insert these eta-expanded versions,
+  with both type and dictionary lambdas; hence the slightly 
+  ad-hoc isDictId
+
+* Never *reduce* arity. For example
+      f = \xy. g x y
+  Then if h has arity 1 we don't want to eta-reduce because then
+  f's arity would decrease, and that is bad
+
+These delicacies are why we don't use exprIsTrivial and exprIsHNF here.
+Alas.
+
+Note [Eta reduction with casted arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider  
+    (\(x:t3). f (x |> g)) :: t3 -> t2
+  where
+    f :: t1 -> t2
+    g :: t3 ~ t1
+This should be eta-reduced to
+
+    f |> (sym g -> t2)
+
+So we need to accumulate a coercion, pushing it inward (past
+variable arguments only) thus:
+   f (x |> co_arg) |> co  -->  (f |> (sym co_arg -> co)) x
+   f (x:t)         |> co  -->  (f |> (t -> co)) x
+   f @ a           |> co  -->  (f |> (forall a.co)) @ a
+   f @ (g:t1~t2)   |> co  -->  (f |> (t1~t2 => co)) @ (g:t1~t2)
+These are the equations for ok_arg.
+
+It's true that we could also hope to eta reduce these:
+    (\xy. (f x |> g) y)
+    (\xy. (f x y) |> g)
+But the simplifier pushes those casts outwards, so we don't
+need to address that here.
+
+\begin{code}
+tryEtaReduce :: [Var] -> CoreExpr -> Maybe CoreExpr
+tryEtaReduce bndrs body 
+  = go (reverse bndrs) body (mkReflCo (exprType body))
+  where
+    incoming_arity = count isId bndrs
+
+    go :: [Var]                   -- Binders, innermost first, types [a3,a2,a1]
+       -> CoreExpr         -- Of type tr
+       -> Coercion         -- Of type tr ~ ts
+       -> Maybe CoreExpr   -- Of type a1 -> a2 -> a3 -> ts
+    -- See Note [Eta reduction with casted arguments]
+    -- for why we have an accumulating coercion
+    go [] fun co
+      | ok_fun fun = Just (mkCoerce co fun)
+
+    go (b : bs) (App fun arg) co
+      | Just co' <- ok_arg b arg co
+      = go bs fun co'
+
+    go _ _ _  = Nothing                -- Failure!
+
+    ---------------
+    -- Note [Eta reduction conditions]
+    ok_fun (App fun (Type ty)) 
+        | not (any (`elemVarSet` tyVarsOfType ty) bndrs)
+       =  ok_fun fun
+    ok_fun (Var fun_id)
+       =  not (fun_id `elem` bndrs)
+       && (ok_fun_id fun_id || all ok_lam bndrs)
+    ok_fun _fun = False
+
+    ---------------
+    ok_fun_id fun = fun_arity fun >= incoming_arity
+
+    ---------------
+    fun_arity fun            -- See Note [Arity care]
+       | isLocalId fun && isLoopBreaker (idOccInfo fun) = 0
+       | otherwise = idArity fun             
+
+    ---------------
+    ok_lam v = isTyVar v || isEvVar v
+
+    ---------------
+    ok_arg :: Var              -- Of type bndr_t
+           -> CoreExpr         -- Of type arg_t
+           -> Coercion         -- Of kind (t1~t2)
+           -> Maybe Coercion   -- Of type (arg_t -> t1 ~  bndr_t -> t2)
+                               --   (and similarly for tyvars, coercion args)
+    -- See Note [Eta reduction with casted arguments]
+    ok_arg bndr (Type ty) co
+       | Just tv <- getTyVar_maybe ty
+       , bndr == tv  = Just (mkForAllCo tv co)
+    ok_arg bndr (Var v) co
+       | bndr == v   = Just (mkFunCo (mkReflCo (idType bndr)) co)
+    ok_arg bndr (Cast (Var v) co_arg) co
+       | bndr == v  = Just (mkFunCo (mkSymCo co_arg) co)
+       -- The simplifier combines multiple casts into one, 
+       -- so we can have a simple-minded pattern match here
+    ok_arg _ _ _ = Nothing
 \end{code}
 
+
 %************************************************************************
 %*                                                                     *
 \subsection{Determining non-updatable right-hand-sides}
@@ -1413,17 +1423,17 @@ arguments, come from another DLL (because we can't refer to static
 labels in other DLLs).
 
 If this happens we simply make the RHS into an updatable thunk, 
-and 'exectute' it rather than allocating it statically.
+and 'execute' it rather than allocating it statically.
 
 \begin{code}
-rhsIsStatic :: PackageId -> CoreExpr -> Bool
--- This function is called only on *top-level* right-hand sides
--- Returns True if the RHS can be allocated statically, with
--- no thunks involved at all.
---
+-- | This function is called only on *top-level* right-hand sides.
+-- Returns @True@ if the RHS can be allocated statically in the output,
+-- with no thunks involved at all.
+rhsIsStatic :: (Name -> Bool) -> CoreExpr -> Bool
 -- It's called (i) in TidyPgm.hasCafRefs to decide if the rhs is, or
--- refers to, CAFs; and (ii) in CoreToStg to decide whether to put an
--- update flag on it.
+-- refers to, CAFs; (ii) in CoreToStg to decide whether to put an
+-- update flag on it and (iii) in DsExpr to decide how to expand
+-- list literals
 --
 -- The basic idea is that rhsIsStatic returns True only if the RHS is
 --     (a) a value lambda
@@ -1469,29 +1479,24 @@ rhsIsStatic :: PackageId -> CoreExpr -> Bool
 -- This is a bit like CoreUtils.exprIsHNF, with the following differences:
 --    a) scc "foo" (\x -> ...) is updatable (so we catch the right SCC)
 --
---    b) (C x xs), where C is a contructors is updatable if the application is
+--    b) (C x xs), where C is a contructor is updatable if the application is
 --        dynamic
 -- 
 --    c) don't look through unfolding of f in (f x).
---
--- When opt_RuntimeTypes is on, we keep type lambdas and treat
--- them as making the RHS re-entrant (non-updatable).
 
-rhsIsStatic this_pkg rhs = is_static False rhs
+rhsIsStatic _is_dynamic_name rhs = is_static False rhs
   where
   is_static :: Bool    -- True <=> in a constructor argument; must be atomic
          -> CoreExpr -> Bool
   
-  is_static False (Lam b e) = isRuntimeVar b || is_static False e
-  
-  is_static in_arg (Note (SCC _) e) = False
-  is_static in_arg (Note _ e)       = is_static in_arg e
-  is_static in_arg (Cast e co)      = is_static in_arg e
+  is_static False (Lam b e)   = isRuntimeVar b || is_static False e
+  is_static in_arg (Note n e) = notSccNote n && is_static in_arg e
+  is_static in_arg (Cast e _) = is_static in_arg e
   
-  is_static in_arg (Lit lit)
+  is_static _      (Lit lit)
     = case lit of
-       MachLabel _ _ -> False
-       other         -> True
+       MachLabel _ _ _ -> False
+        _             -> True
        -- A MachLabel (foreign import "&foo") in an argument
        -- prevents a constructor application from being static.  The
        -- reason is that it might give rise to unresolvable symbols
@@ -1505,7 +1510,7 @@ rhsIsStatic this_pkg rhs = is_static False rhs
    where
     go (Var f) n_val_args
 #if mingw32_TARGET_OS
-        | not (isDllName this_pkg (idName f))
+        | not (_is_dynamic_name (idName f))
 #endif
        =  saturated_data_con f n_val_args
        || (in_arg && n_val_args == 0)  
@@ -1527,11 +1532,9 @@ rhsIsStatic this_pkg rhs = is_static False rhs
         --   x = D# (1.0## /## 2.0##)
         -- can't float because /## can fail.
 
-    go (Note (SCC _) f) n_val_args = False
-    go (Note _ f) n_val_args       = go f n_val_args
-    go (Cast e co) n_val_args      = go e n_val_args
-
-    go other n_val_args = False
+    go (Note n f) n_val_args = notSccNote n && go f n_val_args
+    go (Cast e _) n_val_args = go e n_val_args
+    go _          _          = False
 
     saturated_data_con f n_val_args
        = case isDataConWorkId_maybe f of