+ ; (ret_co, rhs_var, ct) <-
+ if isGiven fl then
+ do { rhs_var <- newFlattenSkolemTy fam_ty
+ ; cv <- newGivOrDerCoVar fam_ty rhs_var fam_co
+ ; let ct = CFunEqCan { cc_id = cv
+ , cc_flavor = fl -- Given
+ , cc_fun = tc
+ , cc_tyargs = xi_args
+ , cc_rhs = rhs_var }
+ ; return $ (mkCoVarCoercion cv, rhs_var, ct) }
+ else -- Derived or Wanted: make a new *unification* flatten variable
+ do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
+ ; cv <- newWantedCoVar fam_ty rhs_var
+ ; let ct = CFunEqCan { cc_id = cv
+ , cc_flavor = mkWantedFlavor fl
+ -- Always Wanted, not Derived
+ , cc_fun = tc
+ , cc_tyargs = xi_args
+ , cc_rhs = rhs_var }
+ ; return $ (mkCoVarCoercion cv, rhs_var, ct) }
+
+ ; return ( foldl AppTy rhs_var xi_rest
+ , foldl AppTy (mkSymCoercion ret_co
+ `mkTransCoercion` mkTyConCoercion tc cos_args) cos_rest
+ , ccs `extendCCans` ct) }