The final batch of changes for the new coercion representation

* Fix bugs in the packing and unpacking of data
  constructors with equality predicates in their types

* Remove PredCo altogether; instead, coercions between predicated
  types (like  (Eq a, [a]~b) => blah) are treated as if they
  were precisely their underlying representation type
       Eq a -> ((~) [a] b) -> blah
  in this case

* Similarly, Type.coreView no longer treats equality
  predciates specially.

* Implement the cast-of-coercion optimisation in
  Simplify.simplCoercionF

Numerous other small bug-fixes and refactorings.

Annoyingly, OptCoercion had Windows line endings, and this
patch switches to Unix, so it looks as if every line has changed.

compiler/basicTypes/DataCon.lhs

@@ -659,7 +659,7 @@ dataConStrictMarks = dcStrictMarks
 -- | Strictness of evidence arguments to the wrapper function
 dataConExStricts :: DataCon -> [HsBang]
 -- Usually empty, so we don't bother to cache this
-dataConExStricts dc = map mk_dict_strict_mark $ (dcOtherTheta dc)
+dataConExStricts dc = map mk_dict_strict_mark $ (dataConTheta dc)
 
 -- | Source-level arity of the data constructor
 dataConSourceArity :: DataCon -> Arity

compiler/basicTypes/MkId.lhs

@@ -230,7 +230,7 @@ mkDataConIds wrap_name wkr_name data_con
   = DCIds Nothing wrk_id
   where
     (univ_tvs, ex_tvs, eq_spec, 
-     theta, orig_arg_tys, res_ty) = dataConFullSig data_con
+     other_theta, orig_arg_tys, res_ty) = dataConFullSig data_con
     tycon = dataConTyCon data_con       -- The representation TyCon (not family)
 
         ----------- Worker (algebraic data types only) --------------
@@ -293,7 +293,7 @@ mkDataConIds wrap_name wkr_name data_con
         -- extra constraints where necessary.
     wrap_tvs    = (univ_tvs `minusList` map fst eq_spec) ++ ex_tvs
     res_ty_args = substTyVars (mkTopTvSubst eq_spec) univ_tvs
-    ev_tys      = mkPredTys theta
+    ev_tys      = mkPredTys other_theta
     wrap_ty     = mkForAllTys wrap_tvs $ 
                   mkFunTys ev_tys $
                   mkFunTys orig_arg_tys $ res_ty
@@ -309,8 +309,9 @@ mkDataConIds wrap_name wkr_name data_con
                     `setStrictnessInfo` Just wrap_sig
 
     all_strict_marks = dataConExStricts data_con ++ dataConStrictMarks data_con
-    wrap_sig = mkStrictSig (mkTopDmdType arg_dmds cpr_info)
-    arg_dmds = map mk_dmd all_strict_marks
+    wrap_sig = mkStrictSig (mkTopDmdType wrap_arg_dmds cpr_info)
+    wrap_stricts = dropList eq_spec all_strict_marks
+    wrap_arg_dmds = map mk_dmd wrap_stricts
     mk_dmd str | isBanged str = evalDmd
                | otherwise    = lazyDmd
         -- The Cpr info can be important inside INLINE rhss, where the
@@ -327,8 +328,11 @@ mkDataConIds wrap_name wkr_name data_con
                mkLams ev_args $
                mkLams id_args $
                foldr mk_case con_app 
-                     (zip (ev_args ++ id_args) all_strict_marks)
+                     (zip (ev_args ++ id_args) wrap_stricts)
                      i3 []
+	     -- The ev_args is the evidence arguments *other than* the eq_spec
+	     -- Because we are going to apply the eq_spec args manually in the
+	     -- wrapper
 
     con_app _ rep_ids = wrapFamInstBody tycon res_ty_args $
                           Var wrk_id `mkTyApps`  res_ty_args
@@ -598,7 +602,7 @@ mkProductBox arg_ids ty
 mkReboxingAlt
   :: [Unique] -- Uniques for the new Ids
   -> DataCon
-  -> [Var]    -- Source-level args, including existential dicts
+  -> [Var]    -- Source-level args, *including* all evidence vars 
   -> CoreExpr -- RHS
   -> CoreAlt
 
@@ -626,8 +630,7 @@ mkReboxingAlt us con args rhs
         -- Term variable case
     go (arg:args) (str:stricts) us
       | isMarkedUnboxed str
-      = 
-        let (binds, unpacked_args')        = go args stricts us'
+      = let (binds, unpacked_args')        = go args stricts us'
             (us', bind_rhs, unpacked_args) = reboxProduct us (idType arg)
         in
             (NonRec arg bind_rhs : binds, unpacked_args ++ unpacked_args')

compiler/coreSyn/CoreFVs.lhs

@@ -513,9 +513,8 @@ freeVars (Let (Rec binds) body)
     body2     = freeVars body
     body_fvs  = freeVarsOf body2
 
-
 freeVars (Cast expr co)
-  = (freeVarsOf expr2 `unionFVs` cfvs, AnnCast expr2 co)
+  = (freeVarsOf expr2 `unionFVs` cfvs, AnnCast expr2 (cfvs, co))
   where
     expr2 = freeVars expr
     cfvs  = tyCoVarsOfCo co

compiler/coreSyn/CoreLint.lhs

@@ -646,20 +646,6 @@ lintCoercion (ForAllCo v co)
        ; (s,t) <- addInScopeVar v (lintCoercion co)
        ; return (ForAllTy v s, ForAllTy v t) }
 
-lintCoercion co@(PredCo (ClassP cls cos))
-  = do { (ss,ts) <- mapAndUnzipM lintCoercion cos
-       ; check_co_app co (tyConKind (classTyCon cls)) ss
-       ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
-
-lintCoercion (PredCo (IParam ip co))
-  = do { (s,t) <- lintCoercion co
-       ; return (PredTy (IParam ip s), PredTy (IParam ip t)) }
-
-lintCoercion (PredCo (EqPred c1 c2))
-  = do { (s1,t1) <- lintCoercion c1
-       ; (s2,t2) <- lintCoercion c2
-       ; return (PredTy (EqPred s1 s2), PredTy (EqPred t1 t2)) }
-
 lintCoercion (CoVarCo cv)
   = do { checkTyCoVarInScope cv
        ; return (coVarKind cv) }

compiler/coreSyn/CoreSyn.lhs

@@ -1191,7 +1191,8 @@ data AnnExpr' bndr annot
   | AnnApp	(AnnExpr bndr annot) (AnnExpr bndr annot)
   | AnnCase	(AnnExpr bndr annot) bndr Type [AnnAlt bndr annot]
   | AnnLet	(AnnBind bndr annot) (AnnExpr bndr annot)
-  | AnnCast     (AnnExpr bndr annot) Coercion
+  | AnnCast     (AnnExpr bndr annot) (annot, Coercion)
+    		   -- Put an annotation on the (root of) the coercion
   | AnnNote	Note (AnnExpr bndr annot)
   | AnnType	Type
   | AnnCoercion Coercion
@@ -1227,7 +1228,7 @@ deAnnotate' (AnnVar  v)           = Var v
 deAnnotate' (AnnLit  lit)         = Lit lit
 deAnnotate' (AnnLam  binder body) = Lam binder (deAnnotate body)
 deAnnotate' (AnnApp  fun arg)     = App (deAnnotate fun) (deAnnotate arg)
-deAnnotate' (AnnCast e co)        = Cast (deAnnotate e) co
+deAnnotate' (AnnCast e (_,co))    = Cast (deAnnotate e) co
 deAnnotate' (AnnNote note body)   = Note note (deAnnotate body)
 
 deAnnotate' (AnnLet bind body)

compiler/coreSyn/MkExternalCore.lhs

@@ -13,8 +13,8 @@ import Module
 import CoreSyn
 import HscTypes	
 import TyCon
-import Class
-import TysPrim( eqPredPrimTyCon )
+-- import Class
+-- import TysPrim( eqPredPrimTyCon )
 import TypeRep
 import Type
 import PprExternalCore () -- Instances
@@ -289,9 +289,6 @@ make_co (Refl ty)             = make_ty ty
 make_co (TyConAppCo tc cos)   = make_conAppCo (qtc tc) cos
 make_co (AppCo c1 c2)         = C.Tapp (make_co c1) (make_co c2)
 make_co (ForAllCo tv co)      = C.Tforall (make_tbind tv) (make_co co)
-make_co (PredCo (ClassP cls cos)) = make_conAppCo (qtc (classTyCon cls)) cos
-make_co (PredCo (IParam _ co))    = make_co co
-make_co (PredCo (EqPred co1 co2)) = make_conAppCo (qtc eqPredPrimTyCon) [co1,co2]
 make_co (CoVarCo cv)          = C.Tvar (make_var_id (coVarName cv))
 make_co (AxiomInstCo cc cos)  = make_conAppCo (qcc cc) cos
 make_co (UnsafeCo t1 t2)      = C.UnsafeCoercion (make_ty t1) (make_ty t2)

compiler/deSugar/DsUtils.lhs

@@ -296,10 +296,11 @@ mkCoPrimCaseMatchResult var ty match_alts
                                                   return (LitAlt lit, [], body)
 
 
-mkCoAlgCaseMatchResult :: Id					-- Scrutinee
-                    -> Type                                     -- Type of exp
-		    -> [(DataCon, [CoreBndr], MatchResult)]	-- Alternatives
-		    -> MatchResult
+mkCoAlgCaseMatchResult 
+  :: Id					   -- Scrutinee
+  -> Type                                  -- Type of exp
+  -> [(DataCon, [CoreBndr], MatchResult)]  -- Alternatives (bndrs *include* tyvars, dicts)
+  -> MatchResult
 mkCoAlgCaseMatchResult var ty match_alts 
   | isNewTyCon tycon		-- Newtype case; use a let
   = ASSERT( null (tail match_alts) && null (tail arg_ids1) )

compiler/iface/IfaceType.lhs

@@ -408,7 +408,6 @@ coToIfaceType (AppCo co1 co2)       = IfaceAppTy    (coToIfaceType co1)
                                                     (coToIfaceType co2)
 coToIfaceType (ForAllCo v co)       = IfaceForAllTy (toIfaceTvBndr v) 
                                                     (coToIfaceType co)
-coToIfaceType (PredCo pco)          = IfacePredTy (toIfacePred coToIfaceType pco)
 coToIfaceType (CoVarCo cv)          = IfaceTyVar  (toIfaceTyCoVar cv)
 coToIfaceType (AxiomInstCo con cos) = IfaceCoConApp (IfaceCoAx (coAxiomName con))
                                                     (map coToIfaceType cos)

compiler/iface/TcIface.lhs

@@ -826,7 +826,8 @@ tcIfaceCo (IfaceTyConApp tc ts) = mkTyConAppCo <$> tcIfaceTyCon tc <*> mapM tcIf
 tcIfaceCo (IfaceCoConApp tc ts) = tcIfaceCoApp tc ts
 tcIfaceCo (IfaceForAllTy tv t)  = bindIfaceTyVar tv $ \ tv' ->
                                   mkForAllCo tv' <$> tcIfaceCo t
-tcIfaceCo (IfacePredTy co)      = mkPredCo <$> tcIfacePred tcIfaceCo co
+-- tcIfaceCo (IfacePredTy co)      = mkPredCo <$> tcIfacePred tcIfaceCo co
+tcIfaceCo (IfacePredTy _)      = panic "tcIfaceCo"
 
 tcIfaceCoApp :: IfaceCoCon -> [IfaceType] -> IfL Coercion
 tcIfaceCoApp IfaceReflCo    [t]     = Refl         <$> tcIfaceType t

compiler/main/PprTyThing.hs

@@ -23,6 +23,7 @@ import DataCon
 import Id
 import IdInfo
 import TyCon
+import Coercion( pprCoAxiom )
 import TcType
 import Name
 import Outputable
@@ -56,7 +57,7 @@ ppr_ty_thing :: PrintExplicitForalls -> ShowMe -> TyThing -> SDoc
 ppr_ty_thing pefas _ 	 (AnId id)          = pprId         pefas id
 ppr_ty_thing pefas _ 	 (ADataCon dataCon) = pprDataConSig pefas dataCon
 ppr_ty_thing pefas show_me (ATyCon tyCon)   = pprTyCon      pefas show_me tyCon
-ppr_ty_thing _     _       (ACoAxiom _  )   = error "ppr_ty_thing (ACoCon)"  -- BAY
+ppr_ty_thing _     _       (ACoAxiom ax)    = pprCoAxiom    ax
 ppr_ty_thing pefas show_me (AClass cls)     = pprClass      pefas show_me cls
 
 -- | Pretty-prints a 'TyThing' in context: that is, if the entity
@@ -94,7 +95,7 @@ pprTyThingHdr :: PrintExplicitForalls -> TyThing -> SDoc
 pprTyThingHdr pefas (AnId id)          = pprId         pefas id
 pprTyThingHdr pefas (ADataCon dataCon) = pprDataConSig pefas dataCon
 pprTyThingHdr pefas (ATyCon tyCon)     = pprTyConHdr   pefas tyCon
-pprTyThingHdr _     (ACoAxiom _)       = error "pprTyThingHdr (ACoCon)" -- BAY
+pprTyThingHdr _     (ACoAxiom ax)      = pprCoAxiom ax
 pprTyThingHdr pefas (AClass cls)       = pprClassHdr   pefas cls
 
 pprTyConHdr :: PrintExplicitForalls -> TyCon -> SDoc

compiler/simplCore/FloatIn.lhs

@@ -126,16 +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 (_, AnnCoercion co) = ASSERT( null to_drop )
-                                     Coercion co
-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

compiler/simplCore/SetLevels.lhs

@@ -288,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)
 
@@ -415,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) }
 

compiler/simplCore/SimplEnv.lhs

@@ -279,7 +279,8 @@ 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
@@ -560,8 +561,6 @@ simplBinder :: SimplEnv -> InBndr -> SimplM (SimplEnv, OutBndr)
 simplBinder env bndr
   | isTyVar bndr  = do	{ let (env', tv) = substTyVarBndr env bndr
 			; seqTyVar tv `seq` return (env', tv) }
-  | isCoVar bndr  = do  { let (env', tv) = substCoVarBndr env bndr
-			; seqId tv `seq` return (env', tv) }
   | otherwise     = do	{ let (env', id) = substIdBndr env bndr
 			; seqId id `seq` return (env', id) }
 
@@ -597,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
@@ -617,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

compiler/simplCore/SimplUtils.lhs

@@ -99,6 +99,7 @@ data SimplCont
 
   | CoerceIt 		-- C `cast` co
 	OutCoercion		-- The coercion simplified
+				-- Invariant: never an identity coercion
 	SimplCont
 
   | ApplyTo  		-- C arg
@@ -788,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
@@ -795,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
@@ -892,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

compiler/simplCore/Simplify.lhs

@@ -369,9 +369,10 @@ 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
-  | Coercion co <- new_rhs
+  | 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
@@ -628,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
@@ -643,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
@@ -872,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 = simplIdF 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
@@ -905,16 +913,7 @@ simplExprF' env expr@(Lam {}) cont
     zap b | isTyVar b = b
           | otherwise = zapLamIdInfo b
 
-simplExprF' env (Type ty) cont
-  = ASSERT( contIsRhsOrArg cont )
-    rebuild env (Type (substTy env ty)) cont
-
-simplExprF' env (Coercion co) cont
-  = ASSERT( contIsRhsOrArg cont )
-    do  { co' <- simplCoercion env co
-        ; rebuild env (Coercion co') cont }
-
-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)
@@ -926,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
@@ -934,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
 
 ---------------------------------
@@ -947,12 +946,30 @@ simplType env ty
     new_ty = substTy env ty
 
 ---------------------------------
+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
-  = -- pprTrace "simplCoercion" (ppr co $$ ppr (getCvSubst env)) $
-    seqCo new_co `seq` return new_co
-  where 
-    new_co = optCoercion (getCvSubst env) co
+  = let opt_co = optCoercion (getCvSubst env) co
+    in opt_co `seq` return opt_co
 \end{code}
 
 
@@ -969,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
@@ -1011,7 +1028,7 @@ simplCast env body co0 cont0
                 -- and we'd like it to simplify to e[y/x] in one round
                 -- of simplification
          , s1 `eqType` t1  = cont            -- The coerces cancel out
-         | otherwise           = CoerceIt (mkTransCo co1 co2) cont
+         | otherwise       = CoerceIt (mkTransCo co1 co2) cont
 
        add_coerce co (Pair s1s2 _t1t2) (ApplyTo dup (Type arg_ty) arg_se cont)
                 -- (f |> g) ty  --->   (f ty) |> (g @ ty)
@@ -1141,18 +1158,13 @@ simplNonRecE env bndr (Type ty_arg, rhs_se) (bndrs, body) cont
     do	{ ty_arg' <- simplType (rhs_se `setInScope` env) ty_arg
 	; simplLam (extendTvSubst env bndr ty_arg') bndrs body cont }
 
-simplNonRecE env bndr (Coercion co_arg, rhs_se) (bndrs, body) cont
-  = ASSERT( isCoVar bndr )
-    do  { co_arg' <- simplCoercion (rhs_se `setInScope` env) co_arg
-        ; simplLam (extendCvSubst env bndr co_arg') bndrs body cont }
-
 simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
   | preInlineUnconditionally env NotTopLevel bndr rhs
   = do  { tick (PreInlineUnconditionally bndr)
         ; -- 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) }
 
@@ -1297,11 +1309,6 @@ rebuildCall env info (ApplyTo dup_flag (Type arg_ty) se cont)
                     else simplType (se `setInScope` env) arg_ty
        ; rebuildCall env (info `addArgTo` Type arg_ty') cont }
 
-rebuildCall env info (ApplyTo dup_flag (Coercion arg_co) se cont)
-  = do { arg_co' <- if isSimplified dup_flag then return arg_co
-                    else simplCoercion (se `setInScope` env) arg_co
-       ; rebuildCall env (info `addArgTo` Coercion arg_co') cont }
-
 rebuildCall env info@(ArgInfo { ai_encl = encl_rules
                               , ai_strs = str:strs, ai_discs = disc:discs })
             (ApplyTo dup_flag arg arg_se cont)

compiler/stgSyn/CoreToStg.lhs

@@ -312,8 +312,9 @@ on these components, but it in turn is not scrutinised as the basis for any
 decisions.  Hence no black holes.
 
 \begin{code}
-coreToStgExpr (Lit l) = return (StgLit l, emptyFVInfo, emptyVarSet)
-coreToStgExpr (Var v) = coreToStgApp Nothing v []
+coreToStgExpr (Lit l)      = return (StgLit l, emptyFVInfo, emptyVarSet)
+coreToStgExpr (Var v)      = coreToStgApp Nothing v               []
+coreToStgExpr (Coercion _) = coreToStgApp Nothing coercionTokenId []
 
 coreToStgExpr expr@(App _ _)
   = coreToStgApp Nothing f args

compiler/typecheck/TcEnv.lhs

@@ -626,7 +626,6 @@ data InstBindings a
 			-- witness dictionary is identical to the argument 
 			-- dictionary.  Hence no bindings, no pragmas.
 
-          -- BAY* : should this be a CoAxiom?
 	Coercion	-- The coercion maps from newtype to the representation type
 			-- (mentioning type variables bound by the forall'd iSpec variables)
 			-- E.g.   newtype instance N [a] = N1 (Tree a)

compiler/typecheck/TcHsSyn.lhs

@@ -52,7 +52,7 @@ import SrcLoc
 import Bag
 import FastString
 import Outputable
-import Data.Traversable( traverse )
+-- import Data.Traversable( traverse )
 \end{code}
 
 \begin{code}
@@ -1129,7 +1129,6 @@ zonkTcCoToCo env co
     go (AxiomInstCo ax cos) = do { cos' <- mapM go cos; return (AxiomInstCo ax cos') }
     go (AppCo co1 co2)      = do { co1' <- go co1; co2' <- go co2
                                  ; return (mkAppCo co1' co2') }
-    go (PredCo pco)         = do { pco' <- go `traverse` pco; return (mkPredCo pco') }
     go (UnsafeCo t1 t2)     = do { t1' <- zonkTcTypeToType env t1
                                  ; t2' <- zonkTcTypeToType env t2
                                  ; return (mkUnsafeCo t1' t2') }

compiler/typecheck/TcRnDriver.lhs

@@ -72,7 +72,6 @@ import Outputable
 import DataCon
 import Type
 import Class
-import Pair
 import TcType   ( orphNamesOfDFunHead )
 import Inst	( tcGetInstEnvs )
 import Data.List ( sortBy )
@@ -1612,7 +1611,7 @@ ppr_tycons fam_insts type_env
   = vcat [ text "TYPE CONSTRUCTORS"
          ,   nest 2 (ppr_tydecls tycons)
          , text "COERCION AXIOMS" 
-         ,   nest 2 (ppr_axioms (typeEnvCoAxioms type_env)) ]
+         ,   nest 2 (vcat (map pprCoAxiom (typeEnvCoAxioms type_env))) ]
   where
     fi_tycons = map famInstTyCon fam_insts
     tycons = [tycon | tycon <- typeEnvTyCons type_env, want_tycon tycon]
@@ -1647,14 +1646,6 @@ ppr_tydecls tycons
     ppr_tycon tycon = ppr (tyThingToIfaceDecl (ATyCon tycon))
       where
 
-ppr_axioms :: [CoAxiom] -> SDoc
-ppr_axioms axs
-  = vcat (map ppr_ax axs)
-  where
-    ppr_ax ax = sep [ ptext (sLit "coercion") <+> ppr ax <+> ppr (co_ax_tvs ax)
-                    , nest 2 (dcolon <+> pprEqPred 
-                                           (Pair (co_ax_lhs ax) (co_ax_rhs ax))) ]
-
 ppr_rules :: [CoreRule] -> SDoc
 ppr_rules [] = empty
 ppr_rules rs = vcat [ptext (sLit "{-# RULES"),

compiler/typecheck/TcType.lhs

@@ -169,8 +169,6 @@ import ListSetOps
 import Outputable
 import FastString
 
-import qualified Data.Foldable as Foldable
-import Data.Functor( (<$>) )
 import Data.List( mapAccumL )
 import Data.IORef
 \end{code}
@@ -545,7 +543,6 @@ tidyCo env@(_, subst) co
     go (ForAllCo tv co)      = ForAllCo tvp $! (tidyCo envp co)
                                where
                                  (envp, tvp) = tidyTyVarBndr env tv
-    go (PredCo pco)          = PredCo $! (go <$> pco)
     go (CoVarCo cv)          = case lookupVarEnv subst cv of
                                  Nothing  -> CoVarCo cv
                                  Just cv' -> CoVarCo cv'
@@ -1079,8 +1076,6 @@ orphNamesOfCo (Refl ty)             = orphNamesOfType ty
 orphNamesOfCo (TyConAppCo tc cos)   = unitNameSet (getName tc) `unionNameSets` orphNamesOfCos cos
 orphNamesOfCo (AppCo co1 co2)       = orphNamesOfCo co1 `unionNameSets` orphNamesOfCo co2
 orphNamesOfCo (ForAllCo _ co)       = orphNamesOfCo co
-orphNamesOfCo (PredCo p)            = Foldable.foldr (unionNameSets . orphNamesOfCo)
-                                                      emptyNameSet p
 orphNamesOfCo (CoVarCo _)           = emptyNameSet
 orphNamesOfCo (AxiomInstCo con cos) = orphNamesOfCoCon con `unionNameSets` orphNamesOfCos cos
 orphNamesOfCo (UnsafeCo ty1 ty2)    = orphNamesOfType ty1 `unionNameSets` orphNamesOfType ty2

compiler/types/FunDeps.lhs

@@ -386,7 +386,7 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
                     fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' irs2'
                         -- Don't discard anything! 
                         -- We could discard equal types but it's an overkill to call 
-                        -- tcEqType again, since we know for sure that /at least one/ 
+                        -- eqType again, since we know for sure that /at least one/ 
                         -- equation in there is useful)
 
 		    qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs

compiler/types/Type.lhs

@@ -231,31 +231,9 @@ coreView :: Type -> Maybe Type
 -- its underlying representation type. 
 -- Returns Nothing if there is nothing to look through.
 --
--- In the case of @newtype@s, it returns one of:
---
--- 1) A vanilla 'TyConApp' (recursive newtype, or non-saturated)
--- 
--- 2) The newtype representation (otherwise), meaning the
---    type written in the RHS of the newtype declaration,
---    which may itself be a newtype
---
--- For example, with:
---
--- > newtype R = MkR S
--- > newtype S = MkS T
--- > newtype T = MkT (T -> T)
---
--- 'expandNewTcApp' on:
---
---  * @R@ gives @Just S@
---  * @S@ gives @Just T@
---  * @T@ gives @Nothing@ (no expansion)
-
 -- By being non-recursive and inlined, this case analysis gets efficiently
 -- joined onto the case analysis that the caller is already doing
-coreView (PredTy p)
---  | isEqPred p             = Nothing
-  | otherwise    	   = Just (predTypeRep p)
+coreView (PredTy p)        = Just (predTypeRep p)
 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys 
 			   = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
 				-- Its important to use mkAppTys, rather than (foldl AppTy),
@@ -264,7 +242,6 @@ coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc
 coreView _                 = Nothing
 
 
-
 -----------------------------------------------
 {-# INLINE tcView #-}
 tcView :: Type -> Maybe Type
@@ -382,10 +359,9 @@ repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
 repSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 repSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 repSplitAppTy_maybe (TyConApp tc tys) 
-  | isDecomposableTyCon tc || length tys > tyConArity tc 
-  = case snocView tys of       -- never create unsaturated type family apps
-      Just (tys', ty') -> Just (TyConApp tc tys', ty')
-      Nothing	       -> Nothing
+  | isDecomposableTyCon tc || tys `lengthExceeds` tyConArity tc 
+  , Just (tys', ty') <- snocView tys
+  = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
 repSplitAppTy_maybe _other = Nothing
 -------------
 splitAppTy :: Type -> (Type, Type)