-unify with a polytype (see GHC.Tc.Utils.Unify.checkTypeEq).

-import GHC.Types.Var

-                              -- emptyCoHoleSet: rhs_redn has no CoercionHoles

-  = do { -- Do checkTypeEq to guarantee (TyEq:OC), (TyEq:F)

-       ; check_result <- checkTypeEq ev eq_rel lhs rhs

-{-

-              | reason `cterHasOnlyProblems` do_not_prevent_rewriting

-              ->   do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs

-                      ; continueWith $ Right $

-                        EqCt { eq_ev  = new_ev, eq_eq_rel = eq_rel

-                             , eq_lhs = lhs , eq_rhs = rhs } }

-

-              | otherwise

--}

-              -> -- Claim: there should be no new_eqs

-                 -- The non-unification check does non promotion nor type-family

-                 -- flattening for Wanteds

-                 do { emitWork new_eqs

-                    ; let new_holes = rewriterSetFromCts new_eqs

-                          lhs_ty    = canEqLHSType lhs

-                    ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn new_holes

-{-

--- | Some problems prevent /unification/ but not /rewriting/:

---

--- Skolem-escape: if we have [W] alpha[2] ~ Maybe b[3]

---    we can't unify (skolem-escape); but it /is/ canonical,

---    and hence we /can/ use it for rewriting

---

--- Concrete-ness:  alpha[conc] ~ b[sk]

---    We can use it to rewrite; we still have to solve the original

-do_not_prevent_rewriting :: CheckTyEqResult

-do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<>

-                           cteProblem cteConcrete

--}

-* In this case we call `checkTypeEq`to see if it is canonical (which in turn

-  calls `checkTypeEqRhs`).

-* Even if `checkTypeEq` returns `PuFail`, we may /still/ be able to add it to the inert

-  set, depending on the reason for failure; examples are given in `do_not_prevent_rewriting`.

-* NB: we do /not/ try to take advantage of the case where `canEqCanLHSFinish_try_unification`

-  has already called `checkTyEqRhs`; doing so caused #27844.   (The first call did fam-app

-  breaking, which concealed a genuine occurs check.)  It's just too clever; better to do

-  the simple thing.

-to our new cbv. This is actually done by `break_given` in

-`GHC.Tc.Solver.Monad.checkTypeEq`.

-    This is done during canonicalisation, in checkTypeEq; invariant

-    pprEq,

-

-    -- Enforcing invariants for type equalities

-    checkTypeEq

-checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType

-            -> TcS (PuResult Ct Reduction)

--- Used for general CanEqLHSs, ones that do

--- not have a touchable type variable on the LHS (i.e. not unifying)

-checkTypeEq ev eq_rel lhs rhs =

-  case ev of

-    CtGiven {} ->

-      do { traceTcS "checkTypeEq (given) {" (vcat [ text "lhs:" <+> ppr lhs

-                                                  , text "rhs:" <+> ppr rhs ])

-         ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs)

-         ; traceTcS "checkTypeEq }" (ppr check_result)

-         ; case check_result of

-              PuFail reason -> return (PuFail reason)

-              PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs

-                                  ; emitWork new_givens

-                                  ; updInertSet (addCycleBreakerBindings prs)

-                                  ; return (pure redn) } }

-    CtWanted {} -> do { traceTcS "checkTypeEq (wanted) {" $

-                        vcat [ text "lhs:" <+> ppr lhs

-                             , text "rhs:" <+> ppr rhs ]

-                      ; check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs)

-                      ; traceTcS "checkTypeEq }" (ppr check_result)

-                      ; return check_result }

-  where

-    wanted_flags :: TyEqFlags TcM Ct

-    wanted_flags = notUnifying_TEFTask occ_prob lhs

-                   -- checkTypeEq deals only with the non-unifying case

-

-    given_flags :: TyEqFlags TcM (TcTyVar, TcType)

-    given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven }

-        -- TEFA_Break used for: [G] a ~ Maybe (F a)

-        --                   or [G] F a ~ Maybe (F a)

-

-    -- occ_prob: see Note [Occurs check and representational equality]

-    occ_prob = case eq_rel of

-                 NomEq  -> cteInsolubleOccurs

-                 ReprEq -> cteSolubleOccurs

-

-    ---------------------------

-    mk_new_given :: (TcTyVar, TcType) -> TcS Ct

-    mk_new_given (new_tv, fam_app)

-      = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term)

-      where

-        new_ty     = mkTyVarTy new_tv

-        given_pred = mkNomEqPred fam_app new_ty

-        given_term = evCoercion $ mkNomReflCo new_ty  -- See Detail (4) of Note

-

-    -- See Detail (7) of the Note

-    cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin

-

--------------------------

-Note [Don't cycle-break Wanteds when not unifying]

-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-Consdier

-  [W] a[2] ~ Maybe (F a[2])

-

-Should we cycle-break this Wanted, thus?

-

-  [W] a[2] ~ Maybe delta[2]

-  [W] delta[2] ~ F a[2]

-

-For a start, this is dodgy because we might just unify delta, thus undoing

-what we have done, and getting an infinite loop in the solver.  Even if we

-somehow prevented ourselves from doing so, is there any merit in the split?

-Maybe: perhaps we can use that equality on `a` to unlock other constraints?

-Consider

-  type instance F (Maybe _) = Bool

-

-  [G] g1: a ~ Maybe Bool

-  [W] w1: a ~ Maybe (F a)

-

-If we loop-break w1 to get

-  [W] w1': a ~ Maybe gamma

-  [W] w3:  gamma ~ F a

-Now rewrite w3 with w1'

-  [W] w3':  gamma ~ F (Maybe gamma)

-Now use the type instance to get

-  gamma := Bool

-Now we are left with

-  [W] w1': a ~ Maybe Bool

-which we can solve from the Given.

-

-BUT in this situation we could have rewritten the

-/original/ Wanted from the Given, like this:

-  [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool))

-and that is readily soluble.

-

-In short: loop-breaking Wanteds, when we aren't unifying,

-seems of no merit.  Hence TEFA_Recurse, rather than TEFA_Break,

-in `wanted_flags` in `checkTypeEq`.

--- See 'checkTypeEq'.

--- (use the full 'checkTypeEq').

-in canEqCanLHS2, before getting to checkTypeEq.