{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RecursiveDo #-}

module GHC.Tc.Solver.Solve (
     simplifyWantedsTcM,
     solveWanteds,        -- Solves WantedConstraints
     solveSimpleGivens,   -- Solves [Ct]
     solveSimpleWanteds,  -- Solves Cts
     trySolveImplication,

     setImplicationStatus
  ) 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, rewriteType )
import GHC.Tc.Errors.Types
import GHC.Tc.Utils.TcType
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.CtLoc( ctLocEnv, ctLocOrigin, setCtLocOrigin )
import GHC.Tc.Types
import GHC.Tc.Types.Origin
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.CtLoc( mkGivenLoc )
import GHC.Tc.Solver.InertSet
import GHC.Tc.Solver.Monad
import GHC.Tc.Utils.Monad   as TcM
import GHC.Tc.Zonk.TcType   as TcM
import GHC.Tc.Solver.Monad  as TcS

import GHC.Core.Predicate
import GHC.Core.Reduction
import GHC.Core.Coercion
import GHC.Core.TyCo.FVs( coVarsOfCos )
import GHC.Core.Class( classHasSCs )

import GHC.Types.Id(  idType )
import GHC.Types.Var( EvVar, tyVarKind )
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Basic ( IntWithInf, intGtLimit )
import GHC.Types.Unique.Set( nonDetStrictFoldUniqSet )

import GHC.Data.Bag

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

import GHC.Driver.Session


import Control.Monad

import Data.List( deleteFirstsBy )
import Data.Maybe ( mapMaybe )
import qualified Data.Semigroup as S
import Data.Void( Void )

{- ********************************************************************************
*                                                                                 *
*                                 Main Simplifier                                 *
*                                                                                 *
******************************************************************************** -}

simplifyWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
-- Solve the specified Wanted constraints
-- Discard the evidence binds
-- Postcondition: fully zonked
simplifyWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
simplifyWantedsTcM [CtEvidence]
wanted
  = do { String -> SDoc -> TcRn ()
traceTc String
"simplifyWantedsTcM {" ([CtEvidence] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [CtEvidence]
wanted)
       ; (result, _) <- TcS WantedConstraints -> TcM (WantedConstraints, EvBindMap)
forall a. TcS a -> TcM (a, EvBindMap)
runTcS (WantedConstraints -> TcS WantedConstraints
solveWanteds ([CtEvidence] -> WantedConstraints
mkSimpleWC [CtEvidence]
wanted))
       ; result <- TcM.liftZonkM $ TcM.zonkWC result
       ; traceTc "simplifyWantedsTcM }" (ppr result)
       ; return result }

solveWanteds :: WantedConstraints -> TcS WantedConstraints
solveWanteds :: WantedConstraints -> TcS WantedConstraints
solveWanteds wc :: WantedConstraints
wc@(WC { wc_errors :: WantedConstraints -> Bag DelayedError
wc_errors = Bag DelayedError
errs })
  = do { cur_lvl <- TcS TcLevel
TcS.getTcLevel
       ; traceTcS "solveWanteds {" $
         vcat [ text "Level =" <+> ppr cur_lvl
              , ppr wc ]

       ; dflags <- getDynFlags
       ; solved_wc <- simplify_loop 0 (solverIterations dflags) True wc

       ; errs' <- simplifyDelayedErrors errs
       ; let final_wc = WantedConstraints
solved_wc { wc_errors = errs' }

       ; ev_binds_var <- getTcEvBindsVar
       ; bb <- TcS.getTcEvBindsMap ev_binds_var
       ; traceTcS "solveWanteds }" $
                 vcat [ text "final wc =" <+> ppr final_wc
                      , text "ev_binds_var =" <+> ppr ev_binds_var
                      , text "current evbinds  =" <+> ppr (evBindMapBinds bb) ]

       ; return final_wc }

simplify_loop :: Int -> IntWithInf -> Bool
              -> WantedConstraints -> TcS WantedConstraints
-- Do a round of solving, and call maybe_simplify_again to iterate
-- The 'definitely_redo_implications' flags is False if the only reason we
-- are iterating is that we have added some new Wanted superclasses
-- hoping for fundeps to help us; see Note [Superclass iteration]
--
-- Does not affect wc_holes at all; reason: wc_holes never affects anything
-- else, so we do them once, at the end in solveWanteds
simplify_loop :: Int
-> IntWithInf -> Bool -> WantedConstraints -> TcS WantedConstraints
simplify_loop Int
n IntWithInf
limit Bool
definitely_redo_implications
              wc :: WantedConstraints
wc@(WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics })
  | WantedConstraints -> Bool
isSolvedWC WantedConstraints
wc  -- Fast path
  = WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return WantedConstraints
wc
  | Bool
otherwise
  = do { SDoc -> TcS ()
csTraceTcS (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
         String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"simplify_loop iteration=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Int -> SDoc
forall doc. IsLine doc => Int -> doc
int Int
n
         SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> (SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
hsep [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"definitely_redo =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
definitely_redo_implications SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
comma
                            , Int -> SDoc
forall doc. IsLine doc => Int -> doc
int (Cts -> Int
forall a. Bag a -> Int
lengthBag Cts
simples) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"simples to solve" ])
       ; String -> SDoc -> TcS ()
traceTcS String
"simplify_loop: wc =" (WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
wc)

       ; (unifs1, simples1) <- TcS Cts -> TcS (Int, Cts)
forall a. TcS a -> TcS (Int, a)
reportUnifications (TcS Cts -> TcS (Int, Cts)) -> TcS Cts -> TcS (Int, Cts)
forall a b. (a -> b) -> a -> b
$  -- See Note [Superclass iteration]
                               Cts -> TcS Cts
solveSimpleWanteds Cts
simples
                -- Any insoluble constraints are in 'simples' and so get rewritten
                -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet

       ; wc2 <- if not definitely_redo_implications  -- See Note [Superclass iteration]
                   && unifs1 == 0                    -- for this conditional
                then return (wc { wc_simple = simples1 })  -- Short cut
                else do { implics1 <- solveNestedImplications implics
                        ; return (wc { wc_simple = simples1
                                     , wc_impl   = implics1 }) }

       ; unif_happened <- resetUnificationFlag
       ; csTraceTcS $ text "unif_happened" <+> ppr unif_happened
         -- Note [The Unification Level Flag] in GHC.Tc.Solver.Monad
       ; maybe_simplify_again (n+1) limit unif_happened wc2 }

maybe_simplify_again :: Int -> IntWithInf -> Bool
                     -> WantedConstraints -> TcS WantedConstraints
maybe_simplify_again :: Int
-> IntWithInf -> Bool -> WantedConstraints -> TcS WantedConstraints
maybe_simplify_again Int
n IntWithInf
limit Bool
unif_happened wc :: WantedConstraints
wc@(WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples })
  | Int
n Int -> IntWithInf -> Bool
`intGtLimit` IntWithInf
limit
  = do { -- Add an error (not a warning) if we blow the limit,
         -- Typically if we blow the limit we are going to report some other error
         -- (an unsolved constraint), and we don't want that error to suppress
         -- the iteration limit warning!
         TcRnMessage -> TcS ()
addErrTcS (TcRnMessage -> TcS ()) -> TcRnMessage -> TcS ()
forall a b. (a -> b) -> a -> b
$ Cts -> IntWithInf -> WantedConstraints -> TcRnMessage
TcRnSimplifierTooManyIterations Cts
simples IntWithInf
limit WantedConstraints
wc
       ; WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return WantedConstraints
wc }

  | Bool
unif_happened
  = Int
-> IntWithInf -> Bool -> WantedConstraints -> TcS WantedConstraints
simplify_loop Int
n IntWithInf
limit Bool
True WantedConstraints
wc

  | WantedConstraints -> Bool
superClassesMightHelp WantedConstraints
wc    -- Returns False quickly if wc is solved
  = -- We still have unsolved goals, and apparently no way to solve them,
    -- so try expanding superclasses at this level, both Given and Wanted
    do { pending_given <- TcS [Ct]
getPendingGivenScs
       ; let (pending_wanted, simples1) = getPendingWantedScs simples
       ; if null pending_given && null pending_wanted
           then return wc  -- After all, superclasses did not help
           else
    do { new_given  <- makeSuperClasses pending_given
       ; new_wanted <- makeSuperClasses pending_wanted
       ; solveSimpleGivens new_given -- Add the new Givens to the inert set
       ; traceTcS "maybe_simplify_again" (vcat [ text "pending_given" <+> ppr pending_given
                                               , text "new_given" <+> ppr new_given
                                               , text "pending_wanted" <+> ppr pending_wanted
                                               , text "new_wanted" <+> ppr new_wanted ])
       ; simplify_loop n limit (not (null pending_given)) $
         wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } }
         -- (not (null pending_given)): see Note [Superclass iteration]

  | Bool
otherwise
  = WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return WantedConstraints
wc

{- Note [Superclass iteration]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this implication constraint
    forall a.
       [W] d: C Int beta
       forall b. blah
where
  class D a b | a -> b
  class D a b => C a b
We will expand d's superclasses, giving [W] D Int beta, in the hope of geting
fundeps to unify beta.  Doing so is usually fruitless (no useful fundeps),
and if so it seems a pity to waste time iterating the implications (forall b. blah)
(If we add new Given superclasses it's a different matter: it's really worth looking
at the implications.)

Hence the definitely_redo_implications flag to simplify_loop.  It's usually
True, but False in the case where the only reason to iterate is new Wanted
superclasses.  In that case we check whether the new Wanteds actually led to
any new unifications, and iterate the implications only if so.
-}

{- Note [Expanding Recursive Superclasses and ExpansionFuel]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the class declaration (T21909)

    class C [a] => C a where
       foo :: a -> Int

and suppose during type inference we obtain an implication constraint:

    forall a. C a => C [[a]]

To solve this implication constraint, we first expand one layer of the superclass
of Given constraints, but not for Wanted constraints.
(See Note [Eagerly expand given superclasses] and Note [Why adding superclasses can help]
in GHC.Tc.Solver.Dict.) We thus get:

    [G] g1 :: C a
    [G] g2 :: C [a]    -- new superclass layer from g1
    [W] w1 :: C [[a]]

Now, we cannot solve `w1` directly from `g1` or `g2` as we may not have
any instances for C. So we expand a layer of superclasses of each Wanteds and Givens
that we haven't expanded yet.
This is done in `maybe_simplify_again`. And we get:

    [G] g1 :: C a
    [G] g2 :: C [a]
    [G] g3 :: C [[a]]    -- new superclass layer from g2, can solve w1
    [W] w1 :: C [[a]]
    [W] w2 :: C [[[a]]]  -- new superclass layer from w1, not solvable

Now, although we can solve `w1` using `g3` (obtained from expanding `g2`),
we have a new wanted constraint `w2` (obtained from expanding `w1`) that cannot be solved.
We thus make another go at solving in `maybe_simplify_again` by expanding more
layers of superclasses. This looping is futile as Givens will never be able to catch up with Wanteds.

Side Note: In principle we don't actually need to /solve/ `w2`, as it is a superclass of `w1`
but we only expand it to expose any functional dependencies (see Note [The superclass story])
But `w2` is a wanted constraint, so we will try to solve it like any other,
even though ultimately we will discard its evidence.

Solution: Simply bound the maximum number of layers of expansion for
Givens and Wanteds, with ExpansionFuel.  Give the Givens more fuel
(say 3 layers) than the Wanteds (say 1 layer). Now the Givens will
win.  The Wanteds don't need much fuel: we are only expanding at all
to expose functional dependencies, and wantedFuel=1 means we will
expand a full recursive layer.  If the superclass hierarchy is
non-recursive (the normal case) one layer is therefore full expansion.

The default value for wantedFuel = Constants.max_WANTEDS_FUEL = 1.
The default value for givenFuel  = Constants.max_GIVENS_FUEL = 3.
Both are configurable via the `-fgivens-fuel` and `-fwanteds-fuel`
compiler flags.

There are two preconditions for the default fuel values:
   (1) default givenFuel >= default wantedsFuel
   (2) default givenFuel < solverIterations

Precondition (1) ensures that we expand givens at least as many times as we expand wanted constraints
preferably givenFuel > wantedsFuel to avoid issues like T21909 while
the precondition (2) ensures that we do not reach the solver iteration limit and fail with a
more meaningful error message (see T19627)

This also applies for quantified constraints; see `-fqcs-fuel` compiler flag and `QCI.qci_pend_sc` field.
-}

{- ********************************************************************************
*                                                                                 *
*                    Solving implication constraints                              *
*                                                                                 *
******************************************************************************** -}

solveNestedImplications :: Bag Implication
                        -> TcS (Bag Implication)
-- Precondition: the TcS inerts may contain unsolved simples which have
-- to be converted to givens before we go inside a nested implication.
solveNestedImplications :: Bag Implication -> TcS (Bag Implication)
solveNestedImplications Bag Implication
implics
  | Bag Implication -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Implication
implics
  = Bag Implication -> TcS (Bag Implication)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bag Implication
forall a. Bag a
emptyBag)
  | Bool
otherwise
  = do { String -> SDoc -> TcS ()
traceTcS String
"solveNestedImplications starting {" SDoc
forall doc. IsOutput doc => doc
empty
       ; unsolved_implics <- (Implication -> TcS Implication)
-> Bag Implication -> TcS (Bag Implication)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Implication -> TcS Implication
solveImplication Bag Implication
implics

       -- ... and we are back in the original TcS inerts
       -- Notice that the original includes the _insoluble_simples so it was safe to ignore
       -- them in the beginning of this function.
       ; traceTcS "solveNestedImplications end }" $
                  vcat [ text "unsolved_implics =" <+> ppr unsolved_implics ]

       ; return unsolved_implics }

{- Note [trySolveImplication]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
`trySolveImplication` may be invoked while solving simple wanteds, notably from
`solveWantedForAll`.  It returns a Bool to say if solving succeeded or failed.

It uses `nestImplicTcS` to build a nested scope.  One subtle point is that
`nestImplicTcS` uses the `inert_givens` (not the `inert_cans`) of the current
inert set to initialse the `InertSet` of the nested scope.  It is super-important not
to pollute the sub-solving problem with the unsolved Wanteds of the current scope.

Whenever we do `solveSimpleGivens`, we snapshot the `inert_cans` into `inert_givens`.
(At that moment there should be no Wanteds.)
-}

trySolveImplication :: Implication -> TcS Bool
-- See Note [trySolveImplication]
trySolveImplication :: Implication -> TcS Bool
trySolveImplication (Implic { ic_tclvl :: Implication -> TcLevel
ic_tclvl  = TcLevel
tclvl
                            , ic_binds :: Implication -> EvBindsVar
ic_binds  = EvBindsVar
ev_binds_var
                            , ic_given :: Implication -> [TcTyVar]
ic_given  = [TcTyVar]
given_ids
                            , ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
wanteds
                            , ic_env :: Implication -> CtLocEnv
ic_env    = CtLocEnv
ct_loc_env
                            , ic_info :: Implication -> SkolemInfoAnon
ic_info   = SkolemInfoAnon
info })
  = EvBindsVar -> TcLevel -> TcS Bool -> TcS Bool
forall a. EvBindsVar -> TcLevel -> TcS a -> TcS a
nestImplicTcS EvBindsVar
ev_binds_var TcLevel
tclvl (TcS Bool -> TcS Bool) -> TcS Bool -> TcS Bool
forall a b. (a -> b) -> a -> b
$
    do { let loc :: CtLoc
loc    = TcLevel -> SkolemInfoAnon -> CtLocEnv -> CtLoc
mkGivenLoc TcLevel
tclvl SkolemInfoAnon
info CtLocEnv
ct_loc_env
             givens :: [Ct]
givens = CtLoc -> [TcTyVar] -> [Ct]
mkGivens CtLoc
loc [TcTyVar]
given_ids
       ; [Ct] -> TcS ()
solveSimpleGivens [Ct]
givens
       ; residual_wanted <- WantedConstraints -> TcS WantedConstraints
solveWanteds WantedConstraints
wanteds
       ; return (isSolvedWC residual_wanted) }

solveImplication :: Implication     -- Wanted
                 -> TcS Implication -- Simplified implication
-- Precondition: The TcS monad contains an empty worklist and given-only inerts
-- which after trying to solve this implication we must restore to their original value
solveImplication :: Implication -> TcS Implication
solveImplication imp :: Implication
imp@(Implic { ic_tclvl :: Implication -> TcLevel
ic_tclvl  = TcLevel
tclvl
                             , ic_binds :: Implication -> EvBindsVar
ic_binds  = EvBindsVar
ev_binds_var
                             , ic_given :: Implication -> [TcTyVar]
ic_given  = [TcTyVar]
given_ids
                             , ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
wanteds
                             , ic_info :: Implication -> SkolemInfoAnon
ic_info   = SkolemInfoAnon
info
                             , ic_env :: Implication -> CtLocEnv
ic_env    = CtLocEnv
ct_loc_env
                             , ic_status :: Implication -> ImplicStatus
ic_status = ImplicStatus
status })
  | ImplicStatus -> Bool
isSolvedStatus ImplicStatus
status
  = Implication -> TcS Implication
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Implication
imp  -- Do nothing

  | Bool
otherwise  -- Even for IC_Insoluble it is worth doing more work
               -- The insoluble stuff might be in one sub-implication
               -- and other unsolved goals in another; and we want to
               -- solve the latter as much as possible
  = do { inerts <- TcS InertSet
getInertSet
       ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)

       -- commented out; see `where` clause below
       -- ; when debugIsOn check_tc_level

         -- Solve the nested constraints
       ; (has_given_eqs, given_insols, residual_wanted)
            <- nestImplicTcS ev_binds_var tclvl $
               do { let loc    = TcLevel -> SkolemInfoAnon -> CtLocEnv -> CtLoc
mkGivenLoc TcLevel
tclvl SkolemInfoAnon
info CtLocEnv
ct_loc_env
                        givens = CtLoc -> [TcTyVar] -> [Ct]
mkGivens CtLoc
loc [TcTyVar]
given_ids
                  ; solveSimpleGivens givens

                  ; residual_wanted <- solveWanteds wanteds

                  ; (has_eqs, given_insols) <- getHasGivenEqs tclvl
                        -- Call getHasGivenEqs /after/ solveWanteds, because
                        -- solveWanteds can augment the givens, via expandSuperClasses,
                        -- to reveal given superclass equalities

                  ; return (has_eqs, given_insols, residual_wanted) }

       ; traceTcS "solveImplication 2"
           (ppr given_insols $$ ppr residual_wanted)
       ; let final_wanted = WantedConstraints
residual_wanted WantedConstraints -> InertIrreds -> WantedConstraints
`addInsols` InertIrreds
given_insols
             -- Don't lose track of the insoluble givens,
             -- which signal unreachable code; put them in ic_wanted

       ; res_implic <- setImplicationStatus (imp { ic_given_eqs = has_given_eqs
                                                 , ic_wanted = final_wanted })

       ; evbinds <- TcS.getTcEvBindsMap ev_binds_var
       ; tcvs    <- TcS.getTcEvTyCoVars ev_binds_var
       ; traceTcS "solveImplication end }" $ vcat
             [ text "has_given_eqs =" <+> ppr has_given_eqs
             , text "res_implic =" <+> ppr res_implic
             , text "implication evbinds =" <+> ppr (evBindMapBinds evbinds)
             , text "implication tvcs =" <+> ppr tcvs ]

       ; return res_implic }

    -- TcLevels must be strictly increasing (see (ImplicInv) in
    -- Note [TcLevel invariants] in GHC.Tc.Utils.TcType),
    -- and in fact I think they should always increase one level at a time.

    -- Though sensible, this check causes lots of testsuite failures. It is
    -- remaining commented out for now.
    {-
    check_tc_level = do { cur_lvl <- TcS.getTcLevel
                        ; massertPpr (tclvl == pushTcLevel cur_lvl)
                                     (text "Cur lvl =" <+> ppr cur_lvl $$ text "Imp lvl =" <+> ppr tclvl) }
    -}

----------------------
setImplicationStatus :: Implication -> TcS Implication
-- Finalise the implication returned from solveImplication,
--   * Set the ic_status field
--   * Prune unnecessary evidence bindings
--   * Prune unnecessary child implications
-- Precondition: the ic_status field is not already IC_Solved
setImplicationStatus :: Implication -> TcS Implication
setImplicationStatus implic :: Implication
implic@(Implic { ic_status :: Implication -> ImplicStatus
ic_status = ImplicStatus
old_status
                                    , ic_info :: Implication -> SkolemInfoAnon
ic_info   = SkolemInfoAnon
info
                                    , ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
wc })
 = Bool -> SDoc -> TcS Implication -> TcS Implication
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Bool -> Bool
not (ImplicStatus -> Bool
isSolvedStatus ImplicStatus
old_status)) (SkolemInfoAnon -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfoAnon
info) (TcS Implication -> TcS Implication)
-> TcS Implication -> TcS Implication
forall a b. (a -> b) -> a -> b
$
   -- Precondition: we only set the status if it is not already solved
   do { String -> SDoc -> TcS ()
traceTcS String
"setImplicationStatus {" (Implication -> SDoc
forall a. Outputable a => a -> SDoc
ppr Implication
implic)

      ; let solved :: Bool
solved = WantedConstraints -> Bool
isSolvedWC WantedConstraints
wc
      ; new_implic    <- Implication -> TcS Implication
neededEvVars Implication
implic
      ; bad_telescope <- if solved then checkBadTelescope implic
                                   else return False

      ; let new_status | WantedConstraints -> Bool
insolubleWC WantedConstraints
wc = ImplicStatus
IC_Insoluble
                       | Bool -> Bool
not Bool
solved     = ImplicStatus
IC_Unsolved
                       | Bool
bad_telescope  = ImplicStatus
IC_BadTelescope
                       | Bool
otherwise      = IC_Solved { ics_dead :: [TcTyVar]
ics_dead = [TcTyVar]
dead_givens }
            dead_givens = Implication -> [TcTyVar]
findRedundantGivens Implication
new_implic
            new_wc      = WantedConstraints -> WantedConstraints
pruneImplications WantedConstraints
wc

            final_implic = Implication
new_implic { ic_status = new_status
                                      , ic_wanted = new_wc }

      ; traceTcS "setImplicationStatus }" (ppr final_implic)
      ; return final_implic }

pruneImplications :: WantedConstraints -> WantedConstraints
-- We have now recorded the `ic_need` variables of the child
-- implications (in `ic_need_implics` of the parent) so we can
-- delete any unnecessary children.
pruneImplications :: WantedConstraints -> WantedConstraints
pruneImplications wc :: WantedConstraints
wc@(WC { wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics })
  = WantedConstraints
wc { wc_impl = filterBag keep_me implics }
         -- Do not prune holes; these should be reported
  where
    keep_me :: Implication -> Bool
    keep_me :: Implication -> Bool
keep_me (Implic { ic_status :: Implication -> ImplicStatus
ic_status = ImplicStatus
status, ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
wanted })
      | IC_Solved { ics_dead :: ImplicStatus -> [TcTyVar]
ics_dead = [TcTyVar]
dead_givens } <- ImplicStatus
status -- Fully solved
      , [TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
dead_givens                               -- No redundant givens to report
      , Bag Implication -> Bool
forall a. Bag a -> Bool
isEmptyBag (WantedConstraints -> Bag Implication
wc_impl WantedConstraints
wanted)                    -- No children that might have things to report
      = Bool
False
      | Bool
otherwise
      = Bool
True        -- Otherwise, keep it

findRedundantGivens :: Implication -> [EvVar]
findRedundantGivens :: Implication -> [TcTyVar]
findRedundantGivens (Implic { ic_info :: Implication -> SkolemInfoAnon
ic_info = SkolemInfoAnon
info, ic_need :: Implication -> EvNeedSet
ic_need = EvNeedSet
need, ic_given :: Implication -> [TcTyVar]
ic_given = [TcTyVar]
givens })
  | Bool -> Bool
not (SkolemInfoAnon -> Bool
warnRedundantGivens SkolemInfoAnon
info)   -- Don't report redundant constraints at all
  = []                    -- See (TRC4) of Note [Tracking redundant constraints]

  | Bool -> Bool
not ([TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
unused_givens)         -- Some givens are literally unused
  = [TcTyVar]
unused_givens

  -- Only try this if unused_givens is empty: see (TRC2a)
  | Bool
otherwise                       -- All givens are used, but some might
  = [TcTyVar]
redundant_givens                -- still be redundant e.g. (Eq a, Ord a)

  where
    in_instance_decl :: Bool
in_instance_decl = case SkolemInfoAnon
info of { InstSkol {} -> Bool
True; SkolemInfoAnon
_ -> Bool
False }
                       -- See Note [Redundant constraints in instance decls]

    unused_givens :: [TcTyVar]
unused_givens = (TcTyVar -> Bool) -> [TcTyVar] -> [TcTyVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut TcTyVar -> Bool
is_used [TcTyVar]
givens

    needed_givens_ignoring_default_methods :: CoVarSet
needed_givens_ignoring_default_methods = EvNeedSet -> CoVarSet
ens_fvs EvNeedSet
need
    is_used :: TcTyVar -> Bool
is_used TcTyVar
given =  TcTyVar -> Bool
is_type_error TcTyVar
given
                  Bool -> Bool -> Bool
|| TcTyVar
given TcTyVar -> CoVarSet -> Bool
`elemVarSet` CoVarSet
needed_givens_ignoring_default_methods
                  Bool -> Bool -> Bool
|| (Bool
in_instance_decl Bool -> Bool -> Bool
&& TcType -> Bool
is_improving (TcTyVar -> TcType
idType TcTyVar
given))

    minimal_givens :: [TcTyVar]
minimal_givens = (TcTyVar -> TcType) -> [TcTyVar] -> [TcTyVar]
forall a. (a -> TcType) -> [a] -> [a]
mkMinimalBySCs TcTyVar -> TcType
evVarPred [TcTyVar]
givens  -- See (TRC2)

    is_minimal :: TcTyVar -> Bool
is_minimal = (TcTyVar -> CoVarSet -> Bool
`elemVarSet` [TcTyVar] -> CoVarSet
mkVarSet [TcTyVar]
minimal_givens)
    redundant_givens :: [TcTyVar]
redundant_givens
      | Bool
in_instance_decl = []
      | Bool
otherwise        = (TcTyVar -> Bool) -> [TcTyVar] -> [TcTyVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut TcTyVar -> Bool
is_minimal [TcTyVar]
givens

    -- See #15232
    is_type_error :: TcTyVar -> Bool
is_type_error TcTyVar
id = TcType -> Bool
isTopLevelUserTypeError (TcTyVar -> TcType
idType TcTyVar
id)

    is_improving :: TcType -> Bool
is_improving TcType
pred -- (transSuperClasses p) does not include p
      = (TcType -> Bool) -> [TcType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TcType -> Bool
isImprovementPred (TcType
pred TcType -> [TcType] -> [TcType]
forall a. a -> [a] -> [a]
: TcType -> [TcType]
transSuperClasses TcType
pred)

warnRedundantGivens :: SkolemInfoAnon -> Bool
warnRedundantGivens :: SkolemInfoAnon -> Bool
warnRedundantGivens (SigSkol UserTypeCtxt
ctxt TcType
_ [(Name, TcTyVar)]
_)
  = case UserTypeCtxt
ctxt of
       FunSigCtxt Name
_ ReportRedundantConstraints
rrc -> ReportRedundantConstraints -> Bool
reportRedundantConstraints ReportRedundantConstraints
rrc
       ExprSigCtxt ReportRedundantConstraints
rrc  -> ReportRedundantConstraints -> Bool
reportRedundantConstraints ReportRedundantConstraints
rrc
       UserTypeCtxt
_                -> Bool
False

warnRedundantGivens (InstSkol ClsInstOrQC
from PatersonSize
_)
 -- Do not report redundant constraints for quantified constraints
 -- See (TRC4) in Note [Tracking redundant constraints]
 -- Fortunately it is easy to spot implications constraints that arise
 -- from quantified constraints, from their SkolInfo
 = case ClsInstOrQC
from of
      IsQC {}      -> Bool
False
      IsClsInst {} -> Bool
True

  -- To think about: do we want to report redundant givens for
  -- pattern synonyms, PatSynSigSkol? c.f #9953, comment:21.
warnRedundantGivens SkolemInfoAnon
_ = Bool
False

{- Note [Redundant constraints in instance decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Instance declarations are special in two ways:

* We don't report unused givens if they can give rise to improvement.
  Example (#10100):
    class Add a b ab | a b -> ab, a ab -> b
    instance Add Zero b b
    instance Add a b ab => Add (Succ a) b (Succ ab)
  The context (Add a b ab) for the instance is clearly unused in terms
  of evidence, since the dictionary has no fields.  But it is still
  needed!  With the context, a wanted constraint
     Add (Succ Zero) beta (Succ Zero)
  we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
  But without the context we won't find beta := Zero.

  This only matters in instance declarations.

* We don't report givens that are a superclass of another given. E.g.
       class Ord r => UserOfRegs r a where ...
       instance (Ord r, UserOfRegs r CmmReg) => UserOfRegs r CmmExpr where
  The (Ord r) is not redundant, even though it is a superclass of
  (UserOfRegs r CmmReg).  See Note [Recursive superclasses] in GHC.Tc.TyCl.Instance.

  Again this is specific to instance declarations.
-}


checkBadTelescope :: Implication -> TcS Bool
-- True <=> the skolems form a bad telescope
-- See Note [Checking telescopes] in GHC.Tc.Types.Constraint
checkBadTelescope :: Implication -> TcS Bool
checkBadTelescope (Implic { ic_info :: Implication -> SkolemInfoAnon
ic_info  = SkolemInfoAnon
info
                          , ic_skols :: Implication -> [TcTyVar]
ic_skols = [TcTyVar]
skols })
  | SkolemInfoAnon -> Bool
checkTelescopeSkol SkolemInfoAnon
info
  = do{ skols <- (TcTyVar -> TcS TcTyVar) -> [TcTyVar] -> TcS [TcTyVar]
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 TcTyVar -> TcS TcTyVar
TcS.zonkTyCoVarKind [TcTyVar]
skols
      ; return (go emptyVarSet (reverse skols))}

  | Bool
otherwise
  = Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

  where
    go :: TyVarSet   -- skolems that appear *later* than the current ones
       -> [TcTyVar]  -- ordered skolems, in reverse order
       -> Bool       -- True <=> there is an out-of-order skolem
    go :: CoVarSet -> [TcTyVar] -> Bool
go CoVarSet
_ [] = Bool
False
    go CoVarSet
later_skols (TcTyVar
one_skol : [TcTyVar]
earlier_skols)
      | TcType -> CoVarSet
tyCoVarsOfType (TcTyVar -> TcType
tyVarKind TcTyVar
one_skol) CoVarSet -> CoVarSet -> Bool
`intersectsVarSet` CoVarSet
later_skols
      = Bool
True
      | Bool
otherwise
      = CoVarSet -> [TcTyVar] -> Bool
go (CoVarSet
later_skols CoVarSet -> TcTyVar -> CoVarSet
`extendVarSet` TcTyVar
one_skol) [TcTyVar]
earlier_skols

neededEvVars :: Implication -> TcS Implication
-- Find all the evidence variables that are "needed",
-- /and/ delete dead evidence bindings
--
--   See Note [Tracking redundant constraints]
--   See Note [Delete dead Given evidence bindings]
--
--   - Start from initial_seeds (from nested implications)
--
--   - Add free vars of RHS of all Wanted evidence bindings
--     and coercion variables accumulated in tcvs (all Wanted)
--
--   - Generate 'needed', the needed set of EvVars, by doing transitive
--     closure through Given bindings
--     e.g.   Needed {a,b}
--            Given  a = sc_sel a2
--            Then a2 is needed too
--
--   - Prune out all Given bindings that are not needed

neededEvVars :: Implication -> TcS Implication
neededEvVars implic :: Implication
implic@(Implic { ic_info :: Implication -> SkolemInfoAnon
ic_info        = SkolemInfoAnon
info
                            , ic_binds :: Implication -> EvBindsVar
ic_binds       = EvBindsVar
ev_binds_var
                            , ic_wanted :: Implication -> WantedConstraints
ic_wanted      = WC { wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics }
                            , ic_need_implic :: Implication -> EvNeedSet
ic_need_implic = EvNeedSet
old_need_implic    -- See (TRC1)
                    })
 = do { ev_binds <- EvBindsVar -> TcS EvBindMap
TcS.getTcEvBindsMap EvBindsVar
ev_binds_var
      ; used_cos <- TcS.getTcEvTyCoVars ev_binds_var

      ; let -- Find the variables needed by `implics`
            new_need_implic@(ENS { ens_dms = dm_seeds, ens_fvs = other_seeds })
                = foldr add_implic old_need_implic implics
                  -- Start from old_need_implic!  See (TRC1)

            -- Get the variables needed by the solved bindings
            -- (It's OK to use a non-deterministic fold here
            --  because add_wanted is commutative.)
            used_covars = [TcCoercion] -> CoVarSet
coVarsOfCos [TcCoercion]
used_cos
            seeds_w = (EvBind -> CoVarSet -> CoVarSet)
-> CoVarSet -> EvBindMap -> CoVarSet
forall a. (EvBind -> a -> a) -> a -> EvBindMap -> a
nonDetStrictFoldEvBindMap EvBind -> CoVarSet -> CoVarSet
add_wanted CoVarSet
used_covars EvBindMap
ev_binds

            need_ignoring_dms = EvBindMap -> CoVarSet -> CoVarSet
findNeededGivenEvVars EvBindMap
ev_binds (CoVarSet
other_seeds CoVarSet -> CoVarSet -> CoVarSet
`unionVarSet` CoVarSet
seeds_w)
            need_from_dms     = EvBindMap -> CoVarSet -> CoVarSet
findNeededGivenEvVars EvBindMap
ev_binds CoVarSet
dm_seeds
            need_full         = CoVarSet
need_ignoring_dms CoVarSet -> CoVarSet -> CoVarSet
`unionVarSet` CoVarSet
need_from_dms

            -- `need`: the Givens from outer scopes that are used in this implication
            -- is_dm_skol: see (TRC5)
            need | SkolemInfoAnon -> Bool
is_dm_skol SkolemInfoAnon
info = ENS { ens_dms :: CoVarSet
ens_dms = EvBindMap -> CoVarSet -> CoVarSet
trim EvBindMap
ev_binds CoVarSet
need_full
                                         , ens_fvs :: CoVarSet
ens_fvs = CoVarSet
emptyVarSet }
                 | Bool
otherwise       = ENS { ens_dms :: CoVarSet
ens_dms = EvBindMap -> CoVarSet -> CoVarSet
trim EvBindMap
ev_binds CoVarSet
need_from_dms
                                         , ens_fvs :: CoVarSet
ens_fvs = EvBindMap -> CoVarSet -> CoVarSet
trim EvBindMap
ev_binds CoVarSet
need_ignoring_dms }

      -- Delete dead Given evidence bindings
      -- See Note [Delete dead Given evidence bindings]
      ; let live_ev_binds = (EvBind -> Bool) -> EvBindMap -> EvBindMap
filterEvBindMap (CoVarSet -> EvBind -> Bool
needed_ev_bind CoVarSet
need_full) EvBindMap
ev_binds
      ; TcS.setTcEvBindsMap ev_binds_var live_ev_binds

      ; traceTcS "neededEvVars" $
        vcat [ text "old_need_implic:" <+> ppr old_need_implic
             , text "new_need_implic:" <+> ppr new_need_implic
             , text "used_covars:" <+> ppr used_covars
             , text "need_ignoring_dms:" <+> ppr need_ignoring_dms
             , text "need_from_dms:"     <+> ppr need_from_dms
             , text "need:" <+> ppr need
             , text "ev_binds:" <+> ppr ev_binds
             , text "live_ev_binds:" <+> ppr live_ev_binds ]
      ; return (implic { ic_need        = need
                       , ic_need_implic = new_need_implic }) }
 where
    trim :: EvBindMap -> VarSet -> VarSet
    -- Delete variables bound by Givens or bindings
    trim :: EvBindMap -> CoVarSet -> CoVarSet
trim EvBindMap
ev_binds CoVarSet
needs = CoVarSet
needs CoVarSet -> EvBindMap -> CoVarSet
`varSetMinusEvBindMap` EvBindMap
ev_binds

    add_implic :: Implication -> EvNeedSet -> EvNeedSet
    add_implic :: Implication -> EvNeedSet -> EvNeedSet
add_implic (Implic { ic_given :: Implication -> [TcTyVar]
ic_given = [TcTyVar]
givens, ic_need :: Implication -> EvNeedSet
ic_need = EvNeedSet
need }) EvNeedSet
acc
       = (EvNeedSet
need EvNeedSet -> [TcTyVar] -> EvNeedSet
`delGivensFromEvNeedSet` [TcTyVar]
givens) EvNeedSet -> EvNeedSet -> EvNeedSet
`unionEvNeedSet` EvNeedSet
acc

    needed_ev_bind :: CoVarSet -> EvBind -> Bool
needed_ev_bind CoVarSet
needed (EvBind { eb_lhs :: EvBind -> TcTyVar
eb_lhs = TcTyVar
ev_var, eb_info :: EvBind -> EvBindInfo
eb_info = EvBindInfo
info })
      | EvBindGiven{} <- EvBindInfo
info = TcTyVar
ev_var TcTyVar -> CoVarSet -> Bool
`elemVarSet` CoVarSet
needed
      | Bool
otherwise             = Bool
True   -- Keep all wanted bindings

    add_wanted :: EvBind -> VarSet -> VarSet
    add_wanted :: EvBind -> CoVarSet -> CoVarSet
add_wanted (EvBind { eb_info :: EvBind -> EvBindInfo
eb_info = EvBindInfo
info, eb_rhs :: EvBind -> EvTerm
eb_rhs = EvTerm
rhs }) CoVarSet
needs
      | EvBindGiven{} <- EvBindInfo
info = CoVarSet
needs  -- Add the rhs vars of the Wanted bindings only
      | Bool
otherwise = EvTerm -> CoVarSet
nestedEvIdsOfTerm EvTerm
rhs CoVarSet -> CoVarSet -> CoVarSet
`unionVarSet` CoVarSet
needs

    is_dm_skol :: SkolemInfoAnon -> Bool
    is_dm_skol :: SkolemInfoAnon -> Bool
is_dm_skol (MethSkol Name
_ Bool
is_dm) = Bool
is_dm
    is_dm_skol SkolemInfoAnon
_                  = Bool
False

findNeededGivenEvVars :: EvBindMap -> VarSet -> VarSet
-- Find all the Given evidence needed by seeds,
-- looking transitively through bindings for Givens (only)
findNeededGivenEvVars :: EvBindMap -> CoVarSet -> CoVarSet
findNeededGivenEvVars EvBindMap
ev_binds CoVarSet
seeds
  = (CoVarSet -> CoVarSet) -> CoVarSet -> CoVarSet
transCloVarSet CoVarSet -> CoVarSet
also_needs CoVarSet
seeds
  where
   also_needs :: VarSet -> VarSet
   also_needs :: CoVarSet -> CoVarSet
also_needs CoVarSet
needs = (TcTyVar -> CoVarSet -> CoVarSet)
-> CoVarSet -> CoVarSet -> CoVarSet
forall elt a. (elt -> a -> a) -> a -> UniqSet elt -> a
nonDetStrictFoldUniqSet TcTyVar -> CoVarSet -> CoVarSet
add CoVarSet
emptyVarSet CoVarSet
needs
     -- It's OK to use a non-deterministic fold here because we immediately
     -- forget about the ordering by creating a set

   add :: Var -> VarSet -> VarSet
   add :: TcTyVar -> CoVarSet -> CoVarSet
add TcTyVar
v CoVarSet
needs
     | Just EvBind
ev_bind <- EvBindMap -> TcTyVar -> Maybe EvBind
lookupEvBind EvBindMap
ev_binds TcTyVar
v
     , EvBind { eb_info :: EvBind -> EvBindInfo
eb_info = EvBindInfo
EvBindGiven, eb_rhs :: EvBind -> EvTerm
eb_rhs = EvTerm
rhs } <- EvBind
ev_bind
       -- Look at Given bindings only
     = EvTerm -> CoVarSet
nestedEvIdsOfTerm EvTerm
rhs CoVarSet -> CoVarSet -> CoVarSet
`unionVarSet` CoVarSet
needs
     | Bool
otherwise
     = CoVarSet
needs

-------------------------------------------------
simplifyDelayedErrors :: Bag DelayedError -> TcS (Bag DelayedError)
-- Simplify any delayed errors: e.g. type and term holes
-- NB: At this point we have finished with all the simple
--     constraints; they are in wc_simple, not in the inert set.
--     So those Wanteds will not rewrite these delayed errors.
--     That's probably no bad thing.
--
--     However if we have [W] alpha ~ Maybe a, [W] alpha ~ Int
--     and _ : alpha, then we'll /unify/ alpha with the first of
--     the Wanteds we get, and thereby report (_ : Maybe a) or
--     (_ : Int) unpredictably, depending on which we happen to see
--     first.  Doesn't matter much; there is a type error anyhow.
--     T17139 is a case in point.
simplifyDelayedErrors :: Bag DelayedError -> TcS (Bag DelayedError)
simplifyDelayedErrors = (DelayedError -> TcS (Maybe DelayedError))
-> Bag DelayedError -> TcS (Bag DelayedError)
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> Bag a -> m (Bag b)
mapMaybeBagM DelayedError -> TcS (Maybe DelayedError)
simpl_err
  where
    simpl_err :: DelayedError -> TcS (Maybe DelayedError)
    simpl_err :: DelayedError -> TcS (Maybe DelayedError)
simpl_err (DE_Hole Hole
hole) = DelayedError -> Maybe DelayedError
forall a. a -> Maybe a
Just (DelayedError -> Maybe DelayedError)
-> (Hole -> DelayedError) -> Hole -> Maybe DelayedError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hole -> DelayedError
DE_Hole (Hole -> Maybe DelayedError)
-> TcS Hole -> TcS (Maybe DelayedError)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Hole -> TcS Hole
simpl_hole Hole
hole
    simpl_err err :: DelayedError
err@(DE_NotConcrete {}) = Maybe DelayedError -> TcS (Maybe DelayedError)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DelayedError -> TcS (Maybe DelayedError))
-> Maybe DelayedError -> TcS (Maybe DelayedError)
forall a b. (a -> b) -> a -> b
$ DelayedError -> Maybe DelayedError
forall a. a -> Maybe a
Just DelayedError
err
    simpl_err (DE_Multiplicity TcCoercion
mult_co CtLoc
loc)
      = do { mult_co' <- TcCoercion -> TcS TcCoercion
TcS.zonkCo TcCoercion
mult_co
           ; if isReflexiveCo mult_co' then
               return Nothing
             else
               return $ Just (DE_Multiplicity mult_co' loc) }

    simpl_hole :: Hole -> TcS Hole

     -- See Note [Do not simplify ConstraintHoles]
    simpl_hole :: Hole -> TcS Hole
simpl_hole h :: Hole
h@(Hole { hole_sort :: Hole -> HoleSort
hole_sort = HoleSort
ConstraintHole }) = Hole -> TcS Hole
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Hole
h

     -- other wildcards should be simplified for printing
     -- we must do so here, and not in the error-message generation
     -- code, because we have all the givens already set up
    simpl_hole h :: Hole
h@(Hole { hole_ty :: Hole -> TcType
hole_ty = TcType
ty, hole_loc :: Hole -> CtLoc
hole_loc = CtLoc
loc })
      = do { ty' <- CtLoc -> TcType -> TcS TcType
rewriteType CtLoc
loc TcType
ty
           ; traceTcS "simpl_hole" (ppr ty $$ ppr ty')
           ; return (h { hole_ty = ty' }) }

{- Note [Delete dead Given evidence bindings]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As a result of superclass expansion, we speculatively
generate evidence bindings for Givens. E.g.
   f :: (a ~ b) => a -> b -> Bool
   f x y = ...
We'll have
   [G] d1 :: (a~b)
and we'll speculatively generate the evidence binding
   [G] d2 :: (a ~# b) = sc_sel d

Now d2 is available for solving.  But it may not be needed!  Usually
such dead superclass selections will eventually be dropped as dead
code, but:

 * It won't always be dropped (#13032).  In the case of an
   unlifted-equality superclass like d2 above, we generate
       case heq_sc d1 of d2 -> ...
   and we can't (in general) drop that case expression in case
   d1 is bottom.  So it's technically unsound to have added it
   in the first place.

 * Simply generating all those extra superclasses can generate lots of
   code that has to be zonked, only to be discarded later.  Better not
   to generate it in the first place.

   Moreover, if we simplify this implication more than once
   (e.g. because we can't solve it completely on the first iteration
   of simpl_loop), we'll generate all the same bindings AGAIN!

Easy solution: take advantage of the work we are doing to track dead
(unused) Givens, and use it to prune the Given bindings too.  This is
all done by neededEvVars.

This led to a remarkable 25% overall compiler allocation decrease in
test T12227.

But we don't get to discard all redundant equality superclasses, alas;
see #15205.

Note [Do not simplify ConstraintHoles]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before printing the inferred value for a type hole (a _ wildcard in
a partial type signature), we simplify it w.r.t. any Givens. This
makes for an easier-to-understand diagnostic for the user.

However, we do not wish to do this for extra-constraint holes. Here is
the example for why (partial-sigs/should_compile/T12844):

  bar :: _ => FooData rngs
  bar = foo

  data FooData rngs

  class Foo xs where foo :: (Head xs ~ '(r,r')) => FooData xs

  type family Head (xs :: [k]) where Head (x ': xs) = x

GHC correctly infers that the extra-constraints wildcard on `bar`
should be (Head rngs ~ '(r, r'), Foo rngs). It then adds this
constraint as a Given on the implication constraint for `bar`. (This
implication is emitted by emitResidualConstraints.) The Hole for the _
is stored within the implication's WantedConstraints.  When
simplifyHoles is called, that constraint is already assumed as a
Given. Simplifying with respect to it turns it into ('(r, r') ~ '(r,
r'), Foo rngs), which is disastrous.

Furthermore, there is no need to simplify here: extra-constraints wildcards
are filled in with the output of the solver, in chooseInferredQuantifiers
(choose_psig_context), so they are already simplified. (Contrast to normal
type holes, which are just bound to a meta-variable.) Avoiding the poor output
is simple: just don't simplify extra-constraints wildcards.

This is the only reason we need to track ConstraintHole separately
from TypeHole in HoleSort.

See also Note [Extra-constraint holes in partial type signatures]
in GHC.Tc.Gen.HsType.

Note [Tracking redundant constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
With Opt_WarnRedundantConstraints, GHC can report which constraints of a type
signature (or instance declaration) are redundant, and can be omitted.  Here is
an overview of how it works.

This is all tested in typecheck/should_compile/T20602 (among others).

How tracking works:

* We maintain the `ic_need` field in an implication:
     ic_need: the set of Given evidence variables that are needed somewhere
              inside this implication; and are bound either by this implication
              or by an enclosing one.

* `setImplicationStatus` does all the work:
  - When the constraint solver finishes solving all the wanteds in
    an implication, it sets its status to IC_Solved

  - `neededEvVars`: computes which evidence variables are needed by an
    implication in `setImplicationStatus`.  A variable is needed if

      a) It is in the ic_need field of this implication, computed in
         a previous call to `setImplicationStatus`; see (TRC1)

      b) It is in the ics_need of a nested implication; see `add_implic`
         in `neededEvVars`

      c) It is free in the RHS of any /Wanted/ EvBind; each such binding
         solves a Wanted, so we want them all.  See `add_wanted` in
         `neededEvVars`

      d) It is free in the RHS of a /Given/ EvBind whose LHS is needed:
         see `findNeededGivenEvVars` called from `neededEvVars`.

  - Next, if the final status is IC_Solved, `setImplicationStatus` uses
    `findRedundantGivens` to decide which of this implication's Givens
    are redundant.

  - It also uses `pruneImplications` to discard any now-unnecessary child
    implications.

* GHC.Tc.Errors does the actual warning, in `warnRedundantConstraints`.


Wrinkles:

(TRC1) `pruneImplications` drops any sub-implications of an Implication
  that are irrelevant for error reporting:
      - no unsolved wanteds
      - no sub-implications
      - no redundant givens to report
  But in doing so we must not lose track of the variables that those implications
  needed!  So we track the ic_needs of all child implications in `ic_need_implics`.
  Crucially, this set includes things need by child implications that have been
  discarded by `pruneImplications`.

(TRC2) A Given can be redundant because it is implied by other Givens
         f :: (Eq a, Ord a)     => blah   -- Eq a unnecessary
         g :: (Eq a, a~b, Eq b) => blah   -- Either Eq a or Eq b unnecessary
   We nail this by using `mkMinimalBySCs` in `findRedundantGivens`.
   (TRC2a) But NOTE that we only attempt this mkMinimalBySCs stuff if all Givens
   used by evidence bindings.  Example:
      f :: (Eq a, Ord a) => a -> Bool
      f x = x == x
   We report (Ord a) as unused because it is. But we must not also report (Eq a)
   as unused because it is a superclass of Ord!

(TRC3) When two Givens are the same, prefer one that does not involve superclass
  selection, or more generally has shallower superclass-selection depth:
  see 2(b,c) in Note [Replacement vs keeping] in GHC.Tc.Solver.InertSet.
    e.g        f :: (Eq a, Ord a) => a -> Bool
               f x = x == x
  Eager superclass expansion gives us two [G] Eq a constraints. We want to keep
  the one from the user-written Eq a, not the superclass selection. This means
  we report the Ord a as redundant with -Wredundant-constraints, not the Eq a.
  Getting this wrong was #20602.

(TRC4) We don't compute redundant givens for *every* implication; only
  for those which reply True to `warnRedundantGivens`:

   - For example, in a class declaration, the default method *can*
     use the class constraint, but it certainly doesn't *have* to,
     and we don't want to report an error there.  Ditto instance decls.

   - More subtly, in a function definition
       f :: (Ord a, Ord a, Ix a) => a -> a
       f x = rhs
     we do an ambiguity check on the type (which would find that one
     of the Ord a constraints was redundant), and then we check that
     the definition has that type (which might find that both are
     redundant).  We don't want to report the same error twice, so we
     disable it for the ambiguity check.  Hence using two different
     FunSigCtxts, one with the warn-redundant field set True, and the
     other set False in
        - GHC.Tc.Gen.Bind.tcSpecPrag
        - GHC.Tc.Gen.Bind.tcTySig

   - We do not want to report redundant constraints for implications
     that come from quantified constraints.  Example #23323:
        data T a
        instance Show (T a) where ...  -- No context!
        foo :: forall f c. (forall a. c a => Show (f a)) => Proxy c -> f Int -> Int
        bar = foo @T @Eq

     The call to `foo` gives us
       [W] d : (forall a. Eq a => Show (T a))
     To solve this, GHC.Tc.Solver.Solve.solveForAll makes an implication constraint:
       forall a. Eq a =>  [W] ds : Show (T a)
     and because of the degnerate instance for `Show (T a)`, we don't need the `Eq a`
     constraint.  But we don't want to report it as redundant!

(TRC5) Consider this (#25992), where `op2` has a default method
        class C a where { op1, op2 :: a -> a
                        ; op2 = op1 . op1 }
        instance C a => C [a] where
          op1 x = x

  Plainly the (C a) constraint is unused; but the expanded decl will look like
        $dmop2 :: C a => a -> a
        $dmop2 = op1 . op2

        $fCList :: forall a. C a => C [a]
        $fCList @a (d::C a) = MkC (\(x:a).x) ($dmop2 @a d)

   Notice that `d` gets passed to `$dmop`: it is "needed".  But it's only
   /really/ needed if some /other/ method (in this case `op1`) uses it.

   So, rather than one set of "needed Givens" we use `EvNeedSet` to track
   a /pair/ of sets:
      ens_dms: needed /only/ by default-method calls
      ens_fvs: needed by something other than a default-method call
   It's a bit of a palaver, but not really difficult.
   All the logic is localised in `neededEvVars`.



----- Reporting redundant constraints


----- Examples

    f, g, h :: (Eq a, Ord a) => a -> Bool
    f x = x == x
    g x = x > x
    h x = x == x && x > x

    All of f,g,h will discover that they have two [G] Eq a constraints: one as
    given and one extracted from the Ord a constraint. They will both discard
    the latter; see (TRC3).

    The body of f uses the [G] Eq a, but not the [G] Ord a. It will report a
    redundant Ord a.

    The body of g uses the [G] Ord a, but not the [G] Eq a. It will report a
    redundant Eq a.

    The body of h uses both [G] Ord a and [G] Eq a; each is used in a solved
    Wanted evidence binding.  But (TRC2) kicks in and discovers the Eq a
    is redundant.

----- Shortcomings

Shortcoming 1.  Consider

  j :: (Eq a, a ~ b) => a -> Bool
  j x = x == x

  k :: (Eq a, b ~ a) => a -> Bool
  k x = x == x

Currently (Nov 2021), j issues no warning, while k says that b ~ a
is redundant. This is because j uses the a ~ b constraint to rewrite
everything to be in terms of b, while k does none of that. This is
ridiculous, but I (Richard E) don't see a good fix.

Shortcoming 2.  Removing a redundant constraint can cause clients to fail to
compile, by making the function more polymorphic. Consider (#16154)

  f :: (a ~ Bool) => a -> Int
  f x = 3

  g :: String -> Int
  g s = f (read s)

The constraint in f's signature is redundant; not used to typecheck
`f`.  And yet if you remove it, `g` won't compile, because there'll
be an ambiguous variable in `g`.


**********************************************************************
*                                                                    *
*                      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

       -- Capture the Givens in the inert_givens of the inert set
       -- for use by subsequent calls of nestImplicTcS
       -- See Note [trySolveImplication]
       ; (InertSet -> InertSet) -> TcS ()
updInertSet (\InertSet
is -> InertSet
is { inert_givens = inert_cans is })

       ; cans <- TcS InertCans
getInertCans
       ; traceTcS "End solveSimpleGivens }" (ppr cans) }
  where
    go :: [Ct] -> TcS ()
go [Ct]
givens = do { Cts -> TcS ()
solveSimples ([Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
givens)
                   ; new_givens <- TcS [Ct]
runTcPluginsGiven
                   ; when (notNull new_givens) $
                     go new_givens }

solveSimpleWanteds :: Cts -> TcS Cts
-- The result is not necessarily zonked
solveSimpleWanteds :: Cts -> TcS Cts
solveSimpleWanteds Cts
simples
  = do { mode   <- TcS TcSMode
getTcSMode
       ; dflags <- getDynFlags
       ; inerts <- getInertSet

       ; traceTcS "solveSimpleWanteds {" $
         vcat [ text "Mode:" <+> ppr mode
              , text "Inerts:" <+> ppr inerts
              , text "Wanteds to solve:" <+> ppr simples ]

       ; (n,wc) <- go 1 (solverIterations dflags) simples

       ; traceTcS "solveSimpleWanteds end }" $
             vcat [ text "iterations =" <+> ppr n
                  , text "residual =" <+> ppr wc ]
       ; return wc }
  where
    go :: Int -> IntWithInf -> Cts -> TcS (Int, Cts)
    -- See Note [The solveSimpleWanteds loop]
    go :: Int -> IntWithInf -> Cts -> TcS (Int, Cts)
go Int
n IntWithInf
limit Cts
wc
      | Int
n Int -> IntWithInf -> Bool
`intGtLimit` IntWithInf
limit
      = TcRnMessage -> TcS (Int, Cts)
forall a. TcRnMessage -> TcS a
failTcS (TcRnMessage -> TcS (Int, Cts)) -> TcRnMessage -> TcS (Int, Cts)
forall a b. (a -> b) -> a -> b
$ Cts -> IntWithInf -> WantedConstraints -> TcRnMessage
TcRnSimplifierTooManyIterations
                         Cts
simples IntWithInf
limit (WantedConstraints
emptyWC { wc_simple = wc })
      | Cts -> Bool
forall a. Bag a -> Bool
isEmptyBag Cts
wc
      = (Int, Cts) -> TcS (Int, Cts)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n,Cts
wc)
      | Bool
otherwise
      = do { -- Solve
             wc1 <- Cts -> TcS Cts
solve_simple_wanteds Cts
wc

             -- Run plugins
             -- NB: runTcPluginsWanted has a fast path for empty wc1,
             --     which is the common case
           ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1

           ; if rerun_plugin
             then do { traceTcS "solveSimple going round again:" (ppr rerun_plugin)
                     ; go (n+1) limit wc2 }   -- Loop
             else return (n, wc2) }           -- Done


solve_simple_wanteds :: Cts -> TcS Cts
-- Try solving these constraints
-- Affects the unification state (of course) but not the inert set
-- The result is not necessarily zonked
solve_simple_wanteds :: Cts -> TcS Cts
solve_simple_wanteds Cts
simples
  = TcS Cts -> TcS Cts
forall a. TcS a -> TcS a
nestTcS (TcS Cts -> TcS Cts) -> TcS Cts -> TcS Cts
forall a b. (a -> b) -> a -> b
$ do { Cts -> TcS ()
solveSimples Cts
simples
                 ; TcS Cts
getUnsolvedInerts }

{- 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 ()
-- Solve this bag of constraints,
-- returning the final InertSet in TcS
-- 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 { sel <- TcS (Maybe Ct)
selectNextWorkItem
           ; case 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 { wl      <- TcS WorkList
getWorkList
       ; inerts  <- getInertSet
       ; tclevel <- TcS.getTcLevel
       ; traceTcS "----------------------------- " empty
       ; traceTcS "Start solver pipeline {" $
                  vcat [ text "tclevel =" <+> ppr tclevel
                       , text "work item =" <+> ppr workItem
                       , text "inerts =" <+> ppr inerts
                       , text "rest of worklist =" <+> ppr wl ]

       ; bumpStepCountTcS    -- One step for each constraint processed
       ; solve 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)
           ; res <- SolverStage Void -> TcS (StopOrContinue Void)
forall a. SolverStage a -> TcS (StopOrContinue a)
runSolverStage (Ct -> SolverStage Void
solveCt Ct
ct)
           ; traceTcS "end solve }" (ppr res)
           ; case 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 -> TcType
eq_rhs = TcType
rhs }))
  = CtEvidence -> EqRel -> TcType -> TcType -> SolverStage Void
solveEquality CtEvidence
ev EqRel
eq_rel (CanEqLHS -> TcType
canEqLHSType CanEqLHS
lhs) TcType
rhs

solveCt (CQuantCan qci :: QCInst
qci@(QCI { qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev }))
  = do { 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 classifyPredType (ctEvPred ev') of
           ForAllPred [TcTyVar]
tvs [TcType]
theta TcType
body_pred
             -> QCInst -> SolverStage Void
solveForAll (QCInst
qci { qci_ev = ev', qci_tvs = tvs
                                 , qci_theta = theta, qci_body = body_pred })
           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 { 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 classifyPredType (ctEvPred ev) of
           ClassPred Class
cls [TcType]
tys
             -> DictCt -> SolverStage Void
solveDict (DictCt { di_ev :: CtEvidence
di_ev = CtEvidence
ev, di_cls :: Class
di_cls = Class
cls
                                  , di_tys :: [TcType]
di_tys = [TcType]
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 HasDebugCallStack => TcType -> Pred
TcType -> Pred
classifyPredType (CtEvidence -> TcType
ctEvPred CtEvidence
ev) of {
        EqPred EqRel
eq_rel TcType
ty1 TcType
ty2 -> CtEvidence -> EqRel -> TcType -> TcType -> SolverStage Void
solveEquality CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ty2 ;
        Pred
_ ->

    -- Do rewriting on the constraint, especially zonking
    do { ev <- CtEvidence -> SolverStage CtEvidence
rewriteEvidence CtEvidence
ev

    -- And then re-classify
       ; case classifyPredType (ctEvPred ev) of
           ClassPred Class
cls [TcType]
tys     -> CtEvidence -> Class -> [TcType] -> SolverStage Void
solveDictNC CtEvidence
ev Class
cls [TcType]
tys
           ForAllPred [TcTyVar]
tvs [TcType]
th TcType
p   -> CtEvidence -> [TcTyVar] -> [TcType] -> TcType -> SolverStage Void
solveForAllNC CtEvidence
ev [TcTyVar]
tvs [TcType]
th TcType
p
           IrredPred {}          -> IrredCt -> SolverStage Void
solveIrred (IrredCt { ir_ev :: CtEvidence
ir_ev = CtEvidence
ev, ir_reason :: CtIrredReason
ir_reason = CtIrredReason
IrredShapeReason })
           EqPred EqRel
eq_rel TcType
ty1 TcType
ty2 -> CtEvidence -> EqRel -> TcType -> TcType -> SolverStage Void
solveEquality CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ty2
              -- EqPred only happens if (say) `c` is unified with `a ~# b`,
              -- but that is rare because 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.

-}

-- | Solve a quantified constraint that came from @CNonCanonical@ (which means
-- that superclasses have not yet been expanded).
--
-- Precondition: the constraint has already been rewritten by the inert set.
solveForAllNC :: CtEvidence -> [TcTyVar] -> TcThetaType -> TcPredType
              -> SolverStage Void
solveForAllNC :: CtEvidence -> [TcTyVar] -> [TcType] -> TcType -> SolverStage Void
solveForAllNC CtEvidence
ev [TcTyVar]
tvs [TcType]
theta TcType
body_pred
  = do { fuel <- TcS Int -> SolverStage Int
forall a. TcS a -> SolverStage a
simpleStage TcS Int
mk_super_classes
       ; solveForAll (QCI { qci_ev = ev, qci_tvs = tvs, qci_theta = theta
                          , qci_body = body_pred, qci_pend_sc = fuel }) }

  where
    mk_super_classes :: TcS ExpansionFuel
    mk_super_classes :: TcS Int
mk_super_classes
       | Just (Class
cls,[TcType]
tys) <- TcType -> Maybe (Class, [TcType])
getClassPredTys_maybe TcType
body_pred
       , Class -> Bool
classHasSCs Class
cls
       = do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
            -- Either expand superclasses (Givens) or provide fuel to do so (Wanteds)
            ; if isGiven ev
              then
                -- See Note [Eagerly expand given superclasses]
                -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
                do { sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev tvs theta cls tys
                   ; emitWork (listToBag sc_cts)
                   ; return doNotExpand }
              else
                -- See invariants (a) and (b) in QCI.qci_pend_sc
                -- qcsFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
                -- See Note [Quantified constraints]
                return (qcsFuel dflags)
            }

       | Bool
otherwise
       = Int -> TcS Int
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
doNotExpand

-- | Solve a canonical quantified constraint.
--
-- Precondition: the constraint has already been rewritten by the inert set.
solveForAll :: QCInst -> SolverStage Void
solveForAll :: QCInst -> SolverStage Void
solveForAll qci :: QCInst
qci@(QCI { qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev, qci_tvs :: QCInst -> [TcTyVar]
qci_tvs = [TcTyVar]
tvs, qci_theta :: QCInst -> [TcType]
qci_theta = [TcType]
theta, qci_body :: QCInst -> TcType
qci_body = TcType
pred })
  = case CtEvidence
ev of
      CtGiven {} ->
        -- See Note [Solving a Given forall-constraint]
        do { TcS () -> SolverStage ()
forall a. TcS a -> SolverStage a
simpleStage (QCInst -> TcS ()
addInertForAll QCInst
qci)
           ; CtEvidence -> String -> SolverStage Void
forall a. CtEvidence -> String -> SolverStage a
stopWithStage CtEvidence
ev String
"Given forall-constraint" }
      CtWanted WantedCtEvidence
wtd ->
        do { QCInst -> SolverStage ()
tryInertQCs QCInst
qci
           ; QCInst
-> [TcTyVar]
-> [TcType]
-> TcType
-> WantedCtEvidence
-> SolverStage Void
solveWantedForAll QCInst
qci [TcTyVar]
tvs [TcType]
theta TcType
pred WantedCtEvidence
wtd }

tryInertQCs :: QCInst -> SolverStage ()
tryInertQCs :: QCInst -> SolverStage ()
tryInertQCs QCInst
qc
  = 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 { inerts <- TcS InertCans
getInertCans
       ; try_inert_qcs qc (inert_insts inerts) }

try_inert_qcs :: QCInst -> [QCInst] -> TcS (StopOrContinue ())
try_inert_qcs :: QCInst -> [QCInst] -> TcS (StopOrContinue ())
try_inert_qcs (QCI { qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev_w }) [QCInst]
inerts =
  case (QCInst -> Maybe CtEvidence) -> [QCInst] -> [CtEvidence]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe QCInst -> Maybe CtEvidence
matching_inert [QCInst]
inerts of
    [] -> do { String -> SDoc -> TcS ()
traceTcS String
"tryInertQCs:nothing" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev_w SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [QCInst] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [QCInst]
inerts)
             ; () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith () }
    CtEvidence
ev_i:[CtEvidence]
_ ->
      do { String -> SDoc -> TcS ()
traceTcS String
"tryInertQCs:KeepInert" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev_i)
         ; CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev_w CanonicalEvidence
EvCanonical (CtEvidence -> EvTerm
ctEvTerm CtEvidence
ev_i)
         ; CtEvidence -> String -> TcS (StopOrContinue ())
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev_w String
"Solved Wanted forall-constraint from inert" }
  where
    matching_inert :: QCInst -> Maybe CtEvidence
matching_inert (QCI { qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev_i })
      | CtEvidence -> TcType
ctEvPred CtEvidence
ev_i HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` CtEvidence -> TcType
ctEvPred CtEvidence
ev_w
      = CtEvidence -> Maybe CtEvidence
forall a. a -> Maybe a
Just CtEvidence
ev_i
      | Bool
otherwise
      = Maybe CtEvidence
forall a. Maybe a
Nothing

-- | Solve a (canonical) Wanted quantified constraint by emitting an implication.
-- See Note [Solving a Wanted forall-constraint]
solveWantedForAll :: QCInst -> [TcTyVar] -> TcThetaType -> PredType
                  -> WantedCtEvidence -> SolverStage Void
solveWantedForAll :: QCInst
-> [TcTyVar]
-> [TcType]
-> TcType
-> WantedCtEvidence
-> SolverStage Void
solveWantedForAll QCInst
qci [TcTyVar]
tvs [TcType]
theta TcType
body_pred
                  wtd :: WantedCtEvidence
wtd@(WantedCt { ctev_dest :: WantedCtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest, ctev_loc :: WantedCtEvidence -> CtLoc
ctev_loc = CtLoc
ct_loc
                                , ctev_rewriters :: WantedCtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters })
  = 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
$
    RealSrcSpan
-> TcS (StopOrContinue Void) -> TcS (StopOrContinue Void)
forall a. RealSrcSpan -> TcS a -> TcS a
TcS.setSrcSpan (CtLocEnv -> RealSrcSpan
getCtLocEnvLoc CtLocEnv
loc_env) (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 { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
         --           in GHC.Tc.Utils.TcType
         -- Very like the code in tcSkolDFunType
         rec { skol_info <- mkSkolemInfo skol_info_anon
             ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs
             ; let inst_pred  = HasDebugCallStack => Subst -> TcType -> TcType
Subst -> TcType -> TcType
substTy    Subst
subst TcType
body_pred
                   inst_theta = HasDebugCallStack => Subst -> [TcType] -> [TcType]
Subst -> [TcType] -> [TcType]
substTheta Subst
subst [TcType]
theta
                   skol_info_anon = ClsInstOrQC -> PatersonSize -> SkolemInfoAnon
InstSkol ClsInstOrQC
is_qc (TcType -> PatersonSize
pSizeHead TcType
inst_pred) }

        ; given_ev_vars <- mapM newEvVar inst_theta
        ; (lvl, (w_id, wanteds))
              <- pushLevelNoWorkList (ppr skol_info) $
                 do { let ct_loc' = CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin CtLoc
ct_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]
                    ; wanted_ev <- newWantedNC ct_loc' rewriters inst_pred
                          -- NB: inst_pred can be an equality
                    ; return ( wantedCtEvEvId wanted_ev
                             , unitBag (mkNonCanonical $ CtWanted wanted_ev)) }


       -- Try to solve the constraint completely
       ; traceTcS "solveForAll {" (ppr skol_tvs $$ ppr given_ev_vars $$ ppr wanteds $$ ppr w_id)
       ; ev_binds_var <- TcS.newTcEvBinds
       ; solved <- trySolveImplication $
                   (implicationPrototype loc_env)
                      { ic_tclvl = lvl
                      , ic_binds = ev_binds_var
                      , ic_info  = skol_info_anon
                      , ic_warn_inaccessible = False
                      , ic_skols = skol_tvs
                      , ic_given = given_ev_vars
                      , ic_wanted = emptyWC { wc_simple = wanteds } }
       ; traceTcS "solveForAll }" (ppr solved)

       -- See if we succeeded in solving it completely
       ; if not solved
         then do { -- Not completely solved; abandon that attempt and add the
                   -- original constraint to the inert set
                   addInertForAll qci
                 ; stopWith (CtWanted wtd) "Wanted forall-constraint:unsolved" }

         else do { -- Completely solved; build an evidence term
                   evbs <- TcS.getTcEvBindsMap ev_binds_var
                 ; setWantedEvTerm dest EvCanonical $
                   EvFun { et_tvs = skol_tvs, et_given = given_ev_vars
                         , et_binds = evBindMapBinds evbs, et_body = w_id }
                 ; stopWith (CtWanted wtd) "Wanted forall-constraint:solved" } }
  where
    loc_env :: CtLocEnv
loc_env = CtLoc -> CtLocEnv
ctLocEnv CtLoc
ct_loc
    is_qc :: ClsInstOrQC
is_qc = CtOrigin -> ClsInstOrQC
IsQC (CtLoc -> CtOrigin
ctLocOrigin CtLoc
ct_loc)

    empty_subst :: Subst
empty_subst = InScopeSet -> Subst
mkEmptySubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ CoVarSet -> InScopeSet
mkInScopeSet (CoVarSet -> InScopeSet) -> CoVarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
                  [TcType] -> CoVarSet
tyCoVarsOfTypes (TcType
body_predTcType -> [TcType] -> [TcType]
forall a. a -> [a] -> [a]
:[TcType]
theta) CoVarSet -> [TcTyVar] -> CoVarSet
`delVarSetList` [TcTyVar]
tvs


{- Note [Solving a Wanted forall-constraint]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Solving a wanted forall (quantified) constraint
  [W] df :: forall a b. (Eq a, Ord b) => C x a b
is delightfully easy in principle.   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.

We do not /actually/ emit an implication to solve later.  Rather we
try to solve it completely immediately using `trySolveImplication`
    - If successful, we can build evidence
    - If unsuccessful, we abandon the attempt and add the unsolved
      forall-constraint to the inert set.

There are several reasons for this "solve immediately" approach

* It saves quite a bit of plumbing, tracking the emitted implications for
  later solving; and the evidence would have to contain as-yet-incomplte
  bindings which complicates tracking of unused Givens.

* We get better error messages, about failing to solve, say
         (forall a. a->a) ~ (forall b. b->Int)

* Consider
    f :: forall f a. (Ix a, forall x. Eq x => Eq (f x)) => a -> f a
    {-# SPECIALISE f :: forall f. (forall x. Eq x => Eq (f x)) => Int -> f Int #-}
  This SPECIALISE is treated like an expression with a type signature, so
  we instantiate the constraints, simplify them and re-generalise.  From the
  instantiation we get  [W] d :: (forall x. Eq a => Eq (f x))
  and we want to generalise over that.  We do not want to attempt to solve it
  and then get stuck, and emit an error message.  If we can't solve it, better
  to leave it alone.

  We still need to simplify quantified constraints that can be
  /fully solved/ from instances, otherwise we would never be able to
  specialise them away. Example: {-# SPECIALISE f @[] @a #-}.

  This last point is a big one: it was the immediate driver for moving to
  the "solve immediately" approach.

You might worry about the wasted work from failed attempts to fully-solve, but
it is seldom repeated (because the constraint solver seldom iterates much).

There are some tricky corners though:

(WFA1) We can take a more straightforward path when there is a matching Given, e.g.
          [W] dg :: forall c d. (Eq c, Ord d) => C x c d
    In this case, it's better to directly solve the Wanted from the Given, instead
    of building an implication. This is more than a simple optimisation; see
    Note [Solving Wanted QCs from Given QCs].

(WFA2) 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 dictionary
  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.

(WFA3) When inferring an appropriate context for a `deriving` instance, we
  really /do/ want to generate an implication, and perhaps leave it half-solved,
  from where we might then gather unsolved class constraints (via
  `approximateWC` called in GHC.Tc.Deriv.Infer.simplifyDeriv).  Rather than
  have a complicated special solver mode, we simply generate an /implication/
  in the first place, in GHC.Tc.Deriv.Utils.emitPredSpecConstraints.
  See Note [Inferred contexts from method constraints] in GHC.Tc.Deriv.Infer

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.

Note [Solving Wanted QCs from Given QCs]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we are about to solve a Wanted quantified constraint, and there is a
Given quantified constraint with the same type, we should directly solve the
Wanted from the Given (instead of building an implication).

Not only is this more direct and efficient, sometimes it is also /necessary/.
Consider:

  f :: forall a k. (Eq a, forall x. Eq x => Eq k x) => a -> blah
  {-# SPECIALISE (f :: forall k. (forall x. Eq x => Eq k x) => Int -> blah #-}

Here we specialise the `a` parameter to `f`, leaving the quantified constraint
untouched.  We want to get a rule like:

  RULE  forall @k (d :: forall x. Eq x => Eq k x).
            f @Int @k d = $sf @k d

But when we typecheck that expression-with-a-type-signature, if we don't solve
Wanted forall constraints directly, we will do so indirectly and end up with
this as the LHS of the RULE:

  (/\k \(df::forall x.Eq x => Eq k x). f @Int @k (/\x \(d:Eq x). df @x d))
     @kk dd

We run the simple optimiser on that, which eliminates the beta-redex. However,
it may not eta-reduce that `/\x \(d:Eq x)...`, because we are cautious about
eta-reduction. So we may be left with an over-complicated and hard-to-match
RULE LHS. It's all a bit silly, because the implication constraint is /identical/;
we just need to spot it.

This came up while implementing GHC proposal 493 (allowing expresions in
SPECIALISE pragmas).

************************************************************************
*                                                                      *
                  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)
               ; (redn, rewriters) <- CtEvidence -> TcType -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev (CtEvidence -> TcType
ctEvPred CtEvidence
ev)
               ; finish_rewrite ev redn 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 TcCoercion
co TcType
new_pred) RewriterSet
rewriters
  | TcCoercion -> Bool
isReflCo TcCoercion
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 -> TcType -> CtEvidence
CtEvidence -> TcType -> CtEvidence
setCtEvPredType CtEvidence
old_ev TcType
new_pred)

finish_rewrite
  ev :: CtEvidence
ev@(CtGiven (GivenCt { ctev_evar :: GivenCtEvidence -> TcTyVar
ctev_evar = TcTyVar
old_evar }))
  (Reduction TcCoercion
co TcType
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 { let loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
             -- mkEvCast optimises ReflCo
             ev_rw_role :: Role
ev_rw_role = HasDebugCallStack => CtEvidence -> Role
CtEvidence -> Role
ctEvRewriteRole CtEvidence
ev
             new_tm :: EvTerm
new_tm = Bool
-> (EvExpr -> TcCoercion -> EvTerm)
-> EvExpr
-> TcCoercion
-> EvTerm
forall a. HasCallStack => Bool -> a -> a
assert (TcCoercion -> Role
coercionRole TcCoercion
co Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
ev_rw_role)
                      EvExpr -> TcCoercion -> EvTerm
evCast (TcTyVar -> EvExpr
evId TcTyVar
old_evar) (TcCoercion -> EvTerm) -> TcCoercion -> EvTerm
forall a b. (a -> b) -> a -> b
$   -- evCast optimises ReflCo
                      Role -> Role -> TcCoercion -> TcCoercion
downgradeRole Role
Representational Role
ev_rw_role TcCoercion
co
       ; new_ev <- CtLoc -> (TcType, EvTerm) -> TcS GivenCtEvidence
newGivenEvVar CtLoc
loc (TcType
new_pred, EvTerm
new_tm)
       ; continueWith $ CtGiven new_ev }

finish_rewrite
  ev :: CtEvidence
ev@(CtWanted (WantedCt { ctev_rewriters :: WantedCtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters, ctev_dest :: WantedCtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest }))
  (Reduction TcCoercion
co TcType
new_pred)
  RewriterSet
new_rewriters
  = do { let loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
             rewriters' :: RewriterSet
rewriters' = RewriterSet
rewriters RewriterSet -> RewriterSet -> RewriterSet
forall a. Semigroup a => a -> a -> a
S.<> RewriterSet
new_rewriters
             ev_rw_role :: Role
ev_rw_role = HasDebugCallStack => CtEvidence -> Role
CtEvidence -> Role
ctEvRewriteRole CtEvidence
ev
       ; mb_new_ev <- CtLoc -> RewriterSet -> TcType -> TcS MaybeNew
newWanted CtLoc
loc RewriterSet
rewriters' TcType
new_pred
       ; massert (coercionRole co == ev_rw_role)
       ; setWantedEvTerm dest EvCanonical $
         evCast (getEvExpr mb_new_ev)     $
         downgradeRole Representational ev_rw_role (mkSymCo co)
       ; case mb_new_ev of
            Fresh  WantedCtEvidence
new_ev -> CtEvidence -> TcS (StopOrContinue CtEvidence)
forall a. a -> TcS (StopOrContinue a)
continueWith (CtEvidence -> TcS (StopOrContinue CtEvidence))
-> CtEvidence -> TcS (StopOrContinue CtEvidence)
forall a b. (a -> b) -> a -> b
$ WantedCtEvidence -> CtEvidence
CtWanted WantedCtEvidence
new_ev
            Cached EvExpr
_      -> CtEvidence -> String -> TcS (StopOrContinue CtEvidence)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Cached wanted" }

{- *******************************************************************
*                                                                    *
*                      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 { solvers <- TcS [TcPluginSolver]
getTcPluginSolvers
       ; if null solvers then return [] else
    do { givens <- getInertGivens
       ; if null givens then return [] else
    do { traceTcS "runTcPluginsGiven {" (ppr givens)
       ; p <- runTcPluginSolvers solvers (givens,[])
       ; let (solved_givens, _) = pluginSolvedCts p
             insols             = (Ct -> IrredCt) -> [Ct] -> [IrredCt]
forall a b. (a -> b) -> [a] -> [b]
map (CtIrredReason -> Ct -> IrredCt
ctIrredCt CtIrredReason
PluginReason) (TcPluginProgress -> [Ct]
pluginBadCts TcPluginProgress
p)
       ; updInertCans (removeInertCts solved_givens .
                       updIrreds (addIrreds insols) )
       ; traceTcS "runTcPluginsGiven }" $
         vcat [ text "solved_givens:" <+> ppr solved_givens
              , text "insols:" <+> ppr insols
              , text "new:" <+> ppr (pluginNewCts p) ]
       ; return (pluginNewCts 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 :: Cts -> TcS (Bool, Cts)
runTcPluginsWanted :: Cts -> TcS (Bool, Cts)
runTcPluginsWanted Cts
wanted
  | Cts -> Bool
forall a. Bag a -> Bool
isEmptyBag Cts
wanted
  = (Bool, Cts) -> TcS (Bool, Cts)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Cts
wanted)
  | Bool
otherwise
  = do { solvers <- TcS [TcPluginSolver]
getTcPluginSolvers
       ; if null solvers then return (False, wanted) else

    do { -- Find the set of Givens to give to the plugin.
         -- If TcSMode = TcSShortCut, we are solving with
         -- no Givens so don't return any (#26258)!
         -- See Note [Shortcut solving] in GHC.Tc.Solver.Dict
         mode <- getTcSMode
       ; given <- case mode of
                     TcSMode
TcSShortCut -> [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return []
                     TcSMode
_           -> TcS [Ct]
getInertGivens

         -- Plugin requires zonked input wanteds
       ; zonked_wanted <- TcS.zonkSimples wanted

       ; traceTcS "Running plugins {" (vcat [ text "Given:" <+> ppr given
                                            , text "Wanted:" <+> ppr zonked_wanted ])
       ; p <- runTcPluginSolvers solvers (given, bagToList zonked_wanted)
       ; let (_, solved_wanted)   = pluginSolvedCts p
             (_, unsolved_wanted) = pluginInputCts p
             new_wanted     = TcPluginProgress -> [Ct]
pluginNewCts TcPluginProgress
p
             insols         = TcPluginProgress -> [Ct]
pluginBadCts TcPluginProgress
p
             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

       ; mapM_ setEv solved_wanted

       ; traceTcS "Finished plugins }" (ppr new_wanted)
       ; return ( notNull (pluginNewCts p), 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 (WantedCt { ctev_dest :: WantedCtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest }) -> TcEvDest -> CanonicalEvidence -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest CanonicalEvidence
EvCanonical 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 { tcg_env <- TcS TcGblEnv
TcS.getGblEnv; return (tcg_tc_plugin_solvers 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 { ev_binds_var <- TcS EvBindsVar
getTcEvBindsVar
       ; foldM (do_plugin ev_binds_var) initialProgress 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
        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))
        return $ progress p 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 -> TcType
ctPred Ct
c HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` Ct -> TcType
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)