Remove static flag opt_RuntimeTypes (has not been used in years)
[ghc-hetmet.git] / compiler / coreSyn / CoreUtils.lhs
index f82435b..2599f4a 100644 (file)
@@ -1,17 +1,26 @@
 %
+% (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
+
 module CoreUtils (
        -- Construction
-       mkInlineMe, mkSCC, mkCoerce, mkCoerce2,
+       mkInlineMe, mkSCC, mkCoerce, mkCoerceI,
        bindNonRec, needsCaseBinding,
        mkIfThenElse, mkAltExpr, mkPiType, mkPiTypes,
 
        -- Taking expressions apart
-       findDefault, findAlt, isDefaultAlt, mergeAlts,
+       findDefault, findAlt, isDefaultAlt, mergeAlts, trimConArgs,
 
        -- Properties of expressions
        exprType, coreAltType,
@@ -25,57 +34,54 @@ module CoreUtils (
        exprEtaExpandArity, etaExpand, 
 
        -- Size
-       coreBindsSize,
+       coreBindsSize, exprSize,
 
        -- Hashing
        hashExpr,
 
        -- Equality
-       cheapEqExpr, tcEqExpr, tcEqExprX, applyTypeToArgs, applyTypeToArg
+       cheapEqExpr, tcEqExpr, tcEqExprX, applyTypeToArgs, applyTypeToArg,
+
+        dataConOrigInstPat, dataConRepInstPat, dataConRepFSInstPat
     ) where
 
 #include "HsVersions.h"
 
-
-import GLAEXTS         -- For `xori` 
-
 import CoreSyn
-import CoreFVs         ( exprFreeVars )
-import PprCore         ( pprCoreExpr )
-import Var             ( Var )
-import VarSet          ( unionVarSet )
+import CoreFVs
+import PprCore
+import Var
+import SrcLoc
+import VarSet
 import VarEnv
-import Name            ( hashName )
-import Packages                ( HomeModules )
+import Name
+import Module
 #if mingw32_TARGET_OS
-import Packages                ( isDllName )
+import Packages
 #endif
-import Literal         ( hashLiteral, literalType, litIsDupable, 
-                         litIsTrivial, isZeroLit, Literal( MachLabel ) )
-import DataCon         ( DataCon, dataConRepArity, dataConInstArgTys,
-                         isVanillaDataCon, dataConTyCon )
-import PrimOp          ( PrimOp(..), primOpOkForSpeculation, primOpIsCheap )
-import Id              ( Id, idType, globalIdDetails, idNewStrictness, 
-                         mkWildId, idArity, idName, idUnfolding, idInfo,
-                         isOneShotBndr, isStateHackType, isDataConWorkId_maybe, mkSysLocal,
-                         isDataConWorkId, isBottomingId
-                       )
-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
-                       )
-import TyCon           ( tyConArity )
-import TysWiredIn      ( boolTy, trueDataCon, falseDataCon )
-import CostCentre      ( CostCentre )
-import BasicTypes      ( Arity )
-import Unique          ( Unique )
+import Literal
+import DataCon
+import PrimOp
+import Id
+import IdInfo
+import NewDemand
+import Type
+import Coercion
+import TyCon
+import TysWiredIn
+import CostCentre
+import BasicTypes
+import Unique
 import Outputable
-import TysPrim         ( alphaTy )     -- Debugging only
-import Util             ( equalLength, lengthAtLeast, foldl2 )
+import DynFlags
+import TysPrim
+import FastString
+import Maybes
+import Util
+import Data.Word
+import Data.Bits
+
+import GHC.Exts                -- For `xori` 
 \end{code}
 
 
@@ -88,13 +94,13 @@ import Util             ( equalLength, lengthAtLeast, foldl2 )
 \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 (Note (Coerce ty _) e) = ty  --  **! should take usage from e
-exprType (Note other_note e)    = exprType e
-exprType (Lam binder expr)      = mkPiType binder (exprType expr)
+exprType (Var var)          = idType var
+exprType (Lit lit)          = literalType lit
+exprType (Let _ body)       = exprType body
+exprType (Case _ _ ty _)     = ty
+exprType (Cast _ co)         = snd (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
@@ -124,13 +130,13 @@ mkPiType v ty
 \begin{code}
 applyTypeToArg :: Type -> CoreExpr -> 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
+applyTypeToArgs _ op_ty [] = op_ty
 
 applyTypeToArgs e op_ty (Type ty : args)
   =    -- Accumulate type arguments so we can instantiate all at once
@@ -141,10 +147,10 @@ applyTypeToArgs e op_ty (Type ty : args)
                                where
                                  op_ty' = applyTys op_ty (reverse rev_tys)
 
-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)
+       Nothing -> pprPanic "applyTypeToArgs" (pprCoreExpr e $$ ppr op_ty)
 \end{code}
 
 
@@ -160,17 +166,10 @@ mkNote removes redundant coercions, and SCCs where possible
 \begin{code}
 #ifdef UNUSED
 mkNote :: Note -> CoreExpr -> CoreExpr
-mkNote (Coerce to_ty from_ty) expr = mkCoerce2 to_ty from_ty expr
 mkNote (SCC cc)        expr               = mkSCC cc expr
 mkNote InlineMe expr              = mkInlineMe expr
 mkNote note     expr              = Note note expr
 #endif
-
--- Slide InlineCall in around the function
---     No longer necessary I think (SLPJ Apr 99)
--- mkNote InlineCall (App f a) = App (mkNote InlineCall f) a
--- mkNote InlineCall (Var v)   = Note InlineCall (Var v)
--- mkNote InlineCall expr      = expr
 \end{code}
 
 Drop trivial InlineMe's.  This is somewhat important, because if we have an unfolding
@@ -195,6 +194,7 @@ 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 :: CoreExpr -> CoreExpr
 mkInlineMe (Var v) = Var v
 mkInlineMe e      = Note InlineMe e
 \end{code}
@@ -202,28 +202,35 @@ mkInlineMe e         = Note InlineMe e
 
 
 \begin{code}
-mkCoerce :: Type -> CoreExpr -> CoreExpr
-mkCoerce to_ty expr = mkCoerce2 to_ty (exprType expr) expr
-
-mkCoerce2 :: Type -> Type -> CoreExpr -> CoreExpr
-mkCoerce2 to_ty from_ty (Note (Coerce to_ty2 from_ty2) expr)
-  = ASSERT( from_ty `coreEqType` to_ty2 )
-    mkCoerce2 to_ty from_ty2 expr
-
-mkCoerce2 to_ty from_ty expr
-  | to_ty `coreEqType` from_ty = expr
-  | otherwise             = ASSERT( from_ty `coreEqType` exprType expr )
-                            Note (Coerce to_ty from_ty) expr
+mkCoerceI :: CoercionI -> CoreExpr -> CoreExpr
+mkCoerceI IdCo e = e
+mkCoerceI (ACo co) e = mkCoerce co e
+
+mkCoerce :: Coercion -> CoreExpr -> CoreExpr
+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
+
+mkCoerce co expr 
+  = let (from_ty, _to_ty) = coercionKind co in
+--    if to_ty `coreEqType` 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))
+         (Cast expr co)
 \end{code}
 
 \begin{code}
 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
+mkSCC cc (Cast e co)        = Cast (mkSCC cc e) co -- Move _scc_ inside cast
 mkSCC cc expr              = Note (SCC cc) expr
 \end{code}
 
@@ -250,6 +257,7 @@ bindNonRec bndr rhs body
   | needsCaseBinding (idType bndr) rhs = Case rhs bndr (exprType body) [(DEFAULT,[],body)]
   | otherwise                         = Let (NonRec bndr rhs) body
 
+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,
@@ -261,9 +269,11 @@ 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 (DataAlt con) args inst_tys
-  = mkConApp con (map Type inst_tys ++ map varToCoreExpr args)
+  = mkConApp con (map Type inst_tys ++ varsToCoreExprs args)
 mkAltExpr (LitAlt lit) [] []
   = Lit lit
+mkAltExpr (LitAlt _) _ _ = panic "mkAltExpr LitAlt"
+mkAltExpr DEFAULT _ _ = panic "mkAltExpr DEFAULT"
 
 mkIfThenElse :: CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
 mkIfThenElse guard then_expr else_expr
@@ -292,7 +302,7 @@ findAlt :: AltCon -> [CoreAlt] -> CoreAlt
 findAlt con alts
   = case alts of
        (deflt@(DEFAULT,_,_):alts) -> go alts deflt
-       other                      -> go alts panic_deflt
+        _                          -> go alts panic_deflt
   where
     panic_deflt = pprPanic "Missing alternative" (ppr con $$ vcat (map ppr alts))
 
@@ -305,7 +315,7 @@ findAlt con alts
 
 isDefaultAlt :: CoreAlt -> Bool
 isDefaultAlt (DEFAULT, _, _) = True
-isDefaultAlt other          = False
+isDefaultAlt _               = False
 
 ---------------------------------
 mergeAlts :: [CoreAlt] -> [CoreAlt] -> [CoreAlt]
@@ -318,6 +328,18 @@ 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}
 
 
@@ -352,14 +374,16 @@ SCC notes.  We do not treat (_scc_ "foo" x) as trivial, because
   b) see the note [SCC-and-exprIsTrivial] in Simplify.simplLazyBind
 
 \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 :: CoreExpr -> Bool
+exprIsTrivial (Var _)          = True        -- See notes above
+exprIsTrivial (Type _)         = 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 (Lam b body) = not (isRuntimeVar b) && exprIsTrivial body
-exprIsTrivial other       = False
+exprIsTrivial (Cast e _)       = exprIsTrivial e
+exprIsTrivial (Lam b body)     = not (isRuntimeVar b) && exprIsTrivial body
+exprIsTrivial _                = False
 \end{code}
 
 
@@ -375,19 +399,21 @@ exprIsTrivial other          = False
 
 
 \begin{code}
-exprIsDupable (Type _)         = True
-exprIsDupable (Var v)          = True
-exprIsDupable (Lit lit)        = litIsDupable lit
-exprIsDupable (Note InlineMe e) = True
+exprIsDupable :: CoreExpr -> Bool
+exprIsDupable (Type _)          = True
+exprIsDupable (Var _)           = True
+exprIsDupable (Lit lit)         = litIsDupable lit
+exprIsDupable (Note InlineMe _) = True
 exprIsDupable (Note _ e)        = exprIsDupable e
-exprIsDupable expr          
+exprIsDupable (Cast e _)        = exprIsDupable e
+exprIsDupable expr
   = go expr 0
   where
-    go (Var v)   n_args = True
+    go (Var _)   _      = True
     go (App f a) n_args =  n_args < dupAppSize
                        && exprIsDupable a
                        && go f (n_args+1)
-    go other n_args    = False
+    go _         _      = False
 
 dupAppSize :: Int
 dupAppSize = 4         -- Size of application we are prepared to duplicate
@@ -423,14 +449,15 @@ because sharing will make sure it is only evaluated once.
 
 \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 (Lam x e)               = isRuntimeVar x || exprIsCheap e
-exprIsCheap (Case e _ _ alts)       = exprIsCheap e && 
-                                   and [exprIsCheap rhs | (_,_,rhs) <- alts]
+exprIsCheap (Lit _)           = True
+exprIsCheap (Type _)          = True
+exprIsCheap (Var _)           = True
+exprIsCheap (Note InlineMe _) = True
+exprIsCheap (Note _ e)        = exprIsCheap e
+exprIsCheap (Cast e _)        = exprIsCheap e
+exprIsCheap (Lam x e)         = isRuntimeVar x || exprIsCheap e
+exprIsCheap (Case e _ _ alts) = exprIsCheap e && 
+                               and [exprIsCheap rhs | (_,_,rhs) <- alts]
        -- Experimentally, treat (case x of ...) as cheap
        -- (and case __coerce x etc.)
        -- This improves arities of overloaded functions where
@@ -438,46 +465,54 @@ exprIsCheap (Case e _ _ alts)       = exprIsCheap e &&
 exprIsCheap (Let (NonRec x _) e)  
       | isUnLiftedType (idType x) = exprIsCheap e
       | otherwise                = False
-       -- strict lets always have cheap right hand sides, and
-       -- do no allocation.
+       -- strict lets always have cheap right hand sides,
+       -- and do no allocation.
 
-exprIsCheap other_expr 
-  = go other_expr 0 True
+exprIsCheap other_expr         -- Applications and variables
+  = go other_expr []
   where
-    go (Var f) n_args args_cheap 
-       = (idAppIsCheap f n_args && args_cheap)
-                       -- A constructor, cheap primop, or partial application
-
-         || idAppIsBottom f n_args 
+       -- Accumulate value arguments, then decide
+    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 globalIdDetails f of
+               RecordSelId {} -> go_sel args
+               ClassOpId _    -> go_sel args
+               PrimOpId op    -> go_primop op args
+
+               DataConWorkId _ -> go_pap args
+               _ | length args < idArity f -> go_pap args
+
+               _ -> isBottomingId f
                        -- Application of a function which
                        -- always gives bottom; we treat this as cheap
                        -- because it certainly doesn't need to be shared!
        
-    go (App f a) n_args args_cheap 
-       | not (isRuntimeArg a) = go f n_args      args_cheap
-       | otherwise            = go f (n_args + 1) (exprIsCheap a && args_cheap)
-
-    go other   n_args args_cheap = False
-
-idAppIsCheap :: Id -> Int -> Bool
-idAppIsCheap id n_val_args 
-  | n_val_args == 0 = True     -- Just a type application of
-                               -- a variable (f t1 t2 t3)
-                               -- counts as WHNF
-  | otherwise 
-  = case globalIdDetails id of
-       DataConWorkId _ -> True
-       RecordSelId {}  -> n_val_args == 1      -- I'm experimenting with making record selection
-       ClassOpId _     -> n_val_args == 1      -- 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)
-
-       PrimOpId op   -> primOpIsCheap op       -- 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
-       other         -> n_val_args < idArity id
+    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_primop op args = primOpIsCheap op && all exprIsCheap 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 _     = 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
@@ -494,6 +529,8 @@ It returns True iff
        without raising an exception,
        without causing a side effect (e.g. writing a mutable variable)
 
+NB: if exprIsHNF e, then exprOkForSpecuation e
+
 E.G.
        let x = case y# +# 1# of { r# -> I# r# }
        in E
@@ -508,17 +545,20 @@ side effects, and can't diverge or raise an exception.
 
 \begin{code}
 exprOkForSpeculation :: CoreExpr -> Bool
-exprOkForSpeculation (Lit _)    = True
-exprOkForSpeculation (Type _)   = True
-exprOkForSpeculation (Var v)    = isUnLiftedType (idType v)
-exprOkForSpeculation (Note _ e) = exprOkForSpeculation e
+exprOkForSpeculation (Lit _)     = True
+exprOkForSpeculation (Type _)    = True
+    -- Tick boxes are *not* suitable for speculation
+exprOkForSpeculation (Var v)     = isUnLiftedType (idType v)
+                                && not (isTickBoxOp v)
+exprOkForSpeculation (Note _ e)  = exprOkForSpeculation e
+exprOkForSpeculation (Cast e _)  = exprOkForSpeculation e
 exprOkForSpeculation other_expr
   = case collectArgs other_expr of
        (Var f, args) -> spec_ok (globalIdDetails f) args
-       other         -> False
+        _             -> 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
@@ -536,7 +576,7 @@ exprOkForSpeculation other_expr
                                -- A bit conservative: we don't really need
                                -- to care about lazy arguments, but this is easy
 
-    spec_ok other args = False
+    spec_ok _ _ = False
 
 isDivOp :: PrimOp -> Bool
 -- True of dyadic operators that can fail 
@@ -552,23 +592,24 @@ isDivOp IntegerQuotRemOp = True
 isDivOp IntegerDivModOp  = True
 isDivOp FloatDivOp       = True
 isDivOp DoubleDivOp      = True
-isDivOp other           = False
+isDivOp _                = 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 (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
+               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
@@ -593,8 +634,8 @@ 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
+Suppose (f x) diverges; then C (f x) is not a value.  However this can't 
+happen: see CoreSyn Note [CoreSyn let/app invariant].  Args of unboxed
 type must be ok-for-speculation (or trivial).
 
 \begin{code}
@@ -608,70 +649,206 @@ exprIsHNF (Var v)        -- NB: There are no value args at this point
        -- 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 (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 other             = False
+exprIsHNF _                = False
 
 -- There is at least one value argument
+app_is_value :: CoreExpr -> [CoreArg] -> Bool
 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
+  = 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
 \end{code}
 
 \begin{code}
+dataConRepInstPat, dataConOrigInstPat :: [Unique] -> DataCon -> [Type] -> ([TyVar], [CoVar], [Id])
+dataConRepFSInstPat :: [FastString] -> [Unique] -> DataCon -> [Type] -> ([TyVar], [CoVar], [Id])
+-- These InstPat functions go here to avoid circularity between DataCon and 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
+-- dataConInstPat arg_fun fss us con inst_tys returns a triple 
+-- (ex_tvs, co_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)
+--
+-- Example.
+--  The following constructor T1
+--
+--  data T a where
+--    T1 :: forall b. Int -> b -> T(a,b)
+--    ...
+--
+--  has representation type 
+--   forall a. forall a1. forall b. (a :=: (a1,b)) => 
+--     Int -> b -> T a
+--
+--  dataConInstPat fss us T1 (a1',b') will return
+--
+--  ([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)
+  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
+
+    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'
+
+      -- 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 fs
+        kind     = tyVarKind var
+
+      -- 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
+    arg_ids = zipWith3 mk_id_var id_uniqs id_fss arg_tys
+
 exprIsConApp_maybe :: CoreExpr -> Maybe (DataCon, [CoreExpr])
-exprIsConApp_maybe (Note (Coerce to_ty from_ty) expr)
-  =    -- 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
+-- Returns (Just (dc, [x1..xn])) if the argument expression is 
+-- a constructor application of the form (dc x1 .. xn)
+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, args)   -> 
-  
+       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 (tc, tc_arg_tys) | tc /= dataConTyCon dc     -> Nothing
-                             | not (isVanillaDataCon dc) -> Nothing
-                             | otherwise                 ->
-               -- Type constructor must match
-               -- We knock out existentials to keep matters simple(r)
+       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
-       arity            = tyConArity tc
-       val_args         = drop arity args
-       to_arg_tys       = dataConInstArgTys dc tc_arg_tys
-       mk_coerce ty arg = mkCoerce ty arg
-       new_val_args     = zipWith mk_coerce to_arg_tys val_args
+       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( all isTypeArg (take arity args) )
-    ASSERT( equalLength val_args to_arg_tys )
-    Just (dc, map Type tc_arg_tys ++ new_val_args)
+    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
@@ -700,7 +877,7 @@ exprIsConApp_maybe expr = analyse (collectArgs expr)
          isCheapUnfolding unf
        = exprIsConApp_maybe (unfoldingTemplate unf)
 
-    analyse other = Nothing
+    analyse _ = Nothing
 \end{code}
 
 
@@ -712,7 +889,7 @@ exprIsConApp_maybe expr = analyse (collectArgs expr)
 %************************************************************************
 
 \begin{code}
-exprEtaExpandArity :: CoreExpr -> Arity
+exprEtaExpandArity :: DynFlags -> CoreExpr -> Arity
 {- The Arity returned is the number of value args the 
    thing can be applied to without doing much work
 
@@ -792,7 +969,7 @@ decopose Int to a function type.   Hence the final case in eta_expand.
 -}
 
 
-exprEtaExpandArity e = arityDepth (arityType e)
+exprEtaExpandArity dflags e = arityDepth (arityType dflags e)
 
 -- A limited sort of function type
 data ArityType = AFun Bool ArityType   -- True <=> one-shot
@@ -801,24 +978,27 @@ data ArityType = AFun Bool ArityType      -- True <=> one-shot
 
 arityDepth :: ArityType -> Arity
 arityDepth (AFun _ ty) = 1 + arityDepth ty
-arityDepth ty         = 0
+arityDepth _           = 0
 
-andArityType ABot          at2           = at2
-andArityType ATop          at2           = ATop
+andArityType :: ArityType -> ArityType -> ArityType
+andArityType ABot           at2           = at2
+andArityType ATop           _             = ATop
 andArityType (AFun t1 at1)  (AFun t2 at2) = AFun (t1 && t2) (andArityType at1 at2)
-andArityType at1           at2           = andArityType at2 at1
+andArityType at1            at2           = andArityType at2 at1
 
-arityType :: CoreExpr -> ArityType
+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
 
-arityType (Note n e) = arityType e
+arityType dflags (Note _ e) = arityType dflags e
 --     Not needed any more: etaExpand is cleverer
---  | ok_note n = arityType e
+--  | ok_note n = arityType dflags e
 --  | otherwise = ATop
 
-arityType (Var v) 
+arityType dflags (Cast e _) = arityType dflags e
+
+arityType _ (Var v)
   = mk (idArity v) (arg_tys (idType v))
   where
     mk :: Arity -> [Type] -> ArityType
@@ -828,8 +1008,9 @@ arityType (Var v)
        --              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
-             | otherwise       = ATop
+    mk 0 tys | isBottomingId v                   = ABot
+             | (ty:_) <- 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) [])
 
@@ -840,14 +1021,19 @@ arityType (Var v)
        | otherwise                                = []
 
        -- Lambdas; increase arity
-arityType (Lam x e) | isId x    = AFun (isOneShotBndr x) (arityType e)
-                   | otherwise = arityType e
+arityType dflags (Lam x e)
+  | isId x    = AFun (isOneShotBndr x) (arityType dflags e)
+  | otherwise = arityType dflags e
 
        -- Applications; decrease arity
-arityType (App f (Type _)) = arityType f
-arityType (App f a)       = case arityType f of
-                               AFun one_shot xs | exprIsCheap a -> xs
-                               other                            -> ATop
+arityType dflags (App f (Type _)) = arityType dflags f
+arityType dflags (App f a)
+   = case arityType dflags f of
+       ABot -> ABot    -- If function diverges, ignore argument
+       ATop -> ATop    -- No no info about function
+       AFun _ xs
+               | exprIsCheap a -> xs
+               | otherwise     -> ATop
                                                           
        -- Case/Let; keep arity if either the expression is cheap
        -- or it's a 1-shot lambda
@@ -856,17 +1042,40 @@ arityType (App f a)         = case arityType f of
        --  ===>
        --      f x y = case x of { (a,b) -> e }
        -- The difference is observable using 'seq'
-arityType (Case scrut _ _ alts) = case foldr1 andArityType [arityType rhs | (_,_,rhs) <- alts] of
-                                 xs@(AFun one_shot _) | one_shot -> xs
-                                 xs | exprIsCheap scrut          -> xs
-                                    | otherwise                  -> ATop
-
-arityType (Let b e) = case arityType e of
-                       xs@(AFun one_shot _) | one_shot                       -> xs
-                       xs                   | all exprIsCheap (rhssOfBind b) -> xs
-                                            | otherwise                      -> ATop
-
-arityType other = ATop
+arityType dflags (Case scrut _ _ alts)
+  = case foldr1 andArityType [arityType dflags rhs | (_,_,rhs) <- alts] of
+        xs | exprIsCheap scrut     -> xs
+        AFun one_shot _ | one_shot -> AFun True ATop
+        _                          -> ATop
+
+arityType dflags (Let b e) 
+  = case arityType dflags e of
+        xs              | cheap_bind b -> xs
+        AFun one_shot _ | one_shot     -> AFun True ATop
+        _                              -> 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 _ _ = ATop
 
 {- NOT NEEDED ANY MORE: etaExpand is cleverer
 ok_note InlineMe = False
@@ -903,7 +1112,8 @@ etaExpand :: Arity         -- Result should have this number of value args
 
 etaExpand n us expr ty
   | manifestArity expr >= n = expr             -- The no-op case
-  | otherwise              = eta_expand n us expr ty
+  | otherwise              
+  = eta_expand n us expr ty
   where
 
 -- manifestArity sees how many leading value lambdas there are
@@ -911,7 +1121,8 @@ manifestArity :: CoreExpr -> Arity
 manifestArity (Lam v e) | isId v    = 1 + manifestArity e
                        | otherwise = manifestArity e
 manifestArity (Note _ e)           = manifestArity e
-manifestArity e                            = 0
+manifestArity (Cast e _)            = manifestArity e
+manifestArity _                     = 0
 
 -- etaExpand deals with for-alls. For example:
 --             etaExpand 1 E
@@ -921,8 +1132,9 @@ manifestArity e                        = 0
 --
 -- It deals with coerces too, though they are now rare
 -- so perhaps the extra code isn't worth it
+eta_expand :: Int -> [Unique] -> CoreExpr -> Type -> CoreExpr
 
-eta_expand n us expr ty
+eta_expand n _ 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 
@@ -957,9 +1169,15 @@ eta_expand n us (Lam v body) ty
 --     and round we go
 
 eta_expand n us expr ty
-  = case splitForAllTy_maybe ty of { 
-         Just (tv,ty') -> Lam tv (eta_expand n us (App expr (Type (mkTyVarTy tv))) 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 = setVarName tv (mkSysTvName uniq FSLIT("etaT"))
+                       -- Using tv as a base retains its tyvar/covar-ness
+                    (uniq:us2) = us 
        ; Nothing ->
   
        case splitFunTy_maybe ty of {
@@ -976,17 +1194,17 @@ eta_expand n us expr ty
                --      eta_expand 1 e T
                -- We want to get
                --      coerce T (\x::[T] -> (coerce ([T]->Int) e) x)
-               -- Only try this for recursive newtypes; the non-recursive kind
-               -- are transparent anyway
 
-       case splitRecNewType_maybe ty of {
-         Just ty' -> mkCoerce2 ty ty' (eta_expand n us (mkCoerce2 ty' ty expr) ty') ;
+       case splitNewTypeRepCo_maybe ty of {
+         Just(ty1,co) -> mkCoerce (mkSymCoercion co) 
+                                  (eta_expand n us (mkCoerce 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.
+       -- Otherwise we'd end up with an explicit lambda having a non-function type
        expr
        }}}
 \end{code}
@@ -1015,22 +1233,51 @@ 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.
 
+Note [exprArity invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+exprArity has the following invariant:
+       (exprArity e) = n, then manifestArity (etaExpand e n) = n
+
+That is, if exprArity says "the arity is n" then etaExpand really can get
+"n" manifest lambdas to the top.
+
+Why is this important?  Because 
+  - In TidyPgm we use exprArity to fix the *final arity* of 
+    each top-level Id, and in
+  - In CorePrep we use etaExpand on each rhs, so that the visible lambdas
+    actually match that arity, which in turn means
+    that the StgRhs has the right number of lambdas
+
+An alternative would be to do the eta-expansion in TidyPgm, at least
+for top-level bindings, in which case we would not need the trim_arity
+in exprArity.  That is a less local change, so I'm going to leave it for today!
+
+
 \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 (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
+  where
+    go (Var v)                          = idArity v
+    go (Lam x e) | isId x       = go e + 1
+                | otherwise     = go e
+    go (Note _ e)                = go e
+    go (Cast e co)               = trim_arity (go e) 0 (snd (coercionKind co))
+    go (App e (Type _))          = 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
+
+       -- Note [exprArity invariant]
+    trim_arity n a ty
+       | n==a                                        = a
+       | Just (_, ty') <- splitForAllTy_maybe ty     = trim_arity n a     ty'
+       | Just (_, ty') <- splitFunTy_maybe ty        = trim_arity n (a+1) ty'
+       | Just (ty',_)  <- splitNewTypeRepCo_maybe ty = trim_arity n a     ty'
+       | otherwise                                   = a
 \end{code}
 
 %************************************************************************
@@ -1053,15 +1300,19 @@ cheapEqExpr (Type t1)  (Type t2)  = t1 `coreEqType` t2
 cheapEqExpr (App f1 a1) (App f2 a2)
   = f1 `cheapEqExpr` f2 && a1 `cheapEqExpr` a2
 
+cheapEqExpr (Cast e1 t1) (Cast e2 t2)
+  = e1 `cheapEqExpr` e2 && t1 `coreEqCoercion` t2
+
 cheapEqExpr _ _ = 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 (Var _)      = False
+exprIsBig (Type _)     = False
 exprIsBig (App f a)    = exprIsBig f || exprIsBig a
-exprIsBig other               = True
+exprIsBig (Cast e _)   = exprIsBig e   -- Hopefully coercions are not too big!
+exprIsBig _            = True
 \end{code}
 
 
@@ -1076,7 +1327,7 @@ tcEqExpr e1 e2 = tcEqExprX rn_env e1 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 _   (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)
@@ -1098,17 +1349,18 @@ tcEqExprX env (Case e1 v1 t1 a1)
                                     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 (Type t1)    (Type t2)    = tcEqTypeX env t1 t2
-tcEqExprX env e1               e2      = False
-                                        
+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 _   _             _             = False
+
+eq_alt :: RnEnv2 -> CoreAlt -> CoreAlt -> Bool
 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 (Coerce t1 f1) (Coerce t2 f2) = tcEqTypeX env t1 t2 && tcEqTypeX env f1 f2
-eq_note env InlineCall     InlineCall     = True
-eq_note env (CoreNote s1)  (CoreNote s2)  = s1 == s2
-eq_note env other1            other2     = False
+eq_note :: RnEnv2 -> Note -> Note -> Bool
+eq_note _ (SCC cc1)     (SCC cc2)      = cc1 == cc2
+eq_note _ (CoreNote s1) (CoreNote s2)  = s1 == s2
+eq_note _ _             _              = False
 \end{code}
 
 
@@ -1131,28 +1383,32 @@ 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 (Note n e)      = noteSize n + exprSize e
 exprSize (Type t)        = seqType t `seq` 1
 
+noteSize :: Note -> Int
 noteSize (SCC cc)       = cc `seq` 1
-noteSize (Coerce t1 t2) = seqType t1 `seq` seqType t2 `seq` 1
-noteSize InlineCall     = 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}
 
@@ -1165,30 +1421,60 @@ altSize (c,bs,e) = c `seq` varsSize bs + exprSize e
 
 \begin{code}
 hashExpr :: CoreExpr -> Int
-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 (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)
+-- 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
+-- 
+-- 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
+--
+-- 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.
+
+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_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
+
+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}
 
 %************************************************************************
@@ -1206,14 +1492,15 @@ If this happens we simply make the RHS into an updatable thunk,
 and 'exectute' it rather than allocating it statically.
 
 \begin{code}
-rhsIsStatic :: HomeModules -> CoreExpr -> Bool
+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.
 --
 -- 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
@@ -1263,24 +1550,22 @@ rhsIsStatic :: HomeModules -> CoreExpr -> Bool
 --        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 hmods rhs = is_static False rhs
+rhsIsStatic _this_pkg 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 _      (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 in_arg (Lit lit)
+  is_static _      (Lit lit)
     = case lit of
        MachLabel _ _ -> False
-       other         -> True
+        _             -> 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
@@ -1294,7 +1579,7 @@ rhsIsStatic hmods rhs = is_static False rhs
    where
     go (Var f) n_val_args
 #if mingw32_TARGET_OS
-        | not (isDllName hmods (idName f))
+        | not (isDllName _this_pkg (idName f))
 #endif
        =  saturated_data_con f n_val_args
        || (in_arg && n_val_args == 0)  
@@ -1316,10 +1601,11 @@ rhsIsStatic hmods 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 (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 other n_val_args = False
+    go _                _          = False
 
     saturated_data_con f n_val_args
        = case isDataConWorkId_maybe f of