--- opt_co sym co = pprTrace "opt_co {" (ppr sym <+> ppr co) $\r
--- co1 `seq` \r
--- pprTrace "opt_co done }" (ppr co1) \r
--- WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (s1,t1) \r
--- $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )\r
--- co1\r
--- where\r
--- co1 = opt_co' sym co\r
--- same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2\r
--- (s,t) = coercionKind co\r
--- (s1,t1) | sym = (t,s)\r
--- | otherwise = (s,t)\r
--- (s2,t2) = coercionKind co1\r
-\r
-opt_co' env sym (AppTy ty1 ty2) = mkAppTy (opt_co env sym ty1) (opt_co env sym ty2)\r
-opt_co' env sym (FunTy ty1 ty2) = FunTy (opt_co env sym ty1) (opt_co env sym ty2)\r
-opt_co' env sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co env sym) tys))\r
-opt_co' env sym (PredTy (IParam n ty)) = PredTy (IParam n (opt_co env sym ty))\r
-opt_co' _ _ co@(PredTy (EqPred {})) = pprPanic "optCoercion" (ppr co)\r
-\r
-opt_co' env sym co@(TyVarTy tv)\r
- | Just ty <- lookupTyVar env tv = opt_co' (zapTvSubstEnv env) sym ty\r
- | not (isCoVar tv) = co -- Identity; does not mention a CoVar\r
- | ty1 `coreEqType` ty2 = ty1 -- Identity; ..ditto..\r
- | not sym = co\r
- | otherwise = mkSymCoercion co\r
+{-\r
+opt_co env sym co\r
+ = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $\r
+ co1 `seq`\r
+ pprTrace "opt_co done }" (ppr co1) $\r
+ (WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (Pair s1 t1)\r
+ $$ ppr co1 <+> dcolon <+> pprEqPred (Pair s2 t2) )\r
+ WARN( not (coreEqCoercion co1 simple_result),\r
+ (text "env=" <+> ppr env) $$\r
+ (text "input=" <+> ppr co) $$\r
+ (text "simple=" <+> ppr simple_result) $$\r
+ (text "opt=" <+> ppr co1) )\r
+ co1)\r
+ where\r
+ co1 = opt_co' env sym co\r
+ same_co_kind = s1 `eqType` s2 && t1 `eqType` t2\r
+ Pair s t = coercionKind (substCo env co)\r
+ (s1,t1) | sym = (t,s)\r
+ | otherwise = (s,t)\r
+ Pair s2 t2 = coercionKind co1\r
+\r
+ simple_result | sym = mkSymCo (substCo env co)\r
+ | otherwise = substCo env co\r
+-}\r
+\r
+opt_co' env _ (Refl ty) = Refl (substTy env ty)\r
+opt_co' env sym (SymCo co) = opt_co env (not sym) co\r
+opt_co' env sym (TyConAppCo tc cos) = mkTyConAppCo tc (map (opt_co env sym) cos)\r
+opt_co' env sym (PredCo cos) = mkPredCo (fmap (opt_co env sym) cos)\r
+opt_co' env sym (AppCo co1 co2) = mkAppCo (opt_co env sym co1) (opt_co env sym co2)\r
+opt_co' env sym (ForAllCo tv co) = case substTyVarBndr env tv of\r
+ (env', tv') -> mkForAllCo tv' (opt_co env' sym co)\r
+ -- Use the "mk" functions to check for nested Refls\r
+\r
+opt_co' env sym (CoVarCo cv)\r
+ | Just co <- lookupCoVar env cv\r
+ = opt_co (zapCvSubstEnv env) sym co\r
+\r
+ | Just cv1 <- lookupInScope (getCvInScope env) cv\r
+ = ASSERT( isCoVar cv1 ) wrapSym sym (CoVarCo cv1)\r
+ -- cv1 might have a substituted kind!\r
+\r
+ | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)\r
+ ASSERT( isCoVar cv )\r
+ wrapSym sym (CoVarCo cv)\r
+\r
+opt_co' env sym (AxiomInstCo con cos)\r
+ -- 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
+ = wrapSym sym $ AxiomInstCo con (map (opt_co env False) cos)\r
+ -- Note that the_co does *not* have sym pushed into it\r
+\r
+opt_co' env sym (UnsafeCo ty1 ty2)\r
+ | ty1' `eqType` ty2' = Refl ty1'\r
+ | sym = mkUnsafeCo ty2' ty1'\r
+ | otherwise = mkUnsafeCo ty1' ty2'\r