+
+doSwap :: Bool -> Coercion -> Coercion
+doSwap swap co = if swap then mkSymCoercion co else co
+
+extendReft :: Bool
+ -> InternalReft
+ -> TyVar
+ -> Coercion
+ -> Type
+ -> UM InternalReft
+extendReft swap subst tv co ty
+ = ASSERT2( (coercionKindPredTy co1 `tcEqType` mkCoKind (mkTyVarTy tv) ty),
+ (text "Refinement invariant failure: co = " <+> ppr co1 <+> ppr (coercionKindPredTy co1) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty)) )
+ return (extendVarEnv subst tv (co1, ty))
+ where
+ co1 = doSwap swap co
+