-- NB: If there is a loop, we cut off, so we have not

                     --     added the superclasses, hence cc_pend_sc = fuel

                     | otherwise

                                      , qci_ev = ev, qci_pend_sc = fuel })

 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

         else do {

         traceTcS "Creating implication for polytype equality" (ppr ev)

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

                               binderVars bndrs1

                                     unifyForAllBody ev (eqRelRole eq_rel) $ \uenv ->

                                     go uenv skol_tvs init_subst2 bndrs1 bndrs2

  | otherwise

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

   = 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

            , inert_funeqs  = fun_eqs

            , inert_irreds  = irreds

            , inert_dicts   = idicts

            } <- getInertCans

       ; let unsolved_tv_eqs  = foldTyEqs  (add_if_unsolved CEqCan)    tv_eqs emptyCts

             unsolved_fun_eqs = foldFunEqs (add_if_unsolved CEqCan)    fun_eqs emptyCts

             unsolved_irreds  = foldr      (add_if_unsolved CIrredCan) emptyCts irreds

             unsolved_dicts   = foldDicts  (add_if_unsolved CDictCan)  idicts emptyCts

       ; implics <- getWorkListImplics

              , text "irreds =" <+> ppr unsolved_irreds

              , text "implics =" <+> ppr implics ]

                           unsolved_fun_eqs `unionBags`

   where

     add_if_unsolved :: (a -> Ct) -> a -> Cts -> Cts

     add_if_unsolved mk_ct thing cts

      solveWanteds,        -- Solves WantedConstraints

      solveSimpleGivens,   -- Solves [Ct]

      solveSimpleWanteds,  -- Solves Cts

      setImplicationStatus

   ) where

                       , eq_lhs = lhs, eq_rhs = rhs }))

   = solveEquality ev eq_rel (canEqLHSType lhs) rhs

          -- It is (much) easier to rewrite and re-classify than to

          -- rewrite the pieces and build a Reduction that will rewrite

          -- the whole constraint

            _ -> pprPanic "SolveCt" (ppr ev) }

 solveCt (CDictCan (DictCt { di_ev = ev, di_pend_sc = pend_sc }))

     -- And then re-classify

        ; case classifyPredType (ctEvPred ev) of

            ClassPred cls tys     -> solveDictNC ev cls tys

            IrredPred {}          -> solveIrred (IrredCt { ir_ev = ev, ir_reason = IrredShapeReason })

            EqPred eq_rel ty1 ty2 -> solveEquality ev eq_rel ty1 ty2

               -- EqPred only happens if (say) `c` is unified with `a ~# b`,

 --

 -- Precondition: the constraint has already been rewritten by the inert set.

 solveForAllNC :: CtEvidence -> [TcTyVar] -> TcThetaType -> TcPredType

 solveForAllNC ev tvs theta body_pred

 -- | Solve a canonical quantified constraint.

 --

 -- Precondition: the constraint has already been rewritten by the inert set.

   = case ev of

       CtGiven {} ->

         -- See Note [Solving a Given forall-constraint]

       CtWanted wtd ->

 tryInertQCs :: QCInst -> SolverStage ()

 tryInertQCs qc

 -- | Solve a (canonical) Wanted quantified constraint by emitting an implication.

 -- See Note [Solving a Wanted forall-constraint]

   = Stage $

     TcS.setSrcSpan (getCtLocEnvLoc loc_env) $

          -- This setSrcSpan is important: the emitImplicationTcS uses that

                              , unitBag (mkNonCanonical $ CtWanted wanted_ev)) }

        ; traceTcS "solveForAll" (ppr given_ev_vars $$ ppr wanteds $$ ppr w_id)

        ; solved <- trySolveImplication $

                       { ic_tclvl = lvl

                       , ic_binds = ev_binds_var

                       , ic_info  = skol_info_anon

                       , ic_skols = skol_tvs

                       , ic_given = given_ev_vars

                       , ic_wanted = emptyWC { wc_simple = wanteds } }

        ; if not solved

   where

     is_qc = IsQC (ctLocOrigin ct_loc)

     empty_subst = mkEmptySubst $ mkInScopeSet $

                       ClassPred cls tys -> pSizeClassPred cls tys

                       _                 -> pSizeType pred

 solveWantedForAll_spec :: WantedCtEvidence -> TcS (StopOrContinue Void)

 -- Solve this implication constraint completely or not at all

 solveWantedForAll_spec wtd

                  ; return $ Stop ev (text "Not fully solved:" <+> ppr wtd) } }

   where

     ev = CtWanted wtd

 {- Note [Solving a Wanted forall-constraint]

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

 module GHC.Tc.Solver.Solve where

 import GHC.Tc.Solver.Monad( TcS )

 -- See Note [Quantified constraints] in GHC.Tc.Solver.Solve

 data QCInst

   -- | A quantified constraint, of type @forall tvs. context => ty@

         , qci_pend_sc :: ExpansionFuel

              -- ^ Invariants: qci_pend_sc > 0 =>

              --

 pendingScInst_maybe :: QCInst -> Maybe QCInst

 -- Same as isPendingScDict, but for QCInsts

   , pendingFuel f = Just (qci { qci_pend_sc = doNotExpand })

   | otherwise     = Nothing