{-# 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 )
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 }
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
, 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
= 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)))
tryQCsIrredCt :: IrredCt -> SolverStage ()
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