{-# LANGUAGE DuplicateRecordFields #-}
{-# 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.Types.Basic( SwapFlag(..) )

import GHC.Utils.Outputable
import GHC.Utils.Panic

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


{- *********************************************************************
*                                                                      *
*                      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 ()
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 -> SwapFlag -> CtEvidence -> TcS ()
setIrredIfWanted CtEvidence
ev_w 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 -> SwapFlag -> CtEvidence -> TcS ()
setIrredIfWanted CtEvidence
ev_i 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

setIrredIfWanted :: CtEvidence -> SwapFlag -> CtEvidence -> TcS ()
-- Irreds can be equalities or dictionaries
setIrredIfWanted :: CtEvidence -> SwapFlag -> CtEvidence -> TcS ()
setIrredIfWanted CtEvidence
ev_dest SwapFlag
swap CtEvidence
ev_source
  | CtWanted (WantedCt { ctev_dest :: WantedCtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest }) <- CtEvidence
ev_dest
  = case TcEvDest
dest of
      HoleDest CoercionHole
hole -> HasDebugCallStack => TcEvDest -> CoercionPlusHoles -> TcS ()
TcEvDest -> CoercionPlusHoles -> TcS ()
setWantedEq TcEvDest
dest (CoercionPlusHoles -> TcS ()) -> CoercionPlusHoles -> TcS ()
forall a b. (a -> b) -> a -> b
$
                       CPH { cph_co :: Coercion
cph_co    = SwapFlag -> Coercion -> Coercion
maybeSymCo SwapFlag
swap (HasDebugCallStack => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion CtEvidence
ev_source)
                           , cph_holes :: CoHoleSet
cph_holes = CoercionHole -> CoHoleSet
unitCoHoleSet CoercionHole
hole }

      EvVarDest {} -> Bool -> SDoc -> TcS () -> TcS ()
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (SwapFlag
swapSwapFlag -> SwapFlag -> Bool
forall a. Eq a => a -> a -> Bool
==SwapFlag
NotSwapped) (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev_dest SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev_source) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
                         -- findMatchingIrreds only returns IsSwapped for equalities
                      TcEvDest -> CanonicalEvidence -> EvTerm -> TcS ()
setWantedDict TcEvDest
dest CanonicalEvidence
EvCanonical (CtEvidence -> EvTerm
ctEvTerm CtEvidence
ev_source)
  | Bool
otherwise
  = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

{- 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 })
  = TcS (StopOrContinue ()) -> SolverStage ()
TcS (StopOrContinue ()) -> SolverStage ()
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue ()) -> SolverStage ())
-> TcS (StopOrContinue ()) -> SolverStage ()
forall a b. (a -> b) -> a -> b
$ case CtEvidence
ev of
      CtGiven {}
        -> () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith ()
      CtWanted wev :: WantedCtEvidence
wev@(WantedCt { ctev_loc :: WantedCtEvidence -> CtLoc
ctev_loc = CtLoc
loc, ctev_pred :: WantedCtEvidence -> TcPredType
ctev_pred = TcPredType
pred })
        -> do { res <- TcPredType -> CtLoc -> TcS ClsInstResult
matchLocalInst TcPredType
pred CtLoc
loc
              ; case res of
                  OneInst {} -> do { WantedCtEvidence -> ClsInstResult -> TcS ()
chooseInstance WantedCtEvidence
wev ClsInstResult
res
                                   ; CtEvidence -> String -> TcS (StopOrContinue ())
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Irred (solved wanted)" }
                  ClsInstResult
_          -> () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith () }