Add {-# OPTIONS_GHC -w #-} and some blurb to all compiler modules
[ghc-hetmet.git] / compiler / coreSyn / CoreUtils.lhs
index e737348..b58825b 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_GHC -w #-}
+-- 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/WorkingConventions#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,
@@ -31,52 +40,48 @@ module CoreUtils (
        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
 #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, isDictId
-                       )
-import IdInfo          ( GlobalIdDetails(..), megaSeqIdInfo )
-import NewDemand       ( appIsBottom )
-import Type            ( Type, mkFunTy, mkForAllTy, splitFunTy_maybe,
-                         splitFunTy, tcEqTypeX,
-                         applyTys, isUnLiftedType, seqType, mkTyVarTy,
-                         splitForAllTy_maybe, isForAllTy, splitRecNewType_maybe, 
-                         splitTyConApp_maybe, coreEqType, funResultTy, applyTy
-                       )
-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 PackageConfig
+import Unique
 import Outputable
-import DynFlags                ( DynFlags, DynFlag(Opt_DictsCheap), dopt )
-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}
 
 
@@ -89,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 alts)  = ty
+exprType (Cast e co)        = snd (coercionKind co)
+exprType (Note other_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
@@ -145,7 +150,7 @@ applyTypeToArgs e op_ty (Type ty : args)
 applyTypeToArgs e op_ty (other_arg : 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}
 
 
@@ -161,7 +166,6 @@ 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
@@ -197,18 +201,24 @@ 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}
@@ -219,6 +229,7 @@ mkSCC cc (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}
 
@@ -256,9 +267,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
@@ -313,6 +326,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 lit) args = ASSERT( null args ) []
+trimConArgs (DataAlt dc) args = dropList (dataConUnivTyVars dc) args
 \end{code}
 
 
@@ -353,6 +378,7 @@ exprIsTrivial (Lit lit)    = litIsTrivial lit
 exprIsTrivial (App e arg)  = not (isRuntimeArg arg) && exprIsTrivial e
 exprIsTrivial (Note (SCC _) e) = False         -- See notes above
 exprIsTrivial (Note _       e) = exprIsTrivial e
+exprIsTrivial (Cast e co)  = exprIsTrivial e
 exprIsTrivial (Lam b body) = not (isRuntimeVar b) && exprIsTrivial body
 exprIsTrivial other       = False
 \end{code}
@@ -375,6 +401,7 @@ exprIsDupable (Var v)               = True
 exprIsDupable (Lit lit)        = litIsDupable lit
 exprIsDupable (Note InlineMe e) = True
 exprIsDupable (Note _ e)        = exprIsDupable e
+exprIsDupable (Cast e co)       = exprIsDupable e
 exprIsDupable expr          
   = go expr 0
   where
@@ -418,14 +445,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 lit)        = True
+exprIsCheap (Type _)          = True
+exprIsCheap (Var _)           = True
+exprIsCheap (Note InlineMe e) = True
+exprIsCheap (Note _ e)        = exprIsCheap e
+exprIsCheap (Cast e co)       = exprIsCheap e
+exprIsCheap (Lam x e)         = isRuntimeVar x || exprIsCheap e
+exprIsCheap (Case e _ _ alts) = exprIsCheap e && 
+                               and [exprIsCheap rhs | (_,_,rhs) <- alts]
        -- Experimentally, treat (case x of ...) as cheap
        -- (and case __coerce x etc.)
        -- This improves arities of overloaded functions where
@@ -436,43 +464,51 @@ exprIsCheap (Let (NonRec x _) e)
        -- 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 f) [] = True       -- Just a type application of a variable
+                               -- (f t1 t2 t3) counts as WHNF
+    go (Var f) args
+       = case globalIdDetails f of
+               RecordSelId {} -> go_sel args
+               ClassOpId _    -> go_sel args
+               PrimOpId op    -> go_primop op args
+
+               DataConWorkId _ -> go_pap args
+               other | length args < idArity f -> go_pap args
+
+               other -> isBottomingId f
                        -- 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 other args = 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 other = 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
@@ -488,6 +524,9 @@ It returns True iff
        soon, 
        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
@@ -502,10 +541,13 @@ 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 co) = exprOkForSpeculation e
 exprOkForSpeculation other_expr
   = case collectArgs other_expr of
        (Var f, args) -> spec_ok (globalIdDetails f) args
@@ -556,6 +598,7 @@ exprIsBottom e = go 0 e
               where
                -- n is the number of args
                 go n (Note _ e)     = go n e
+                 go n (Cast e co)    = go n e
                 go n (Let _ e)      = go n e
                 go n (Case e _ _ _) = go 0 e   -- Just check the scrut
                 go n (App e _)      = go (n+1) e
@@ -587,8 +630,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}
@@ -602,70 +645,195 @@ 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 l)         = True
+exprIsHNF (Type ty)       = True       -- Types are honorary Values; 
+                                       -- we don't mind copying them
+exprIsHNF (Lam b e)       = isRuntimeVar b || exprIsHNF e
+exprIsHNF (Note _ e)      = exprIsHNF e
+exprIsHNF (Cast e co)      = exprIsHNF e
 exprIsHNF (App e (Type _)) = exprIsHNF e
 exprIsHNF (App e a)        = app_is_value e [a]
-exprIsHNF other             = False
+exprIsHNF other                   = False
 
 -- There is at least one value argument
 app_is_value (Var fun) args
-  |  isDataConWorkId fun                       -- Constructor apps are values
-  || idArity fun > valArgCount args    -- Under-applied function
-  = check_args (idType fun) args
-app_is_value (App f a) as = app_is_value f (a:as)
-app_is_value other     as = False
-
-       -- 'check_args' checks that unlifted-type args
-       -- are in fact guaranteed non-divergent
-check_args fun_ty []             = True
-check_args fun_ty (Type _ : args) = case splitForAllTy_maybe fun_ty of
-                                     Just (_, ty) -> check_args ty args
-check_args fun_ty (arg : args)
-  | isUnLiftedType arg_ty = exprOkForSpeculation arg
-  | otherwise            = check_args res_ty args
-  where
-    (arg_ty, res_ty) = splitFunTy fun_ty
+  = idArity fun > valArgCount args     -- Under-applied function
+    ||  isDataConWorkId fun            --  or data constructor
+app_is_value (Note n 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 other      as = False
 \end{code}
 
 \begin{code}
+-- 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 PushC 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, val_args) = splitAt n_cos rest2
+
+        arg_tys            = dataConRepArgTys dc
+       dc_univ_tyvars      = dataConUnivTyVars dc
+        dc_ex_tyvars        = dataConExTyVars dc
+       dc_eq_spec          = dataConEqSpec dc
+        dc_tyvars           = dc_univ_tyvars ++ dc_ex_tyvars
+        n_ex_tvs            = length dc_ex_tyvars
+       n_cos               = length dc_eq_spec
+
+       -- 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 (tv,ty) (Type co) = Type $ mkSymCoercion (substTyVar theta tv)
+                                          `mkTransCoercion` co
+                                          `mkTransCoercion` (substTy theta ty)
+        new_co_args = zipWith cast_co dc_eq_spec co_args
+  
+          -- ...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
@@ -812,6 +980,8 @@ arityType dflags (Note n e) = arityType dflags e
 --  | ok_note n = arityType dflags e
 --  | otherwise = ATop
 
+arityType dflags (Cast e co) = arityType dflags e
+
 arityType dflags (Var v) 
   = mk (idArity v) (arg_tys (idType v))
   where
@@ -922,7 +1092,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
@@ -930,6 +1101,7 @@ manifestArity :: CoreExpr -> Arity
 manifestArity (Lam v e) | isId v    = 1 + manifestArity e
                        | otherwise = manifestArity e
 manifestArity (Note _ e)           = manifestArity e
+manifestArity (Cast e _)            = manifestArity e
 manifestArity e                            = 0
 
 -- etaExpand deals with for-alls. For example:
@@ -976,9 +1148,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 {
@@ -995,11 +1173,10 @@ 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
@@ -1042,6 +1219,7 @@ exprArity e = go e
              go (Lam x e) | isId x        = go e + 1
                           | otherwise     = go e
              go (Note n e)                = go e
+              go (Cast e _)                = go e
              go (App e (Type t))          = go e
              go (App f a) | exprIsCheap a = (go f - 1) `max` 0
                -- NB: exprIsCheap a!  
@@ -1080,6 +1258,7 @@ exprIsBig (Lit _)      = False
 exprIsBig (Var v)      = False
 exprIsBig (Type t)     = False
 exprIsBig (App f a)    = exprIsBig f || exprIsBig a
+exprIsBig (Cast e _)   = exprIsBig e   -- Hopefully coercions are not too big!
 exprIsBig other               = True
 \end{code}
 
@@ -1118,13 +1297,13 @@ tcEqExprX env (Case e1 v1 t1 a1)
                                       env' = rnBndr2 env v1 v2
 
 tcEqExprX env (Note n1 e1) (Note n2 e2) = eq_note env n1 n2 && tcEqExprX env e1 e2
+tcEqExprX env (Cast e1 co1) (Cast e2 co2) = tcEqTypeX env co1 co2 && tcEqExprX env e1 e2
 tcEqExprX env (Type t1)    (Type t2)    = tcEqTypeX env t1 t2
 tcEqExprX env e1               e2      = False
                                         
 eq_alt env (c1,vs1,r1) (c2,vs2,r2) = c1==c2 && tcEqExprX (rnBndrs2 env vs1  vs2) r1 r2
 
 eq_note env (SCC cc1)      (SCC cc2)      = cc1 == cc2
-eq_note env (Coerce t1 f1) (Coerce t2 f2) = tcEqTypeX env t1 t2 && tcEqTypeX env f1 f2
 eq_note env (CoreNote s1)  (CoreNote s2)  = s1 == s2
 eq_note env other1            other2     = False
 \end{code}
@@ -1149,14 +1328,14 @@ 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 (SCC cc)       = cc `seq` 1
-noteSize (Coerce t1 t2) = seqType t1 `seq` seqType t2 `seq` 1
 noteSize InlineMe       = 1
 noteSize (CoreNote s)   = s `seq` 1  -- hdaume: core annotations
-
 varSize :: Var -> Int
 varSize b  | isTyVar b = 1
           | otherwise = seqType (idType b)             `seq`
@@ -1182,30 +1361,59 @@ 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 co)             = hash_expr env e
+hash_expr env (Var v)                = hashVar env v
+hash_expr env (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,r):_)) 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 env (Type t)               = 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 env (Var v)             = hashVar env v
+fast_hash_expr env (Type t)    = fast_hash_type env t
+fast_hash_expr env (Lit lit)   = fromIntegral (hashLiteral lit)
+fast_hash_expr env (Cast e co)  = fast_hash_expr env e
+fast_hash_expr env (Note n e)   = fast_hash_expr env e
+fast_hash_expr env (App f a)    = fast_hash_expr env a -- A bit idiosyncratic ('a' not 'f')!
+fast_hash_expr env other        = 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}
 
 %************************************************************************
@@ -1223,7 +1431,7 @@ 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.
@@ -1284,7 +1492,7 @@ rhsIsStatic :: HomeModules -> CoreExpr -> Bool
 -- 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
@@ -1293,6 +1501,7 @@ rhsIsStatic hmods rhs = is_static False rhs
   
   is_static in_arg (Note (SCC _) e) = False
   is_static in_arg (Note _ e)       = is_static in_arg e
+  is_static in_arg (Cast e co)      = is_static in_arg e
   
   is_static in_arg (Lit lit)
     = case lit of
@@ -1311,7 +1520,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)  
@@ -1335,6 +1544,7 @@ rhsIsStatic hmods rhs = is_static False rhs
 
     go (Note (SCC _) f) n_val_args = False
     go (Note _ f) n_val_args       = go f n_val_args
+    go (Cast e co) n_val_args      = go e n_val_args
 
     go other n_val_args = False