TL;DR: instantiation variables are short-lived. So it is fine for them

          to have an infinite level (=QLInstVar) because they are monomorphised

 * The constraint solver never sees an instantiation variable

   [not quite true; see below]

    because we want to /gather/ the equality constraint (to put in the implication)

    rather than /emit/ them into the monad, as `wrapUnifierAndEmit` does.

 -}

 {- Note [Unwrap newtypes first]

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

 -- See also GHC.Tc.Solver.Dict Note [Equality superclasses in quantified constraints]

 lookup_eq_in_qcis (CtGiven {}) _ _ _

 lookup_eq_in_qcis ev@(CtWanted (WantedCt { ctev_dest = dest, ctev_loc = loc })) eq_rel lhs rhs

   = do { ev_binds_var <- simpleStage getTcEvBindsVar

        ; ics          <- simpleStage getInertCans

             || isCoEvBindsVar ev_binds_var -- See Note [Instances in no-evidence implications]

          else -- Try looking for both (lhs~rhs) anr (rhs~lhs); see #23333

               do { try NotSwapped; try IsSwapped } }

   where

 {- Note [Kick out after filling a coercion hole]

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

 we should kick out `co` so that we can now unify it, which might unlock other stuff.

 See Note [Unify only if the rewriter set is empty] in GHC.Tc.Solver.Equality for

 why solving `kco` might unlock `co`, especially (URW2).

 Hence `kickOutAfterFillingCoercionHole`.  It looks at inert constraints that are

   * Wanted

 and kicks out any that will have an empty rewriter set after filling the hole.

 Wrinkles:

        because it still can't be unified.  So we only kick out if the co's

        rewriter-set becomes empty.

     IdDetails:  RepPolyId [ r :-> ConcreteFRR (FixedRuntimeRepOrigin b (..)) ]

 * When instantiating the type of an Id at a call site, at the call to

   create ConcreteTv metavariables (instead of TauTvs) based on the

   ConcreteTyVars stored in the IdDetails of the Id.

   , (theta, body_ty) <- tcSplitPhiTy phi_ty

   , not (null tvs && null theta)

   = do { (subst, inst_tvs) <- newMetaTyVarsX empty_subst tvs

            -- See Note [Representation-polymorphism checking built-ins]

            -- in GHC.Tc.Utils.Concrete.

 which we need to apply to the 'frr_type' field in order for the type variables

 in the error message to match up.

 Wrinkle [Extending the substitution]

     bad2 :: forall {s} (z :: TYPE s). z -> z

     bad2 = coerce @z

   of 'coerce', as it needs to leave 'a' un-instantiated so that the visible

   type application '@z' makes sense. In this case, we end up with a substitution

 --   Mostly for backwards compatibility.

 -- One-shot endomorphisms

 -- the one-shot trick from

 --    Note [The one-shot state monad trick] in  GHC.Utils.Monad.