import GHC.Data.BooleanFormula

 import GHC.Core.Class             ( className, classSCSelIds )

 import GHC.Core.ConLike           ( conLikeName )

 import GHC.Core.DataCon           ( dataConNonlinearType )

 import GHC.Types.FieldLabel

 import GHC.Hs

 import GHC.Hs.Syn.Type

 import GHC.Utils.Monad            ( concatMapM, MonadIO(liftIO) )

 import GHC.Types.Id               ( isDataConId_maybe )

 import GHC.Types.Name             ( Name, nameSrcSpan, nameUnique, wiredInNameTyThing_maybe, getName )

 import GHC.Types.Name.Env         ( NameEnv, emptyNameEnv, extendNameEnv, lookupNameEnv )

 import GHC.Types.SrcLoc

 import GHC.Core.Type              ( Type, ForAllTyFlag(..) )

 import GHC.Core.TyCon             ( TyCon, tyConClass_maybe )

 import GHC.Core.InstEnv

 import GHC.Tc.Types

 import GHC.Tc.Types.Evidence

 import GHC.Types.Var              ( Id, Var, EvId, varName, varType, varUnique )

 instance ToHie (Context (Located (WithUserRdr Name))) where

   toHie (C c (L l (WithUserRdr _ n))) = toHie $ C c (L l n)

 instance ToHie (EvBindContext (LocatedA TcEvBinds)) where

   toHie (EvBindContext sc sp (L span (EvBinds bs)))

     = concatMapM go $ bagToList bs

     where

       go evbind = do

               depNames = EvBindDeps $ map varName evDeps

           concatM $

             [ toHie (C (EvidenceVarBind (EvLetBind depNames) (combineScopes sc (mkScope span)) sp)

           toHie $ C (EvidenceVarBind EvWrapperBind (mkScope osp) (getRealSpanA osp))

                 $ L osp a

         (WpEvApp a) ->

         _               -> pure []

 instance HiePass p => HasType (LocatedA (HsBind (GhcPass p))) where

 -- EarlyDerivSpec from it.

 mk_eqn_from_mechanism :: DerivSpecMechanism -> DerivM EarlyDerivSpec

 mk_eqn_from_mechanism mechanism

        user_ctxt <- askDerivUserTypeCtxt

        doDerivInstErrorChecks1 mechanism

        loc       <- lift getSrcSpanM

        case deriv_ctxt of

         InferContext wildcard ->

           do { (inferred_constraints, tvs', inst_tys', mechanism')

              ; return $ InferTheta $ DS

                    { ds_loc = loc

                    , ds_name = dfun_name, ds_tvs = tvs'

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

                  -> DerivM (ThetaSpec, [TyVar], [TcType], DerivSpecMechanism)

 -- inferConstraints figures out the constraints needed for the

 -- instance declaration generated by a 'deriving' clause on a

 -- Generate a sufficiently large set of constraints that typechecking the

 -- generated method definitions should succeed.   This set will be simplified

 -- before being used in the instance declaration

              infer_constraints =

                case mechanism of

                  DerivSpecStock{dsm_stock_dit = dit}

                                         , dit_tc_args     = tc_args

                                         , dit_rep_tc      = rep_tc

                                         , dit_rep_tc_args = rep_tc_args })

                 , denv_cls      = main_cls

                 , denv_inst_tys = inst_tys } <- ask

            tc_binders = tyConBinders rep_tc

            choose_level bndr

              | isNamedTyConBinder bndr = KindLevel

 -- derived instance context.

 inferConstraintsAnyclass :: DerivM ThetaSpec

 inferConstraintsAnyclass

                   , denv_inst_tys  = inst_tys } <- ask

        ; let gen_dms = [ (sel_id, dm_ty)

                        | (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls ]

                -- (Id,Type) are the selector Id and the generic default method type

                -- NB: the latter is /not/ quantified over the class variables

                -- See Note [Gathering and simplifying constraints for DeriveAnyClass]

 inferConstraintsCoerceBased :: [Type] -> Type

                             -> DerivM ThetaSpec

 inferConstraintsCoerceBased cls_tys rep_ty = do

            , denv_cls      = cls

            , denv_inst_tys = inst_tys } <- ask

   let -- rep_ty might come from:

       --   GeneralizedNewtypeDeriving / DerivSpecNewtype:

       --       the underlying type of the newtype ()

               -- we are going to get all the methods for the final

               -- dictionary

       deriv_origin = mkDerivOrigin sa_wildcard

       -- Next we collect constraints for the class methods

       -- If there are no methods, we don't need any constraints

 T20815a):

   class Alt f where

   newtype T f a = T (f a) deriving Alt

 import GHC.Tc.Deriv.Functor

 import GHC.Tc.Deriv.Generics

 import GHC.Tc.Errors.Types

 import GHC.Tc.Types.Origin

 import GHC.Tc.Utils.Monad

 import GHC.Tc.Utils.TcType

 import GHC.Tc.Zonk.Type

 import GHC.Core.Class

 import GHC.Utils.Unique (sameUnique)

 import Control.Monad.Trans.Reader

 import Data.Maybe

 import qualified GHC.LanguageExtensions as LangExt

 import GHC.Data.List.SetOps (assocMaybe)

 -- | Is GHC processing a standalone deriving declaration with an

 -- extra-constraints wildcard as the context?

 -- (e.g., @deriving instance _ => Eq (Foo a)@)

 -- | Return 'InstDeclCtxt' if processing with a standalone @deriving@

 -- declaration or 'DerivClauseCtxt' if processing a @deriving@ clause.

     SimplePredSpec

       { sps_pred :: TcPredType

         -- ^ The constraint to emit as a wanted

       , sps_origin :: CtOrigin

         -- ^ The origin of the constraint

       , sps_type_or_kind :: TypeOrKind

         -- ^ Whether the constraint is a type or kind

       }

   | -- | A special 'PredSpec' that is only used by @DeriveAnyClass@. This

     -- will check if @stps_ty_actual@ is a subtype of (i.e., more polymorphic

     -- than) @stps_ty_expected@ in the constraint solving machinery, emitting an

                   -- @deriving@ declaration

   -> ThetaSpec    -- ^ The specs from which constraints will be created

   -> TcM (TcLevel, WantedConstraints)

   where

     -- Create the constraints we need to solve. For stock and newtype

     -- deriving, these constraints will be simple wanted constraints

     mk_wanteds :: ThetaSpec -> TcM WantedConstraints

     mk_wanteds preds

       = do { (_, wanteds) <- captureConstraints $

            ; pure wanteds }

 {-

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

     -- report2: we suppress these if there are insolubles elsewhere in the tree

     report2 = [ ("Implicit params", is_ip,           False, mkGroupReporter mkIPErr)

               , ("Irreds",          is_irred,        False, mkGroupReporter mkIrredErr)

     -- report3: suppressed errors should be reported as categorized by either report1

     -- or report2. Keep this in sync with the suppress function above

     is_irred _ (IrredPred {}) = True

     is_irred _ _              = False

      -- See situation (1) of Note [Suppressing confusing errors]

     is_ww_fundep item _ = is_ww_fundep_item item

     is_ww_fundep_item = isWantedWantedFunDepOrigin . errorItemOrigin

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

 -}

 mkDictErr :: HasDebugCallStack => SolverReportErrCtxt -> NonEmpty ErrorItem -> TcM SolverReport

 mkDictErr ctxt orig_items

   = do { inst_envs <- tcGetInstEnvs

        ; return $

            SolverReport

              { sr_important_msg = SolverReportWithCtxt ctxt err

              , sr_hints = hints

              }

         }

        ; res_expr <- if isTagToEnum tc_fun

                      then tcTagToEnum tc_head tc_args app_res_rho

                      else return (rebuildHsApps tc_head tc_args)

        ; return (mkHsWrap res_wrap res_expr) }

 checkResultTy :: HsExpr GhcRn

             vcat [ text "relevant_con:" <+> ppr relevant_con

                  , text "res_ty:" <+> ppr res_ty

                  , text "ds_res_ty:" <+> ppr ds_res_ty

                  ]

         ; return (ds_expr, ds_res_ty, RecordUpdCtxt relevant_cons upd_fld_names ex_tvs) }

          -- See `Note [Quantification and partial signatures]` Wrinkle 2

        ; return (map (box_pred . ctPred) $

   where

      box_pred :: PredType -> PredType

      box_pred pred = case classifyPredType pred of

                ; new_wanteds <- sequence [ new_wtd_ct wtd

                                          | CtWanted wtd <- map ctEvidence wanteds

                                          ]

           | otherwise

           = return Nothing

 import GHC.Prelude

 import GHC.Tc.Solver.Irred( solveIrred )

 import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance )

 import GHC.Tc.Solver.Rewrite

 -- 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

                           , ppr flags1, ppr flags2 ]

                 ; canEqHardFailure ev s1 s2 }

       ; (subst1, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst1 $

                               binderVars bndrs1

             init_subst2 = mkEmptySubst (substInScopeSet subst1)

       -- Generate the constraints that live in the body of the implication

       -- See (SF5) in Note [Solving forall equalities]

       ; (lvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info)   $

                                     unifyForAllBody ev (eqRelRole eq_rel) $ \uenv ->

                                     go uenv skol_tvs init_subst2 bndrs1 bndrs2

  | otherwise

  = do { traceTcS "Omitting decomposition of given polytype equality" $

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

 To solve an equality between foralls

    [W] (forall a. t1) ~ (forall b. t2)

    [W] forall a. { t1 ~ (t2[a/b]) }

 The evidence we produce is a ForAllCo; see the typing rule for

    especially Refl ones.  We use the `unifyForAllBody` wrapper for `uType`,

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

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

 -}

 {- Note [Unwrap newtypes first]

   = do { inerts <- getInertSet

        ; if can_decompose inerts

          then canDecomposableTyConAppOK ev eq_rel tc1 (ty1,tys1) (ty2,tys2)

   -- See Note [Skolem abstract data] in GHC.Core.Tycon

   | tyConSkolem tc1 || tyConSkolem tc2

   = do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)

        ; finishCanWithIrred AbstractTyConReason ev }

   where

      -- See Note [Decomposing TyConApp equalities]

      -- and Note [Decomposing newtype equalities]

 -- | Call canEqSoftFailure when canonicalizing an equality fails, but if the

 -- equality is representational, there is some hope for the future.

                  -> TcS (StopOrContinue (Either IrredCt a))

   = do { (redn1, rewriters1) <- rewrite ev ty1

        ; (redn2, rewriters2) <- rewrite ev ty2

             -- We must rewrite the types before putting them in the

             -- inert set, so that we are sure to kick them out when

             -- new equalities become available

          vcat [ ppr ev, ppr redn1, ppr redn2 ]

        ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2

 -- | Call when canonicalizing an equality fails with utterly no hope.

 canEqHardFailure :: CtEvidence -> TcType -> TcType

 tryInertEqs work_item@(EqCt { eq_ev = ev, eq_eq_rel = eq_rel })

   = Stage $

     do { inerts <- getInertCans

             -> do { setEvBindIfWanted ev EvCanonical $

                     evCoercion (maybeSymCo swapped $

                                 downgradeRole (eqRelRole eq_rel)

             | otherwise

             -> continueWith () }

                                 , eq_ev = ev_w, eq_eq_rel = eq_rel })

   | (ev_i : _) <- [ ev_i | EqCt { eq_ev = ev_i, eq_rhs = rhs_i

                                 , eq_eq_rel = eq_rel }

              -- Prefer the one that has no rewriters

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

   NB: since we do not currently apply the substitution to the

   inert_solved_dicts, the knot-tying still seems a bit fragile.

   But this makes it better.

 -}

 -- See Note [WorkList priorities]

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

        , wl_rest :: [Ct]

     }

 isNominalEqualityCt :: Ct -> Bool

 appendWorkList :: WorkList -> WorkList -> WorkList

 appendWorkList

    = WL { wl_eqs_N   = eqs1_N   ++ eqs2_N

         , wl_eqs_X   = eqs1_X   ++ eqs2_X

         , wl_rw_eqs  = rw_eqs1  ++ rw_eqs2

 workListSize :: WorkList -> Int

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

 -- Extension by non equality

 extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }

 extendWorkListCt :: Ct -> WorkList -> WorkList

 -- Agnostic about what kind of constraint

 extendWorkListCt ct wl

 extendWorkListCts cts wl = foldr extendWorkListCt wl cts

 isEmptyWorkList :: WorkList -> Bool

 emptyWorkList :: WorkList

 emptyWorkList = WL { wl_eqs_N = [], wl_eqs_X = []

 -- Pretty printing

 instance Outputable WorkList where

    = text "WL" <+> (braces $

      vcat [ ppUnless (null eqs_N) $

             text "Eqs_N =" <+> vcat (map ppr eqs_N)

             text "RwEqs =" <+> vcat (map ppr rw_eqs)

           , ppUnless (null rest) $

             text "Non-eqs =" <+> vcat (map ppr rest)

           ])

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

                             , int (lengthBag simples) <+> text "simples to solve" ])

        ; traceTcS "simplify_loop: wc =" (ppr wc)

                 -- Any insoluble constraints are in 'simples' and so get rewritten

                 -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet

        ; wc2 <- if not definitely_redo_implications  -- See Note [Superclass iteration]

                    && unifs1 == 0                    -- for this conditional

        ; unif_happened <- resetUnificationFlag

        ; csTraceTcS $ text "unif_happened" <+> ppr unif_happened

 This also applies for quantified constraints; see `-fqcs-fuel` compiler flag and `QCI.qci_pend_sc` field.

 -}

 solveNestedImplications :: Bag Implication

                         -> TcS (Bag Implication)

        ; return unsolved_implics }