{-# 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 -> CanonicalEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev_w CanonicalEvidence
EvCanonical (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 -> CanonicalEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev_i CanonicalEvidence
EvCanonical (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