\r
opt_co' env _ (Refl ty) = Refl (substTy env ty)\r
opt_co' env sym (SymCo co) = opt_co env (not sym) co\r
- \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') -> ForAllCo tv' (opt_co env' sym co)\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