go (InferContext Just{})  = InstDeclCtxt True

     go (InferContext Nothing) = DerivClauseCtxt

 mkDerivOrigin :: Bool -> CtOrigin

 -- | Contains all of the information known about a derived instance when

 -- determining what its @EarlyDerivSpec@ should be.

       { sps_pred :: TcPredType

         -- ^ The constraint to emit as a wanted

         -- Usually just a simple predicate like (Eq a) or (ki ~# Type),

       , sps_origin :: CtOrigin

         -- ^ The origin of the constraint

     -- but here when we are trying to infer the context for an instance decl, we

     -- need that half-solved implication.  See deriving/should_compile/T20815

     -- and Note [Inferred contexts from method constraints]

                = case orig of

                    DerivOriginCoerce meth _ _ _ -> MethSkol (idName meth) False

                    _ -> pprPanic "emitPredSpecConstraints" (ppr orig $$ ppr wanted_pred)

        ; skol_info <- mkSkolemInfo skol_info_anon

        ; (_wrapper, tv_prs, givens, wanted_rho) <- topSkolemise skol_info wanted_pred

          -- _wrapper: we ignore the evidence from all these constraints

                = empty

     drv_fixes = case orig of

                    DerivOriginDC _ _       standalone -> [drv_fix standalone]

                    DerivOriginCoerce _ _ _ standalone -> [drv_fix standalone]

                    _                                  -> []

              ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs

              ; let inst_pred  = substTy    subst body_pred

                    inst_theta = substTheta subst theta

         ; given_ev_vars <- mapM newEvVar inst_theta

         ; (lvl, (w_id, wanteds))

                     ; return ( wantedCtEvEvId wanted_ev

                              , unitBag (mkNonCanonical $ CtWanted wanted_ev)) }

        -- Try to solve the constraint completely

        ; ev_binds_var <- TcS.newTcEvBinds

        ; solved <- trySolveImplication $

                    (implicationPrototype loc_env)

                       , ic_given = given_ev_vars

                       , ic_wanted = emptyWC { wc_simple = wanteds } }

        ; traceTcS "solveForAll }" (ppr solved)

        ; if not solved

          then do { -- Not completely solved; abandon that attempt and add the

                    -- original constraint to the inert set

                  ; stopWith (CtWanted wtd) "Wanted forall-constraint:unsolved" }

          else do { -- Completely solved; build an evidence term

                    EvFun { et_tvs = skol_tvs, et_given = given_ev_vars

                          , et_binds = evBindMapBinds evbs, et_body = w_id }

                  ; stopWith (CtWanted wtd) "Wanted forall-constraint:solved" } }

     empty_subst = mkEmptySubst $ mkInScopeSet $

                   tyCoVarsOfTypes (body_pred:theta) `delVarSetList` tvs

 {- Note [Solving a Wanted forall-constraint]

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

   isWantedSuperclassOrigin,

   ClsInstOrQC(..), NakedScFlag(..), NonLinearPatternReason(..),

   HsImplicitLiftSplice(..),

   TypedThing(..), TyVarBndrs(..),

       ClsInstOrQC   -- Whether class instance or quantified constraint

       NakedScFlag

       -- Checking constraints arising from this data con and field index. The

       -- Bool argument in DerivOriginDC and DerivOriginCoerce is True if

       -- standalong deriving (with a wildcard constraint) is being used. This

       -- the argument is True, then don't recommend "use standalone deriving",

       -- but rather "fill in the wildcard constraint yourself").

       -- See Note [Inferring the instance context] in GHC.Tc.Deriv.Infer

   | DefaultOrigin       -- Typechecking a default decl

   | DoOrigin            -- Arising from a do expression

   | DoPatOrigin (LPat GhcRn) -- Arising from a failable pattern in

   | ViewPatternReason

   | OtherPatternReason

 -- | The number of superclass selections needed to get this Given.

 -- If @d :: C ty@   has @ScDepth=2@, then the evidence @d@ will look

 -- like @sc_sel (sc_sel dg)@, where @dg@ is a Given.

 pprCtO NegateOrigin          = text "a use of syntactic negation"

 pprCtO (ScOrigin IsClsInst _) = text "the superclasses of an instance declaration"

 pprCtO (ScOrigin (IsQC {}) _) = text "the head of a quantified constraint"

 pprCtO DefaultOrigin         = text "a 'default' declaration"

 pprCtO DoOrigin              = text "a do statement"

 pprCtO MCompOrigin           = text "a statement in a monad comprehension"

   pSizeZero, pSizeOne,

   pSizeType, pSizeTypeX, pSizeTypes,

   pSizeClassPred, pSizeClassPredX,

   noMoreTyVars, allDistinctTyVars,

   TypeSize, sizeType, sizeTypes, scopedSort,

   isTerminatingClass, isStuckTypeFamily,

  | isStuckTypeFamily tc = pSizeZero

  | otherwise            = PS_TyFam tc

 pSizeClassPred :: Class -> [Type] -> PatersonSize

 pSizeClassPred = pSizeClassPredX emptyVarSet