CoercionN, CoercionR, CoercionP, KindCoercion,

         MCoercion(..), MCoercionR, MCoercionN, KindMCoercion,

         -- * Functions over types

         mkNakedTyConTy, mkTyVarTy, mkTyVarTys,

 {- **********************************************************************

 %*                                                                      *

 %*                                                                      *

 %********************************************************************* -}

   = CoercionHole { ch_co_var  :: CoVar

                        -- See Note [CoercionHoles and coercion free variables]

                        -- the free coercion holes of the coercion

                  }

 coHoleCoVar :: CoercionHole -> CoVar

   getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv

 -- a constraint.  See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint

   deriving newtype (Outputable, Semigroup, Monoid)

 addRewriter = coerce (addOneToUniqSet @CoercionHole)

 {- Note [Coercion holes]

    But nowadays this is all irrelevant because we don't float constraints.

 A constraint C carries a set of "rewriters", a set of Wanted CoercionHoles that have been

 used to rewrite C; see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint.

 CoercionHole, so that it can be inherited by other constraints that have C in /their/

 -}

     ctev_pred = varType dict_var,

     ctev_dest = EvVarDest dict_var,

     ctev_loc = loc,

   }

 -- Find instances where the head unifies with the provided type

                    -- see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint

                      CtGiven {} -> (False, Nothing)

                      CtWanted (WantedCt { ctev_rewriters = rws, ctev_dest = dest })

        ; let m_reason = case ct of

                 CIrredCan (IrredCt { ir_reason = reason }) -> Just reason

          -- Catch an awkward (and probably rare) case in which /all/ errors are

          -- suppressed: see Wrinkle (PER2) in Note [Prioritise Wanteds with empty

          --

          -- Unless we are sure that an error will be reported some other way

          -- (details in the defn of tidy_items) un-suppress the lot. This makes

              -> do { -- See Note [Deferred errors for coercion holes]

                      let co_var = coHoleCoVar hole

                    ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var EvNonCanonical err_tm

 addDeferredBinding _ _ _ _ _ = return ()    -- Do not set any evidence for Given

 mkSolverErrorTerm :: CtLoc -> Type  -- of the error term

           WantedCt { ctev_pred      = pred

                    , ctev_dest      = dest

                    , ctev_loc       = loc

       | otherwise

       = Nothing   -- The ErrorItem was a Given

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

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

                                            -- TcS unification counter

                ; return True

                }

             -- See Note [Defaulting representational equalities].

            ; if null new_eqs

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

                      ; return True }

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

                      ; return False } }

 try_instances :: InertSet -> DictCt -> TcS (StopOrContinue ())

 -- Try to use type-class instance declarations to simplify the constraint

   | Just solved_ev <- lookupSolvedDict inerts cls xis   -- Cached

   = do { setDictIfWanted ev EvCanonical (ctEvTerm solved_ev)

        ; stopWith ev "Dict/Top (cached)" }

                           then stopWith ev "shortCutSolver worked(2)"

                           else do { insertSafeOverlapFailureTcS what work_item

                                   ; updSolvedDicts what work_item

                _  -> -- NoInstance or NotSure: we didn't solve it

                      continueWith () }

    where

      dict_loc = ctEvLoc ev

                (OneInst { cir_new_theta   = theta

                         , cir_what        = what

                         , cir_mk_ev       = mk_ev

        ; checkReductionDepth deeper_loc pred

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

                     (ppr work_item)

 chooseInstance work_item lookup_res

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

 -- Literals

 can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _

  | l1 == l2

        ; stopWith ev "Equal LitTy" }

 -- Decompose FunTy: (s -> t) and (c => t)

                      -- CoercionHoles, from the nested solve, and we may miss the

                      -- use of CoVars.  Test T7196 showed this up

                 ; stopWith ev "Polytype equality: solved" }

         else canEqSoftFailure IrredShapeReason ev s1 s2 } }

        ; let redn1 = mkReduction co1 ty1'

                      redn1 (mkReflRedn Representational ps_ty2)

        ; can_eq_nc False rdr_env envs new_ev ReprEq ty1' ty1' ty2 ps_ty2 }

   = do { traceTcS "Decomposing cast" (vcat [ ppr ev

                                            , ppr ty1 <+> text "|>" <+> ppr co1

                                            , ppr ps_ty2 ])

                       (mkGReflLeftRedn role ty1 co1)

                       (mkReflRedn role ps_ty2)

        ; can_eq_nc rewritten rdr_env envs new_ev eq_rel ty1 ty1 ty2 ps_ty2 }

                     kind_loc = mkKindEqLoc xi1 xi2 loc

               ; kind_ev <- newGivenEv kind_loc (pred_ty, evCoercion kind_co)

               ; emitWorkNC [CtGiven kind_ev]

       CtWanted {}

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

     finish_with_swapping

       = do { let lhs1_redn = mkGReflRightMRedn role lhs1_ty sym_mco

                  lhs2_redn = mkGReflLeftMRedn  role lhs2_ty mco

            ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }

     put_tyvar_on_lhs = isWanted ev && eq_rel == NomEq

                           -- ContinueWith, to allow using this constraint for

                           -- rewriting (e.g. alpha[2] ~ beta[3]).

                           do { let role = eqRelRole eq_rel

                                  (mkReflRedn role (canEqLHSType lhs))

                                  (mkReflRedn role rhs)

                              ; continueWith $ Right $

            --           co' = <Int>

            new_ev <- if isReflCo (reductionCoercion rhs_redn)

                      then return ev

                               (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn

          ; let tv_ty     = mkTyVarTy tv

                final_rhs = reductionReducedType rhs_redn

          -- Provide Refl evidence for the constraint

          -- Ignore 'swapped' because it's Refl!

          -- Kick out any constraints that can now be rewritten

          ; kickOutAfterUnification (unitVarSet tv)

               | reason `cterHasOnlyProblems` do_not_prevent_rewriting

               -> do { let role = eqRelRole eq_rel

                         (mkReflRedn role (canEqLHSType lhs))

                         (mkReflRedn role rhs)

                     ; continueWith $ Right $

               -> tryIrredInstead reason ev eq_rel swapped lhs rhs

             PuOK _ rhs_redn

                                    (mkReflRedn (eqRelRole eq_rel) lhs_ty)

                                    rhs_redn

 -- We want to flip it to (F tys ~ a), whereupon it is canonical

 swapAndFinish ev eq_rel swapped lhs_ty can_rhs

   = do { let role = eqRelRole eq_rel

                        (mkReflRedn role (canEqLHSType can_rhs))

                        (mkReflRedn role lhs_ty)

        ; continueWith $ Right $

 tryIrredInstead reason ev eq_rel swapped lhs rhs

   = do { traceTcS "cantMakeCanonical" (ppr reason $$ ppr lhs $$ ppr rhs)

        ; let role = eqRelRole eq_rel

                        (mkReflRedn role (canEqLHSType lhs))

                        (mkReflRedn role rhs)

        ; finishCanWithIrred (NonCanonicalReason reason) new_ev }

                -> TcType        -- ty

                -> TcS (StopOrContinue a)   -- always Stop

 canEqReflexive ev eq_rel ty

        ; stopWith ev "Solved by reflexivity" }

 {- Note [Equalities with heterogeneous kinds]

 Wrinkles:

 (EIK1) When X=Wanted, the new type-level wanted for `co` is effectively rewritten by

      for the type-level one. See Note [Wanteds rewrite Wanteds] in

      GHC.Tc.Types.Constraint.  This is done in canEqCanLHSHetero.

        the kind of the parent type-equality.  See the calls to `mkKindEqLoc`

        in `canEqCanLHSHetero`.

        parent constraint; see the call to `rewriteEqEvidence` in `finish` in

        `canEqCanLHSHetero`.

 **********************************************************************

 -}

                                         -- See GHC.Tc.Types.Constraint

                                         -- Note [Wanteds rewrite Wanteds]

                   -> CtEvidence         -- Old evidence :: olhs ~ orhs (not swapped)

        ; let co = maybeSymCo swapped $

                   lhs_co `mkTransCo` mkHoleCo hole `mkTransCo` mkSymCo rhs_co

              -- new_rewriters has all the holes from lhs_co and rhs_co

        ; traceTcS "rewriteEqEvidence" (vcat [ ppr old_ev

                                             , ppr nlhs

                                             , ppr nrhs

    TL;DR: Better to hang on to `g1` (with no rewriters), in preference

    to `g2` (which has a rewriter).

 -}

 tryInertEqs :: EqCt -> SolverStage ()

   = Stage $

     do { inerts <- getInertCans

        ; if | Just (ev_i, swapped) <- inertsEqsCanDischarge inerts work_item

                     maybeSymCo swapped $

                     downgradeRole (eqRelRole eq_rel)

                                   (ctEvRewriteRole ev_i)

     loc_w  = ctEvLoc ev_w

     flav_w = ctEvFlavour ev_w

     fr_w   = (flav_w, eq_rel)

     inert_beats_wanted ev_i eq_rel

       = -- eqCanRewriteFR:        see second bullet of Note [Combining equalities]

     prefer_wanted ev_i

       =  (loc_w `strictly_more_visible` ctEvLoc ev_i)

              -- strictly_more_visible: see (CE3) in Note [Combining equalities]

              -- Prefer the one that has no rewriters

              -- See (CE4) in Note [Combining equalities]

    However the solver prioritises equalities with an empty rewriter

    set, to try to avoid unnecessary kick-out.  See GHC.Tc.Types.Constraint

 Note [Solve by unification]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

 tryQCsIrredEqCt :: IrredCt -> SolverStage ()

   | EqPred eq_rel t1 t2 <- classifyPredType (ctEvPred ev)

   | otherwise  -- All the calls come from in this module, where we deal only with

                -- equalities, so ctEvPred ev) must be an equality. Indeed, we could

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

 tryQCsEqCt :: EqCt -> SolverStage ()

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

 -- The "final QCI check" checks to see if we have

 --    [W] t1 ~# t2

 -- and a Given quantified contraint like (forall a b. blah => a ~ b)

 -- Why?  See Note [Looking up primitive equalities in quantified constraints]

 -- See also GHC.Tc.Solver.Dict

 -- Note [Equality superclasses in quantified constraints]

   where

             ; case res of

        | otherwise

 {- Note [Instances in no-evidence implications]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

        , wl_rw_eqs  :: [Ct]  -- Like wl_eqs, but ones that may have a non-empty

                              -- rewriter set

          -- We prioritise wl_eqs over wl_rw_eqs;

          -- in GHC.Tc.Types.Constraint for more details.

        , wl_rest :: [Ct]

 workListSize (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs, wl_rest = rest })

   = length eqs_N + length eqs_X + length rw_eqs + length rest

 extendWorkListEq rewriters ct

     wl@(WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs })

     --                         in GHC.Tc.Types.Constraint

   = if isNominalEqualityCt ct

     then wl { wl_eqs_N = ct : eqs_N }

 -- Precondition: new_eqs is non-empty

 extendWorkListChildEqs parent_ev new_eqs

     wl@(WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs })

     --                         in GHC.Tc.Types.Constraint

     -- If the rewriter set is empty, add to wl_eqs_X and wl_eqs_N

   = case partitionBag isNominalEqualityCt new_eqs of

     push_on_front new_eqs eqs = foldr (:) eqs new_eqs

 extendWorkListRewrittenEqs :: [EqCt] -> WorkList -> WorkList

 extendWorkListRewrittenEqs new_eqs wl@(WL { wl_rw_eqs = rw_eqs })

   = wl { wl_rw_eqs = foldr ((:) . CEqCan) rw_eqs new_eqs }

         -- If only one has an empty rewriter set, use it

         -- c.f. GHC.Tc.Solver.Equality.inertsCanDischarge, and especially

         --      (CE4) in Note [Combining equalities]

         -> res

         -- If only one is a WantedSuperclassOrigin (arising from expanding

 {-# LANGUAGE DeriveFunctor #-}

 {-# LANGUAGE MultiWayIf #-}

 {-# LANGUAGE RecursiveDo #-}

 setIrredIfWanted ev_dest swap ev_source

   | CtWanted (WantedCt { ctev_dest = dest }) <- ev_dest

   = case dest of

                                   (maybeSymCo swap (ctEvCoercion ev_source))

       EvVarDest {} -> assertPpr (swap==NotSwapped) (ppr ev_dest $$ ppr ev_source) $

 -- Try local quantified constraints for

 -- and CIrredCan e.g.  (c a)

 tryQCsIrredCt (IrredCt { ir_ev = ev })

     newBoundEvVarId,

     unifyTyVar, reportFineGrainUnifications, reportCoarseGrainUnifications,

     setEvBind, setWantedEq, setWantedDict, setEqIfWanted, setDictIfWanted,

     newEvVar, newGivenEv, emitNewGivens,

     emitChildEqs, checkReductionDepth,

        ; traceTcS "kickOutAfterUnification" (ppr tv_set $$ text "n_kicked =" <+> ppr n_kicked)

        ; return n_kicked }

 -- See Wrinkle (URW2) in Note [Unify only if the rewriter set is empty]

 -- in GHC.Tc.Solver.Equality

 --

       | CtWanted (wev@(WantedCt { ctev_rewriters = rewriters })) <- ev

       , TyVarLHS tv <- lhs

       , isMetaTyVar tv

             eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = holes' }) }

         then Left eq_ct'    -- Kick out

         else Right eq_ct'   -- Keep, but with trimmed holes

       | otherwise

 --

 -- Suppose a constraint c1 is rewritten by another, c2.  When c2

 -- gets solved, c1 has no rewriters, and can be prioritised; see

 -- GHC.Tc.Types.Constraint wrinkle (PER1)

 -- ToDo: if wl_rw_eqs is long, we'll re-zonk it each time we pick

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

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

              try_rws acc (ct:cts)

                      ; if ctHasNoRewriters ct'

                        then pick_me ct' (wl { wl_rw_eqs = cts ++ acc })

                        else try_rws (ct':acc) cts }

   = do { ev_binds_var <- getTcEvBindsVar

        ; wrapTcS (TcM.updTcRef (ebv_tcvs ev_binds_var) (co :)) }

 setEqIfWanted ev rewriters co

   = case ev of

       CtWanted (WantedCt { ctev_dest = dest })

          -> setWantedEq dest rewriters co

       _  -> return ()

 -- ^ Equalities only

 setWantedEq dest rewriters co

   = case dest of

       EvVarDest ev_id -> setEvBind (mkWantedEvBind ev_id canonical tm)

       HoleDest h      -> pprPanic "setWantedEq: HoleDest" (ppr h)

 fillCoercionHole hole rewriters co

   = do { addUsedCoercion co

        ; wrapTcS $ TcM.fillCoercionHole hole (co, rewriters)

 -- | Create a new Wanted constraint holding a coercion hole

 -- for an equality between the two types at the given 'Role'.