Remove very dead Java backend code.
[ghc-hetmet.git] / compiler / coreSyn / CoreUtils.lhs
index 379da8a..4146b62 100644 (file)
@@ -16,7 +16,7 @@ Utility functions on @Core@ syntax
 -- | Commonly useful utilites for manipulating the Core language
 module CoreUtils (
        -- * Constructing expressions
-       mkInlineMe, mkSCC, mkCoerce, mkCoerceI,
+       mkSCC, mkCoerce,
        bindNonRec, needsCaseBinding,
        mkAltExpr, mkPiType, mkPiTypes,
 
@@ -25,23 +25,27 @@ module CoreUtils (
 
        -- * Properties of expressions
        exprType, coreAltType, coreAltsType,
-       exprIsDupable, exprIsTrivial, exprIsCheap, exprIsExpandable,
-       exprIsHNF,exprOkForSpeculation, exprIsBig, 
-       exprIsConApp_maybe, exprIsBottom,
-       rhsIsStatic,
+       exprIsDupable, exprIsTrivial, exprIsBottom,
+        exprIsCheap, exprIsExpandable, exprIsCheap', CheapAppFun,
+       exprIsHNF, exprOkForSpeculation, exprIsBig, exprIsConLike,
+       rhsIsStatic, isCheapApp, isExpandableApp,
 
        -- * Expression and bindings size
        coreBindsSize, exprSize,
+        CoreStats(..), coreBindsStats, 
 
        -- * Hashing
        hashExpr,
 
        -- * Equality
-       cheapEqExpr, 
+       cheapEqExpr, eqExpr, eqExprX,
+
+       -- * Eta reduction
+       tryEtaReduce,
 
        -- * Manipulating data constructors and types
        applyTypeToArgs, applyTypeToArg,
-        dataConOrigInstPat, dataConRepInstPat, dataConRepFSInstPat
+        dataConRepInstPat, dataConRepFSInstPat
     ) where
 
 #include "HsVersions.h"
@@ -51,17 +55,13 @@ import PprCore
 import Var
 import SrcLoc
 import VarEnv
+import VarSet
 import Name
-import Module
-#if mingw32_TARGET_OS
-import Packages
-#endif
 import Literal
 import DataCon
 import PrimOp
 import Id
 import IdInfo
-import NewDemand
 import Type
 import Coercion
 import TyCon
@@ -72,10 +72,9 @@ import TysPrim
 import FastString
 import Maybes
 import Util
+import Pair
 import Data.Word
 import Data.Bits
-
-import GHC.Exts                -- For `xori` 
 \end{code}
 
 
@@ -92,9 +91,10 @@ exprType :: CoreExpr -> Type
 -- 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)         = snd (coercionKind co)
+exprType (Cast _ co)         = pSnd (coercionKind co)
 exprType (Note _ e)          = exprType e
 exprType (Lam binder expr)   = mkPiType binder (exprType expr)
 exprType e@(App _ _)
@@ -105,7 +105,13 @@ exprType other = pprTrace "exprType" (pprCoreExpr other) alphaTy
 
 coreAltType :: CoreAlt -> Type
 -- ^ Returns the type of the alternatives right hand side
-coreAltType (_,_,rhs) = exprType rhs
+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
@@ -113,8 +119,32 @@ coreAltsType (alt:_) = coreAltType alt
 coreAltsType []             = panic "corAltsType"
 \end{code}
 
+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
+
+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.
+
+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
+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
@@ -143,11 +173,11 @@ applyTypeToArgs e op_ty (Type ty : args)
     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' = applyTysD msg op_ty (reverse rev_tys)
-                                 msg = ptext (sLit "applyTypeToArgs") <+> 
-                                       panic_msg e op_ty
+    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 (_ : args)
   = case (splitFunTy_maybe op_ty) of
@@ -164,66 +194,23 @@ panic_msg e op_ty = pprCoreExpr e $$ ppr op_ty
 %*                                                                     *
 %************************************************************************
 
-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}
--- | Wraps the given expression in an inlining hint unless the expression
--- is trivial in some sense, so that doing so would usually hurt us
-mkInlineMe :: CoreExpr -> CoreExpr
-mkInlineMe (Var v) = Var v
-mkInlineMe e      = Note InlineMe e
-\end{code}
-
 \begin{code}
--- | Wrap the given expression in the coercion, dropping identity coercions and coalescing nested coercions
-mkCoerceI :: CoercionI -> CoreExpr -> CoreExpr
-mkCoerceI IdCo e = e
-mkCoerceI (ACo co) e = mkCoerce co e
-
--- | Wrap the given expression in the coercion safely, coalescing nested coercions
+-- | 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}
 
@@ -308,27 +295,28 @@ findDefault :: [CoreAlt] -> ([CoreAlt], Maybe CoreExpr)
 findDefault ((DEFAULT,args,rhs) : alts) = ASSERT( null args ) (alts, Just rhs)
 findDefault alts                       =                     (alts, Nothing)
 
+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] -> CoreAlt
+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
-        _                          -> 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 _               = False
-
 ---------------------------------
 mergeAlts :: [CoreAlt] -> [CoreAlt] -> [CoreAlt]
 -- ^ Merge alternatives preserving order; alternatives in
@@ -357,18 +345,51 @@ 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 
 
+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
@@ -380,25 +401,56 @@ 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 :: CoreExpr -> Bool
-exprIsTrivial (Var _)          = True        -- See notes above
-exprIsTrivial (Type _)         = True
+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 (SCC _) _) = False       -- See notes above
-exprIsTrivial (Note _       e) = 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.
@@ -412,25 +464,38 @@ exprIsTrivial _                = False
 
 \begin{code}
 exprIsDupable :: CoreExpr -> Bool
-exprIsDupable (Type _)          = True
-exprIsDupable (Var _)           = True
-exprIsDupable (Lit lit)         = litIsDupable lit
-exprIsDupable (Note InlineMe _) = True
-exprIsDupable (Note _ e)        = exprIsDupable e
-exprIsDupable (Cast e _)        = exprIsDupable e
-exprIsDupable expr
-  = go expr 0
+exprIsDupable e
+  = isJust (go dupAppSize e)
   where
-    go (Var _)   _      = True
-    go (App f a) n_args =  n_args < dupAppSize
-                       && exprIsDupable a
-                       && go f (n_args+1)
-    go _         _      = 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
@@ -459,47 +524,64 @@ 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' :: (Id -> Bool) -> CoreExpr -> Bool
-exprIsCheap' _          (Lit _)           = True
-exprIsCheap' _          (Type _)          = True
-exprIsCheap' _          (Var _)           = True
-exprIsCheap' _          (Note InlineMe _) = True
-exprIsCheap' is_conlike (Note _ e)        = exprIsCheap' is_conlike e
-exprIsCheap' is_conlike (Cast e _)        = exprIsCheap' is_conlike e
-exprIsCheap' is_conlike (Lam x e)         = isRuntimeVar x
-                                            || exprIsCheap' is_conlike e
-exprIsCheap' is_conlike (Case e _ _ alts) = exprIsCheap' is_conlike e && 
-                               and [exprIsCheap' is_conlike rhs | (_,_,rhs) <- alts]
+exprIsCheap :: CoreExpr -> Bool
+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' is_conlike (Let (NonRec x _) e)  
-      | isUnLiftedType (idType x) = exprIsCheap' is_conlike e
-      | otherwise                = False
-       -- strict lets always have cheap right hand sides,
-       -- and do no allocation.
 
-exprIsCheap' is_conlike 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 _) [] = True       -- Just a type application of a variable
                                -- (f t1 t2 t3) counts as WHNF
     go (Var f) args
-       = case idDetails f of
-               RecSelId {}  -> go_sel args
-               ClassOpId _  -> go_sel args
-               PrimOpId op  -> go_primop op args
-
-               _ | is_conlike f -> go_pap args
-                  | length args < idArity f -> go_pap args
-
-               _ -> 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!
@@ -507,33 +589,64 @@ exprIsCheap' is_conlike other_expr        -- Applications and variables
     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' is_conlike) 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' is_conlike arg -- I'm experimenting with making record selection
+    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)
 
-exprIsCheap :: CoreExpr -> Bool
-exprIsCheap = exprIsCheap' isDataConWorkId
+isCheapApp :: CheapAppFun
+isCheapApp fn n_val_args
+  = isDataConWorkId fn 
+  || n_val_args < idArity fn
 
-exprIsExpandable :: CoreExpr -> Bool
-exprIsExpandable = exprIsCheap' isConLikeId
+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}
 
+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.
+
+
+%************************************************************************
+%*                                                                     *
+             exprOkForSpeculation
+%*                                                                     *
+%************************************************************************
+
 \begin{code}
 -- | 'exprOkForSpeculation' returns True of an expression that is:
 --
@@ -542,14 +655,16 @@ exprIsExpandable = exprIsCheap' isConLikeId
 --
 --  * 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@.
@@ -568,13 +683,24 @@ exprIsExpandable = exprIsCheap' isConLikeId
 -- 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
-    -- Tick boxes are *not* suitable for speculation
-exprOkForSpeculation (Var v)     = isUnLiftedType (idType v)
-                                && not (isTickBoxOp 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 _)  = 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 (idDetails f) args
@@ -593,12 +719,19 @@ 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 (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!
@@ -610,46 +743,82 @@ 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 _                = False
 \end{code}
 
-\begin{code}
--- | True of expressions that are guaranteed to diverge upon execution
-exprIsBottom :: CoreExpr -> Bool
-exprIsBottom e = go 0 e
-               where
-                -- n is the number of args
-                 go n (Note _ e)     = go n e
-                 go n (Cast e _)     = go n e
-                 go n (Let _ e)      = go n e
-                 go _ (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 _ (Lit _)        = False
-                 go _ (Lam _ _)      = False
-                 go _ (Type _)       = False
-
-idAppIsBottom :: Id -> Int -> Bool
-idAppIsBottom id n_val_args = appIsBottom (idNewStrictness id) n_val_args
-\end{code}
+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
 
-\begin{code}
 
--- | This returns true for expressions that are certainly /already/ 
+%************************************************************************
+%*                                                                     *
+             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:
+--    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
@@ -658,7 +827,7 @@ idAppIsBottom id n_val_args = appIsBottom (idNewStrictness id) n_val_args
 -- > (:) (f x) (map f xs)
 -- > map (...redex...)
 --
--- Because 'seq' on such things completes immediately.
+-- because 'seq' on such things completes immediately.
 --
 -- For unlifted argument types, we have to be careful:
 --
@@ -668,69 +837,87 @@ idAppIsBottom id n_val_args = appIsBottom (idNewStrictness id) n_val_args
 -- 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 _)          = True
-exprIsHNF (Type _)         = 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 _)       = exprIsHNF e
-exprIsHNF (App e (Type _)) = exprIsHNF e
-exprIsHNF (App e a)        = app_is_value e [a]
-exprIsHNF _                = 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
-    ||  isDataConWorkId fun            --  or data constructor
-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
+       -- 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}
-dataConRepInstPat, dataConOrigInstPat :: [Unique] -> DataCon -> [Type] -> ([TyVar], [CoVar], [Id])
-dataConRepFSInstPat :: [FastString] -> [Unique] -> DataCon -> [Type] -> ([TyVar], [CoVar], [Id])
+dataConRepInstPat   ::                 [Unique] -> DataCon -> [Type] -> ([TyVar], [Id])
+dataConRepFSInstPat :: [FastString] -> [Unique] -> DataCon -> [Type] -> ([TyVar], [Id])
 
-dataConRepInstPat   = dataConInstPat dataConRepArgTys (repeat ((fsLit "ipv")))
-dataConRepFSInstPat = dataConInstPat dataConRepArgTys
-dataConOrigInstPat  = dataConInstPat dc_arg_tys       (repeat ((fsLit "ipv")))
-  where 
-    dc_arg_tys dc = map mkPredTy (dataConEqTheta dc) ++ map mkPredTy (dataConDictTheta dc) ++ dataConOrigArgTys dc
-       -- Remember to include the existential dictionaries
-
-dataConInstPat :: (DataCon -> [Type])      -- function used to find arg tys
-                  -> [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
+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], [Id])          -- Return instantiated variables
 -- dataConInstPat arg_fun fss us con inst_tys returns a triple 
--- (ex_tvs, co_tvs, arg_ids),
+-- (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
---     The co_tvs include both GADT equalities (dcEqSpec) and 
---     programmer-specified equalities (dcEqTheta)
---
 --   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 dicts (dcDictTheta) and
---     programmer-specified arguments (after rep-ing) (deRepArgTys)
+--     The arg_ids include both evidence and
+--     programmer-specified arguments (both after rep-ing)
 --
 -- Example.
 --  The following constructor T1
@@ -745,29 +932,22 @@ dataConInstPat :: (DataCon -> [Type])      -- function used to find arg tys
 --
 --  dataConInstPat fss us T1 (a1',b') will return
 --
---  ([a1'', b''], [c :: (a1', b')~(a1'', b'')], [x :: Int, y :: b''])
+--  ([a1'', b''], [c :: (a1', b')~(a1'', b''), x :: Int, y :: b''])
 --
 --  where the double-primed variables are created with the FastStrings and
 --  Uniques given as fss and us
-dataConInstPat arg_fun fss uniqs con inst_tys 
-  = (ex_bndrs, co_bndrs, arg_ids)
+dataConInstPat fss uniqs con inst_tys 
+  = (ex_bndrs, arg_ids)
   where 
     univ_tvs = dataConUnivTyVars con
     ex_tvs   = dataConExTyVars con
-    arg_tys  = arg_fun con
-    eq_spec  = dataConEqSpec con
-    eq_theta = dataConEqTheta con
-    eq_preds = eqSpecPreds eq_spec ++ eq_theta
+    arg_tys  = dataConRepArgTys con
 
     n_ex = length ex_tvs
-    n_co = length eq_preds
 
       -- split the Uniques and FastStrings
-    (ex_uniqs, uniqs')   = splitAt n_ex uniqs
-    (co_uniqs, id_uniqs) = splitAt n_co uniqs'
-
-    (ex_fss, fss')     = splitAt n_ex fss
-    (co_fss, id_fss)   = splitAt n_co fss'
+    (ex_uniqs, id_uniqs) = splitAt n_ex uniqs
+    (ex_fss,   id_fss)   = splitAt n_ex fss
 
       -- Make existential type variables
     ex_bndrs = zipWith3 mk_ex_var ex_uniqs ex_fss ex_tvs
@@ -779,142 +959,14 @@ dataConInstPat arg_fun fss uniqs con inst_tys
       -- Make the instantiating substitution
     subst = zipOpenTvSubst (univ_tvs ++ ex_tvs) (inst_tys ++ map mkTyVarTy ex_bndrs)
 
-      -- Make new coercion vars, instantiating kind
-    co_bndrs = zipWith3 mk_co_var co_uniqs co_fss eq_preds
-    mk_co_var uniq fs eq_pred = mkCoVar new_name co_kind
-       where
-         new_name = mkSysTvName uniq fs
-         co_kind  = substTy subst (mkPredTy eq_pred)
-
-      -- make value vars, instantiating types
-    mk_id_var uniq fs ty = mkUserLocal (mkVarOccFS fs) uniq (substTy subst ty) noSrcSpan
+      -- 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
-
--- | Returns @Just (dc, [x1..xn])@ if the argument expression is 
--- a constructor application of the form @dc x1 .. xn@
-exprIsConApp_maybe :: CoreExpr -> Maybe (DataCon, [CoreExpr])
-exprIsConApp_maybe (Cast expr co)
-  =     -- Here we do the KPush reduction rule as described in the FC paper
-    case exprIsConApp_maybe expr of {
-       Nothing            -> Nothing ;
-       Just (dc, dc_args) -> 
-
-       -- The transformation applies iff we have
-       --      (C e1 ... en) `cast` co
-       -- where co :: (T t1 .. tn) ~ (T s1 ..sn)
-       -- That is, with a T at the top of both sides
-       -- The left-hand one must be a T, because exprIsConApp returned True
-       -- but the right-hand one might not be.  (Though it usually will.)
-
-    let (from_ty, to_ty)          = coercionKind co
-       (from_tc, from_tc_arg_tys) = splitTyConApp from_ty
-               -- The inner one must be a TyConApp
-    in
-    case splitTyConApp_maybe to_ty of {
-       Nothing -> Nothing ;
-       Just (to_tc, to_tc_arg_tys) 
-               | from_tc /= to_tc -> Nothing
-               -- These two Nothing cases are possible; we might see 
-               --      (C x y) `cast` (g :: T a ~ S [a]),
-               -- where S is a type function.  In fact, exprIsConApp
-               -- will probably not be called in such circumstances,
-               -- but there't nothing wrong with it 
-
-               | otherwise  ->
-    let
-       tc_arity = tyConArity from_tc
-
-        (univ_args, rest1)        = splitAt tc_arity dc_args
-        (ex_args, rest2)          = splitAt n_ex_tvs rest1
-       (co_args_spec, rest3)     = splitAt n_cos_spec rest2
-       (co_args_theta, val_args) = splitAt n_cos_theta rest3
-
-        arg_tys            = dataConRepArgTys dc
-       dc_univ_tyvars      = dataConUnivTyVars dc
-        dc_ex_tyvars        = dataConExTyVars dc
-       dc_eq_spec          = dataConEqSpec dc
-        dc_eq_theta         = dataConEqTheta dc
-        dc_tyvars           = dc_univ_tyvars ++ dc_ex_tyvars
-        n_ex_tvs            = length dc_ex_tyvars
-       n_cos_spec          = length dc_eq_spec
-       n_cos_theta         = length dc_eq_theta
-
-       -- Make the "theta" from Fig 3 of the paper
-        gammas              = decomposeCo tc_arity co
-        new_tys             = gammas ++ map (\ (Type t) -> t) ex_args
-        theta               = zipOpenTvSubst dc_tyvars new_tys
-
-          -- First we cast the existential coercion arguments
-        cast_co_spec (tv, ty) co 
-          = cast_co_theta (mkEqPred (mkTyVarTy tv, ty)) co
-        cast_co_theta eqPred (Type co) 
-          | (ty1, ty2) <- getEqPredTys eqPred
-          = Type $ mkSymCoercion (substTy theta ty1)
-                  `mkTransCoercion` co
-                  `mkTransCoercion` (substTy theta ty2)
-        new_co_args = zipWith cast_co_spec  dc_eq_spec  co_args_spec ++
-                      zipWith cast_co_theta dc_eq_theta co_args_theta
-  
-          -- ...and now value arguments
-       new_val_args = zipWith cast_arg arg_tys val_args
-       cast_arg arg_ty arg = mkCoerce (substTy theta arg_ty) arg
-
-    in
-    ASSERT( length univ_args == tc_arity )
-    ASSERT( from_tc == dataConTyCon dc )
-    ASSERT( and (zipWith coreEqType [t | Type t <- univ_args] from_tc_arg_tys) )
-    ASSERT( all isTypeArg (univ_args ++ ex_args) )
-    ASSERT2( equalLength val_args arg_tys, ppr dc $$ ppr dc_tyvars $$ ppr dc_ex_tyvars $$ ppr arg_tys $$ ppr dc_args $$ ppr univ_args $$ ppr ex_args $$ ppr val_args $$ ppr arg_tys  )
-
-    Just (dc, map Type to_tc_arg_tys ++ ex_args ++ new_co_args ++ new_val_args)
-    }}
-
-{-
--- We do not want to tell the world that we have a
--- Cons, to *stop* Case of Known Cons, which removes
--- the TickBox.
-exprIsConApp_maybe (Note (TickBox {}) expr)
-  = Nothing
-exprIsConApp_maybe (Note (BinaryTickBox {}) expr)
-  = Nothing
--}
-
-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,
-         isExpandableUnfolding unf
-       = exprIsConApp_maybe (unfoldingTemplate unf)
-
-    analyse _ = Nothing
 \end{code}
 
-
-
 %************************************************************************
 %*                                                                     *
-\subsection{Equality}
+         Equality
 %*                                                                     *
 %************************************************************************
 
@@ -928,7 +980,8 @@ cheapEqExpr :: Expr b -> Expr b -> Bool
 
 cheapEqExpr (Var v1)   (Var v2)   = v1==v2
 cheapEqExpr (Lit lit1) (Lit lit2) = lit1 == lit2
-cheapEqExpr (Type t1)  (Type t2)  = t1 `coreEqType` t2
+cheapEqExpr (Type t1) (Type t2) = t1 `eqType` t2
+cheapEqExpr (Coercion c1) (Coercion c2) = c1 `coreEqCoercion` c2
 
 cheapEqExpr (App f1 a1) (App f2 a2)
   = f1 `cheapEqExpr` f2 && a1 `cheapEqExpr` a2
@@ -937,17 +990,102 @@ cheapEqExpr (Cast e1 t1) (Cast e2 t2)
   = e1 `cheapEqExpr` e2 && t1 `coreEqCoercion` t2
 
 cheapEqExpr _ _ = False
+\end{code}
 
+\begin{code}
 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 (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}
 
+\begin{code}
+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}
+    
+\begin{code}
+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
+
+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
+
+    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
+
+    go _ _ _ = False
+
+    -----------
+    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}
+locallyBoundL, locallyBoundR :: RnEnv2 -> Var -> Bool
+locallyBoundL rn_env v = inRnEnvL rn_env v
+locallyBoundR rn_env v = inRnEnvR rn_env v
+\end{code}
 
 
 %************************************************************************
@@ -963,19 +1101,20 @@ coreBindsSize bs = foldr ((+) . bindSize) 0 bs
 exprSize :: CoreExpr -> Int
 -- ^ 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
@@ -998,6 +1137,55 @@ 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}
 
 %************************************************************************
 %*                                                                     *
@@ -1038,15 +1226,17 @@ 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 _   (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_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 
@@ -1055,6 +1245,13 @@ fast_hash_type env ty
                                              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)
 
@@ -1063,6 +1260,157 @@ 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}
@@ -1081,7 +1429,7 @@ and 'execute' it rather than allocating it statically.
 -- | 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 :: PackageId -> CoreExpr -> Bool
+rhsIsStatic :: (Name -> Bool) -> CoreExpr -> Bool
 -- It's called (i) in TidyPgm.hasCafRefs to decide if the rhs is, or
 -- 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
@@ -1131,21 +1479,19 @@ 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).
 
-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 _      (Note (SCC _) _) = False
-  is_static in_arg (Note _ e)       = is_static in_arg e
-  is_static in_arg (Cast e _)       = 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 _      (Lit lit)
     = case lit of
@@ -1164,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)  
@@ -1186,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 _) _) _          = False
-    go (Note _ f)       n_val_args = go f n_val_args
-    go (Cast e _)       n_val_args = go e n_val_args
-
-    go _                _          = 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