{-# LANGUAGE RecursiveDo #-}

module GHC.Tc.Solver.Solve (
     solveSimpleGivens,   -- Solves [Ct]
     solveSimpleWanteds   -- Solves Cts
  ) where

import GHC.Prelude

import GHC.Tc.Solver.Dict
import GHC.Tc.Solver.Equality( solveEquality )
import GHC.Tc.Solver.Irred( solveIrred )
import GHC.Tc.Solver.Rewrite( rewrite )
import GHC.Tc.Errors.Types
import GHC.Tc.Utils.TcType
import GHC.Tc.Types.Evidence
import GHC.Tc.Types
import GHC.Tc.Types.Origin
import GHC.Tc.Types.Constraint
import GHC.Tc.Solver.InertSet
import GHC.Tc.Solver.Monad

import GHC.Core.Predicate
import GHC.Core.Reduction
import GHC.Core.Coercion
import GHC.Core.Class( classHasSCs )

import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Basic ( IntWithInf, intGtLimit )

import GHC.Data.Bag

import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Utils.Misc

import GHC.Driver.Session

import Data.List( deleteFirstsBy )

import Control.Monad
import Data.Semigroup as S
import Data.Void( Void )

{-
**********************************************************************
*                                                                    *
*                      Main Solver                                   *
*                                                                    *
**********************************************************************

Note [Basic Simplifier Plan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1. Pick an element from the WorkList if there exists one with depth
   less than our context-stack depth.

2. Run it down the 'stage' pipeline. Stages are:
      - canonicalization
      - inert reactions
      - spontaneous reactions
      - top-level interactions
   Each stage returns a StopOrContinue and may have sideeffected
   the inerts or worklist.

   The threading of the stages is as follows:
      - If (Stop) is returned by a stage then we start again from Step 1.
      - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to
        the next stage in the pipeline.
4. If the element has survived (i.e. ContinueWith x) the last stage
   then we add it in the inerts and jump back to Step 1.

If in Step 1 no such element exists, we have exceeded our context-stack
depth and will simply fail.
-}

solveSimpleGivens :: [Ct] -> TcS ()
solveSimpleGivens :: [Ct] -> TcS ()
solveSimpleGivens [Ct]
givens
  | [Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
givens  -- Shortcut for common case
  = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = do { String -> SDoc -> TcS ()
traceTcS String
"solveSimpleGivens {" ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
givens)
       ; [Ct] -> TcS ()
go [Ct]
givens
       ; String -> SDoc -> TcS ()
traceTcS String
"End solveSimpleGivens }" SDoc
forall doc. IsOutput doc => doc
empty }
  where
    go :: [Ct] -> TcS ()
go [Ct]
givens = do { Cts -> TcS ()
solveSimples ([Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
givens)
                   ; [Ct]
new_givens <- TcS [Ct]
runTcPluginsGiven
                   ; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Ct] -> Bool
forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull [Ct]
new_givens) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
                     [Ct] -> TcS ()
go [Ct]
new_givens }

solveSimpleWanteds :: Cts -> TcS WantedConstraints
-- The result is not necessarily zonked
solveSimpleWanteds :: Cts -> TcS WantedConstraints
solveSimpleWanteds Cts
simples
  = do { String -> SDoc -> TcS ()
traceTcS String
"solveSimpleWanteds {" (Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
simples)
       ; DynFlags
dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; (Int
n,WantedConstraints
wc) <- Int
-> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
go Int
1 (DynFlags -> IntWithInf
solverIterations DynFlags
dflags) (WantedConstraints
emptyWC { wc_simple = simples })
       ; String -> SDoc -> TcS ()
traceTcS String
"solveSimpleWanteds end }" (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
"iterations =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n
                  , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"residual =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
wc ]
       ; WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return WantedConstraints
wc }
  where
    go :: Int -> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
    -- See Note [The solveSimpleWanteds loop]
    go :: Int
-> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
go Int
n IntWithInf
limit WantedConstraints
wc
      | Int
n Int -> IntWithInf -> Bool
`intGtLimit` IntWithInf
limit
      = TcRnMessage -> TcS (Int, WantedConstraints)
forall a. TcRnMessage -> TcS a
failTcS (TcRnMessage -> TcS (Int, WantedConstraints))
-> TcRnMessage -> TcS (Int, WantedConstraints)
forall a b. (a -> b) -> a -> b
$ Cts -> IntWithInf -> WantedConstraints -> TcRnMessage
TcRnSimplifierTooManyIterations Cts
simples IntWithInf
limit WantedConstraints
wc
     | Cts -> Bool
forall a. Bag a -> Bool
isEmptyBag (WantedConstraints -> Cts
wc_simple WantedConstraints
wc)
     = (Int, WantedConstraints) -> TcS (Int, WantedConstraints)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n,WantedConstraints
wc)

     | Bool
otherwise
     = do { -- Solve
            WantedConstraints
wc1 <- WantedConstraints -> TcS WantedConstraints
solve_simple_wanteds WantedConstraints
wc

            -- Run plugins
          ; (Bool
rerun_plugin, WantedConstraints
wc2) <- WantedConstraints -> TcS (Bool, WantedConstraints)
runTcPluginsWanted WantedConstraints
wc1

          ; if Bool
rerun_plugin
            then do { String -> SDoc -> TcS ()
traceTcS String
"solveSimple going round again:" (Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
rerun_plugin)
                    ; Int
-> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) IntWithInf
limit WantedConstraints
wc2 }   -- Loop
            else (Int, WantedConstraints) -> TcS (Int, WantedConstraints)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n, WantedConstraints
wc2) }           -- Done


solve_simple_wanteds :: WantedConstraints -> TcS WantedConstraints
-- Try solving these constraints
-- Affects the unification state (of course) but not the inert set
-- The result is not necessarily zonked
solve_simple_wanteds :: WantedConstraints -> TcS WantedConstraints
solve_simple_wanteds (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples1, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics1, wc_errors :: WantedConstraints -> Bag DelayedError
wc_errors = Bag DelayedError
errs })
  = TcS WantedConstraints -> TcS WantedConstraints
forall a. TcS a -> TcS a
nestTcS (TcS WantedConstraints -> TcS WantedConstraints)
-> TcS WantedConstraints -> TcS WantedConstraints
forall a b. (a -> b) -> a -> b
$
    do { Cts -> TcS ()
solveSimples Cts
simples1
       ; (Bag Implication
implics2, Cts
unsolved) <- TcS (Bag Implication, Cts)
getUnsolvedInerts
       ; WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (WC { wc_simple :: Cts
wc_simple = Cts
unsolved
                    , wc_impl :: Bag Implication
wc_impl   = Bag Implication
implics1 Bag Implication -> Bag Implication -> Bag Implication
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Implication
implics2
                    , wc_errors :: Bag DelayedError
wc_errors = Bag DelayedError
errs }) }

{- Note [The solveSimpleWanteds loop]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Solving a bunch of simple constraints is done in a loop,
(the 'go' loop of 'solveSimpleWanteds'):
  1. Try to solve them
  2. Try the plugin
  3. If the plugin wants to run again, go back to step 1
-}

{-
************************************************************************
*                                                                      *
           Solving flat constraints: solveSimples
*                                                                      *
********************************************************************* -}

-- The main solver loop implements Note [Basic Simplifier Plan]
---------------------------------------------------------------
solveSimples :: Cts -> TcS ()
-- Returns the final InertSet in TcS
-- Has no effect on work-list or residual-implications
-- The constraints are initially examined in left-to-right order

solveSimples :: Cts -> TcS ()
solveSimples Cts
cts
  = {-# SCC "solveSimples" #-}
    do { Cts -> TcS ()
emitWork Cts
cts; TcS ()
solve_loop }
  where
    solve_loop :: TcS ()
solve_loop
      = {-# SCC "solve_loop" #-}
        do { Maybe Ct
sel <- TcS (Maybe Ct)
selectNextWorkItem
           ; case Maybe Ct
sel of
              Maybe Ct
Nothing -> () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just Ct
ct -> do { Ct -> TcS ()
solveOne Ct
ct
                            ; TcS ()
solve_loop } }

solveOne :: Ct -> TcS ()  -- Solve one constraint
solveOne :: Ct -> TcS ()
solveOne Ct
workItem
  = do { WorkList
wl      <- TcS WorkList
getWorkList
       ; InertSet
inerts  <- TcS InertSet
getInertSet
       ; TcLevel
tclevel <- TcS TcLevel
getTcLevel
       ; String -> SDoc -> TcS ()
traceTcS String
"----------------------------- " SDoc
forall doc. IsOutput doc => doc
empty
       ; String -> SDoc -> TcS ()
traceTcS String
"Start solver pipeline {" (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
"tclevel =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclevel
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"work item =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
workItem
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"inerts =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> InertSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertSet
inerts
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rest of worklist =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> WorkList -> SDoc
forall a. Outputable a => a -> SDoc
ppr WorkList
wl ]

       ; TcS ()
bumpStepCountTcS    -- One step for each constraint processed
       ; Ct -> TcS ()
solve Ct
workItem }
  where
    solve :: Ct -> TcS ()
    solve :: Ct -> TcS ()
solve Ct
ct
      = do { String -> SDoc -> TcS ()
traceTcS String
"solve {" (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"workitem = " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)
           ; StopOrContinue Void
res <- SolverStage Void -> TcS (StopOrContinue Void)
forall a. SolverStage a -> TcS (StopOrContinue a)
runSolverStage (Ct -> SolverStage Void
solveCt Ct
ct)
           ; String -> SDoc -> TcS ()
traceTcS String
"end solve }" (StopOrContinue Void -> SDoc
forall a. Outputable a => a -> SDoc
ppr StopOrContinue Void
res)
           ; case StopOrContinue Void
res of
               StartAgain Ct
ct -> do { String -> SDoc -> TcS ()
traceTcS String
"Go round again" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)
                                   ; Ct -> TcS ()
solve Ct
ct }

               Stop CtEvidence
ev SDoc
s -> do { CtEvidence -> SDoc -> TcS ()
traceFireTcS CtEvidence
ev SDoc
s
                               ; String -> SDoc -> TcS ()
traceTcS String
"End solver pipeline }" SDoc
forall doc. IsOutput doc => doc
empty
                               ; () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return () }

               -- ContinueWith can't happen: res :: SolverStage Void
               -- solveCt either solves the constraint, or puts
               -- the unsolved constraint in the inert set.
            }

{- *********************************************************************
*                                                                      *
*              Solving one constraint: solveCt
*                                                                      *
************************************************************************

Note [Canonicalization]
~~~~~~~~~~~~~~~~~~~~~~~
Canonicalization converts a simple constraint to a canonical form. It is
unary (i.e. treats individual constraints one at a time).

Constraints originating from user-written code come into being as
CNonCanonicals. We know nothing about these constraints. So, first:

     Classify CNonCanoncal constraints, depending on whether they
     are equalities, class predicates, or other.

Then proceed depending on the shape of the constraint. Generally speaking,
each constraint gets rewritten and then decomposed into one of several forms
(see type Ct in GHC.Tc.Types).

When an already-canonicalized constraint gets kicked out of the inert set,
it must be recanonicalized. But we know a bit about its shape from the
last time through, so we can skip the classification step.
-}

solveCt :: Ct -> SolverStage Void
-- The Void result tells us that solveCt cannot return
-- a ContinueWith; it must return Stop or StartAgain.
solveCt :: Ct -> SolverStage Void
solveCt (CNonCanonical CtEvidence
ev)                   = CtEvidence -> SolverStage Void
solveNC CtEvidence
ev
solveCt (CIrredCan (IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev })) = CtEvidence -> SolverStage Void
solveNC CtEvidence
ev

solveCt (CEqCan (EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ev, eq_eq_rel :: EqCt -> EqRel
eq_eq_rel = EqRel
eq_rel
                           , eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs, eq_rhs :: EqCt -> Xi
eq_rhs = Xi
rhs }))
  = CtEvidence -> EqRel -> Xi -> Xi -> SolverStage Void
solveEquality CtEvidence
ev EqRel
eq_rel (CanEqLHS -> Xi
canEqLHSType CanEqLHS
lhs) Xi
rhs

solveCt (CQuantCan (QCI { qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev, qci_pend_sc :: QCInst -> Int
qci_pend_sc = Int
pend_sc }))
  = do { CtEvidence
ev <- CtEvidence -> SolverStage CtEvidence
rewriteEvidence CtEvidence
ev
         -- It is (much) easier to rewrite and re-classify than to
         -- rewrite the pieces and build a Reduction that will rewrite
         -- the whole constraint
       ; case Xi -> Pred
classifyPredType (CtEvidence -> Xi
ctEvPred CtEvidence
ev) of
           ForAllPred [TyVar]
tvs [Xi]
th Xi
p -> TcS (StopOrContinue Void) -> SolverStage Void
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue Void) -> SolverStage Void)
-> TcS (StopOrContinue Void) -> SolverStage Void
forall a b. (a -> b) -> a -> b
$ CtEvidence
-> [TyVar] -> [Xi] -> Xi -> Int -> TcS (StopOrContinue Void)
solveForAll CtEvidence
ev [TyVar]
tvs [Xi]
th Xi
p Int
pend_sc
           Pred
_ -> String -> SDoc -> SolverStage Void
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"SolveCt" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev) }

solveCt (CDictCan (DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev, di_pend_sc :: DictCt -> Int
di_pend_sc = Int
pend_sc }))
  = do { CtEvidence
ev <- CtEvidence -> SolverStage CtEvidence
rewriteEvidence CtEvidence
ev
         -- It is easier to rewrite and re-classify than to rewrite
         -- the pieces and build a Reduction that will rewrite the
         -- whole constraint
       ; case Xi -> Pred
classifyPredType (CtEvidence -> Xi
ctEvPred CtEvidence
ev) of
           ClassPred Class
cls [Xi]
tys
             -> DictCt -> SolverStage Void
solveDict (DictCt { di_ev :: CtEvidence
di_ev = CtEvidence
ev, di_cls :: Class
di_cls = Class
cls
                                  , di_tys :: [Xi]
di_tys = [Xi]
tys, di_pend_sc :: Int
di_pend_sc = Int
pend_sc })
           Pred
_ -> String -> SDoc -> SolverStage Void
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"solveCt" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev) }

------------------
solveNC :: CtEvidence -> SolverStage Void
solveNC :: CtEvidence -> SolverStage Void
solveNC CtEvidence
ev
  = -- Instead of rewriting the evidence before classifying, it's possible we
    -- can make progress without the rewrite. Try this first.
    -- For insolubles (all of which are equalities), do /not/ rewrite the arguments
    -- In #14350 doing so led entire-unnecessary and ridiculously large
    -- type function expansion.  Instead, canEqNC just applies
    -- the substitution to the predicate, and may do decomposition;
    --    e.g. a ~ [a], where [G] a ~ [Int], can decompose
    case Xi -> Pred
classifyPredType (CtEvidence -> Xi
ctEvPred CtEvidence
ev) of {
        EqPred EqRel
eq_rel Xi
ty1 Xi
ty2 -> CtEvidence -> EqRel -> Xi -> Xi -> SolverStage Void
solveEquality CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
ty2 ;
        Pred
_ ->

    -- Do rewriting on the constraint, especially zonking
    do { CtEvidence
ev <- CtEvidence -> SolverStage CtEvidence
rewriteEvidence CtEvidence
ev
       ; let irred :: IrredCt
irred = IrredCt { ir_ev :: CtEvidence
ir_ev = CtEvidence
ev, ir_reason :: CtIrredReason
ir_reason = CtIrredReason
IrredShapeReason }

    -- And then re-classify
       ; case Xi -> Pred
classifyPredType (CtEvidence -> Xi
ctEvPred CtEvidence
ev) of
           ClassPred Class
cls [Xi]
tys     -> CtEvidence -> Class -> [Xi] -> SolverStage Void
solveDictNC CtEvidence
ev Class
cls [Xi]
tys
           ForAllPred [TyVar]
tvs [Xi]
th Xi
p   -> TcS (StopOrContinue Void) -> SolverStage Void
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue Void) -> SolverStage Void)
-> TcS (StopOrContinue Void) -> SolverStage Void
forall a b. (a -> b) -> a -> b
$ CtEvidence -> [TyVar] -> [Xi] -> Xi -> TcS (StopOrContinue Void)
solveForAllNC CtEvidence
ev [TyVar]
tvs [Xi]
th Xi
p
           IrredPred {}          -> IrredCt -> SolverStage Void
solveIrred IrredCt
irred
           EqPred EqRel
eq_rel Xi
ty1 Xi
ty2 -> CtEvidence -> EqRel -> Xi -> Xi -> SolverStage Void
solveEquality CtEvidence
ev EqRel
eq_rel Xi
ty1 Xi
ty2
              -- This case only happens if (say) `c` is unified with `a ~# b`,
              -- but that is rare becuase it requires c :: CONSTRAINT UnliftedRep

    }}


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

{- Note [Quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The -XQuantifiedConstraints extension allows type-class contexts like this:

  data Rose f x = Rose x (f (Rose f x))

  instance (Eq a, forall b. Eq b => Eq (f b))
        => Eq (Rose f a)  where
    (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 == rs2

Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
This quantified constraint is needed to solve the
 [W] (Eq (f (Rose f x)))
constraint which arises form the (==) definition.

The wiki page is
  https://gitlab.haskell.org/ghc/ghc/wikis/quantified-constraints
which in turn contains a link to the GHC Proposal where the change
is specified, and a Haskell Symposium paper about it.

We implement two main extensions to the design in the paper:

 1. We allow a variable in the instance head, e.g.
      f :: forall m a. (forall b. m b) => D (m a)
    Notice the 'm' in the head of the quantified constraint, not
    a class.

 2. We support superclasses to quantified constraints.
    For example (contrived):
      f :: (Ord b, forall b. Ord b => Ord (m b)) => m a -> m a -> Bool
      f x y = x==y
    Here we need (Eq (m a)); but the quantified constraint deals only
    with Ord.  But we can make it work by using its superclass.

Here are the moving parts
  * Language extension {-# LANGUAGE QuantifiedConstraints #-}
    and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension

  * A new form of evidence, EvDFun, that is used to discharge
    such wanted constraints

  * checkValidType gets some changes to accept forall-constraints
    only in the right places.

  * Predicate.Pred gets a new constructor ForAllPred, and
    and classifyPredType analyses a PredType to decompose
    the new forall-constraints

  * GHC.Tc.Solver.Monad.InertCans gets an extra field, inert_insts,
    which holds all the Given forall-constraints.  In effect,
    such Given constraints are like local instance decls.

  * When trying to solve a class constraint, via
    GHC.Tc.Solver.Instance.Class.matchInstEnv, use the InstEnv from inert_insts
    so that we include the local Given forall-constraints
    in the lookup.  (See GHC.Tc.Solver.Monad.getInstEnvs.)

  * `solveForAll` deals with solving a forall-constraint.  See
       Note [Solving a Wanted forall-constraint]

  * We augment the kick-out code to kick out an inert
    forall constraint if it can be rewritten by a new
    type equality; see GHC.Tc.Solver.Monad.kick_out_rewritable

Note that a quantified constraint is never /inferred/
(by GHC.Tc.Solver.simplifyInfer).  A function can only have a
quantified constraint in its type if it is given an explicit
type signature.

-}

solveForAllNC :: CtEvidence -> [TcTyVar] -> TcThetaType -> TcPredType
              -> TcS (StopOrContinue Void)
-- NC: this came from CNonCanonical, so we have not yet expanded superclasses
-- Precondition: already rewritten by inert set
solveForAllNC :: CtEvidence -> [TyVar] -> [Xi] -> Xi -> TcS (StopOrContinue Void)
solveForAllNC CtEvidence
ev [TyVar]
tvs [Xi]
theta Xi
pred
  | CtEvidence -> Bool
isGiven CtEvidence
ev  -- See Note [Eagerly expand given superclasses]
  , Just (Class
cls, [Xi]
tys) <- Maybe (Class, [Xi])
cls_pred_tys_maybe
  = do { DynFlags
dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; [Ct]
sc_cts <- Int -> CtEvidence -> [TyVar] -> [Xi] -> Class -> [Xi] -> TcS [Ct]
mkStrictSuperClasses (DynFlags -> Int
givensFuel DynFlags
dflags) CtEvidence
ev [TyVar]
tvs [Xi]
theta Class
cls [Xi]
tys
       -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
       ; Cts -> TcS ()
emitWork ([Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
sc_cts)
       ; CtEvidence
-> [TyVar] -> [Xi] -> Xi -> Int -> TcS (StopOrContinue Void)
solveForAll CtEvidence
ev [TyVar]
tvs [Xi]
theta Xi
pred Int
doNotExpand }
       -- doNotExpand: as we have already (eagerly) expanded superclasses for this class

  | Bool
otherwise
  = do { DynFlags
dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; let fuel :: Int
fuel | Just (Class
cls, [Xi]
_) <- Maybe (Class, [Xi])
cls_pred_tys_maybe
                  , Class -> Bool
classHasSCs Class
cls = DynFlags -> Int
qcsFuel DynFlags
dflags
                  -- See invariants (a) and (b) in QCI.qci_pend_sc
                  -- qcsFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
                  -- See Note [Quantified constraints]
                  | Bool
otherwise = Int
doNotExpand
       ; CtEvidence
-> [TyVar] -> [Xi] -> Xi -> Int -> TcS (StopOrContinue Void)
solveForAll CtEvidence
ev [TyVar]
tvs [Xi]
theta Xi
pred Int
fuel }
  where
    cls_pred_tys_maybe :: Maybe (Class, [Xi])
cls_pred_tys_maybe = Xi -> Maybe (Class, [Xi])
getClassPredTys_maybe Xi
pred

solveForAll :: CtEvidence -> [TcTyVar] -> TcThetaType -> PredType -> ExpansionFuel
            -> TcS (StopOrContinue Void)
-- Precondition: already rewritten by inert set
solveForAll :: CtEvidence
-> [TyVar] -> [Xi] -> Xi -> Int -> TcS (StopOrContinue Void)
solveForAll ev :: CtEvidence
ev@(CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest, ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc })
            [TyVar]
tvs [Xi]
theta Xi
pred Int
_fuel
  = -- See Note [Solving a Wanted forall-constraint]
    RealSrcSpan
-> TcS (StopOrContinue Void) -> TcS (StopOrContinue Void)
forall a. RealSrcSpan -> TcS a -> TcS a
setSrcSpan (CtLocEnv -> RealSrcSpan
getCtLocEnvLoc (CtLocEnv -> RealSrcSpan) -> CtLocEnv -> RealSrcSpan
forall a b. (a -> b) -> a -> b
$ CtLoc -> CtLocEnv
ctLocEnv CtLoc
loc) (TcS (StopOrContinue Void) -> TcS (StopOrContinue Void))
-> TcS (StopOrContinue Void) -> TcS (StopOrContinue Void)
forall a b. (a -> b) -> a -> b
$
    -- This setSrcSpan is important: the emitImplicationTcS uses that
    -- TcLclEnv for the implication, and that in turn sets the location
    -- for the Givens when solving the constraint (#21006)
    do { let empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
                           [Xi] -> VarSet
tyCoVarsOfTypes (Xi
predXi -> [Xi] -> [Xi]
forall a. a -> [a] -> [a]
:[Xi]
theta) VarSet -> [TyVar] -> VarSet
`delVarSetList` [TyVar]
tvs
             is_qc :: ClsInstOrQC
is_qc = CtOrigin -> ClsInstOrQC
IsQC (CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc)

         -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
         --           in GHC.Tc.Utils.TcType
         -- Very like the code in tcSkolDFunType
       ; rec { SkolemInfo
skol_info <- SkolemInfoAnon -> TcS SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo SkolemInfoAnon
skol_info_anon
             ; (Subst
subst, [TyVar]
skol_tvs) <- SkolemInfo -> Subst -> [TyVar] -> TcS (Subst, [TyVar])
tcInstSkolTyVarsX SkolemInfo
skol_info Subst
empty_subst [TyVar]
tvs
             ; let inst_pred :: Xi
inst_pred  = HasDebugCallStack => Subst -> Xi -> Xi
Subst -> Xi -> Xi
substTy    Subst
subst Xi
pred
                   inst_theta :: [Xi]
inst_theta = HasDebugCallStack => Subst -> [Xi] -> [Xi]
Subst -> [Xi] -> [Xi]
substTheta Subst
subst [Xi]
theta
                   skol_info_anon :: SkolemInfoAnon
skol_info_anon = ClsInstOrQC -> PatersonSize -> SkolemInfoAnon
InstSkol ClsInstOrQC
is_qc (Xi -> PatersonSize
get_size Xi
inst_pred) }

       ; [TyVar]
given_ev_vars <- (Xi -> TcS TyVar) -> [Xi] -> TcS [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Xi -> TcS TyVar
newEvVar [Xi]
inst_theta
       ; (TcLevel
lvl, (TyVar
w_id, Cts
wanteds))
             <- SDoc -> TcS (TyVar, Cts) -> TcS (TcLevel, (TyVar, Cts))
forall a. SDoc -> TcS a -> TcS (TcLevel, a)
pushLevelNoWorkList (SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfo
skol_info) (TcS (TyVar, Cts) -> TcS (TcLevel, (TyVar, Cts)))
-> TcS (TyVar, Cts) -> TcS (TcLevel, (TyVar, Cts))
forall a b. (a -> b) -> a -> b
$
                do { let loc' :: CtLoc
loc' = CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin CtLoc
loc (ClsInstOrQC -> NakedScFlag -> CtOrigin
ScOrigin ClsInstOrQC
is_qc NakedScFlag
NakedSc)
                         -- Set the thing to prove to have a ScOrigin, so we are
                         -- careful about its termination checks.
                         -- See (QC-INV) in Note [Solving a Wanted forall-constraint]
                   ; CtEvidence
wanted_ev <- CtLoc -> RewriterSet -> Xi -> TcS CtEvidence
newWantedEvVarNC CtLoc
loc' RewriterSet
rewriters Xi
inst_pred
                   ; (TyVar, Cts) -> TcS (TyVar, Cts)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ( CtEvidence -> TyVar
ctEvEvId CtEvidence
wanted_ev
                            , Ct -> Cts
forall a. a -> Bag a
unitBag (CtEvidence -> Ct
mkNonCanonical CtEvidence
wanted_ev)) }

      ; TcEvBinds
ev_binds <- TcLevel
-> SkolemInfoAnon -> [TyVar] -> [TyVar] -> Cts -> TcS TcEvBinds
emitImplicationTcS TcLevel
lvl SkolemInfoAnon
skol_info_anon [TyVar]
skol_tvs [TyVar]
given_ev_vars Cts
wanteds

      ; TcEvDest -> Bool -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest Bool
True (EvTerm -> TcS ()) -> EvTerm -> TcS ()
forall a b. (a -> b) -> a -> b
$
        EvFun { et_tvs :: [TyVar]
et_tvs = [TyVar]
skol_tvs, et_given :: [TyVar]
et_given = [TyVar]
given_ev_vars
              , et_binds :: TcEvBinds
et_binds = TcEvBinds
ev_binds, et_body :: TyVar
et_body = TyVar
w_id }

      ; CtEvidence -> String -> TcS (StopOrContinue Void)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Wanted forall-constraint" }
  where
    -- Getting the size of the head is a bit horrible
    -- because of the special treament for class predicates
    get_size :: Xi -> PatersonSize
get_size Xi
pred = case Xi -> Pred
classifyPredType Xi
pred of
                      ClassPred Class
cls [Xi]
tys -> Class -> [Xi] -> PatersonSize
pSizeClassPred Class
cls [Xi]
tys
                      Pred
_                 -> Xi -> PatersonSize
pSizeType Xi
pred

 -- See Note [Solving a Given forall-constraint]
solveForAll ev :: CtEvidence
ev@(CtGiven {}) [TyVar]
tvs [Xi]
_theta Xi
pred Int
fuel
  = do { QCInst -> TcS ()
addInertForAll QCInst
qci
       ; CtEvidence -> String -> TcS (StopOrContinue Void)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Given forall-constraint" }
  where
    qci :: QCInst
qci = QCI { qci_ev :: CtEvidence
qci_ev = CtEvidence
ev, qci_tvs :: [TyVar]
qci_tvs = [TyVar]
tvs
              , qci_pred :: Xi
qci_pred = Xi
pred, qci_pend_sc :: Int
qci_pend_sc = Int
fuel }

{- Note [Solving a Wanted forall-constraint]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Solving a wanted forall (quantified) constraint
  [W] df :: forall ab. (Eq a, Ord b) => C x a b
is delightfully easy.   Just build an implication constraint
    forall ab. (g1::Eq a, g2::Ord b) => [W] d :: C x a
and discharge df thus:
    df = /\ab. \g1 g2. let <binds> in d
where <binds> is filled in by solving the implication constraint.
All the machinery is to hand; there is little to do.

The tricky point is about termination: see #19690.  We want to maintain
the invariant (QC-INV):

  (QC-INV) Every quantified constraint returns a non-bottom dictionary

just as every top-level instance declaration guarantees to return a non-bottom
dictionary.  But as #19690 shows, it is possible to get a bottom dicionary
by superclass selection if we aren't careful.  The situation is very similar
to that described in Note [Recursive superclasses] in GHC.Tc.TyCl.Instance;
and we use the same solution:

* Give the Givens a CtOrigin of (GivenOrigin (InstSkol IsQC head_size))
* Give the Wanted a CtOrigin of (ScOrigin IsQC NakedSc)

Both of these things are done in solveForAll.  Now the mechanism described
in Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance takes over.

Note [Solving a Given forall-constraint]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For a Given constraint
  [G] df :: forall ab. (Eq a, Ord b) => C x a b
we just add it to TcS's local InstEnv of known instances,
via addInertForall.  Then, if we look up (C x Int Bool), say,
we'll find a match in the InstEnv.


************************************************************************
*                                                                      *
                  Evidence transformation
*                                                                      *
************************************************************************
-}

rewriteEvidence :: CtEvidence -> SolverStage CtEvidence
-- (rewriteEvidence old_ev new_pred co do_next)
-- Main purpose: create new evidence for new_pred;
--                 unless new_pred is cached already
-- * Calls do_next with (new_ev :: new_pred), with same wanted/given flag as old_ev
-- * If old_ev was wanted, create a binding for old_ev, in terms of new_ev
-- * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
-- * Stops if new_ev is already cached
--
--        Old evidence    New predicate is               Return new evidence
--        flavour                                        of same flavor
--        -------------------------------------------------------------------
--        Wanted          Already solved or in inert     Stop
--                        Not                            do_next new_evidence
--
--        Given           Already in inert               Stop
--                        Not                            do_next new_evidence

{- Note [Rewriting with Refl]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If the coercion is just reflexivity then you may re-use the same
evidence variable.  But be careful!  Although the coercion is Refl, new_pred
may reflect the result of unification alpha := ty, so new_pred might
not _look_ the same as old_pred, and it's vital to proceed from now on
using new_pred.

The rewriter preserves type synonyms, so they should appear in new_pred
as well as in old_pred; that is important for good error messages.

If we are rewriting with Refl, then there are no new rewriters to add to
the rewriter set. We check this with an assertion.
 -}


rewriteEvidence :: CtEvidence -> SolverStage CtEvidence
rewriteEvidence CtEvidence
ev
  = TcS (StopOrContinue CtEvidence) -> SolverStage CtEvidence
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue CtEvidence) -> SolverStage CtEvidence)
-> TcS (StopOrContinue CtEvidence) -> SolverStage CtEvidence
forall a b. (a -> b) -> a -> b
$ do { String -> SDoc -> TcS ()
traceTcS String
"rewriteEvidence" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev)
               ; (Reduction
redn, RewriterSet
rewriters) <- CtEvidence -> Xi -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev (CtEvidence -> Xi
ctEvPred CtEvidence
ev)
               ; CtEvidence
-> Reduction -> RewriterSet -> TcS (StopOrContinue CtEvidence)
finish_rewrite CtEvidence
ev Reduction
redn RewriterSet
rewriters }

finish_rewrite :: CtEvidence   -- ^ old evidence
               -> Reduction    -- ^ new predicate + coercion, of type <type of old evidence> ~ new predicate
               -> RewriterSet  -- ^ See Note [Wanteds rewrite Wanteds]
                               -- in GHC.Tc.Types.Constraint
               -> TcS (StopOrContinue CtEvidence)
finish_rewrite :: CtEvidence
-> Reduction -> RewriterSet -> TcS (StopOrContinue CtEvidence)
finish_rewrite CtEvidence
old_ev (Reduction Coercion
co Xi
new_pred) RewriterSet
rewriters
  | Coercion -> Bool
isReflCo Coercion
co -- See Note [Rewriting with Refl]
  = Bool
-> TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence)
forall a. HasCallStack => Bool -> a -> a
assert (RewriterSet -> Bool
isEmptyRewriterSet RewriterSet
rewriters) (TcS (StopOrContinue CtEvidence)
 -> TcS (StopOrContinue CtEvidence))
-> TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence)
forall a b. (a -> b) -> a -> b
$
    CtEvidence -> TcS (StopOrContinue CtEvidence)
forall a. a -> TcS (StopOrContinue a)
continueWith (HasDebugCallStack => CtEvidence -> Xi -> CtEvidence
CtEvidence -> Xi -> CtEvidence
setCtEvPredType CtEvidence
old_ev Xi
new_pred)

finish_rewrite ev :: CtEvidence
ev@(CtGiven { ctev_evar :: CtEvidence -> TyVar
ctev_evar = TyVar
old_evar, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc })
                (Reduction Coercion
co Xi
new_pred) RewriterSet
rewriters
  = Bool
-> TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence)
forall a. HasCallStack => Bool -> a -> a
assert (RewriterSet -> Bool
isEmptyRewriterSet RewriterSet
rewriters) (TcS (StopOrContinue CtEvidence)
 -> TcS (StopOrContinue CtEvidence))
-> TcS (StopOrContinue CtEvidence)
-> TcS (StopOrContinue CtEvidence)
forall a b. (a -> b) -> a -> b
$ -- this is a Given, not a wanted
    do { CtEvidence
new_ev <- CtLoc -> (Xi, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (Xi
new_pred, EvTerm
new_tm)
       ; CtEvidence -> TcS (StopOrContinue CtEvidence)
forall a. a -> TcS (StopOrContinue a)
continueWith CtEvidence
new_ev }
  where
    -- mkEvCast optimises ReflCo
    new_tm :: EvTerm
new_tm = EvExpr -> Coercion -> EvTerm
mkEvCast (TyVar -> EvExpr
evId TyVar
old_evar)
                (Role -> Role -> Coercion -> Coercion
downgradeRole Role
Representational (CtEvidence -> Role
ctEvRole CtEvidence
ev) Coercion
co)

finish_rewrite ev :: CtEvidence
ev@(CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest
                             , ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc
                             , ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters })
                (Reduction Coercion
co Xi
new_pred) RewriterSet
new_rewriters
  = do { MaybeNew
mb_new_ev <- CtLoc -> RewriterSet -> Xi -> TcS MaybeNew
newWanted CtLoc
loc RewriterSet
rewriters' Xi
new_pred
       ; Bool -> TcS ()
forall (m :: * -> *). (HasCallStack, Applicative m) => Bool -> m ()
massert (Coercion -> Role
coercionRole Coercion
co Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== CtEvidence -> Role
ctEvRole CtEvidence
ev)
       ; TcEvDest -> Bool -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest Bool
True (EvTerm -> TcS ()) -> EvTerm -> TcS ()
forall a b. (a -> b) -> a -> b
$
            EvExpr -> Coercion -> EvTerm
mkEvCast (MaybeNew -> EvExpr
getEvExpr MaybeNew
mb_new_ev)
                     (Role -> Role -> Coercion -> Coercion
downgradeRole Role
Representational (CtEvidence -> Role
ctEvRole CtEvidence
ev) (Coercion -> Coercion
mkSymCo Coercion
co))
       ; case MaybeNew
mb_new_ev of
            Fresh  CtEvidence
new_ev -> CtEvidence -> TcS (StopOrContinue CtEvidence)
forall a. a -> TcS (StopOrContinue a)
continueWith CtEvidence
new_ev
            Cached EvExpr
_      -> CtEvidence -> String -> TcS (StopOrContinue CtEvidence)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Cached wanted" }
  where
    rewriters' :: RewriterSet
rewriters' = RewriterSet
rewriters RewriterSet -> RewriterSet -> RewriterSet
forall a. Semigroup a => a -> a -> a
S.<> RewriterSet
new_rewriters

{- *******************************************************************
*                                                                    *
*                      Typechecker plugins
*                                                                    *
******************************************************************* -}

-- | Extract the (inert) givens and invoke the plugins on them.
-- Remove solved givens from the inert set and emit insolubles, but
-- return new work produced so that 'solveSimpleGivens' can feed it back
-- into the main solver.
runTcPluginsGiven :: TcS [Ct]
runTcPluginsGiven :: TcS [Ct]
runTcPluginsGiven
  = do { [TcPluginSolver]
solvers <- TcS [TcPluginSolver]
getTcPluginSolvers
       ; if [TcPluginSolver] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcPluginSolver]
solvers then [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return [] else
    do { [Ct]
givens <- TcS [Ct]
getInertGivens
       ; if [Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
givens then [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return [] else
    do { String -> SDoc -> TcS ()
traceTcS String
"runTcPluginsGiven {" ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
givens)
       ; TcPluginProgress
p <- [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPluginSolvers [TcPluginSolver]
solvers ([Ct]
givens,[])
       ; let ([Ct]
solved_givens, [(EvTerm, Ct)]
_) = TcPluginProgress -> ([Ct], [(EvTerm, Ct)])
pluginSolvedCts TcPluginProgress
p
             insols :: [IrredCt]
insols             = (Ct -> IrredCt) -> [Ct] -> [IrredCt]
forall a b. (a -> b) -> [a] -> [b]
map (CtIrredReason -> Ct -> IrredCt
ctIrredCt CtIrredReason
PluginReason) (TcPluginProgress -> [Ct]
pluginBadCts TcPluginProgress
p)
       ; (InertCans -> InertCans) -> TcS ()
updInertCans ([Ct] -> InertCans -> InertCans
removeInertCts [Ct]
solved_givens (InertCans -> InertCans)
-> (InertCans -> InertCans) -> InertCans -> InertCans
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                       (InertIrreds -> InertIrreds) -> InertCans -> InertCans
updIrreds ([IrredCt] -> InertIrreds -> InertIrreds
addIrreds [IrredCt]
insols) )
       ; String -> SDoc -> TcS ()
traceTcS String
"runTcPluginsGiven }" (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
"solved_givens:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
solved_givens
              , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"insols:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [IrredCt] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [IrredCt]
insols
              , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"new:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcPluginProgress -> [Ct]
pluginNewCts TcPluginProgress
p) ]
       ; [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginProgress -> [Ct]
pluginNewCts TcPluginProgress
p) } } }

-- | Given a bag of (rewritten, zonked) wanteds, invoke the plugins on
-- them and produce an updated bag of wanteds (possibly with some new
-- work) and a bag of insolubles.  The boolean indicates whether
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
-- main solver.
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
runTcPluginsWanted wc :: WantedConstraints
wc@(WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples1 })
  | Cts -> Bool
forall a. Bag a -> Bool
isEmptyBag Cts
simples1
  = (Bool, WantedConstraints) -> TcS (Bool, WantedConstraints)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, WantedConstraints
wc)
  | Bool
otherwise
  = do { [TcPluginSolver]
solvers <- TcS [TcPluginSolver]
getTcPluginSolvers
       ; if [TcPluginSolver] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcPluginSolver]
solvers then (Bool, WantedConstraints) -> TcS (Bool, WantedConstraints)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, WantedConstraints
wc) else

    do { [Ct]
given <- TcS [Ct]
getInertGivens
       ; Cts
wanted <- Cts -> TcS Cts
zonkSimples Cts
simples1    -- Plugin requires zonked inputs

       ; String -> SDoc -> TcS ()
traceTcS String
"Running plugins (" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Given:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
given
                                            , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Watned:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
wanted ])
       ; TcPluginProgress
p <- [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPluginSolvers [TcPluginSolver]
solvers ([Ct]
given, Cts -> [Ct]
forall a. Bag a -> [a]
bagToList Cts
wanted)
       ; let ([Ct]
_, [(EvTerm, Ct)]
solved_wanted)   = TcPluginProgress -> ([Ct], [(EvTerm, Ct)])
pluginSolvedCts TcPluginProgress
p
             ([Ct]
_, [Ct]
unsolved_wanted) = TcPluginProgress -> SplitCts
pluginInputCts TcPluginProgress
p
             new_wanted :: [Ct]
new_wanted     = TcPluginProgress -> [Ct]
pluginNewCts TcPluginProgress
p
             insols :: [Ct]
insols         = TcPluginProgress -> [Ct]
pluginBadCts TcPluginProgress
p
             all_new_wanted :: Cts
all_new_wanted = [Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
new_wanted       Cts -> Cts -> Cts
`andCts`
                              [Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
unsolved_wanted  Cts -> Cts -> Cts
`andCts`
                              [Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
insols

-- SLPJ: I'm deeply suspicious of this
--       ; updInertCans (removeInertCts $ solved_givens)

       ; ((EvTerm, Ct) -> TcS ()) -> [(EvTerm, Ct)] -> TcS ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (EvTerm, Ct) -> TcS ()
setEv [(EvTerm, Ct)]
solved_wanted

       ; String -> SDoc -> TcS ()
traceTcS String
"Finished plugins }" ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
new_wanted)
       ; (Bool, WantedConstraints) -> TcS (Bool, WantedConstraints)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ( [Ct] -> Bool
forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull (TcPluginProgress -> [Ct]
pluginNewCts TcPluginProgress
p)
                , WantedConstraints
wc { wc_simple = all_new_wanted } ) } }
  where
    setEv :: (EvTerm,Ct) -> TcS ()
    setEv :: (EvTerm, Ct) -> TcS ()
setEv (EvTerm
ev,Ct
ct) = case Ct -> CtEvidence
ctEvidence Ct
ct of
      CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest } -> TcEvDest -> Bool -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest Bool
True EvTerm
ev -- TODO: plugins should be able to signal non-canonicity
      CtEvidence
_ -> String -> TcS ()
forall a. HasCallStack => String -> a
panic String
"runTcPluginsWanted.setEv: attempt to solve non-wanted!"

-- | A pair of (given, wanted) constraints to pass to plugins
type SplitCts  = ([Ct], [Ct])

-- | A solved pair of constraints, with evidence for wanteds
type SolvedCts = ([Ct], [(EvTerm,Ct)])

-- | Represents collections of constraints generated by typechecker
-- plugins
data TcPluginProgress = TcPluginProgress
    { TcPluginProgress -> SplitCts
pluginInputCts  :: SplitCts
      -- ^ Original inputs to the plugins with solved/bad constraints
      -- removed, but otherwise unmodified
    , TcPluginProgress -> ([Ct], [(EvTerm, Ct)])
pluginSolvedCts :: SolvedCts
      -- ^ Constraints solved by plugins
    , TcPluginProgress -> [Ct]
pluginBadCts    :: [Ct]
      -- ^ Constraints reported as insoluble by plugins
    , TcPluginProgress -> [Ct]
pluginNewCts    :: [Ct]
      -- ^ New constraints emitted by plugins
    }

getTcPluginSolvers :: TcS [TcPluginSolver]
getTcPluginSolvers :: TcS [TcPluginSolver]
getTcPluginSolvers
  = do { TcGblEnv
tcg_env <- TcS TcGblEnv
getGblEnv; [TcPluginSolver] -> TcS [TcPluginSolver]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcGblEnv -> [TcPluginSolver]
tcg_tc_plugin_solvers TcGblEnv
tcg_env) }

-- | Starting from a pair of (given, wanted) constraints,
-- invoke each of the typechecker constraint-solving plugins in turn and return
--
--  * the remaining unmodified constraints,
--  * constraints that have been solved,
--  * constraints that are insoluble, and
--  * new work.
--
-- Note that new work generated by one plugin will not be seen by
-- other plugins on this pass (but the main constraint solver will be
-- re-invoked and they will see it later).  There is no check that new
-- work differs from the original constraints supplied to the plugin:
-- the plugin itself should perform this check if necessary.
runTcPluginSolvers :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPluginSolvers :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPluginSolvers [TcPluginSolver]
solvers SplitCts
all_cts
  = do { EvBindsVar
ev_binds_var <- TcS EvBindsVar
getTcEvBindsVar
       ; (TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress)
-> TcPluginProgress -> [TcPluginSolver] -> TcS TcPluginProgress
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (EvBindsVar
-> TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
do_plugin EvBindsVar
ev_binds_var) TcPluginProgress
initialProgress [TcPluginSolver]
solvers }
  where
    do_plugin :: EvBindsVar -> TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
    do_plugin :: EvBindsVar
-> TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
do_plugin EvBindsVar
ev_binds_var TcPluginProgress
p TcPluginSolver
solver = do
        TcPluginSolveResult
result <- TcPluginM TcPluginSolveResult -> TcS TcPluginSolveResult
forall a. TcPluginM a -> TcS a
runTcPluginTcS (([Ct] -> [Ct] -> TcPluginM TcPluginSolveResult)
-> SplitCts -> TcPluginM TcPluginSolveResult
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (TcPluginSolver
solver EvBindsVar
ev_binds_var) (TcPluginProgress -> SplitCts
pluginInputCts TcPluginProgress
p))
        TcPluginProgress -> TcS TcPluginProgress
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginProgress -> TcS TcPluginProgress)
-> TcPluginProgress -> TcS TcPluginProgress
forall a b. (a -> b) -> a -> b
$ TcPluginProgress -> TcPluginSolveResult -> TcPluginProgress
progress TcPluginProgress
p TcPluginSolveResult
result

    progress :: TcPluginProgress -> TcPluginSolveResult -> TcPluginProgress
    progress :: TcPluginProgress -> TcPluginSolveResult -> TcPluginProgress
progress TcPluginProgress
p
      (TcPluginSolveResult
        { tcPluginInsolubleCts :: TcPluginSolveResult -> [Ct]
tcPluginInsolubleCts = [Ct]
bad_cts
        , tcPluginSolvedCts :: TcPluginSolveResult -> [(EvTerm, Ct)]
tcPluginSolvedCts    = [(EvTerm, Ct)]
solved_cts
        , tcPluginNewCts :: TcPluginSolveResult -> [Ct]
tcPluginNewCts       = [Ct]
new_cts
        }
      ) =
        TcPluginProgress
p { pluginInputCts  = discard (bad_cts ++ map snd solved_cts) (pluginInputCts p)
          , pluginSolvedCts = add solved_cts (pluginSolvedCts p)
          , pluginNewCts    = new_cts ++ pluginNewCts p
          , pluginBadCts    = bad_cts ++ pluginBadCts p
          }

    initialProgress :: TcPluginProgress
initialProgress = SplitCts
-> ([Ct], [(EvTerm, Ct)]) -> [Ct] -> [Ct] -> TcPluginProgress
TcPluginProgress SplitCts
all_cts ([], []) [] []

    discard :: [Ct] -> SplitCts -> SplitCts
    discard :: [Ct] -> SplitCts -> SplitCts
discard [Ct]
cts ([Ct]
xs, [Ct]
ys) =
        ([Ct]
xs [Ct] -> [Ct] -> [Ct]
`without` [Ct]
cts, [Ct]
ys [Ct] -> [Ct] -> [Ct]
`without` [Ct]
cts)

    without :: [Ct] -> [Ct] -> [Ct]
    without :: [Ct] -> [Ct] -> [Ct]
without = (Ct -> Ct -> Bool) -> [Ct] -> [Ct] -> [Ct]
forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
deleteFirstsBy Ct -> Ct -> Bool
eq_ct

    eq_ct :: Ct -> Ct -> Bool
    eq_ct :: Ct -> Ct -> Bool
eq_ct Ct
c Ct
c' = Ct -> CtFlavour
ctFlavour Ct
c CtFlavour -> CtFlavour -> Bool
forall a. Eq a => a -> a -> Bool
== Ct -> CtFlavour
ctFlavour Ct
c'
              Bool -> Bool -> Bool
&& Ct -> Xi
ctPred Ct
c HasDebugCallStack => Xi -> Xi -> Bool
Xi -> Xi -> Bool
`tcEqType` Ct -> Xi
ctPred Ct
c'

    add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
    add :: [(EvTerm, Ct)] -> ([Ct], [(EvTerm, Ct)]) -> ([Ct], [(EvTerm, Ct)])
add [(EvTerm, Ct)]
xs ([Ct], [(EvTerm, Ct)])
scs = (([Ct], [(EvTerm, Ct)]) -> (EvTerm, Ct) -> ([Ct], [(EvTerm, Ct)]))
-> ([Ct], [(EvTerm, Ct)])
-> [(EvTerm, Ct)]
-> ([Ct], [(EvTerm, Ct)])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ([Ct], [(EvTerm, Ct)]) -> (EvTerm, Ct) -> ([Ct], [(EvTerm, Ct)])
addOne ([Ct], [(EvTerm, Ct)])
scs [(EvTerm, Ct)]
xs

    addOne :: SolvedCts -> (EvTerm,Ct) -> SolvedCts
    addOne :: ([Ct], [(EvTerm, Ct)]) -> (EvTerm, Ct) -> ([Ct], [(EvTerm, Ct)])
addOne ([Ct]
givens, [(EvTerm, Ct)]
wanteds) (EvTerm
ev,Ct
ct) = case Ct -> CtEvidence
ctEvidence Ct
ct of
      CtGiven  {} -> (Ct
ctCt -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
:[Ct]
givens, [(EvTerm, Ct)]
wanteds)
      CtWanted {} -> ([Ct]
givens, (EvTerm
ev,Ct
ct)(EvTerm, Ct) -> [(EvTerm, Ct)] -> [(EvTerm, Ct)]
forall a. a -> [a] -> [a]
:[(EvTerm, Ct)]
wanteds)