    {-# LANGUAGE DeriveFunctor #-}
    {-# LANGUAGE MultiWayIf #-}
    {-# LANGUAGE RecursiveDo #-}

    module GHC.Tc.Solver.Irred(
         solveIrred
      ) where

    import GHC.Prelude

    import GHC.Tc.Types.Constraint
    import GHC.Tc.Solver.InertSet
    import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance )
    import GHC.Tc.Solver.Monad
    import GHC.Tc.Types.Evidence

    import GHC.Core.Coercion

    import GHC.Types.Basic( SwapFlag(..) )

    import GHC.Utils.Outputable

    import GHC.Data.Bag

    import Data.Void( Void )

    {- *********************************************************************
    *                                                                      *
    *                      Irreducibles
    *                                                                      *
    ********************************************************************* -}

    solveIrred :: IrredCt -> SolverStage Void
    solveIrred :: IrredCt -> SolverStage Void
    solveIrred IrredCt
    irred
      = do { TcS () -> SolverStage ()
    forall a. TcS a -> SolverStage a
    simpleStage (TcS () -> SolverStage ()) -> TcS () -> SolverStage ()
    forall a b. (a -> b) -> a -> b
    $ String -> SDoc -> TcS ()
    traceTcS String
    "solveIrred:" (IrredCt -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr IrredCt
    irred)
           ; IrredCt -> SolverStage ()
    tryInertIrreds IrredCt
    irred
           ; IrredCt -> SolverStage ()
    tryQCsIrredCt IrredCt
    irred
           ; TcS () -> SolverStage ()
    forall a. TcS a -> SolverStage a
    simpleStage (IrredCt -> TcS ()
    updInertIrreds IrredCt
    irred)
           ; CtEvidence -> String -> SolverStage Void
    forall a. CtEvidence -> String -> SolverStage a
    stopWithStage (IrredCt -> CtEvidence
    irredCtEvidence IrredCt
    irred) String
    "Kept inert IrredCt" }

    updInertIrreds :: IrredCt -> TcS ()
    updInertIrreds :: IrredCt -> TcS ()
    updInertIrreds IrredCt
    irred
      = do { tc_lvl <- TcS TcLevel
    getTcLevel
           ; updInertCans $ addIrredToCans tc_lvl irred }

    {- *********************************************************************
    *                                                                      *
    *                      Inert Irreducibles
    *                                                                      *
    ********************************************************************* -}

    -- Two pieces of irreducible evidence: if their types are *exactly identical*
    -- we can rewrite them. We can never improve using this:
    -- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
    -- mean that (ty1 ~ ty2)
    tryInertIrreds :: IrredCt -> SolverStage ()
    tryInertIrreds :: IrredCt -> SolverStage ()
    tryInertIrreds IrredCt
    irred
      = TcS (StopOrContinue ()) -> SolverStage ()
    forall a. TcS (StopOrContinue a) -> SolverStage a
    Stage (TcS (StopOrContinue ()) -> SolverStage ())
    -> TcS (StopOrContinue ()) -> SolverStage ()
    forall a b. (a -> b) -> a -> b
    $ do { ics <- TcS InertCans
    getInertCans
                   ; try_inert_irreds ics irred }

    try_inert_irreds :: InertCans -> IrredCt -> TcS (StopOrContinue ())

    try_inert_irreds :: InertCans -> IrredCt -> TcS (StopOrContinue ())
    try_inert_irreds InertCans
    inerts irred_w :: IrredCt
    irred_w@(IrredCt { ir_ev :: IrredCt -> CtEvidence
    ir_ev = CtEvidence
    ev_w, ir_reason :: IrredCt -> CtIrredReason
    ir_reason = CtIrredReason
    reason })
      | let (Bag (IrredCt, SwapFlag)
    matching_irreds, InertIrreds
    others) = InertIrreds -> CtEvidence -> (Bag (IrredCt, SwapFlag), InertIrreds)
    findMatchingIrreds (InertCans -> InertIrreds
    inert_irreds InertCans
    inerts) CtEvidence
    ev_w
      , ((IrredCt
    irred_i, SwapFlag
    swap) : [(IrredCt, SwapFlag)]
    _rest) <- Bag (IrredCt, SwapFlag) -> [(IrredCt, SwapFlag)]
    forall a. Bag a -> [a]
    bagToList Bag (IrredCt, SwapFlag)
    matching_irreds
            -- See Note [Multiple matching irreds]
      , let ev_i :: CtEvidence
    ev_i = IrredCt -> CtEvidence
    irredCtEvidence IrredCt
    irred_i
            ct_i :: Ct
    ct_i = IrredCt -> Ct
    CIrredCan IrredCt
    irred_i
      , Bool -> Bool
    not (CtIrredReason -> Bool
    isInsolubleReason CtIrredReason
    reason) Bool -> Bool -> Bool
    || CtEvidence -> Bool
    isGiven CtEvidence
    ev_i Bool -> Bool -> Bool
    || CtEvidence -> Bool
    isGiven CtEvidence
    ev_w
            -- See Note [Insoluble irreds]
      = do { String -> SDoc -> TcS ()
    traceTcS String
    "iteractIrred" (SDoc -> TcS ()) -> SDoc -> TcS ()
    forall a b. (a -> b) -> a -> b
    $
             [SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat [ String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "wanted:" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> (Ct -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Ct
    ct_w SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ CtOrigin -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Ct -> CtOrigin
    ctOrigin Ct
    ct_w))
                  , String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "inert: " SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> (Ct -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Ct
    ct_i SDoc -> SDoc -> SDoc
    forall doc. IsDoc doc => doc -> doc -> doc
    $$ CtOrigin -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr (Ct -> CtOrigin
    ctOrigin Ct
    ct_i)) ]
           ; case Ct -> Ct -> InteractResult
    solveOneFromTheOther Ct
    ct_i Ct
    ct_w of
                InteractResult
    KeepInert -> do { CtEvidence -> Bool -> EvTerm -> TcS ()
    setEvBindIfWanted CtEvidence
    ev_w Bool
    True (SwapFlag -> CtEvidence -> EvTerm
    swap_me SwapFlag
    swap CtEvidence
    ev_i)
                                ; StopOrContinue () -> TcS (StopOrContinue ())
    forall a. a -> TcS a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CtEvidence -> SDoc -> StopOrContinue ()
    forall a. CtEvidence -> SDoc -> StopOrContinue a
    Stop CtEvidence
    ev_w (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "Irred equal:KeepInert" SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Ct -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Ct
    ct_w)) }
                InteractResult
    KeepWork ->  do { CtEvidence -> Bool -> EvTerm -> TcS ()
    setEvBindIfWanted CtEvidence
    ev_i Bool
    True (SwapFlag -> CtEvidence -> EvTerm
    swap_me SwapFlag
    swap CtEvidence
    ev_w)
                                ; (InertCans -> InertCans) -> TcS ()
    updInertCans ((InertIrreds -> InertIrreds) -> InertCans -> InertCans
    updIrreds (\InertIrreds
    _ -> InertIrreds
    others))
                                ; () -> TcS (StopOrContinue ())
    forall a. a -> TcS (StopOrContinue a)
    continueWith () } }

      | Bool
    otherwise
      = () -> TcS (StopOrContinue ())
    forall a. a -> TcS (StopOrContinue a)
    continueWith ()

      where
        ct_w :: Ct
    ct_w = IrredCt -> Ct
    CIrredCan IrredCt
    irred_w

        swap_me :: SwapFlag -> CtEvidence -> EvTerm
        swap_me :: SwapFlag -> CtEvidence -> EvTerm
    swap_me SwapFlag
    swap CtEvidence
    ev
          = case SwapFlag
    swap of
               SwapFlag
    NotSwapped -> CtEvidence -> EvTerm
    ctEvTerm CtEvidence
    ev
               SwapFlag
    IsSwapped  -> TcCoercion -> EvTerm
    evCoercion (TcCoercion -> TcCoercion
    mkSymCo (EvTerm -> TcCoercion
    evTermCoercion (CtEvidence -> EvTerm
    ctEvTerm CtEvidence
    ev)))

    {- Note [Multiple matching irreds]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    You might think that it's impossible to have multiple irreds all match the
    work item; after all, interactIrred looks for matches and solves one from the
    other. However, note that interacting insoluble, non-droppable irreds does not
    do this matching. We thus might end up with several insoluble, non-droppable,
    matching irreds in the inert set. When another irred comes along that we have
    not yet labeled insoluble, we can find multiple matches. These multiple matches
    cause no harm, but it would be wrong to ASSERT that they aren't there (as we
    once had done). This problem can be tickled by typecheck/should_compile/holes.

    Note [Insoluble irreds]
    ~~~~~~~~~~~~~~~~~~~~~~~
    We don't allow an /insoluble/ Wanted to be solved from another identical
    Wanted.  We want to keep all the insoluble Wanteds distinct, so that we get
    distinct error messages with -fdefer-type-errors

    However we /do/ allow an insoluble constraint (Given or Wanted) to be solved
    from an identical insoluble Given.  This might seem a little odd, but there is
    lots of discussion in #23413 and #17543.  We currently implement the PermissivePlan
    of #23413.  An alternative would be the LibertarianPlan, but that is harder to
    implemnent.

    By "identical" we include swapping.  See Note [Solving irreducible equalities]
    in GHC.Tc.Solver.InertSet.

    Test cases that are involved bkpfail24.run, T15450, GivenForallLoop, T20189, T8392a.
    -}

    {- *********************************************************************
    *                                                                      *
    *                      Quantified constraints
    *                                                                      *
    ********************************************************************* -}

    tryQCsIrredCt :: IrredCt -> SolverStage ()
    -- Try local quantified constraints for
    -- and CIrredCan e.g.  (c a)
    tryQCsIrredCt :: IrredCt -> SolverStage ()
    tryQCsIrredCt (IrredCt { ir_ev :: IrredCt -> CtEvidence
    ir_ev = CtEvidence
    ev })
      | CtEvidence -> Bool
    isGiven CtEvidence
    ev
      = TcS (StopOrContinue ()) -> SolverStage ()
    forall a. TcS (StopOrContinue a) -> SolverStage a
    Stage (TcS (StopOrContinue ()) -> SolverStage ())
    -> TcS (StopOrContinue ()) -> SolverStage ()
    forall a b. (a -> b) -> a -> b
    $ () -> TcS (StopOrContinue ())
    forall a. a -> TcS (StopOrContinue a)
    continueWith ()

      | Bool
    otherwise
      = TcS (StopOrContinue ()) -> SolverStage ()
    forall a. TcS (StopOrContinue a) -> SolverStage a
    Stage (TcS (StopOrContinue ()) -> SolverStage ())
    -> TcS (StopOrContinue ()) -> SolverStage ()
    forall a b. (a -> b) -> a -> b
    $ do { res <- TcPredType -> CtLoc -> TcS ClsInstResult
    matchLocalInst TcPredType
    pred CtLoc
    loc
                   ; case res of
                        OneInst {} -> CtEvidence -> ClsInstResult -> TcS (StopOrContinue ())
    forall a. CtEvidence -> ClsInstResult -> TcS (StopOrContinue a)
    chooseInstance CtEvidence
    ev ClsInstResult
    res
                        ClsInstResult
    _          -> () -> TcS (StopOrContinue ())
    forall a. a -> TcS (StopOrContinue a)
    continueWith () }
      where
        loc :: CtLoc
    loc  = CtEvidence -> CtLoc
    ctEvLoc CtEvidence
    ev
        pred :: TcPredType
    pred = CtEvidence -> TcPredType
    ctEvPred CtEvidence
    ev