-simplCoercion :: SimplEnv -> InType -> SimplM OutType
--- The InType isn't *necessarily* a coercion, but it might be
--- (in a type application, say) and optCoercion is a no-op on types
+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