Merge branch 'master' of ssh://darcs.haskell.org/srv/darcs/ghc into encodingencoding

10 files changed, 296 insertions, 200 deletions

diff --git a/compiler/simplCore/CSE.lhs b/compiler/simplCore/CSE.lhs
index 523431fec0..5bec8f0c3d 100644
--- a/compiler/simplCore/CSE.lhs
+++ b/compiler/simplCore/CSE.lhs
@@ -207,6 +207,7 @@ do_one env (id, rhs)
 
 tryForCSE :: CSEnv -> CoreExpr -> CoreExpr
 tryForCSE _   (Type t) = Type t
+tryForCSE _   (Coercion c) = Coercion c
 tryForCSE env expr     = case lookupCSEnv env expr' of
 			    Just smaller_expr -> smaller_expr
  			    Nothing  	      -> expr'
@@ -215,6 +216,7 @@ tryForCSE env expr     = case lookupCSEnv env expr' of
 
 cseExpr :: CSEnv -> CoreExpr -> CoreExpr
 cseExpr _   (Type t)               = Type t
+cseExpr _   (Coercion co)          = Coercion co
 cseExpr _   (Lit lit)              = Lit lit
 cseExpr env (Var v)		   = Var (lookupSubst env v)
 cseExpr env (App f a)        	   = App (cseExpr env f) (tryForCSE env a)
diff --git a/compiler/simplCore/FloatIn.lhs b/compiler/simplCore/FloatIn.lhs
index b9f44c95c1..48daf7853b 100644
--- a/compiler/simplCore/FloatIn.lhs
+++ b/compiler/simplCore/FloatIn.lhs
@@ -126,14 +126,15 @@ fiExpr :: FloatingBinds		-- Binds we're trying to drop
        -> CoreExprWithFVs	-- Input expr
        -> CoreExpr		-- Result
 
-fiExpr to_drop (_, AnnVar v) = mkCoLets' to_drop (Var v)
-
-fiExpr to_drop (_, AnnType ty) = ASSERT( null to_drop )
-				 Type ty
-fiExpr to_drop (_, AnnCast expr co)
-  = Cast (fiExpr to_drop expr) co	-- Just float in past coercion
-
-fiExpr _ (_, AnnLit lit) = Lit lit
+fiExpr to_drop (_, AnnLit lit)     = ASSERT( null to_drop ) Lit lit
+fiExpr to_drop (_, AnnType ty)     = ASSERT( null to_drop ) Type ty
+fiExpr to_drop (_, AnnVar v)       = mkCoLets' to_drop (Var v)
+fiExpr to_drop (_, AnnCoercion co) = mkCoLets' to_drop (Coercion co)
+fiExpr to_drop (_, AnnCast expr (fvs_co, co))
+  = mkCoLets' (drop_here ++ co_drop) $
+    Cast (fiExpr e_drop expr) co
+  where
+    [drop_here, e_drop, co_drop] = sepBindsByDropPoint False [freeVarsOf expr, fvs_co] to_drop
 \end{code}
 
 Applications: we do float inside applications, mainly because we
@@ -198,7 +199,7 @@ fiExpr to_drop lam@(_, AnnLam _ _)
 
     go seen_one_shot_id [] = seen_one_shot_id
     go seen_one_shot_id (b:bs)
-      | isTyCoVar       b = go seen_one_shot_id bs
+      | isTyVar       b = go seen_one_shot_id bs
       | isOneShotBndr b = go True bs
       | otherwise       = False	 -- Give up at a non-one-shot Id
 \end{code}
diff --git a/compiler/simplCore/FloatOut.lhs b/compiler/simplCore/FloatOut.lhs
index 2a51a2100e..e5db7d93ce 100644
--- a/compiler/simplCore/FloatOut.lhs
+++ b/compiler/simplCore/FloatOut.lhs
@@ -225,6 +225,7 @@ floatRhs lvl arg	-- Used for nested non-rec rhss, and fn args
 -----------------
 floatExpr _ (Var v)   = (zeroStats, emptyFloats, Var v)
 floatExpr _ (Type ty) = (zeroStats, emptyFloats, Type ty)
+floatExpr _ (Coercion co) = (zeroStats, emptyFloats, Coercion co)
 floatExpr _ (Lit lit) = (zeroStats, emptyFloats, Lit lit)
 	  
 floatExpr lvl (App e a)
diff --git a/compiler/simplCore/LiberateCase.lhs b/compiler/simplCore/LiberateCase.lhs
index 2b190621d6..fe1f758551 100644
--- a/compiler/simplCore/LiberateCase.lhs
+++ b/compiler/simplCore/LiberateCase.lhs
@@ -199,6 +199,7 @@ libCase :: LibCaseEnv
 libCase env (Var v)             = libCaseId env v
 libCase _   (Lit lit)           = Lit lit
 libCase _   (Type ty)           = Type ty
+libCase _   (Coercion co)       = Coercion co
 libCase env (App fun arg)       = App (libCase env fun) (libCase env arg)
 libCase env (Note note body)    = Note note (libCase env body)
 libCase env (Cast e co)         = Cast (libCase env e) co
diff --git a/compiler/simplCore/OccurAnal.lhs b/compiler/simplCore/OccurAnal.lhs
index 7692b628ab..ba7d19295b 100644
--- a/compiler/simplCore/OccurAnal.lhs
+++ b/compiler/simplCore/OccurAnal.lhs
@@ -19,17 +19,18 @@ module OccurAnal (
 
 import CoreSyn
 import CoreFVs
-import Type		( tyVarsOfType )
-import CoreUtils        ( exprIsTrivial, isDefaultAlt, mkCoerceI, isExpandableApp )
-import Coercion		( CoercionI(..), mkSymCoI )
+import CoreUtils        ( exprIsTrivial, isDefaultAlt, isExpandableApp, mkCoerce )
 import Id
 import NameEnv
 import NameSet
 import Name		( Name, localiseName )
 import BasicTypes
+import Coercion
+
 import VarSet
 import VarEnv
-import Var              ( varUnique )
+import Var
+
 import Maybes           ( orElse )
 import Digraph          ( SCC(..), stronglyConnCompFromEdgedVerticesR )
 import PrelNames        ( buildIdKey, foldrIdKey, runSTRepIdKey, augmentIdKey )
@@ -97,7 +98,7 @@ occAnalBind :: OccEnv 		-- The incoming OccEnv
                 [CoreBind])
 
 occAnalBind env _ (NonRec binder rhs) body_usage
-  | isTyCoVar binder			-- A type let; we don't gather usage info
+  | isTyVar binder	-- A type let; we don't gather usage info
   = (body_usage, [NonRec binder rhs])
 
   | not (binder `usedIn` body_usage)    -- It's not mentioned
@@ -381,7 +382,7 @@ occAnalBind _ env (Rec pairs) body_usage
     
     make_node (bndr, rhs)
         = (details, varUnique bndr, keysUFM out_edges)
-	where
+        where
           details = ND { nd_bndr = bndr, nd_rhs = rhs'
                        , nd_uds = rhs_usage3, nd_inl = inl_fvs}
 
@@ -872,33 +873,27 @@ occAnal :: OccEnv
         -> (UsageDetails,       -- Gives info only about the "interesting" Ids
             CoreExpr)
 
-occAnal _   (Type t)  = (emptyDetails, Type t)
-occAnal env (Var v)   = (mkOneOcc env v False, Var v)
+occAnal _   expr@(Type _) = (emptyDetails, 	   expr)
+occAnal _   expr@(Lit _)  = (emptyDetails, 	   expr)   
+occAnal env expr@(Var v)  = (mkOneOcc env v False, expr)
     -- At one stage, I gathered the idRuleVars for v here too,
     -- which in a way is the right thing to do.
     -- But that went wrong right after specialisation, when
     -- the *occurrences* of the overloaded function didn't have any
     -- rules in them, so the *specialised* versions looked as if they
     -- weren't used at all.
-\end{code}
 
-We regard variables that occur as constructor arguments as "dangerousToDup":
-
-\begin{verbatim}
-module A where
-f x = let y = expensive x in
-      let z = (True,y) in
-      (case z of {(p,q)->q}, case z of {(p,q)->q})
-\end{verbatim}
-
-We feel free to duplicate the WHNF (True,y), but that means
-that y may be duplicated thereby.
+occAnal _ (Coercion co) 
+  = (addIdOccs emptyDetails (coVarsOfCo co), Coercion co)
+	-- See Note [Gather occurrences of coercion veriables]
+\end{code}
 
-If we aren't careful we duplicate the (expensive x) call!
-Constructors are rather like lambdas in this way.
+Note [Gather occurrences of coercion veriables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We need to gather info about what coercion variables appear, so that
+we can sort them into the right place when doing dependency analysis.
 
 \begin{code}
-occAnal _   expr@(Lit _) = (emptyDetails, expr)
 \end{code}
 
 \begin{code}
@@ -914,7 +909,10 @@ occAnal env (Note note body)
 
 occAnal env (Cast expr co)
   = case occAnal env expr of { (usage, expr') ->
-      (markManyIf (isRhsEnv env) usage, Cast expr' co)
+    let usage1 = markManyIf (isRhsEnv env) usage
+        usage2 = addIdOccs usage1 (coVarsOfCo co)
+          -- See Note [Gather occurrences of coercion veriables]
+    in (usage2, Cast expr' co)
         -- If we see let x = y `cast` co
         -- then mark y as 'Many' so that we don't
         -- immediately inline y again.
@@ -929,7 +927,7 @@ occAnal env app@(App _ _)
 --   (a) occurrences inside type lambdas only not marked as InsideLam
 --   (b) type variables not in environment
 
-occAnal env (Lam x body) | isTyCoVar x
+occAnal env (Lam x body) | isTyVar x
   = case occAnal env body of { (body_usage, body') ->
     (body_usage, Lam x body')
     }
@@ -1021,6 +1019,18 @@ occAnalArgs env args
 Applications are dealt with specially because we want
 the "build hack" to work.
 
+Note [Arguments of let-bound constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+    f x = let y = expensive x in
+          let z = (True,y) in
+          (case z of {(p,q)->q}, case z of {(p,q)->q})
+We feel free to duplicate the WHNF (True,y), but that means
+that y may be duplicated thereby.
+
+If we aren't careful we duplicate the (expensive x) call!
+Constructors are rather like lambdas in this way.
+
 \begin{code}
 occAnalApp :: OccEnv
            -> (Expr CoreBndr, [Arg CoreBndr])
@@ -1036,6 +1046,7 @@ occAnalApp env (Var fun, args)
 	  -- arguments are just variables, or trivial expressions.
 	  --
 	  -- This is the *whole point* of the isRhsEnv predicate
+	  -- See Note [Arguments of let-bound constructors]
     in
     (fun_uds +++ final_args_uds, mkApps (Var fun) args') }
   where
@@ -1146,7 +1157,7 @@ wrapProxy (bndr, rhs_var, co) (body_usg, body)
   where
     (body_usg', tagged_bndr) = tagBinder body_usg bndr
     rhs_usg = unitVarEnv rhs_var NoOccInfo	-- We don't need exact info
-    rhs = mkCoerceI co (Var (zapIdOccInfo rhs_var)) -- See Note [Zap case binders in proxy bindings]
+    rhs = mkCoerce co (Var (zapIdOccInfo rhs_var)) -- See Note [Zap case binders in proxy bindings]
 \end{code}
 
 
@@ -1355,7 +1366,7 @@ extendFvs env s
 data ProxyEnv	-- See Note [ProxyEnv]
    = PE (IdEnv	-- Domain = scrutinee variables
            (Id,                  -- The scrutinee variable again
-            [(Id,CoercionI)])) 	 -- The case binders that it maps to
+            [(Id,Coercion)])) 	 -- The case binders that it maps to
         VarSet	-- Free variables of both range and domain
 \end{code}
 
@@ -1572,7 +1583,7 @@ binder-swap unconditionally and still get occurrence analysis
 information right.
 
 \begin{code}
-extendProxyEnv :: ProxyEnv -> Id -> CoercionI -> Id -> ProxyEnv
+extendProxyEnv :: ProxyEnv -> Id -> Coercion -> Id -> ProxyEnv
 -- (extendPE x co y) typically arises from 
 --		  case (x |> co) of y { ... }
 -- It extends the proxy env with the binding 
@@ -1585,7 +1596,7 @@ extendProxyEnv pe scrut co case_bndr
     env2 = extendVarEnv_Acc add single env1 scrut1 (case_bndr,co)
     single cb_co = (scrut1, [cb_co]) 
     add cb_co (x, cb_cos) = (x, cb_co:cb_cos)
-    fvs2 = fvs1 `unionVarSet`  freeVarsCoI co
+    fvs2 = fvs1 `unionVarSet`  tyCoVarsOfCo co
 		`extendVarSet` case_bndr
 		`extendVarSet` scrut1
 
@@ -1596,7 +1607,7 @@ extendProxyEnv pe scrut co case_bndr
 	-- Also we don't want any INLINE or NOINLINE pragmas!
 
 -----------
-type ProxyBind = (Id, Id, CoercionI)
+type ProxyBind = (Id, Id, Coercion)
      -- (scrut variable, case-binder variable, coercion)
 
 getProxies :: OccEnv -> Id -> Bag ProxyBind
@@ -1607,7 +1618,7 @@ getProxies (OccEnv { occ_proxy = PE pe _ }) case_bndr
   = -- pprTrace "wrapProxies" (ppr case_bndr) $
     go_fwd case_bndr
   where
-    fwd_pe :: IdEnv (Id, CoercionI)
+    fwd_pe :: IdEnv (Id, Coercion)
     fwd_pe = foldVarEnv add1 emptyVarEnv pe
            where
              add1 (x,ycos) env = foldr (add2 x) env ycos
@@ -1621,23 +1632,23 @@ getProxies (OccEnv { occ_proxy = PE pe _ }) case_bndr
 
     go_fwd' case_bndr
         | Just (scrut, co) <- lookupVarEnv fwd_pe case_bndr
-        = unitBag (scrut,  case_bndr, mkSymCoI co)
+        = unitBag (scrut,  case_bndr, mkSymCo co)
 	  `unionBags` go_fwd scrut
           `unionBags` go_bwd scrut [pr | pr@(cb,_) <- lookup_bwd scrut
                                        , cb /= case_bndr]
         | otherwise 
         = emptyBag
 
-    lookup_bwd :: Id -> [(Id, CoercionI)]
+    lookup_bwd :: Id -> [(Id, Coercion)]
 	-- Return case_bndrs that are connected to scrut 
     lookup_bwd scrut = case lookupVarEnv pe scrut of
           		  Nothing          -> []
 	  		  Just (_, cb_cos) -> cb_cos
 
-    go_bwd :: Id -> [(Id, CoercionI)] -> Bag ProxyBind
+    go_bwd :: Id -> [(Id, Coercion)] -> Bag ProxyBind
     go_bwd scrut cb_cos = foldr (unionBags . go_bwd1 scrut) emptyBag cb_cos
 
-    go_bwd1 :: Id -> (Id, CoercionI) -> Bag ProxyBind
+    go_bwd1 :: Id -> (Id, Coercion) -> Bag ProxyBind
     go_bwd1 scrut (case_bndr, co) 
        = -- pprTrace "go_bwd1" (ppr case_bndr) $
          unitBag (case_bndr, scrut, co)
@@ -1652,9 +1663,9 @@ mkAltEnv env scrut cb
   where
     pe  = occ_proxy env
     pe' = case scrut of
-             Var v           -> extendProxyEnv pe v (IdCo (idType v)) cb
-             Cast (Var v) co -> extendProxyEnv pe v (ACo co)          cb
-	     _other          -> trimProxyEnv pe [cb]
+             Var v           -> extendProxyEnv pe v (mkReflCo (idType v)) cb
+             Cast (Var v) co -> extendProxyEnv pe v co                    cb
+             _other          -> trimProxyEnv pe [cb]
 
 -----------
 trimOccEnv :: OccEnv -> [CoreBndr] -> OccEnv
@@ -1675,12 +1686,7 @@ trimProxyEnv (PE pe fvs) bndrs
     trim (scrut, cb_cos) | scrut `elemVarSet` bndr_set = (scrut, [])
 			 | otherwise = (scrut, filterOut discard cb_cos)
     discard (cb,co) = bndr_set `intersectsVarSet` 
-                      extendVarSet (freeVarsCoI co) cb
-                             
------------
-freeVarsCoI :: CoercionI -> VarSet
-freeVarsCoI (IdCo t) = tyVarsOfType t
-freeVarsCoI (ACo co) = tyVarsOfType co
+                      extendVarSet (tyCoVarsOfCo co) cb
 \end{code}
 
 
@@ -1747,7 +1753,7 @@ tagBinder usage binder
 
 setBinderOcc :: UsageDetails -> CoreBndr -> CoreBndr
 setBinderOcc usage bndr
-  | isTyCoVar bndr    = bndr
+  | isTyVar bndr      = bndr
   | isExportedId bndr = case idOccInfo bndr of
                           NoOccInfo -> bndr
                           _         -> setIdOccInfo bndr NoOccInfo
diff --git a/compiler/simplCore/SAT.lhs b/compiler/simplCore/SAT.lhs
index d398055744..61182895cf 100644
--- a/compiler/simplCore/SAT.lhs
+++ b/compiler/simplCore/SAT.lhs
@@ -56,6 +56,7 @@ import Var
 import CoreSyn
 import CoreUtils
 import Type
+import Coercion
 import Id
 import Name
 import VarEnv
@@ -112,7 +113,7 @@ satBind (Rec pairs) interesting_ids = do
     return (Rec (zipEqual "satBind" binders rhss'), mergeIdSATInfos sat_info_rhss')
 \end{code}
 \begin{code}
-data App = VarApp Id | TypeApp Type
+data App = VarApp Id | TypeApp Type | CoApp Coercion
 data Staticness a = Static a | NotStatic
 
 type IdAppInfo = (Id, SATInfo)
@@ -133,6 +134,7 @@ pprSATInfo staticness = hcat $ map pprStaticness staticness
 pprStaticness :: Staticness App -> SDoc
 pprStaticness (Static (VarApp _))  = ptext (sLit "SV") 
 pprStaticness (Static (TypeApp _)) = ptext (sLit "ST") 
+pprStaticness (Static (CoApp _))   = ptext (sLit "SC")
 pprStaticness NotStatic            = ptext (sLit "NS")
 
 
@@ -142,7 +144,8 @@ mergeSATInfo _  [] = []
 mergeSATInfo (NotStatic:statics) (_:apps) = NotStatic : mergeSATInfo statics apps
 mergeSATInfo (_:statics) (NotStatic:apps) = NotStatic : mergeSATInfo statics apps
 mergeSATInfo ((Static (VarApp v)):statics)  ((Static (VarApp v')):apps)  = (if v == v' then Static (VarApp v) else NotStatic) : mergeSATInfo statics apps
-mergeSATInfo ((Static (TypeApp t)):statics) ((Static (TypeApp t')):apps) = (if t `coreEqType` t' then Static (TypeApp t) else NotStatic) : mergeSATInfo statics apps
+mergeSATInfo ((Static (TypeApp t)):statics) ((Static (TypeApp t')):apps) = (if t `eqType` t' then Static (TypeApp t) else NotStatic) : mergeSATInfo statics apps
+mergeSATInfo ((Static (CoApp c)):statics) ((Static (CoApp c')):apps)     = (if c `coreEqCoercion` c' then Static (CoApp c) else NotStatic) : mergeSATInfo statics apps
 mergeSATInfo l  r  = pprPanic "mergeSATInfo" $ ptext (sLit "Left:") <> pprSATInfo l <> ptext (sLit ", ")
                                             <> ptext (sLit "Right:") <> pprSATInfo r
 
@@ -154,9 +157,9 @@ mergeIdSATInfos = foldl' mergeIdSATInfo emptyIdSATInfo
 
 bindersToSATInfo :: [Id] -> SATInfo
 bindersToSATInfo vs = map (Static . binderToApp) vs
-    where binderToApp v = if isId v
-                          then VarApp v
-                          else TypeApp $ mkTyVarTy v
+    where binderToApp v | isId v    = VarApp v
+                        | isTyVar v = TypeApp $ mkTyVarTy v
+                        | otherwise = CoApp $ mkCoVarCo v
 
 finalizeApp :: Maybe IdAppInfo -> IdSATInfo -> IdSATInfo
 finalizeApp Nothing id_sat_info = id_sat_info
@@ -195,9 +198,10 @@ satExpr (App fn arg) interesting_ids = do
             -- TODO: remove this use of append somehow (use a data structure with O(1) append but a left-to-right kind of interface)
             let satRemainderWithStaticness arg_staticness = satRemainder $ Just (fn_id, fn_app_info ++ [arg_staticness])
             in case arg of
-                Type t -> satRemainderWithStaticness $ Static (TypeApp t)
-                Var v  -> satRemainderWithStaticness $ Static (VarApp v)
-                _      -> satRemainderWithStaticness $ NotStatic
+                Type t     -> satRemainderWithStaticness $ Static (TypeApp t)
+                Coercion c -> satRemainderWithStaticness $ Static (CoApp c)
+                Var v      -> satRemainderWithStaticness $ Static (VarApp v)
+                _          -> satRemainderWithStaticness $ NotStatic
   where
     boring :: CoreExpr -> IdSATInfo -> Maybe IdAppInfo -> SatM (CoreExpr, IdSATInfo, Maybe IdAppInfo)
     boring fn' sat_info_fn app_info = 
@@ -229,6 +233,9 @@ satExpr (Note note expr) interesting_ids = do
 
 satExpr ty@(Type _) _ = do
     return (ty, emptyIdSATInfo, Nothing)
+    
+satExpr co@(Coercion _) _ = do
+    return (co, emptyIdSATInfo, Nothing)
 
 satExpr (Cast expr coercion) interesting_ids = do
     (expr', sat_info_expr, expr_app) <- satExpr expr interesting_ids
diff --git a/compiler/simplCore/SetLevels.lhs b/compiler/simplCore/SetLevels.lhs
index 6871faa798..21dca615c3 100644
--- a/compiler/simplCore/SetLevels.lhs
+++ b/compiler/simplCore/SetLevels.lhs
@@ -243,6 +243,7 @@ If there were another lambda in @r@'s rhs, it would get level-2 as well.
 
 \begin{code}
 lvlExpr _ _ (  _, AnnType ty) = return (Type ty)
+lvlExpr _ _ ( _, AnnCoercion co) = return (Coercion co)
 lvlExpr _ env (_, AnnVar v)   = return (lookupVar env v)
 lvlExpr _ _   (_, AnnLit lit) = return (Lit lit)
 
@@ -287,7 +288,7 @@ lvlExpr ctxt_lvl env (_, AnnNote note expr) = do
     expr' <- lvlExpr ctxt_lvl env expr
     return (Note note expr')
 
-lvlExpr ctxt_lvl env (_, AnnCast expr co) = do
+lvlExpr ctxt_lvl env (_, AnnCast expr (_, co)) = do
     expr' <- lvlExpr ctxt_lvl env expr
     return (Cast expr' co)
 
@@ -414,7 +415,7 @@ lvlMFE strict_ctxt ctxt_lvl env (_, AnnNote n e)
   = do { e' <- lvlMFE strict_ctxt ctxt_lvl env e
        ; return (Note n e') }
 
-lvlMFE strict_ctxt ctxt_lvl env (_, AnnCast e co)
+lvlMFE strict_ctxt ctxt_lvl env (_, AnnCast e (_, co))
   = do	{ e' <- lvlMFE strict_ctxt ctxt_lvl env e
 	; return (Cast e' co) }
 
@@ -423,7 +424,9 @@ lvlMFE True ctxt_lvl env e@(_, AnnCase {})
   = lvlExpr ctxt_lvl env e     -- Don't share cases
 
 lvlMFE strict_ctxt ctxt_lvl env ann_expr@(fvs, _)
-  |  isUnLiftedType ty			-- Can't let-bind it; see Note [Unlifted MFEs]
+  |  isUnLiftedType ty		-- Can't let-bind it; see Note [Unlifted MFEs]
+     		    		-- This includes coercions, which we don't
+				-- want to float anyway
   || notWorthFloating ann_expr abs_vars
   || not good_destination
   = 	-- Don't float it out
@@ -491,6 +494,7 @@ notWorthFloating e abs_vars
     go (_, AnnCast e _)  n = go e n
     go (_, AnnApp e arg) n 
        | (_, AnnType {}) <- arg = go e n
+       | (_, AnnCoercion {}) <- arg = go e n
        | n==0                   = False
        | is_triv arg       	= go e (n-1)
        | otherwise         	= False
@@ -500,6 +504,7 @@ notWorthFloating e abs_vars
     is_triv (_, AnnVar {})   	       	  = True	-- (ie not worth floating)
     is_triv (_, AnnCast e _) 	       	  = is_triv e
     is_triv (_, AnnApp e (_, AnnType {})) = is_triv e
+    is_triv (_, AnnApp e (_, AnnCoercion {})) = is_triv e
     is_triv _                             = False     
 \end{code}
 
@@ -563,7 +568,7 @@ lvlBind :: TopLevelFlag		-- Used solely to decide whether to clone
 	-> LvlM (LevelledBind, LevelEnv)
 
 lvlBind top_lvl ctxt_lvl env (AnnNonRec bndr rhs@(rhs_fvs,_))
-  |  isTyCoVar bndr 		-- Don't do anything for TyVar binders
+  |  isTyVar bndr 		-- Don't do anything for TyVar binders
 				--   (simplifier gets rid of them pronto)
   = do rhs' <- lvlExpr ctxt_lvl env rhs
        return (NonRec (TB bndr ctxt_lvl) rhs', env)
@@ -883,7 +888,7 @@ abstractVars dest_lvl (LE { le_lvl_env = lvl_env, le_env = id_env }) fvs
 		   (False, True) -> False
 		   _    	 -> v1 <= v2	-- Same family
 
-    is_tv v = isTyCoVar v && not (isCoVar v)
+    is_tv v = isTyVar v 
 
     uniq :: [Var] -> [Var]
 	-- Remove adjacent duplicates; the sort will have brought them together
@@ -914,9 +919,7 @@ absVarsOf :: IdEnv ([Var], LevelledExpr) -> Var -> [Var]
 absVarsOf id_env v 
   | isId v    = [av2 | av1 <- lookup_avs v
 		     , av2 <- add_tyvars av1]
-  | isCoVar v = add_tyvars v
-  | otherwise = [v]
-
+  | otherwise = ASSERT( isTyVar v ) [v]
   where
     lookup_avs v = case lookupVarEnv id_env v of
 			Just (abs_vars, _) -> abs_vars
diff --git a/compiler/simplCore/SimplEnv.lhs b/compiler/simplCore/SimplEnv.lhs
index d9eea39ed6..677a1e9d02 100644
--- a/compiler/simplCore/SimplEnv.lhs
+++ b/compiler/simplCore/SimplEnv.lhs
@@ -16,7 +16,7 @@ module SimplEnv (
 
 	-- Environments
 	SimplEnv(..), StaticEnv, pprSimplEnv,	-- Temp not abstract
-	mkSimplEnv, extendIdSubst, SimplEnv.extendTvSubst, 
+        mkSimplEnv, extendIdSubst, SimplEnv.extendTvSubst, SimplEnv.extendCvSubst,
 	zapSubstEnv, setSubstEnv, 
 	getInScope, setInScope, setInScopeSet, modifyInScope, addNewInScopeIds,
         getSimplRules,
@@ -24,8 +24,10 @@ module SimplEnv (
 	SimplSR(..), mkContEx, substId, lookupRecBndr,
 
 	simplNonRecBndr, simplRecBndrs, simplLamBndr, simplLamBndrs, 
- 	simplBinder, simplBinders, addBndrRules,
-	substExpr, substTy, substTyVar, getTvSubst, mkCoreSubst,
+ 	simplBinder, simplBinders, addBndrRules, 
+	substExpr, substTy, substTyVar, getTvSubst, 
+	getCvSubst, substCo, substCoVar,
+	mkCoreSubst,
 
 	-- Floats
   	Floats, emptyFloats, isEmptyFloats, addNonRec, addFloats, extendFloats,
@@ -49,9 +51,10 @@ import Id
 import MkCore
 import TysWiredIn
 import qualified CoreSubst
-import qualified Type		( substTy, substTyVarBndr, substTyVar )
+import qualified Type
 import Type hiding		( substTy, substTyVarBndr, substTyVar )
-import Coercion
+import qualified Coercion
+import Coercion hiding          ( substCo, substTy, substCoVar, substCoVarBndr, substTyVarBndr )
 import BasicTypes	
 import MonadUtils
 import Outputable
@@ -107,8 +110,9 @@ data SimplEnv
         seCC        :: CostCentreStack, -- The enclosing CCS (when profiling)
 
 	-- The current substitution
-	seTvSubst   :: TvSubstEnv,	-- InTyVar |--> OutType
-	seIdSubst   :: SimplIdSubst,	-- InId    |--> OutExpr
+	seTvSubst   :: TvSubstEnv,	-- InTyVar   |--> OutType
+        seCvSubst   :: CvSubstEnv,      -- InTyCoVar |--> OutCoercion
+	seIdSubst   :: SimplIdSubst,	-- InId      |--> OutExpr
 
      ----------- Dynamic part of the environment -----------
      -- Dynamic in the sense of describing the setup where
@@ -143,13 +147,14 @@ data SimplSR
   = DoneEx OutExpr		-- Completed term
   | DoneId OutId		-- Completed term variable
   | ContEx TvSubstEnv	 	-- A suspended substitution
+           CvSubstEnv
 	   SimplIdSubst
 	   InExpr 	 
 
 instance Outputable SimplSR where
   ppr (DoneEx e) = ptext (sLit "DoneEx") <+> ppr e
   ppr (DoneId v) = ptext (sLit "DoneId") <+> ppr v
-  ppr (ContEx _tv _id e) = vcat [ptext (sLit "ContEx") <+> ppr e {-,
+  ppr (ContEx _tv _cv _id e) = vcat [ptext (sLit "ContEx") <+> ppr e {-,
 				ppr (filter_env tv), ppr (filter_env id) -}]
 	-- where
 	-- fvs = exprFreeVars e
@@ -227,6 +232,7 @@ mkSimplEnv mode
              , seInScope = init_in_scope
              , seFloats = emptyFloats
              , seTvSubst = emptyVarEnv
+             , seCvSubst = emptyVarEnv 
              , seIdSubst = emptyVarEnv }
 	-- The top level "enclosing CC" is "SUBSUMED".
 
@@ -273,12 +279,17 @@ setEnclosingCC env cc = env {seCC = cc}
 ---------------------
 extendIdSubst :: SimplEnv -> Id -> SimplSR -> SimplEnv
 extendIdSubst env@(SimplEnv {seIdSubst = subst}) var res
-  = env {seIdSubst = extendVarEnv subst var res}
+  = ASSERT2( isId var && not (isCoVar var), ppr var )
+    env {seIdSubst = extendVarEnv subst var res}
 
 extendTvSubst :: SimplEnv -> TyVar -> Type -> SimplEnv
 extendTvSubst env@(SimplEnv {seTvSubst = subst}) var res
   = env {seTvSubst = extendVarEnv subst var res}
 
+extendCvSubst :: SimplEnv -> CoVar -> Coercion -> SimplEnv
+extendCvSubst env@(SimplEnv {seCvSubst = subst}) var res
+  = env {seCvSubst = extendVarEnv subst var res}
+
 ---------------------
 getInScope :: SimplEnv -> InScopeSet
 getInScope env = seInScope env
@@ -318,13 +329,13 @@ modifyInScope env@(SimplEnv {seInScope = in_scope}) v
 
 ---------------------
 zapSubstEnv :: SimplEnv -> SimplEnv
-zapSubstEnv env = env {seTvSubst = emptyVarEnv, seIdSubst = emptyVarEnv}
+zapSubstEnv env = env {seTvSubst = emptyVarEnv, seCvSubst = emptyVarEnv, seIdSubst = emptyVarEnv}
 
-setSubstEnv :: SimplEnv -> TvSubstEnv -> SimplIdSubst -> SimplEnv
-setSubstEnv env tvs ids = env { seTvSubst = tvs, seIdSubst = ids }
+setSubstEnv :: SimplEnv -> TvSubstEnv -> CvSubstEnv -> SimplIdSubst -> SimplEnv
+setSubstEnv env tvs cvs ids = env { seTvSubst = tvs, seCvSubst = cvs, seIdSubst = ids }
 
 mkContEx :: SimplEnv -> InExpr -> SimplSR
-mkContEx (SimplEnv { seTvSubst = tvs, seIdSubst = ids }) e = ContEx tvs ids e
+mkContEx (SimplEnv { seTvSubst = tvs, seCvSubst = cvs, seIdSubst = ids }) e = ContEx tvs cvs ids e
 \end{code}
 
 
@@ -503,7 +514,6 @@ substId (SimplEnv { seInScope = in_scope, seIdSubst = ids }) v
 	Just (DoneId v)       -> DoneId (refine in_scope v)
 	Just (DoneEx (Var v)) -> DoneId (refine in_scope v)
 	Just res	      -> res	-- DoneEx non-var, or ContEx
-  where
 
 	-- Get the most up-to-date thing from the in-scope set
 	-- Even though it isn't in the substitution, it may be in
@@ -549,7 +559,7 @@ simplBinder :: SimplEnv -> InBndr -> SimplM (SimplEnv, OutBndr)
 -- The substitution is extended only if the variable is cloned, because
 -- we *don't* need to use it to track occurrence info.
 simplBinder env bndr
-  | isTyCoVar bndr  = do	{ let (env', tv) = substTyVarBndr env bndr
+  | isTyVar bndr  = do	{ let (env', tv) = substTyVarBndr env bndr
 			; seqTyVar tv `seq` return (env', tv) }
   | otherwise     = do	{ let (env', id) = substIdBndr env bndr
 			; seqId id `seq` return (env', id) }
@@ -586,9 +596,17 @@ simplRecBndrs env@(SimplEnv {}) ids
 	; seqIds ids1 `seq` return env1 }
 
 ---------------
-substIdBndr :: SimplEnv 	
-	    -> InBndr 	-- Env and binder to transform
-	    -> (SimplEnv, OutBndr)
+substIdBndr :: SimplEnv -> InBndr -> (SimplEnv, OutBndr)
+-- Might be a coercion variable
+substIdBndr env bndr
+  | isCoVar bndr  = substCoVarBndr env bndr
+  | otherwise     = substNonCoVarIdBndr env bndr
+
+---------------
+substNonCoVarIdBndr 
+   :: SimplEnv 	
+   -> InBndr 	-- Env and binder to transform
+   -> (SimplEnv, OutBndr)
 -- Clone Id if necessary, substitute its type
 -- Return an Id with its 
 --	* Type substituted
@@ -606,10 +624,10 @@ substIdBndr :: SimplEnv
 -- Similar to CoreSubst.substIdBndr, except that 
 --	the type of id_subst differs
 --	all fragile info is zapped
-
-substIdBndr env@(SimplEnv { seInScope = in_scope, seIdSubst = id_subst }) 
-	       old_id
-  = (env { seInScope = in_scope `extendInScopeSet` new_id, 
+substNonCoVarIdBndr env@(SimplEnv { seInScope = in_scope, seIdSubst = id_subst })
+                    old_id
+  = ASSERT2( not (isCoVar old_id), ppr old_id )
+    (env { seInScope = in_scope `extendInScopeSet` new_id, 
 	   seIdSubst = new_subst }, new_id)
   where
     id1	   = uniqAway in_scope old_id
@@ -714,6 +732,10 @@ getTvSubst :: SimplEnv -> TvSubst
 getTvSubst (SimplEnv { seInScope = in_scope, seTvSubst = tv_env })
   = mkTvSubst in_scope tv_env
 
+getCvSubst :: SimplEnv -> CvSubst
+getCvSubst (SimplEnv { seInScope = in_scope, seTvSubst = tv_env, seCvSubst = cv_env })
+  = CvSubst in_scope tv_env cv_env
+
 substTy :: SimplEnv -> Type -> Type 
 substTy env ty = Type.substTy (getTvSubst env) ty
 
@@ -724,7 +746,19 @@ substTyVarBndr :: SimplEnv -> TyVar -> (SimplEnv, TyVar)
 substTyVarBndr env tv
   = case Type.substTyVarBndr (getTvSubst env) tv of
 	(TvSubst in_scope' tv_env', tv') 
-	   -> (env { seInScope = in_scope', seTvSubst = tv_env'}, tv')
+	   -> (env { seInScope = in_scope', seTvSubst = tv_env' }, tv')
+
+substCoVar :: SimplEnv -> CoVar -> Coercion
+substCoVar env tv = Coercion.substCoVar (getCvSubst env) tv
+
+substCoVarBndr :: SimplEnv -> CoVar -> (SimplEnv, CoVar)
+substCoVarBndr env cv
+  = case Coercion.substCoVarBndr (getCvSubst env) cv of
+	(CvSubst in_scope' tv_env' cv_env', cv') 
+	   -> (env { seInScope = in_scope', seTvSubst = tv_env', seCvSubst = cv_env' }, cv')
+
+substCo :: SimplEnv -> Coercion -> Coercion
+substCo env co = Coercion.substCo (getCvSubst env) co
 
 -- When substituting in rules etc we can get CoreSubst to do the work
 -- But CoreSubst uses a simpler form of IdSubstEnv, so we must impedence-match
@@ -732,19 +766,19 @@ substTyVarBndr env tv
 -- the substitutions are typically small, and laziness will avoid work in many cases.
 
 mkCoreSubst  :: SDoc -> SimplEnv -> CoreSubst.Subst
-mkCoreSubst doc (SimplEnv { seInScope = in_scope, seTvSubst = tv_env, seIdSubst = id_env })
-  = mk_subst tv_env id_env
+mkCoreSubst doc (SimplEnv { seInScope = in_scope, seTvSubst = tv_env, seCvSubst = cv_env, seIdSubst = id_env })
+  = mk_subst tv_env cv_env id_env
   where
-    mk_subst tv_env id_env = CoreSubst.mkSubst in_scope tv_env (mapVarEnv fiddle id_env)
+    mk_subst tv_env cv_env id_env = CoreSubst.mkSubst in_scope tv_env cv_env (mapVarEnv fiddle id_env)
 
-    fiddle (DoneEx e)       = e
-    fiddle (DoneId v)       = Var v
-    fiddle (ContEx tv id e) = CoreSubst.substExpr (text "mkCoreSubst" <+> doc) (mk_subst tv id) e
+    fiddle (DoneEx e)          = e
+    fiddle (DoneId v)          = Var v
+    fiddle (ContEx tv cv id e) = CoreSubst.substExpr (text "mkCoreSubst" <+> doc) (mk_subst tv cv id) e
     	   	      	      			-- Don't shortcut here
 
 ------------------
 substIdType :: SimplEnv -> Id -> Id
-substIdType (SimplEnv { seInScope = in_scope,  seTvSubst = tv_env}) id
+substIdType (SimplEnv { seInScope = in_scope,  seTvSubst = tv_env }) id
   | isEmptyVarEnv tv_env || isEmptyVarSet (tyVarsOfType old_ty) = id
   | otherwise	= Id.setIdType id (Type.substTy (TvSubst in_scope tv_env) old_ty)
 		-- The tyVarsOfType is cheaper than it looks
diff --git a/compiler/simplCore/SimplUtils.lhs b/compiler/simplCore/SimplUtils.lhs
index 7e9a010051..7d5d764fc6 100644
--- a/compiler/simplCore/SimplUtils.lhs
+++ b/compiler/simplCore/SimplUtils.lhs
@@ -36,6 +36,7 @@ import StaticFlags
 import CoreSyn
 import qualified CoreSubst
 import PprCore
+import DataCon	( dataConCannotMatch )
 import CoreFVs
 import CoreUtils
 import CoreArity
@@ -45,17 +46,16 @@ import Id
 import Var
 import Demand
 import SimplMonad
-import TcType	( isDictLikeTy )
 import Type	hiding( substTy )
-import Coercion ( coercionKind )
+import Coercion hiding( substCo )
 import TyCon
-import Unify	( dataConCannotMatch )
 import VarSet
 import BasicTypes
 import Util
 import MonadUtils
 import Outputable
 import FastString
+import Pair
 
 import Data.List
 \end{code}
@@ -99,6 +99,7 @@ data SimplCont
 
   | CoerceIt 		-- C `cast` co
 	OutCoercion		-- The coercion simplified
+				-- Invariant: never an identity coercion
 	SimplCont
 
   | ApplyTo  		-- C arg
@@ -208,6 +209,7 @@ contIsDupable _                          = False
 contIsTrivial :: SimplCont -> Bool
 contIsTrivial (Stop {})                   = True
 contIsTrivial (ApplyTo _ (Type _) _ cont) = contIsTrivial cont
+contIsTrivial (ApplyTo _ (Coercion _) _ cont) = contIsTrivial cont
 contIsTrivial (CoerceIt _ cont)           = contIsTrivial cont
 contIsTrivial _                           = False
 
@@ -216,17 +218,19 @@ contResultType :: SimplEnv -> OutType -> SimplCont -> OutType
 contResultType env ty cont
   = go cont ty
   where
-    subst_ty se ty = substTy (se `setInScope` env) ty
+    subst_ty se ty = SimplEnv.substTy (se `setInScope` env) ty
+    subst_co se co = SimplEnv.substCo (se `setInScope` env) co
 
     go (Stop {})                      ty = ty
-    go (CoerceIt co cont)             _  = go cont (snd (coercionKind co))
+    go (CoerceIt co cont)             _  = go cont (pSnd (coercionKind co))
     go (StrictBind _ bs body se cont) _  = go cont (subst_ty se (exprType (mkLams bs body)))
     go (StrictArg ai _ cont)          _  = go cont (funResultTy (argInfoResultTy ai))
     go (Select _ _ alts se cont)      _  = go cont (subst_ty se (coreAltsType alts))
     go (ApplyTo _ arg se cont)        ty = go cont (apply_to_arg ty arg se)
 
-    apply_to_arg ty (Type ty_arg) se = applyTy ty (subst_ty se ty_arg)
-    apply_to_arg ty _             _  = funResultTy ty
+    apply_to_arg ty (Type ty_arg)     se = applyTy ty (subst_ty se ty_arg)
+    apply_to_arg ty (Coercion co_arg) se = applyCo ty (subst_co se co_arg)
+    apply_to_arg ty _                 _  = funResultTy ty
 
 argInfoResultTy :: ArgInfo -> OutType
 argInfoResultTy (ArgInfo { ai_fun = fun, ai_args = args })
@@ -235,6 +239,7 @@ argInfoResultTy (ArgInfo { ai_fun = fun, ai_args = args })
 -------------------
 countValArgs :: SimplCont -> Int
 countValArgs (ApplyTo _ (Type _) _ cont) = countValArgs cont
+countValArgs (ApplyTo _ (Coercion _) _ cont) = countValArgs cont
 countValArgs (ApplyTo _ _        _ cont) = 1 + countValArgs cont
 countValArgs _                           = 0
 
@@ -784,6 +789,11 @@ Don't inline top-level Ids that are bottoming, even if they are used just
 once, because FloatOut has gone to some trouble to extract them out.
 Inlining them won't make the program run faster!
 
+Note [Do not inline CoVars unconditionally]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Coercion variables appear inside coercions, and have a separate
+substitution, so don't inline them via the IdSubst!
+
 \begin{code}
 preInlineUnconditionally :: SimplEnv -> TopLevelFlag -> InId -> InExpr -> Bool
 preInlineUnconditionally env top_lvl bndr rhs
@@ -791,6 +801,7 @@ preInlineUnconditionally env top_lvl bndr rhs
   | isStableUnfolding (idUnfolding bndr)     = False    -- Note [InlineRule and preInlineUnconditionally]
   | isTopLevel top_lvl && isBottomingId bndr = False	-- Note [Top-level bottoming Ids]
   | opt_SimplNoPreInlining                   = False
+  | isCoVar bndr                             = False -- Note [Do not inline CoVars unconditionally]
   | otherwise = case idOccInfo bndr of
 		  IAmDead	     	     -> True	-- Happens in ((\x.1) v)
 	  	  OneOcc in_lam True int_cxt -> try_once in_lam int_cxt
@@ -888,6 +899,7 @@ story for now.
 postInlineUnconditionally 
     :: SimplEnv -> TopLevelFlag
     -> OutId		-- The binder (an InId would be fine too)
+       			--            (*not* a CoVar)
     -> OccInfo 		-- From the InId
     -> OutExpr
     -> Unfolding
@@ -1032,9 +1044,9 @@ mkLam _env bndrs body
       | not (any bad bndrs)
 	-- Note [Casts and lambdas]
       = do { lam <- mkLam' dflags bndrs body
-	   ; return (mkCoerce (mkPiTypes bndrs co) lam) }
+           ; return (mkCoerce (mkPiCos bndrs co) lam) }
       where
-	co_vars  = tyVarsOfType co
+        co_vars  = tyCoVarsOfCo co
 	bad bndr = isCoVar bndr && bndr `elemVarSet` co_vars      
 
     mkLam' dflags bndrs body@(Lam {})
@@ -1048,7 +1060,7 @@ mkLam _env bndrs body
       = do { tick (EtaReduction (head bndrs))
 	   ; return etad_lam }
 
-      | otherwise 
+      | otherwise
       = return (mkLams bndrs body)
 \end{code}
 
@@ -1091,9 +1103,6 @@ because the latter is not well-kinded.
 %*									*
 %************************************************************************
 
-When we meet a let-binding we try eta-expansion.  To find the 
-arity of the RHS we use a little fixpoint analysis; see Note [Arity analysis]
-
 \begin{code}
 tryEtaExpand :: SimplEnv -> OutId -> OutExpr -> SimplM (Arity, OutExpr)
 -- See Note [Eta-expanding at let bindings]
@@ -1336,9 +1345,7 @@ abstractFloats main_tvs body_env body
 	   ; return (subst', (NonRec poly_id poly_rhs)) }
       where
 	rhs' = CoreSubst.substExpr (text "abstract_floats2") subst rhs
-	tvs_here | any isCoVar main_tvs = main_tvs	-- Note [Abstract over coercions]
-		 | otherwise 
-		 = varSetElems (main_tv_set `intersectVarSet` exprSomeFreeVars isTyCoVar rhs')
+	tvs_here = varSetElems (main_tv_set `intersectVarSet` exprSomeFreeVars isTyVar rhs')
 	
 		-- Abstract only over the type variables free in the rhs
 		-- wrt which the new binding is abstracted.  But the naive
@@ -1550,9 +1557,8 @@ prepareDefault case_bndr (Just (tycon, inst_tys)) imposs_cons (Just deflt_rhs)
 	[con] -> 	-- It matches exactly one constructor, so fill it in
 		 do { tick (FillInCaseDefault case_bndr)
                     ; us <- getUniquesM
-                    ; let (ex_tvs, co_tvs, arg_ids) =
-                              dataConRepInstPat us con inst_tys
-                    ; return [(DataAlt con, ex_tvs ++ co_tvs ++ arg_ids, deflt_rhs)] }
+                    ; let (ex_tvs, arg_ids) = dataConRepInstPat us con inst_tys
+                    ; return [(DataAlt con, ex_tvs ++ arg_ids, deflt_rhs)] }
 
 	_ -> return [(DEFAULT, [], deflt_rhs)]
 
diff --git a/compiler/simplCore/Simplify.lhs b/compiler/simplCore/Simplify.lhs
index db84c90fc2..b187897f89 100644
--- a/compiler/simplCore/Simplify.lhs
+++ b/compiler/simplCore/Simplify.lhs
@@ -17,10 +17,9 @@ import FamInstEnv	( FamInstEnv )
 import Id
 import MkId		( seqId, realWorldPrimId )
 import MkCore		( mkImpossibleExpr )
-import Var
 import IdInfo
 import Name		( mkSystemVarName, isExternalName )
-import Coercion
+import Coercion hiding  ( substCo, substTy, substCoVar, extendTvSubst )
 import OptCoercion	( optCoercion )
 import FamInstEnv       ( topNormaliseType )
 import DataCon          ( DataCon, dataConWorkId, dataConRepStrictness )
@@ -42,6 +41,7 @@ import Maybes           ( orElse, isNothing )
 import Data.List        ( mapAccumL )
 import Outputable
 import FastString
+import Pair
 \end{code}
 
 
@@ -369,8 +369,11 @@ simplNonRecX :: SimplEnv
              -> SimplM SimplEnv
 
 simplNonRecX env bndr new_rhs
-  | isDeadBinder bndr	-- Not uncommon; e.g. case (a,b) of b { (p,q) -> p }
-  = return env		-- 		 Here b is dead, and we avoid creating
+  | isDeadBinder bndr	-- Not uncommon; e.g. case (a,b) of c { (p,q) -> p }
+  = return env		-- 		 Here c is dead, and we avoid creating
+    	   		--               the binding c = (a,b)
+  | Coercion co <- new_rhs    
+  = return (extendCvSubst env bndr co)
   | otherwise		--		 the binding b = (a,b)
   = do  { (env', bndr') <- simplBinder env bndr
         ; completeNonRecX NotTopLevel env' (isStrictId bndr) bndr bndr' new_rhs }
@@ -438,7 +441,7 @@ That's what the 'go' loop in prepareRhs does
 prepareRhs :: TopLevelFlag -> SimplEnv -> OutId -> OutExpr -> SimplM (SimplEnv, OutExpr)
 -- Adds new floats to the env iff that allows us to return a good RHS
 prepareRhs top_lvl env id (Cast rhs co)    -- Note [Float coercions]
-  | (ty1, _ty2) <- coercionKind co       -- Do *not* do this if rhs has an unlifted type
+  | Pair ty1 _ty2 <- coercionKind co       -- Do *not* do this if rhs has an unlifted type
   , not (isUnLiftedType ty1)            -- see Note [Float coercions (unlifted)]
   = do  { (env', rhs') <- makeTrivialWithInfo top_lvl env sanitised_info rhs
         ; return (env', Cast rhs' co) }
@@ -626,6 +629,12 @@ completeBind :: SimplEnv
 --      * or by adding to the floats in the envt
 
 completeBind env top_lvl old_bndr new_bndr new_rhs
+ | isCoVar old_bndr
+ = case new_rhs of
+     Coercion co -> return (extendCvSubst env old_bndr co)
+     _           -> return (addNonRec env new_bndr new_rhs)
+
+ | otherwise
  = ASSERT( isId new_bndr )
    do { let old_info = idInfo old_bndr
 	    old_unf  = unfoldingInfo old_info
@@ -641,9 +650,7 @@ completeBind env top_lvl old_bndr new_bndr new_rhs
       ; if postInlineUnconditionally env top_lvl new_bndr occ_info final_rhs new_unfolding
 	                -- Inline and discard the binding
 	then do  { tick (PostInlineUnconditionally old_bndr)
-	         ; -- pprTrace "postInlineUnconditionally" 
-                   --         (ppr old_bndr <+> equals <+> ppr final_rhs $$ ppr occ_info) $
-                   return (extendIdSubst env old_bndr (DoneEx final_rhs)) }
+	         ; return (extendIdSubst env old_bndr (DoneEx final_rhs)) }
 	        -- Use the substitution to make quite, quite sure that the
 	        -- substitution will happen, since we are going to discard the binding
 	else
@@ -658,7 +665,7 @@ completeBind env top_lvl old_bndr new_bndr new_rhs
 
             final_id = new_bndr `setIdInfo` info3
 
-      ; -- pprTrace "Binding" (ppr final_id <+> ppr unfolding) $
+      ; -- pprTrace "Binding" (ppr final_id <+> ppr new_unfolding) $
         return (addNonRec env final_id final_rhs) } }
 		-- The addNonRec adds it to the in-scope set too
 
@@ -870,18 +877,21 @@ simplExprF :: SimplEnv -> InExpr -> SimplCont
 
 simplExprF env e cont
   = -- pprTrace "simplExprF" (ppr e $$ ppr cont $$ ppr (seTvSubst env) $$ ppr (seIdSubst env) {- $$ ppr (seFloats env) -} ) $
-    simplExprF' env e cont
+    simplExprF1 env e cont
 
-simplExprF' :: SimplEnv -> InExpr -> SimplCont
+simplExprF1 :: SimplEnv -> InExpr -> SimplCont
             -> SimplM (SimplEnv, OutExpr)
-simplExprF' env (Var v)        cont = simplVarF env v cont
-simplExprF' env (Lit lit)      cont = rebuild env (Lit lit) cont
-simplExprF' env (Note n expr)  cont = simplNote env n expr cont
-simplExprF' env (Cast body co) cont = simplCast env body co cont
-simplExprF' env (App fun arg)  cont = simplExprF env fun $
+simplExprF1 env (Var v)        cont = simplIdF env v cont
+simplExprF1 env (Lit lit)      cont = rebuild env (Lit lit) cont
+simplExprF1 env (Note n expr)  cont = simplNote env n expr cont
+simplExprF1 env (Cast body co) cont = simplCast env body co cont
+simplExprF1 env (Coercion co)  cont = simplCoercionF env co cont
+simplExprF1 env (Type ty)      cont = ASSERT( contIsRhsOrArg cont )
+                                      rebuild env (Type (substTy env ty)) cont
+simplExprF1 env (App fun arg)  cont = simplExprF env fun $
                                       ApplyTo NoDup arg env cont
 
-simplExprF' env expr@(Lam _ _) cont
+simplExprF1 env expr@(Lam {}) cont
   = simplLam env zapped_bndrs body cont
         -- The main issue here is under-saturated lambdas
         --   (\x1. \x2. e) arg1
@@ -898,17 +908,12 @@ simplExprF' env expr@(Lam _ _) cont
     n_args = countArgs cont
         -- NB: countArgs counts all the args (incl type args)
         -- and likewise drop counts all binders (incl type lambdas)
-        
-    zappable_bndr b = isId b && not (isOneShotBndr b)
-    zap b | isTyCoVar b = b
-          | otherwise   = zapLamIdInfo b
 
-simplExprF' env (Type ty) cont
-  = ASSERT( contIsRhsOrArg cont )
-    do  { ty' <- simplCoercion env ty
-        ; rebuild env (Type ty') cont }
+    zappable_bndr b = isId b && not (isOneShotBndr b)
+    zap b | isTyVar b = b
+          | otherwise = zapLamIdInfo b
 
-simplExprF' env (Case scrut bndr _ alts) cont
+simplExprF1 env (Case scrut bndr _ alts) cont
   | sm_case_case (getMode env)
   =     -- Simplify the scrutinee with a Select continuation
     simplExprF env scrut (Select NoDup bndr alts env cont)
@@ -920,7 +925,7 @@ simplExprF' env (Case scrut bndr _ alts) cont
                              (Select NoDup bndr alts env mkBoringStop)
         ; rebuild env case_expr' cont }
 
-simplExprF' env (Let (Rec pairs) body) cont
+simplExprF1 env (Let (Rec pairs) body) cont
   = do  { env' <- simplRecBndrs env (map fst pairs)
                 -- NB: bndrs' don't have unfoldings or rules
                 -- We add them as we go down
@@ -928,7 +933,7 @@ simplExprF' env (Let (Rec pairs) body) cont
         ; env'' <- simplRecBind env' NotTopLevel pairs
         ; simplExprF env'' body cont }
 
-simplExprF' env (Let (NonRec bndr rhs) body) cont
+simplExprF1 env (Let (NonRec bndr rhs) body) cont
   = simplNonRecE env bndr (rhs, env) ([], body) cont
 
 ---------------------------------
@@ -941,13 +946,30 @@ simplType env ty
     new_ty = substTy env ty
 
 ---------------------------------
-simplCoercion :: SimplEnv -> InType -> SimplM OutType
--- The InType isn't *necessarily* a coercion, but it might be
--- (in a type application, say) and optCoercion is a no-op on types
+simplCoercionF :: SimplEnv -> InCoercion -> SimplCont
+               -> SimplM (SimplEnv, OutExpr)
+-- We are simplifying a term of form (Coercion co)
+-- Simplify the InCoercion, and then try to combine with the 
+-- context, to implememt the rule
+--     (Coercion co) |> g
+--  =  Coercion (syn (nth 0 g) ; co ; nth 1 g) 
+simplCoercionF env co cont 
+  = do { co' <- simplCoercion env co
+       ; simpl_co co' cont }
+  where
+    simpl_co co (CoerceIt g cont)
+       = simpl_co new_co cont
+     where
+       new_co = mkSymCo g0 `mkTransCo` co `mkTransCo` g1
+       [g0, g1] = decomposeCo 2 g
+
+    simpl_co co cont
+       = seqCo co `seq` rebuild env (Coercion co) cont
+
+simplCoercion :: SimplEnv -> InCoercion -> SimplM OutCoercion
 simplCoercion env co
-  = seqType new_co `seq` return new_co
-  where 
-    new_co = optCoercion (getTvSubst env) co
+  = let opt_co = optCoercion (getCvSubst env) co
+    in opt_co `seq` return opt_co
 \end{code}
 
 
@@ -964,7 +986,7 @@ rebuild :: SimplEnv -> OutExpr -> SimplCont -> SimplM (SimplEnv, OutExpr)
 rebuild env expr cont
   = case cont of
       Stop {}                      -> return (env, expr)
-      CoerceIt co cont             -> rebuild env (mkCoerce co expr) cont
+      CoerceIt co cont             -> rebuild env (Cast expr co) cont
       Select _ bndr alts se cont   -> rebuildCase (se `setFloats` env) expr bndr alts cont
       StrictArg info _ cont        -> rebuildCall env (info `addArgTo` expr) cont
       StrictBind b bs body se cont -> do { env' <- simplNonRecX (se `setFloats` env) b expr
@@ -991,11 +1013,11 @@ simplCast env body co0 cont0
   where
        addCoerce co cont = add_coerce co (coercionKind co) cont
 
-       add_coerce _co (s1, k1) cont     -- co :: ty~ty
-         | s1 `coreEqType` k1 = cont    -- is a no-op
+       add_coerce _co (Pair s1 k1) cont     -- co :: ty~ty
+         | s1 `eqType` k1 = cont    -- is a no-op
 
-       add_coerce co1 (s1, _k2) (CoerceIt co2 cont)
-         | (_l1, t1) <- coercionKind co2
+       add_coerce co1 (Pair s1 _k2) (CoerceIt co2 cont)
+         | (Pair _l1 t1) <- coercionKind co2
 		-- 	e |> (g1 :: S1~L) |> (g2 :: L~T1)
                 -- ==>
                 --      e,                       if S1=T1
@@ -1005,28 +1027,40 @@ simplCast env body co0 cont0
                 -- we may find  (coerce T (coerce S (\x.e))) y
                 -- and we'd like it to simplify to e[y/x] in one round
                 -- of simplification
-         , s1 `coreEqType` t1  = cont            -- The coerces cancel out
-         | otherwise           = CoerceIt (mkTransCoercion co1 co2) cont
+         , s1 `eqType` t1  = cont            -- The coerces cancel out
+         | otherwise       = CoerceIt (mkTransCo co1 co2) cont
 
-       add_coerce co (s1s2, _t1t2) (ApplyTo dup (Type arg_ty) arg_se cont)
+       add_coerce co (Pair s1s2 _t1t2) (ApplyTo dup (Type arg_ty) arg_se cont)
                 -- (f |> g) ty  --->   (f ty) |> (g @ ty)
-                -- This implements the PushT and PushC rules from the paper
+                -- This implements the PushT rule from the paper
          | Just (tyvar,_) <- splitForAllTy_maybe s1s2
-         = let 
-             (new_arg_ty, new_cast)
-               | isCoVar tyvar = (new_arg_co, mkCselRCoercion co)       -- PushC rule
-               | otherwise     = (ty',        mkInstCoercion co ty')    -- PushT rule
-           in 
-           ApplyTo dup (Type new_arg_ty) (zapSubstEnv arg_se) (addCoerce new_cast cont)
+         = ASSERT( isTyVar tyvar )
+           ApplyTo Simplified (Type arg_ty') (zapSubstEnv arg_se) (addCoerce new_cast cont)
+         where
+           new_cast = mkInstCo co arg_ty'
+           arg_ty' | isSimplified dup = arg_ty
+                   | otherwise        = substTy (arg_se `setInScope` env) arg_ty
+
+{-
+       add_coerce co (Pair s1s2 _t1t2) (ApplyTo dup (Coercion arg_co) arg_se cont)
+                -- This implements the PushC rule from the paper
+         | Just (covar,_) <- splitForAllTy_maybe s1s2
+         = ASSERT( isCoVar covar )
+           ApplyTo Simplified (Coercion new_arg_co) (zapSubstEnv arg_se) (addCoerce co1 cont)
          where
-           ty' = substTy (arg_se `setInScope` env) arg_ty
-	   new_arg_co = mkCsel1Coercion co  `mkTransCoercion`
-                              ty'           `mkTransCoercion`
-                        mkSymCoercion (mkCsel2Coercion co)
-
-       add_coerce co (s1s2, _t1t2) (ApplyTo dup arg arg_se cont)
-         | not (isTypeArg arg)  -- This implements the Push rule from the paper
-         , isFunTy s1s2   -- t1t2 must be a function type, becuase it's applied
+           [co0, co1]   = decomposeCo 2 co
+           [co00, co01] = decomposeCo 2 co0
+
+           arg_co' | isSimplified dup = arg_co
+                   | otherwise        = substCo (arg_se `setInScope` env) arg_co
+           new_arg_co = co00    `mkTransCo`
+                        arg_co' `mkTransCo`
+                        mkSymCo co01
+-}
+
+       add_coerce co (Pair s1s2 t1t2) (ApplyTo dup arg arg_se cont)
+         | isFunTy s1s2   -- This implements the Push rule from the paper
+         , isFunTy t1t2   -- Check t1t2 to ensure 'arg' is a value arg
                 --      (e |> (g :: s1s2 ~ t1->t2)) f
                 -- ===>
                 --      (e (f |> (arg g :: t1~s1))
@@ -1047,7 +1081,7 @@ simplCast env body co0 cont0
            -- t2 ~ s2 with left and right on the curried form:
            --    (->) t1 t2 ~ (->) s1 s2
            [co1, co2] = decomposeCo 2 co
-           new_arg    = mkCoerce (mkSymCoercion co1) arg'
+           new_arg    = mkCoerce (mkSymCo co1) arg'
            arg'       = substExpr (text "move-cast") (arg_se `setInScope` env) arg
 
        add_coerce co _ cont = CoerceIt co cont
@@ -1120,7 +1154,7 @@ simplNonRecE :: SimplEnv
 	-- First deal with type applications and type lets
 	--   (/\a. e) (Type ty)   and   (let a = Type ty in e)
 simplNonRecE env bndr (Type ty_arg, rhs_se) (bndrs, body) cont
-  = ASSERT( isTyCoVar bndr )
+  = ASSERT( isTyVar bndr )
     do	{ ty_arg' <- simplType (rhs_se `setInScope` env) ty_arg
 	; simplLam (extendTvSubst env bndr ty_arg') bndrs body cont }
 
@@ -1130,12 +1164,12 @@ simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
         ; -- pprTrace "preInlineUncond" (ppr bndr <+> ppr rhs) $
           simplLam (extendIdSubst env bndr (mkContEx rhs_se rhs)) bndrs body cont }
 
-  | isStrictId bndr
+  | isStrictId bndr		  -- Includes coercions
   = do  { simplExprF (rhs_se `setFloats` env) rhs
                      (StrictBind bndr bndrs body env cont) }
 
   | otherwise
-  = ASSERT( not (isTyCoVar bndr) )
+  = ASSERT( not (isTyVar bndr) )
     do  { (env1, bndr1) <- simplNonRecBndr env bndr
         ; let (env2, bndr2) = addBndrRules env1 bndr bndr1
         ; env3 <- simplLazyBind env2 NotTopLevel NonRecursive bndr bndr2 rhs rhs_se
@@ -1177,20 +1211,20 @@ simplNote env (CoreNote s) e cont
 simplVar :: SimplEnv -> InVar -> SimplM OutExpr
 -- Look up an InVar in the environment
 simplVar env var
-  | isTyCoVar var 
-  = return (Type (substTyVar env var))
+  | isTyVar var = return (Type (substTyVar env var))
+  | isCoVar var = return (Coercion (substCoVar env var))
   | otherwise
   = case substId env var of
-        DoneId var1      -> return (Var var1)
-        DoneEx e         -> return e
-        ContEx tvs ids e -> simplExpr (setSubstEnv env tvs ids) e
+        DoneId var1          -> return (Var var1)
+        DoneEx e             -> return e
+        ContEx tvs cvs ids e -> simplExpr (setSubstEnv env tvs cvs ids) e
 
-simplVarF :: SimplEnv -> InId -> SimplCont -> SimplM (SimplEnv, OutExpr)
-simplVarF env var cont
+simplIdF :: SimplEnv -> InId -> SimplCont -> SimplM (SimplEnv, OutExpr)
+simplIdF env var cont
   = case substId env var of
-        DoneEx e         -> simplExprF (zapSubstEnv env) e cont
-        ContEx tvs ids e -> simplExprF (setSubstEnv env tvs ids) e cont
-        DoneId var1      -> completeCall env var1 cont
+        DoneEx e             -> simplExprF (zapSubstEnv env) e cont
+        ContEx tvs cvs ids e -> simplExprF (setSubstEnv env tvs cvs ids) e cont
+        DoneId var1          -> completeCall env var1 cont
                 -- Note [zapSubstEnv]
                 -- The template is already simplified, so don't re-substitute.
                 -- This is VITAL.  Consider
@@ -1266,13 +1300,14 @@ rebuildCall env (ArgInfo { ai_fun = fun, ai_args = rev_args, ai_strs = [] }) con
     res     = mkApps (Var fun) (reverse rev_args)
     res_ty  = exprType res
     cont_ty = contResultType env res_ty cont
-    co      = mkUnsafeCoercion res_ty cont_ty
-    mk_coerce expr | cont_ty `coreEqType` res_ty = expr
+    co      = mkUnsafeCo res_ty cont_ty
+    mk_coerce expr | cont_ty `eqType` res_ty = expr
                    | otherwise = mkCoerce co expr
 
-rebuildCall env info (ApplyTo _ (Type arg_ty) se cont)
-  = do  { ty' <- simplCoercion (se `setInScope` env) arg_ty
-        ; rebuildCall env (info `addArgTo` Type ty') cont }
+rebuildCall env info (ApplyTo dup_flag (Type arg_ty) se cont)
+  = do { arg_ty' <- if isSimplified dup_flag then return arg_ty
+                    else simplType (se `setInScope` env) arg_ty
+       ; rebuildCall env (info `addArgTo` Type arg_ty') cont }
 
 rebuildCall env info@(ArgInfo { ai_encl = encl_rules
                               , ai_strs = str:strs, ai_discs = disc:discs })
@@ -1280,7 +1315,7 @@ rebuildCall env info@(ArgInfo { ai_encl = encl_rules
   | isSimplified dup_flag     -- See Note [Avoid redundant simplification]
   = rebuildCall env (addArgTo info' arg) cont
 
-  | str 	        -- Strict argument
+  | str                 -- Strict argument
   = -- pprTrace "Strict Arg" (ppr arg $$ ppr (seIdSubst env) $$ ppr (seInScope env)) $
     simplExprF (arg_se `setFloats` env) arg
                (StrictArg info' cci cont)
@@ -1771,7 +1806,7 @@ improveSeq fam_envs env scrut case_bndr case_bndr1 [(DEFAULT,_,_)]
   | not (isDeadBinder case_bndr)	-- Not a pure seq!  See Note [Improving seq]
   , Just (co, ty2) <- topNormaliseType fam_envs (idType case_bndr1)
   = do { case_bndr2 <- newId (fsLit "nt") ty2
-        ; let rhs  = DoneEx (Var case_bndr2 `Cast` mkSymCoercion co)
+        ; let rhs  = DoneEx (Var case_bndr2 `Cast` mkSymCo co)
               env2 = extendIdSubst env case_bndr rhs
         ; return (env2, scrut `Cast` co, case_bndr2) }
 
@@ -1834,7 +1869,7 @@ simplAlt env scrut _ case_bndr' cont' (DataAlt con, vs, rhs)
         = go vs the_strs
         where
           go [] [] = []
-          go (v:vs') strs | isTyCoVar v = v : go vs' strs
+          go (v:vs') strs | isTyVar v = v : go vs' strs
           go (v:vs') (str:strs)
             | isMarkedStrict str = evald_v  : go vs' strs
             | otherwise          = zapped_v : go vs' strs
@@ -1933,7 +1968,7 @@ knownCon env scrut dc dc_ty_args dc_args bndr bs rhs cont
     bind_args env' [] _  = return env'
 
     bind_args env' (b:bs') (Type ty : args)
-      = ASSERT( isTyCoVar b )
+      = ASSERT( isTyVar b )
         bind_args (extendTvSubst env' b ty) bs' args
 
     bind_args env' (b:bs') (arg : args)
@@ -2151,7 +2186,7 @@ mkDupableAlt env case_bndr (con, bndrs', rhs')
 			  | otherwise		   = bndrs' ++ [case_bndr_w_unf]
 	      
               abstract_over bndr
-                  | isTyCoVar bndr = True -- Abstract over all type variables just in case
+                  | isTyVar bndr = True -- Abstract over all type variables just in case
                   | otherwise    = not (isDeadBinder bndr)
                         -- The deadness info on the new Ids is preserved by simplBinders