- (co1,co2) = coVarKind co_var\r
- co1' = opt_co' env sym co1\r
- co2' = opt_co' env sym co2\r
- cor' = opt_co' env sym cor\r
- co_var' = uniqAway (getTvInScope env) (mkWildCoVar (mkCoKind co1' co2'))\r
- -- See Note [Subtle shadowing in coercions]\r
-\r
-opt_co' env sym (TyConApp tc cos)\r
- | Just (arity, desc) <- isCoercionTyCon_maybe tc\r
- = mkAppTys (opt_co_tc_app env sym tc desc (take arity cos))\r
- (map (opt_co env sym) (drop arity cos))\r
- | otherwise\r
- = TyConApp tc (map (opt_co env sym) cos)\r
-\r
---------\r
-opt_co_tc_app :: TvSubst -> Bool -> TyCon -> CoTyConDesc -> [Coercion] -> NormalCo\r
--- Used for CoercionTyCons only\r
--- Arguments are *not* already simplified/substituted\r
-opt_co_tc_app env sym tc desc cos\r
- = case desc of\r
- CoAxiom {} -- Do *not* push sym inside top-level axioms\r
- -- e.g. if g is a top-level axiom\r
- -- g a : F a ~ a\r
- -- Then (sym (g ty)) /= g (sym ty) !!\r
- | sym -> mkSymCoercion the_co \r
- | otherwise -> the_co\r
- where\r
- the_co = TyConApp tc (map (opt_co env False) cos)\r
- -- Note that the_co does *not* have sym pushed into it\r
- \r
- CoTrans \r
- | sym -> opt_trans opt_co2 opt_co1 -- sym (g `o` h) = sym h `o` sym g\r
- | otherwise -> opt_trans opt_co1 opt_co2\r
-\r
- CoUnsafe\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
- CoRight -> opt_lr snd\r
- CoCsel1 -> opt_csel fstOf3\r
- CoCsel2 -> opt_csel sndOf3\r
- CoCselR -> opt_csel thirdOf3\r
-\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 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] [ty2'] opt_co1_body -- An inefficient one-variable substitution\r
-\r
- | otherwise\r
- -> TyConApp tc [opt_co1, ty2']\r