| otherwise -> opt_trans opt_co1 opt_co2\r
\r
CoUnsafe\r
- | sym -> TyConApp tc [opt_co2,opt_co1]\r
- | otherwise -> TyConApp tc [opt_co1,opt_co2]\r
+ | sym -> mkUnsafeCoercion ty2' ty1'\r
+ | otherwise -> mkUnsafeCoercion ty1' ty2'\r
\r
CoSym -> opt_co env (not sym) co1\r
CoLeft -> opt_lr fst\r
CoInst -- See if the first arg is already a forall\r
-- ...then we can just extend the current substitution\r
| Just (tv, co1_body) <- splitForAllTy_maybe co1\r
- -> opt_co (extendTvSubst env tv ty') sym co1_body\r
+ -> opt_co (extendTvSubst env tv ty2') sym co1_body\r
\r
-- See if is *now* a forall\r
| Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1\r
- -> substTyWith [tv] [ty'] opt_co1_body -- An inefficient one-variable substitution\r
+ -> substTyWith [tv] [ty2'] opt_co1_body -- An inefficient one-variable substitution\r
\r
| otherwise\r
- -> TyConApp tc [opt_co1, ty']\r
- where\r
- ty' = substTy env co2\r
+ -> TyConApp tc [opt_co1, ty2']\r
\r
where\r
(co1 : cos1) = cos\r
(co2 : _) = cos1\r
\r
+ ty1' = substTy env co1\r
+ ty2' = substTy env co2\r
+\r
-- These opt_cos have the sym pushed into them\r
opt_co1 = opt_co env sym co1\r
opt_co2 = opt_co env sym co2\r
= Nothing\r
\r
etaApp_maybe :: Coercion -> Maybe (Coercion, Coercion)\r
+-- Split a coercion g :: t1a t1b ~ t2a t2b\r
+-- into (left g, right g) if possible\r
etaApp_maybe co\r
| Just (co1, co2) <- splitAppTy_maybe co\r
= Just (co1, co2)\r