= return False

   where

     -- try_default_tv_nom: used for tv ~#N ty

     try_default_tv_nom lhs_tv rhs_ty

       | MetaTv { mtv_info = info } <- tcTyVarDetails lhs_tv

           = do { traceTcS "defaultEquality success:" (ppr rhs_ty)

                ; unifyTyVar lhs_tv rhs_ty  -- NB: unifyTyVar adds to the

                                            -- TcS unification counter

                ; return True

                }

             -- This handles cases such as @IO alpha[tau] ~R# IO Int@

             -- by defaulting @alpha := Int@, which is useful in practice

             -- (see Note [Defaulting representational equalities]).

                               -- NB: nominal equality!

                               uType uenv z_ty1 z_ty2

             -- See Note [Defaulting representational equalities].

            ; if null new_eqs

              then do { traceTcS "defaultEquality ReprEq } (yes)" empty

                        CPH { cph_co = mkSubCo co, cph_holes = emptyCoHoleSet }

                      ; return True }

              else do { traceTcS "defaultEquality ReprEq } (no)" empty

 -- | Solving Class constraints CDictCan

 module GHC.Tc.Solver.Dict (

   solveDict, solveDictNC, solveCallStack,

   matchLocalInst, chooseInstance,

   makeSuperClasses, mkStrictSuperClasses

   ) where

                         , cir_mk_ev       = mk_ev

                         , cir_canonical   = canonical })

   = do { traceTcS "doTopReact/found instance for" $ ppr work_item

        ; assertPprM (getTcEvBindsVar >>= return . not . isCoEvBindsVar)

                     (ppr work_item)

        ; evc_vars <- mapM (newWanted deeper_loc rws) theta

 chooseInstance work_item lookup_res

   = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res)

 matchClassInst :: DynFlags -> InertSet

                -> Class -> [Type]

                -> CtLoc -> TcS ClsInstResult

 -- See Note [Solving forall equalities]

 can_eq_nc_forall ev eq_rel s1 s2

  = do { let (bndrs1, phi1, bndrs2, phi2) = split_foralls s1 s2

             flags1 = binderFlags bndrs1

             flags2 = binderFlags bndrs2

                 do { -- Generate constraints

                      (tclvl, (all_co, wanteds))

                           <- pushLevelNoWorkList (ppr skol_info) $

                              go uenv skol_tvs init_subst2 bndrs1 bndrs2

                    ; traceTcS "Trying to solve the implication" (ppr s1 $$ ppr s2 $$ ppr wanteds)

          -- Check for blowing our stack, and increase the depth

          -- See Note [Newtypes can blow the stack]

          -- Next, we record uses of newtype constructors, since coercing

          -- through newtypes is tantamount to using their constructors.

               ; emitWorkNC [CtGiven kind_ev]

               ; finish emptyCoHoleSet (givenCtEvCoercion kind_ev) }

          -> do { (unifs, (kind_co, eqs)) <- reportFineGrainUnifications $

                                             let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2)

                                             in uType uenv' ki2 ki1

                       -- kind_co :: ki2 ~N ki1

 import GHC.Core.Coercion

 import GHC.Core.Predicate( EqRel(..) )

 import GHC.Core.TyCon

 import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart )

 import GHC.Core.Coercion.Axiom

 import GHC.Core.TyCo.Subst( elemSubst )

 import GHC.Utils.Outputable

 import GHC.Utils.Panic

 import GHC.Data.Pair

 import Data.Maybe( isNothing, isJust, mapMaybe )

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

 mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> Xi -> TcS [FunDepEqns]

 mkTopClosedFamEqFDs ax work_args work_rhs

   = do { let branches = fromBranches (coAxiomBranches ax)

        ; traceTcS "mkTopClosed" (ppr branches $$ ppr work_args $$ ppr work_rhs)

        ; case getRelevantBranches ax work_args work_rhs of

            [eqn] -> return [eqn]  -- If there is just one relevant equation, use it

            _     -> return [] }

 hasRelevantGiven :: [EqCt] -> [TcType] -> EqCt -> Bool

 -- A Given is relevant if it is not apart from the Wanted

   = return False -- Common case no-op

   | otherwise

              <- reportFineGrainUnifications $

                 nestFunDepsTcS              $

                 TcS.pushTcLevelM_           $

                    -- pushTcLevelTcM: increase the level so that unification variables

                    -- allocated by the fundep-creation itself don't count as useful unifications

                    -- See Note [Deeper TcLevel for partial improvement unification variables]

                    ; solveSimpleWanteds eqs }

     -- Why solveSimpleWanteds?  Answer

     --     (a) We don't want to rely on the eager unifier being clever

   | null tvs

   = return rev_eqs

   | otherwise

        ; (_, subst) <- instFlexiXTcM emptySubst tvs  -- Takes account of kind substitution

        ; return (map (subst_pair subst) rev_eqs) }

   where

     setEvBind, setWantedEq, setWantedDict, setEqIfWanted, setDictIfWanted,

     fillCoercionHole,

     newEvVar, newGivenEv, emitNewGivens,

     getInstEnvs, getFamInstEnvs,                -- Getting the environments

     getTopEnv, getGblEnv, getLclEnv, setSrcSpan,

              pick_me ct new_wl

                = do { writeTcRef wl_var new_wl

                     ; return (Just ct) }

              -- try_rws looks through rw_eqs to find one that has an empty

              -- rewriter set, after zonking.  If none such, call try_rest.

 -- | Checks if the depth of the given location is too much. Fails if

 -- it's too big, with an appropriate error message.

   = do { dflags <- getDynFlags

        ; when (subGoalDepthExceeded (reductionDepth dflags) (ctLocDepth loc)) $

 matchFam :: TyCon -> [Type] -> TcS (Maybe ReductionN)

 matchFam tycon args = wrapTcS $ matchFamTcM tycon args

 --    returns a CoHoleSet describing the new unsolved goals

 wrapUnifierAndEmit ev role do_unifications

   = do { (unifs, (co, eqs)) <- reportFineGrainUnifications $

        -- Emit the deferred constraints

        ; emitChildEqs ev eqs

        ; return (CPH { cph_co = co, cph_holes = rewriterSetFromCts eqs }) }

              -> (UnifyEnv -> TcM a)  -- Some calls to uType

              -> TcS (a, Bag Ct)

 -- Invokes the do_unifications argument, with a suitable UnifyEnv.

 --    See Note [wrapUnifier]

 -- The (Bag Ct) are the deferred constraints; we emit them but

 -- also return them

   = do { given_eq_lvl <- getInnermostGivenEqLevel

        ; what_uni     <- getWhatUnifications

          do { defer_ref    <- TcM.newTcRef emptyBag

             ; let env = UE { u_role         = role

                            , u_given_eq_lvl = given_eq_lvl

                            , u_defer        = defer_ref

                            , u_what         = what_uni }

               -- u_rewriters: the rewriter set and location from

                       RewriteEnv(..),

                       runTcPluginM )

 import GHC.Tc.Types.Constraint

 import GHC.Core.Predicate

 import GHC.Tc.Utils.TcType

 import GHC.Core.Type

        ; eq_rel <- getEqRel

        ; return (flavour, eq_rel) }

 -- | Change the 'EqRel' in a 'RewriteM'.

 setEqRel :: EqRel -> RewriteM a -> RewriteM a

 setEqRel new_eq_rel thing_inside

     else runRewriteM thing_inside (env { re_eq_rel = new_eq_rel })

 {-# INLINE setEqRel #-}

   = mkRewriteM $ \env -> do

       ; thing_inside env' }

 recordRewriter :: CtEvidence -> RewriteM ()

 -- | Rewrite a reduction, composing the resulting coercions.

 rewrite_reduction :: Reduction -> RewriteM Reduction

 rewrite_reduction (Reduction co xi)

        ; return $ co `mkTransRedn` redn }

 -- rewrite (nested) AppTys

 -- See Note [How to normalise a family application]

 rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction

 rewrite_exact_fam_app tc tys

        ; tc_rewriters <- getTcPluginRewritersForTyCon tc

        -- STEP 1. Try to reduce without reducing arguments first.