{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}

-- | Monadic definitions for the constraint solver
module GHC.Tc.Solver.Monad (

    -- The TcS monad
    TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds, runTcSInerts,
    failTcS, warnTcS, addErrTcS, wrapTcS,
    runTcSEqualities,
    nestTcS, nestImplicTcS, setEvBindsTcS,
    emitImplicationTcS, emitTvImplicationTcS,

    selectNextWorkItem,
    getWorkList,
    updWorkListTcS,
    pushLevelNoWorkList,

    runTcPluginTcS, addUsedGRE, addUsedGREs, keepAlive,
    matchGlobalInst, TcM.ClsInstResult(..),

    QCInst(..),

    -- Tracing etc
    panicTcS, traceTcS,
    traceFireTcS, bumpStepCountTcS, csTraceTcS,
    wrapErrTcS, wrapWarnTcS,
    resetUnificationFlag, setUnificationFlag,

    -- Evidence creation and transformation
    MaybeNew(..), freshGoals, isFresh, getEvExpr,

    newTcEvBinds, newNoTcEvBinds,
    newWantedEq, newWantedEq_SI, emitNewWantedEq,
    newWanted, newWanted_SI, newWantedEvVar,
    newWantedNC, newWantedEvVarNC,
    newDerivedNC,
    newBoundEvVarId,
    unifyTyVar, reportUnifications,
    setEvBind, setWantedEq,
    setWantedEvTerm, setEvBindIfWanted,
    newEvVar, newGivenEvVar, newGivenEvVars,
    emitNewDeriveds, emitNewDerivedEq,
    checkReductionDepth,
    getSolvedDicts, setSolvedDicts,

    getInstEnvs, getFamInstEnvs,                -- Getting the environments
    getTopEnv, getGblEnv, getLclEnv,
    getTcEvBindsVar, getTcLevel,
    getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
    tcLookupClass, tcLookupId,

    -- Inerts
    updInertTcS, updInertCans, updInertDicts, updInertIrreds,
    getHasGivenEqs, setInertCans,
    getInertEqs, getInertCans, getInertGivens,
    getInertInsols, getInnermostGivenEqLevel,
    getTcSInerts, setTcSInerts,
    getUnsolvedInerts,
    removeInertCts, getPendingGivenScs,
    addInertCan, insertFunEq, addInertForAll,
    emitWorkNC, emitWork,
    isImprovable,
    lookupInertDict,

    -- The Model
    kickOutAfterUnification,

    -- Inert Safe Haskell safe-overlap failures
    addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
    getSafeOverlapFailures,

    -- Inert solved dictionaries
    addSolvedDict, lookupSolvedDict,

    -- Irreds
    foldIrreds,

    -- The family application cache
    lookupFamAppInert, lookupFamAppCache, extendFamAppCache,
    pprKicked,

    instDFunType,                              -- Instantiation

    -- MetaTyVars
    newFlexiTcSTy, instFlexi, instFlexiX,
    cloneMetaTyVar,
    tcInstSkolTyVarsX,

    TcLevel,
    isFilledMetaTyVar_maybe, isFilledMetaTyVar,
    zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
    zonkTyCoVarsAndFVList,
    zonkSimples, zonkWC,
    zonkTyCoVarKind,

    -- References
    newTcRef, readTcRef, writeTcRef, updTcRef,

    -- Misc
    getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
    matchFam, matchFamTcM,
    checkWellStagedDFun,
    pprEq,                                   -- Smaller utils, re-exported from TcM
                                             -- TODO (DV): these are only really used in the
                                             -- instance matcher in GHC.Tc.Solver. I am wondering
                                             -- if the whole instance matcher simply belongs
                                             -- here

    breakTyVarCycle, rewriterView
) where

import GHC.Prelude

import GHC.Driver.Env

import qualified GHC.Tc.Utils.Instantiate as TcM
import GHC.Core.InstEnv
import GHC.Tc.Instance.Family as FamInst
import GHC.Core.FamInstEnv

import qualified GHC.Tc.Utils.Monad    as TcM
import qualified GHC.Tc.Utils.TcMType  as TcM
import qualified GHC.Tc.Instance.Class as TcM( matchGlobalInst, ClsInstResult(..) )
import qualified GHC.Tc.Utils.Env      as TcM
       ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl )
import GHC.Tc.Instance.Class( InstanceWhat(..), safeOverlap, instanceReturnsDictCon )
import GHC.Tc.Utils.TcType
import GHC.Driver.Session
import GHC.Core.Type
import qualified GHC.Core.TyCo.Rep as Rep  -- this needs to be used only very locally
import GHC.Core.Coercion

import GHC.Tc.Solver.Types
import GHC.Tc.Solver.InertSet

import GHC.Tc.Types.Evidence
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Tc.Errors   ( solverDepthErrorTcS )

import GHC.Types.Name
import GHC.Types.TyThing
import GHC.Unit.Module ( HasModule, getModule )
import GHC.Types.Name.Reader ( GlobalRdrEnv, GlobalRdrElt )
import qualified GHC.Rename.Env as TcM
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Logger
import GHC.Data.Bag as Bag
import GHC.Types.Unique.Supply
import GHC.Tc.Types
import GHC.Tc.Types.Origin
import GHC.Tc.Types.Constraint
import GHC.Core.Predicate

import GHC.Types.Unique.Set

import Control.Monad
import GHC.Utils.Monad
import Data.IORef
import GHC.Exts (oneShot)
import Data.List ( mapAccumL )
import Data.List.NonEmpty ( NonEmpty(..) )
import Control.Arrow ( first )

#if defined(DEBUG)
import GHC.Data.Graph.Directed
#endif

{- *********************************************************************
*                                                                      *
             Shadow constraints and improvement
*                                                                      *
************************************************************************

Note [The improvement story and derived shadows]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Because Wanteds cannot rewrite Wanteds (see Note [Wanteds do not
rewrite Wanteds] in GHC.Tc.Types.Constraint), we may miss some opportunities for
solving.  Here's a classic example (indexed-types/should_fail/T4093a)

    Ambiguity check for f: (Foo e ~ Maybe e) => Foo e

    We get [G] Foo e ~ Maybe e    (CEqCan)
           [W] Foo ee ~ Foo e     (CEqCan)       -- ee is a unification variable
           [W] Foo ee ~ Maybe ee  (CEqCan)

    The first Wanted gets rewritten to

           [W] Foo ee ~ Maybe e

    But now we appear to be stuck, since we don't rewrite Wanteds with
    Wanteds.  This is silly because we can see that ee := e is the
    only solution.

The basic plan is
  * generate Derived constraints that shadow Wanted constraints
  * allow Derived to rewrite Derived
  * in order to cause some unifications to take place
  * that in turn solve the original Wanteds

The ONLY reason for all these Derived equalities is to tell us how to
unify a variable: that is, what Mark Jones calls "improvement".

The same idea is sometimes also called "saturation"; find all the
equalities that must hold in any solution.

Or, equivalently, you can think of the derived shadows as implementing
the "model": a non-idempotent but no-occurs-check substitution,
reflecting *all* *Nominal* equalities (a ~N ty) that are not
immediately soluble by unification.

More specifically, here's how it works (Oct 16):

* Wanted constraints are born as [WD]; this behaves like a
  [W] and a [D] paired together.

* When we are about to add a [WD] to the inert set, if it can
  be rewritten by a [D] a ~ ty, then we split it into [W] and [D],
  putting the latter into the work list (see maybeEmitShadow).

In the example above, we get to the point where we are stuck:
    [WD] Foo ee ~ Foo e
    [WD] Foo ee ~ Maybe ee

But now when [WD] Foo ee ~ Maybe ee is about to be added, we'll
split it into [W] and [D], since the inert [WD] Foo ee ~ Foo e
can rewrite it.  Then:
    work item: [D] Foo ee ~ Maybe ee
    inert:     [W] Foo ee ~ Maybe ee
               [WD] Foo ee ~ Maybe e

See Note [Splitting WD constraints].  Now the work item is rewritten
by the [WD] and we soon get ee := e.

Additional notes:

  * The derived shadow equalities live in inert_eqs, along with
    the Givens and Wanteds; see Note [EqualCtList invariants]
    in GHC.Tc.Solver.Types.

  * We make Derived shadows only for Wanteds, not Givens.  So we
    have only [G], not [GD] and [G] plus splitting.  See
    Note [Add derived shadows only for Wanteds]

  * We also get Derived equalities from functional dependencies
    and type-function injectivity; see calls to unifyDerived.

  * It's worth having [WD] rather than just [W] and [D] because
    * efficiency: silly to process the same thing twice
    * inert_dicts is a finite map keyed by
      the type; it's inconvenient for it to map to TWO constraints

Another example requiring Deriveds is in
Note [Put touchable variables on the left] in GHC.Tc.Solver.Canonical.

Note [Splitting WD constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We are about to add a [WD] constraint to the inert set; and we
know that the inert set has fully rewritten it.  Should we split
it into [W] and [D], and put the [D] in the work list for further
work?

* CDictCan (C tys):
  Yes if the inert set could rewrite tys to make the class constraint,
  or type family, fire.  That is, yes if the inert_eqs intersects
  with the free vars of tys.  For this test we use
  (anyRewritableTyVar True) which ignores casts and coercions in tys,
  because rewriting the casts or coercions won't make the thing fire
  more often.

* CEqCan (lhs ~ ty): Yes if the inert set could rewrite 'lhs' or 'ty'.
  We need to check both 'lhs' and 'ty' against the inert set:
    - Inert set contains  [D] a ~ ty2
      Then we want to put [D] a ~ ty in the worklist, so we'll
      get [D] ty ~ ty2 with consequent good things

    - Inert set contains [D] b ~ a, where b is in ty.
      We can't just add [WD] a ~ ty[b] to the inert set, because
      that breaks the inert-set invariants.  If we tried to
      canonicalise another [D] constraint mentioning 'a', we'd
      get an infinite loop

  Moreover we must use (anyRewritableTyVar False) for the RHS,
  because even tyvars in the casts and coercions could give
  an infinite loop if we don't expose it

* CIrredCan: Yes if the inert set can rewrite the constraint.
  We used to think splitting irreds was unnecessary, but
  see Note [Splitting Irred WD constraints]

* Others: nothing is gained by splitting.

Note [Splitting Irred WD constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Splitting Irred constraints can make a difference. Here is the
scenario:

  a[sk] :: F v     -- F is a type family
  beta :: alpha

  work item: [WD] a ~ beta

This is heterogeneous, so we emit a kind equality and make the work item an
inert Irred.

  work item: [D] F v ~ alpha
  inert: [WD] (a |> co) ~ beta (CIrredCan)

Can't make progress on the work item. Add to inert set. This kicks out the
old inert, because a [D] can rewrite a [WD].

  work item: [WD] (a |> co) ~ beta
  inert: [D] F v ~ alpha (CEqCan)

Can't make progress on this work item either (although GHC tries by
decomposing the cast and rewriting... but that doesn't make a difference),
which is still hetero. Emit a new kind equality and add to inert set. But,
critically, we split the Irred.

  work list:
   [D] F v ~ alpha (CEqCan)
   [D] (a |> co) ~ beta (CIrred) -- this one was split off
  inert:
   [W] (a |> co) ~ beta
   [D] F v ~ alpha

We quickly solve the first work item, as it's the same as an inert.

  work item: [D] (a |> co) ~ beta
  inert:
   [W] (a |> co) ~ beta
   [D] F v ~ alpha

We decompose the cast, yielding

  [D] a ~ beta

We then rewrite the kinds. The lhs kind is F v, which flattens to alpha.

  co' :: F v ~ alpha
  [D] (a |> co') ~ beta

Now this equality is homo-kinded. So we swizzle it around to

  [D] beta ~ (a |> co')

and set beta := a |> co', and go home happy.

If we don't split the Irreds, we loop. This is all dangerously subtle.

This is triggered by test case typecheck/should_compile/SplitWD.

Note [Add derived shadows only for Wanteds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We only add shadows for Wanted constraints. That is, we have
[WD] but not [GD]; and maybeEmitShaodw looks only at [WD]
constraints.

It does just possibly make sense ot add a derived shadow for a
Given. If we created a Derived shadow of a Given, it could be
rewritten by other Deriveds, and that could, conceivably, lead to a
useful unification.

But (a) I have been unable to come up with an example of this
        happening
    (b) see #12660 for how adding the derived shadows
        of a Given led to an infinite loop.
    (c) It's unlikely that rewriting derived Givens will lead
        to a unification because Givens don't mention touchable
        unification variables

For (b) there may be other ways to solve the loop, but simply
reraining from adding derived shadows of Givens is particularly
simple.  And it's more efficient too!

Still, here's one possible reason for adding derived shadows
for Givens.  Consider
           work-item [G] a ~ [b], inerts has [D] b ~ a.
If we added the derived shadow (into the work list)
         [D] a ~ [b]
When we process it, we'll rewrite to a ~ [a] and get an
occurs check.  Without it we'll miss the occurs check (reporting
inaccessible code); but that's probably OK.

Note [Keep CDictCan shadows as CDictCan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
  class C a => D a b
and [G] D a b, [G] C a in the inert set.  Now we insert
[D] b ~ c.  We want to kick out a derived shadow for [D] D a b,
so we can rewrite it with the new constraint, and perhaps get
instance reduction or other consequences.

BUT we do not want to kick out a *non-canonical* (D a b). If we
did, we would do this:
  - rewrite it to [D] D a c, with pend_sc = True
  - use expandSuperClasses to add C a
  - go round again, which solves C a from the givens
This loop goes on for ever and triggers the simpl_loop limit.

Solution: kick out the CDictCan which will have pend_sc = False,
because we've already added its superclasses.  So we won't re-add
them.  If we forget the pend_sc flag, our cunning scheme for avoiding
generating superclasses repeatedly will fail.

See #11379 for a case of this.

Note [Do not do improvement for WOnly]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We do improvement between two constraints (e.g. for injectivity
or functional dependencies) only if both are "improvable". And
we improve a constraint wrt the top-level instances only if
it is improvable.

Improvable:     [G] [WD] [D}
Not improvable: [W]

Reasons:

* It's less work: fewer pairs to compare

* Every [W] has a shadow [D] so nothing is lost

* Consider [WD] C Int b,  where 'b' is a skolem, and
    class C a b | a -> b
    instance C Int Bool
  We'll do a fundep on it and emit [D] b ~ Bool
  That will kick out constraint [WD] C Int b
  Then we'll split it to [W] C Int b (keep in inert)
                     and [D] C Int b (in work list)
  When processing the latter we'll rewrite it to
        [D] C Int Bool
  At that point it would be /stupid/ to interact it
  with the inert [W] C Int b in the inert set; after all,
  it's the very constraint from which the [D] C Int Bool
  was split!  We can avoid this by not doing improvement
  on [W] constraints. This came up in #12860.
-}

maybeEmitShadow :: InertCans -> Ct -> TcS Ct
-- See Note [The improvement story and derived shadows]
maybeEmitShadow :: InertCans -> Ct -> TcS Ct
maybeEmitShadow InertCans
ics Ct
ct
  | let ev :: CtEvidence
ev = Ct -> CtEvidence
ctEvidence Ct
ct
  , CtWanted { ctev_pred :: CtEvidence -> TcPredType
ctev_pred = TcPredType
pred, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc
             , ctev_nosh :: CtEvidence -> ShadowInfo
ctev_nosh = ShadowInfo
WDeriv } <- CtEvidence
ev
  , InertEqs -> FunEqMap EqualCtList -> Ct -> Bool
shouldSplitWD (InertCans -> InertEqs
inert_eqs InertCans
ics) (InertCans -> FunEqMap EqualCtList
inert_funeqs InertCans
ics) Ct
ct
  = do { String -> SDoc -> TcS ()
traceTcS String
"Emit derived shadow" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)
       ; let derived_ev :: CtEvidence
derived_ev = CtDerived :: TcPredType -> CtLoc -> CtEvidence
CtDerived { ctev_pred :: TcPredType
ctev_pred = TcPredType
pred
                                    , ctev_loc :: CtLoc
ctev_loc  = CtLoc
loc }
             shadow_ct :: Ct
shadow_ct = Ct
ct { cc_ev :: CtEvidence
cc_ev = CtEvidence
derived_ev }
               -- Te shadow constraint keeps the canonical shape.
               -- This just saves work, but is sometimes important;
               -- see Note [Keep CDictCan shadows as CDictCan]
       ; [Ct] -> TcS ()
emitWork [Ct
shadow_ct]

       ; let ev' :: CtEvidence
ev' = CtEvidence
ev { ctev_nosh :: ShadowInfo
ctev_nosh = ShadowInfo
WOnly }
             ct' :: Ct
ct' = Ct
ct { cc_ev :: CtEvidence
cc_ev = CtEvidence
ev' }
                 -- Record that it now has a shadow
                 -- This is /the/ place we set the flag to WOnly
       ; Ct -> TcS Ct
forall (m :: * -> *) a. Monad m => a -> m a
return Ct
ct' }

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

shouldSplitWD :: InertEqs -> FunEqMap EqualCtList -> Ct -> Bool
-- Precondition: 'ct' is [WD], and is inert
-- True <=> we should split ct ito [W] and [D] because
--          the inert_eqs can make progress on the [D]
-- See Note [Splitting WD constraints]

shouldSplitWD :: InertEqs -> FunEqMap EqualCtList -> Ct -> Bool
shouldSplitWD InertEqs
inert_eqs FunEqMap EqualCtList
fun_eqs (CDictCan { cc_tyargs :: Ct -> [TcPredType]
cc_tyargs = [TcPredType]
tys })
  = InertEqs -> FunEqMap EqualCtList -> [TcPredType] -> Bool
should_split_match_args InertEqs
inert_eqs FunEqMap EqualCtList
fun_eqs [TcPredType]
tys
    -- NB True: ignore coercions
    -- See Note [Splitting WD constraints]

shouldSplitWD InertEqs
inert_eqs FunEqMap EqualCtList
fun_eqs (CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = TyVarLHS TcTyVar
tv, cc_rhs :: Ct -> TcPredType
cc_rhs = TcPredType
ty
                                        , cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
  =  TcTyVar
tv TcTyVar -> InertEqs -> Bool
forall a. TcTyVar -> DVarEnv a -> Bool
`elemDVarEnv` InertEqs
inert_eqs
  Bool -> Bool -> Bool
|| EqRel
-> (EqRel -> TcTyVar -> Bool)
-> (EqRel -> TyCon -> [TcPredType] -> Bool)
-> TcPredType
-> Bool
anyRewritableCanEqLHS EqRel
eq_rel (InertEqs -> EqRel -> TcTyVar -> Bool
canRewriteTv InertEqs
inert_eqs) (FunEqMap EqualCtList -> EqRel -> TyCon -> [TcPredType] -> Bool
canRewriteTyFam FunEqMap EqualCtList
fun_eqs) TcPredType
ty
  -- NB False: do not ignore casts and coercions
  -- See Note [Splitting WD constraints]

shouldSplitWD InertEqs
inert_eqs FunEqMap EqualCtList
fun_eqs (CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
  = EqRel
-> (EqRel -> TcTyVar -> Bool)
-> (EqRel -> TyCon -> [TcPredType] -> Bool)
-> TcPredType
-> Bool
anyRewritableCanEqLHS EqRel
eq_rel (InertEqs -> EqRel -> TcTyVar -> Bool
canRewriteTv InertEqs
inert_eqs) (FunEqMap EqualCtList -> EqRel -> TyCon -> [TcPredType] -> Bool
canRewriteTyFam FunEqMap EqualCtList
fun_eqs)
                          (CtEvidence -> TcPredType
ctEvPred CtEvidence
ev)

shouldSplitWD InertEqs
inert_eqs FunEqMap EqualCtList
fun_eqs (CIrredCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev })
  = EqRel
-> (EqRel -> TcTyVar -> Bool)
-> (EqRel -> TyCon -> [TcPredType] -> Bool)
-> TcPredType
-> Bool
anyRewritableCanEqLHS (CtEvidence -> EqRel
ctEvEqRel CtEvidence
ev) (InertEqs -> EqRel -> TcTyVar -> Bool
canRewriteTv InertEqs
inert_eqs)
                          (FunEqMap EqualCtList -> EqRel -> TyCon -> [TcPredType] -> Bool
canRewriteTyFam FunEqMap EqualCtList
fun_eqs) (CtEvidence -> TcPredType
ctEvPred CtEvidence
ev)

shouldSplitWD InertEqs
_ FunEqMap EqualCtList
_ Ct
_ = Bool
False   -- No point in splitting otherwise

should_split_match_args :: InertEqs -> FunEqMap EqualCtList -> [TcType] -> Bool
-- True if the inert_eqs can rewrite anything in the argument types
should_split_match_args :: InertEqs -> FunEqMap EqualCtList -> [TcPredType] -> Bool
should_split_match_args InertEqs
inert_eqs FunEqMap EqualCtList
fun_eqs [TcPredType]
tys
  = (TcPredType -> Bool) -> [TcPredType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (EqRel
-> (EqRel -> TcTyVar -> Bool)
-> (EqRel -> TyCon -> [TcPredType] -> Bool)
-> TcPredType
-> Bool
anyRewritableCanEqLHS EqRel
NomEq (InertEqs -> EqRel -> TcTyVar -> Bool
canRewriteTv InertEqs
inert_eqs) (FunEqMap EqualCtList -> EqRel -> TyCon -> [TcPredType] -> Bool
canRewriteTyFam FunEqMap EqualCtList
fun_eqs)) [TcPredType]
tys
    -- See Note [Splitting WD constraints]

canRewriteTv :: InertEqs -> EqRel -> TyVar -> Bool
canRewriteTv :: InertEqs -> EqRel -> TcTyVar -> Bool
canRewriteTv InertEqs
inert_eqs EqRel
eq_rel TcTyVar
tv
  | Just (EqualCtList (Ct
ct :| [Ct]
_)) <- InertEqs -> TcTyVar -> Maybe EqualCtList
forall a. DVarEnv a -> TcTyVar -> Maybe a
lookupDVarEnv InertEqs
inert_eqs TcTyVar
tv
  , CEqCan { cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel1 } <- Ct
ct
  = EqRel
eq_rel1 EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
eq_rel
  | Bool
otherwise
  = Bool
False

canRewriteTyFam :: FunEqMap EqualCtList -> EqRel -> TyCon -> [Type] -> Bool
canRewriteTyFam :: FunEqMap EqualCtList -> EqRel -> TyCon -> [TcPredType] -> Bool
canRewriteTyFam FunEqMap EqualCtList
fun_eqs EqRel
eq_rel TyCon
tf [TcPredType]
args
  | Just (EqualCtList (Ct
ct :| [Ct]
_)) <- FunEqMap EqualCtList -> TyCon -> [TcPredType] -> Maybe EqualCtList
forall a. FunEqMap a -> TyCon -> [TcPredType] -> Maybe a
findFunEq FunEqMap EqualCtList
fun_eqs TyCon
tf [TcPredType]
args
  , CEqCan { cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel1 } <- Ct
ct
  = EqRel
eq_rel1 EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
eq_rel
  | Bool
otherwise
  = Bool
False

isImprovable :: CtEvidence -> Bool
-- See Note [Do not do improvement for WOnly]
isImprovable :: CtEvidence -> Bool
isImprovable (CtWanted { ctev_nosh :: CtEvidence -> ShadowInfo
ctev_nosh = ShadowInfo
WOnly }) = Bool
False
isImprovable CtEvidence
_                                = Bool
True


{- *********************************************************************
*                                                                      *
                   Inert instances: inert_insts
*                                                                      *
********************************************************************* -}

addInertForAll :: QCInst -> TcS ()
-- Add a local Given instance, typically arising from a type signature
addInertForAll :: QCInst -> TcS ()
addInertForAll QCInst
new_qci
  = do { InertCans
ics  <- TcS InertCans
getInertCans
       ; InertCans
ics1 <- InertCans -> TcS InertCans
add_qci InertCans
ics

       -- Update given equalities. C.f updateGivenEqs
       ; TcLevel
tclvl <- TcS TcLevel
getTcLevel
       ; let pred :: TcPredType
pred         = QCInst -> TcPredType
qci_pred QCInst
new_qci
             not_equality :: Bool
not_equality = TcPredType -> Bool
isClassPred TcPredType
pred Bool -> Bool -> Bool
&& Bool -> Bool
not (TcPredType -> Bool
isEqPred TcPredType
pred)
                  -- True <=> definitely not an equality
                  -- A qci_pred like (f a) might be an equality

             ics2 :: InertCans
ics2 | Bool
not_equality = InertCans
ics1
                  | Bool
otherwise    = InertCans
ics1 { inert_given_eq_lvl :: TcLevel
inert_given_eq_lvl = TcLevel
tclvl
                                        , inert_given_eqs :: Bool
inert_given_eqs    = Bool
True }

       ; InertCans -> TcS ()
setInertCans InertCans
ics2 }
  where
    add_qci :: InertCans -> TcS InertCans
    -- See Note [Do not add duplicate quantified instances]
    add_qci :: InertCans -> TcS InertCans
add_qci ics :: InertCans
ics@(IC { inert_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
qcis })
      | (QCInst -> Bool) -> [QCInst] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any QCInst -> Bool
same_qci [QCInst]
qcis
      = do { String -> SDoc -> TcS ()
traceTcS String
"skipping duplicate quantified instance" (QCInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr QCInst
new_qci)
           ; InertCans -> TcS InertCans
forall (m :: * -> *) a. Monad m => a -> m a
return InertCans
ics }

      | Bool
otherwise
      = do { String -> SDoc -> TcS ()
traceTcS String
"adding new inert quantified instance" (QCInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr QCInst
new_qci)
           ; InertCans -> TcS InertCans
forall (m :: * -> *) a. Monad m => a -> m a
return (InertCans
ics { inert_insts :: [QCInst]
inert_insts = QCInst
new_qci QCInst -> [QCInst] -> [QCInst]
forall a. a -> [a] -> [a]
: [QCInst]
qcis }) }

    same_qci :: QCInst -> Bool
same_qci QCInst
old_qci = HasDebugCallStack => TcPredType -> TcPredType -> Bool
TcPredType -> TcPredType -> Bool
tcEqType (CtEvidence -> TcPredType
ctEvPred (QCInst -> CtEvidence
qci_ev QCInst
old_qci))
                                (CtEvidence -> TcPredType
ctEvPred (QCInst -> CtEvidence
qci_ev QCInst
new_qci))

{- Note [Do not add duplicate quantified instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (#15244):

  f :: (C g, D g) => ....
  class S g => C g where ...
  class S g => D g where ...
  class (forall a. Eq a => Eq (g a)) => S g where ...

Then in f's RHS there are two identical quantified constraints
available, one via the superclasses of C and one via the superclasses
of D.  The two are identical, and it seems wrong to reject the program
because of that. But without doing duplicate-elimination we will have
two matching QCInsts when we try to solve constraints arising from f's
RHS.

The simplest thing is simply to eliminate duplicates, which we do here.
-}

{- *********************************************************************
*                                                                      *
                  Adding an inert
*                                                                      *
************************************************************************

Note [Adding an equality to the InertCans]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When adding an equality to the inerts:

* Split [WD] into [W] and [D] if the inerts can rewrite the latter;
  done by maybeEmitShadow.

* Kick out any constraints that can be rewritten by the thing
  we are adding.  Done by kickOutRewritable.

* Note that unifying a:=ty, is like adding [G] a~ty; just use
  kickOutRewritable with Nominal, Given.  See kickOutAfterUnification.
-}

addInertCan :: Ct -> TcS ()
-- Precondition: item /is/ canonical
-- See Note [Adding an equality to the InertCans]
addInertCan :: Ct -> TcS ()
addInertCan Ct
ct
  = do { String -> SDoc -> TcS ()
traceTcS String
"addInertCan {" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
         String -> SDoc
text String
"Trying to insert new inert item:" SDoc -> SDoc -> SDoc
<+> Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct

       ; InertCans
ics <- TcS InertCans
getInertCans
       ; Ct
ct  <- InertCans -> Ct -> TcS Ct
maybeEmitShadow InertCans
ics Ct
ct
       ; InertCans
ics <- InertCans -> Ct -> TcS InertCans
maybeKickOut InertCans
ics Ct
ct
       ; TcLevel
tclvl <- TcS TcLevel
getTcLevel
       ; InertCans -> TcS ()
setInertCans (TcLevel -> InertCans -> Ct -> InertCans
addInertItem TcLevel
tclvl InertCans
ics Ct
ct)

       ; String -> SDoc -> TcS ()
traceTcS String
"addInertCan }" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ SDoc
empty }

maybeKickOut :: InertCans -> Ct -> TcS InertCans
-- For a CEqCan, kick out any inert that can be rewritten by the CEqCan
maybeKickOut :: InertCans -> Ct -> TcS InertCans
maybeKickOut InertCans
ics Ct
ct
  | CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs, cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel } <- Ct
ct
  = do { (Int
_, InertCans
ics') <- CtFlavourRole -> CanEqLHS -> InertCans -> TcS (Int, InertCans)
kickOutRewritable (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
eq_rel) CanEqLHS
lhs InertCans
ics
       ; InertCans -> TcS InertCans
forall (m :: * -> *) a. Monad m => a -> m a
return InertCans
ics' }
  | Bool
otherwise
  = InertCans -> TcS InertCans
forall (m :: * -> *) a. Monad m => a -> m a
return InertCans
ics

-----------------------------------------
kickOutRewritable  :: CtFlavourRole  -- Flavour/role of the equality that
                                      -- is being added to the inert set
                   -> CanEqLHS        -- The new equality is lhs ~ ty
                   -> InertCans
                   -> TcS (Int, InertCans)
kickOutRewritable :: CtFlavourRole -> CanEqLHS -> InertCans -> TcS (Int, InertCans)
kickOutRewritable CtFlavourRole
new_fr CanEqLHS
new_lhs InertCans
ics
  = do { let (WorkList
kicked_out, InertCans
ics') = CtFlavourRole -> CanEqLHS -> InertCans -> (WorkList, InertCans)
kickOutRewritableLHS CtFlavourRole
new_fr CanEqLHS
new_lhs InertCans
ics
             n_kicked :: Int
n_kicked = WorkList -> Int
workListSize WorkList
kicked_out

       ; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n_kicked Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
         do { (WorkList -> WorkList) -> TcS ()
updWorkListTcS (WorkList -> WorkList -> WorkList
appendWorkList WorkList
kicked_out)

              -- The famapp-cache contains Given evidence from the inert set.
              -- If we're kicking out Givens, we need to remove this evidence
              -- from the cache, too.
            ; let kicked_given_ev_vars :: [TcTyVar]
kicked_given_ev_vars =
                    [ TcTyVar
ev_var | Ct
ct <- WorkList -> [Ct]
wl_eqs WorkList
kicked_out
                             , CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
ev_var } <- [Ct -> CtEvidence
ctEvidence Ct
ct] ]
            ; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CtFlavourRole
new_fr CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` (CtFlavour
Given, EqRel
NomEq) Bool -> Bool -> Bool
&&
                   -- if this isn't true, no use looking through the constraints
                    Bool -> Bool
not ([TcTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
kicked_given_ev_vars)) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
              do { String -> SDoc -> TcS ()
traceTcS String
"Given(s) have been kicked out; drop from famapp-cache"
                            ([TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
kicked_given_ev_vars)
                 ; VarSet -> TcS ()
dropFromFamAppCache ([TcTyVar] -> VarSet
mkVarSet [TcTyVar]
kicked_given_ev_vars) }

            ; SDoc -> TcS ()
csTraceTcS (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Kick out, lhs =" SDoc -> SDoc -> SDoc
<+> CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
new_lhs)
                 Int
2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"n-kicked =" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
n_kicked
                         , String -> SDoc
text String
"kicked_out =" SDoc -> SDoc -> SDoc
<+> WorkList -> SDoc
forall a. Outputable a => a -> SDoc
ppr WorkList
kicked_out
                         , String -> SDoc
text String
"Residual inerts =" SDoc -> SDoc -> SDoc
<+> InertCans -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertCans
ics' ]) }

       ; (Int, InertCans) -> TcS (Int, InertCans)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n_kicked, InertCans
ics') }

kickOutAfterUnification :: TcTyVar -> TcS Int
kickOutAfterUnification :: TcTyVar -> TcS Int
kickOutAfterUnification TcTyVar
new_tv
  = do { InertCans
ics <- TcS InertCans
getInertCans
       ; (Int
n_kicked, InertCans
ics2) <- CtFlavourRole -> CanEqLHS -> InertCans -> TcS (Int, InertCans)
kickOutRewritable (CtFlavour
Given,EqRel
NomEq)
                                                 (TcTyVar -> CanEqLHS
TyVarLHS TcTyVar
new_tv) InertCans
ics
                     -- Given because the tv := xi is given; NomEq because
                     -- only nominal equalities are solved by unification

       ; InertCans -> TcS ()
setInertCans InertCans
ics2
       ; Int -> TcS Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n_kicked }

-- See Wrinkle (2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
kickOutAfterFillingCoercionHole :: CoercionHole -> Coercion -> TcS ()
kickOutAfterFillingCoercionHole :: CoercionHole -> Coercion -> TcS ()
kickOutAfterFillingCoercionHole CoercionHole
hole Coercion
filled_co
  = do { InertCans
ics <- TcS InertCans
getInertCans
       ; let (WorkList
kicked_out, InertCans
ics') = InertCans -> (WorkList, InertCans)
kick_out InertCans
ics
             n_kicked :: Int
n_kicked           = WorkList -> Int
workListSize WorkList
kicked_out

       ; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n_kicked Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
         do { (WorkList -> WorkList) -> TcS ()
updWorkListTcS (WorkList -> WorkList -> WorkList
appendWorkList WorkList
kicked_out)
            ; SDoc -> TcS ()
csTraceTcS (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Kick out, hole =" SDoc -> SDoc -> SDoc
<+> CoercionHole -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoercionHole
hole)
                 Int
2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"n-kicked =" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
n_kicked
                         , String -> SDoc
text String
"kicked_out =" SDoc -> SDoc -> SDoc
<+> WorkList -> SDoc
forall a. Outputable a => a -> SDoc
ppr WorkList
kicked_out
                         , String -> SDoc
text String
"Residual inerts =" SDoc -> SDoc -> SDoc
<+> InertCans -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertCans
ics' ]) }

       ; InertCans -> TcS ()
setInertCans InertCans
ics' }
  where
    holes_of_co :: UniqSet CoercionHole
holes_of_co = Coercion -> UniqSet CoercionHole
coercionHolesOfCo Coercion
filled_co

    kick_out :: InertCans -> (WorkList, InertCans)
    kick_out :: InertCans -> (WorkList, InertCans)
kick_out ics :: InertCans
ics@(IC { inert_irreds :: InertCans -> Cts
inert_irreds = Cts
irreds })
      = let (Cts
to_kick, Cts
to_keep) = (Ct -> Either Ct Ct) -> Cts -> (Cts, Cts)
forall a b c. (a -> Either b c) -> Bag a -> (Bag b, Bag c)
partitionBagWith Ct -> Either Ct Ct
kick_ct Cts
irreds

            kicked_out :: WorkList
kicked_out = [Ct] -> WorkList -> WorkList
extendWorkListCts (Cts -> [Ct]
forall a. Bag a -> [a]
bagToList Cts
to_kick) WorkList
emptyWorkList
            ics' :: InertCans
ics'       = InertCans
ics { inert_irreds :: Cts
inert_irreds = Cts
to_keep }
        in
        (WorkList
kicked_out, InertCans
ics')

    kick_ct :: Ct -> Either Ct Ct
         -- Left: kick out; Right: keep. But even if we keep, we may need
         -- to update the set of blocking holes
    kick_ct :: Ct -> Either Ct Ct
kick_ct ct :: Ct
ct@(CIrredCan { cc_status :: Ct -> CtIrredStatus
cc_status = BlockedCIS UniqSet CoercionHole
holes })
      | CoercionHole
hole CoercionHole -> UniqSet CoercionHole -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
`elementOfUniqSet` UniqSet CoercionHole
holes
      = let new_holes :: UniqSet CoercionHole
new_holes = UniqSet CoercionHole
holes UniqSet CoercionHole -> CoercionHole -> UniqSet CoercionHole
forall a. Uniquable a => UniqSet a -> a -> UniqSet a
`delOneFromUniqSet` CoercionHole
hole
                              UniqSet CoercionHole
-> UniqSet CoercionHole -> UniqSet CoercionHole
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` UniqSet CoercionHole
holes_of_co
            updated_ct :: Ct
updated_ct = Ct
ct { cc_status :: CtIrredStatus
cc_status = UniqSet CoercionHole -> CtIrredStatus
BlockedCIS UniqSet CoercionHole
new_holes }
        in
        if UniqSet CoercionHole -> Bool
forall a. UniqSet a -> Bool
isEmptyUniqSet UniqSet CoercionHole
new_holes
        then Ct -> Either Ct Ct
forall a b. a -> Either a b
Left Ct
updated_ct
        else Ct -> Either Ct Ct
forall a b. b -> Either a b
Right Ct
updated_ct
    kick_ct Ct
other = Ct -> Either Ct Ct
forall a b. b -> Either a b
Right Ct
other

--------------
addInertSafehask :: InertCans -> Ct -> InertCans
addInertSafehask :: InertCans -> Ct -> InertCans
addInertSafehask InertCans
ics item :: Ct
item@(CDictCan { cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [TcPredType]
cc_tyargs = [TcPredType]
tys })
  = InertCans
ics { inert_safehask :: DictMap Ct
inert_safehask = DictMap Ct -> Class -> [TcPredType] -> Ct -> DictMap Ct
addDictCt (InertCans -> DictMap Ct
inert_dicts InertCans
ics) Class
cls [TcPredType]
tys Ct
item }

addInertSafehask InertCans
_ Ct
item
  = String -> SDoc -> InertCans
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"addInertSafehask: can't happen! Inserting " (SDoc -> InertCans) -> SDoc -> InertCans
forall a b. (a -> b) -> a -> b
$ Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
item

insertSafeOverlapFailureTcS :: InstanceWhat -> Ct -> TcS ()
-- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
insertSafeOverlapFailureTcS :: InstanceWhat -> Ct -> TcS ()
insertSafeOverlapFailureTcS InstanceWhat
what Ct
item
  | InstanceWhat -> Bool
safeOverlap InstanceWhat
what = () -> TcS ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise        = (InertCans -> InertCans) -> TcS ()
updInertCans (\InertCans
ics -> InertCans -> Ct -> InertCans
addInertSafehask InertCans
ics Ct
item)

getSafeOverlapFailures :: TcS Cts
-- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
getSafeOverlapFailures :: TcS Cts
getSafeOverlapFailures
 = do { IC { inert_safehask :: InertCans -> DictMap Ct
inert_safehask = DictMap Ct
safehask } <- TcS InertCans
getInertCans
      ; Cts -> TcS Cts
forall (m :: * -> *) a. Monad m => a -> m a
return (Cts -> TcS Cts) -> Cts -> TcS Cts
forall a b. (a -> b) -> a -> b
$ (Ct -> Cts -> Cts) -> DictMap Ct -> Cts -> Cts
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts Ct -> Cts -> Cts
consCts DictMap Ct
safehask Cts
emptyCts }

--------------
addSolvedDict :: InstanceWhat -> CtEvidence -> Class -> [Type] -> TcS ()
-- Conditionally add a new item in the solved set of the monad
-- See Note [Solved dictionaries] in GHC.Tc.Solver.InertSet
addSolvedDict :: InstanceWhat -> CtEvidence -> Class -> [TcPredType] -> TcS ()
addSolvedDict InstanceWhat
what CtEvidence
item Class
cls [TcPredType]
tys
  | CtEvidence -> Bool
isWanted CtEvidence
item
  , InstanceWhat -> Bool
instanceReturnsDictCon InstanceWhat
what
  = do { String -> SDoc -> TcS ()
traceTcS String
"updSolvedSetTcs:" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
item
       ; (InertSet -> InertSet) -> TcS ()
updInertTcS ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertSet
ics ->
             InertSet
ics { inert_solved_dicts :: DictMap CtEvidence
inert_solved_dicts = DictMap CtEvidence
-> Class -> [TcPredType] -> CtEvidence -> DictMap CtEvidence
forall a. DictMap a -> Class -> [TcPredType] -> a -> DictMap a
addDict (InertSet -> DictMap CtEvidence
inert_solved_dicts InertSet
ics) Class
cls [TcPredType]
tys CtEvidence
item } }
  | Bool
otherwise
  = () -> TcS ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

getSolvedDicts :: TcS (DictMap CtEvidence)
getSolvedDicts :: TcS (DictMap CtEvidence)
getSolvedDicts = do { InertSet
ics <- TcS InertSet
getTcSInerts; DictMap CtEvidence -> TcS (DictMap CtEvidence)
forall (m :: * -> *) a. Monad m => a -> m a
return (InertSet -> DictMap CtEvidence
inert_solved_dicts InertSet
ics) }

setSolvedDicts :: DictMap CtEvidence -> TcS ()
setSolvedDicts :: DictMap CtEvidence -> TcS ()
setSolvedDicts DictMap CtEvidence
solved_dicts
  = (InertSet -> InertSet) -> TcS ()
updInertTcS ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertSet
ics ->
    InertSet
ics { inert_solved_dicts :: DictMap CtEvidence
inert_solved_dicts = DictMap CtEvidence
solved_dicts }


{- *********************************************************************
*                                                                      *
                  Other inert-set operations
*                                                                      *
********************************************************************* -}

updInertTcS :: (InertSet -> InertSet) -> TcS ()
-- Modify the inert set with the supplied function
updInertTcS :: (InertSet -> InertSet) -> TcS ()
updInertTcS InertSet -> InertSet
upd_fn
  = do { IORef InertSet
is_var <- TcS (IORef InertSet)
getTcSInertsRef
       ; TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (do { InertSet
curr_inert <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
is_var
                     ; IORef InertSet -> InertSet -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef InertSet
is_var (InertSet -> InertSet
upd_fn InertSet
curr_inert) }) }

getInertCans :: TcS InertCans
getInertCans :: TcS InertCans
getInertCans = do { InertSet
inerts <- TcS InertSet
getTcSInerts; InertCans -> TcS InertCans
forall (m :: * -> *) a. Monad m => a -> m a
return (InertSet -> InertCans
inert_cans InertSet
inerts) }

setInertCans :: InertCans -> TcS ()
setInertCans :: InertCans -> TcS ()
setInertCans InertCans
ics = (InertSet -> InertSet) -> TcS ()
updInertTcS ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertSet
inerts -> InertSet
inerts { inert_cans :: InertCans
inert_cans = InertCans
ics }

updRetInertCans :: (InertCans -> (a, InertCans)) -> TcS a
-- Modify the inert set with the supplied function
updRetInertCans :: (InertCans -> (a, InertCans)) -> TcS a
updRetInertCans InertCans -> (a, InertCans)
upd_fn
  = do { IORef InertSet
is_var <- TcS (IORef InertSet)
getTcSInertsRef
       ; TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS (do { InertSet
inerts <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
is_var
                     ; let (a
res, InertCans
cans') = InertCans -> (a, InertCans)
upd_fn (InertSet -> InertCans
inert_cans InertSet
inerts)
                     ; IORef InertSet -> InertSet -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef InertSet
is_var (InertSet
inerts { inert_cans :: InertCans
inert_cans = InertCans
cans' })
                     ; a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res }) }

updInertCans :: (InertCans -> InertCans) -> TcS ()
-- Modify the inert set with the supplied function
updInertCans :: (InertCans -> InertCans) -> TcS ()
updInertCans InertCans -> InertCans
upd_fn
  = (InertSet -> InertSet) -> TcS ()
updInertTcS ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertSet
inerts -> InertSet
inerts { inert_cans :: InertCans
inert_cans = InertCans -> InertCans
upd_fn (InertSet -> InertCans
inert_cans InertSet
inerts) }

updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
-- Modify the inert set with the supplied function
updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertDicts DictMap Ct -> DictMap Ct
upd_fn
  = (InertCans -> InertCans) -> TcS ()
updInertCans ((InertCans -> InertCans) -> TcS ())
-> (InertCans -> InertCans) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertCans
ics -> InertCans
ics { inert_dicts :: DictMap Ct
inert_dicts = DictMap Ct -> DictMap Ct
upd_fn (InertCans -> DictMap Ct
inert_dicts InertCans
ics) }

updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
-- Modify the inert set with the supplied function
updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertSafehask DictMap Ct -> DictMap Ct
upd_fn
  = (InertCans -> InertCans) -> TcS ()
updInertCans ((InertCans -> InertCans) -> TcS ())
-> (InertCans -> InertCans) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertCans
ics -> InertCans
ics { inert_safehask :: DictMap Ct
inert_safehask = DictMap Ct -> DictMap Ct
upd_fn (InertCans -> DictMap Ct
inert_safehask InertCans
ics) }

updInertIrreds :: (Cts -> Cts) -> TcS ()
-- Modify the inert set with the supplied function
updInertIrreds :: (Cts -> Cts) -> TcS ()
updInertIrreds Cts -> Cts
upd_fn
  = (InertCans -> InertCans) -> TcS ()
updInertCans ((InertCans -> InertCans) -> TcS ())
-> (InertCans -> InertCans) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertCans
ics -> InertCans
ics { inert_irreds :: Cts
inert_irreds = Cts -> Cts
upd_fn (InertCans -> Cts
inert_irreds InertCans
ics) }

getInertEqs :: TcS (DTyVarEnv EqualCtList)
getInertEqs :: TcS InertEqs
getInertEqs = do { InertCans
inert <- TcS InertCans
getInertCans; InertEqs -> TcS InertEqs
forall (m :: * -> *) a. Monad m => a -> m a
return (InertCans -> InertEqs
inert_eqs InertCans
inert) }

getInnermostGivenEqLevel :: TcS TcLevel
getInnermostGivenEqLevel :: TcS TcLevel
getInnermostGivenEqLevel = do { InertCans
inert <- TcS InertCans
getInertCans
                              ; TcLevel -> TcS TcLevel
forall (m :: * -> *) a. Monad m => a -> m a
return (InertCans -> TcLevel
inert_given_eq_lvl InertCans
inert) }

getInertInsols :: TcS Cts
-- Returns insoluble equality constraints
-- specifically including Givens
getInertInsols :: TcS Cts
getInertInsols = do { InertCans
inert <- TcS InertCans
getInertCans
                    ; Cts -> TcS Cts
forall (m :: * -> *) a. Monad m => a -> m a
return ((Ct -> Bool) -> Cts -> Cts
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Ct -> Bool
insolubleEqCt (InertCans -> Cts
inert_irreds InertCans
inert)) }

getInertGivens :: TcS [Ct]
-- Returns the Given constraints in the inert set
getInertGivens :: TcS [Ct]
getInertGivens
  = do { InertCans
inerts <- TcS InertCans
getInertCans
       ; let all_cts :: [Ct]
all_cts = (Ct -> [Ct] -> [Ct]) -> DictMap Ct -> [Ct] -> [Ct]
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts (:) (InertCans -> DictMap Ct
inert_dicts InertCans
inerts)
                     ([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ (EqualCtList -> [Ct] -> [Ct])
-> FunEqMap EqualCtList -> [Ct] -> [Ct]
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldFunEqs (\EqualCtList
ecl [Ct]
out -> EqualCtList -> [Ct]
equalCtListToList EqualCtList
ecl [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
out)
                                  (InertCans -> FunEqMap EqualCtList
inert_funeqs InertCans
inerts)
                     ([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ (EqualCtList -> [Ct]) -> [EqualCtList] -> [Ct]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap EqualCtList -> [Ct]
equalCtListToList (InertEqs -> [EqualCtList]
forall a. DVarEnv a -> [a]
dVarEnvElts (InertCans -> InertEqs
inert_eqs InertCans
inerts))
       ; [Ct] -> TcS [Ct]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Ct -> Bool) -> [Ct] -> [Ct]
forall a. (a -> Bool) -> [a] -> [a]
filter Ct -> Bool
isGivenCt [Ct]
all_cts) }

getPendingGivenScs :: TcS [Ct]
-- Find all inert Given dictionaries, or quantified constraints,
--     whose cc_pend_sc flag is True
--     and that belong to the current level
-- Set their cc_pend_sc flag to False in the inert set, and return that Ct
getPendingGivenScs :: TcS [Ct]
getPendingGivenScs = do { TcLevel
lvl <- TcS TcLevel
getTcLevel
                        ; (InertCans -> ([Ct], InertCans)) -> TcS [Ct]
forall a. (InertCans -> (a, InertCans)) -> TcS a
updRetInertCans (TcLevel -> InertCans -> ([Ct], InertCans)
get_sc_pending TcLevel
lvl) }

get_sc_pending :: TcLevel -> InertCans -> ([Ct], InertCans)
get_sc_pending :: TcLevel -> InertCans -> ([Ct], InertCans)
get_sc_pending TcLevel
this_lvl ic :: InertCans
ic@(IC { inert_dicts :: InertCans -> DictMap Ct
inert_dicts = DictMap Ct
dicts, inert_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
insts })
  = Bool -> SDoc -> ([Ct], InertCans) -> ([Ct], InertCans)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ((Ct -> Bool) -> [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Ct -> Bool
isGivenCt [Ct]
sc_pending) ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
sc_pending)
       -- When getPendingScDics is called,
       -- there are never any Wanteds in the inert set
    ([Ct]
sc_pending, InertCans
ic { inert_dicts :: DictMap Ct
inert_dicts = DictMap Ct
dicts', inert_insts :: [QCInst]
inert_insts = [QCInst]
insts' })
  where
    sc_pending :: [Ct]
sc_pending = [Ct]
sc_pend_insts [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
sc_pend_dicts

    sc_pend_dicts :: [Ct]
sc_pend_dicts = (Ct -> [Ct] -> [Ct]) -> DictMap Ct -> [Ct] -> [Ct]
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts Ct -> [Ct] -> [Ct]
get_pending DictMap Ct
dicts []
    dicts' :: DictMap Ct
dicts' = (Ct -> DictMap Ct -> DictMap Ct)
-> DictMap Ct -> [Ct] -> DictMap Ct
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> DictMap Ct -> DictMap Ct
add DictMap Ct
dicts [Ct]
sc_pend_dicts

    ([Ct]
sc_pend_insts, [QCInst]
insts') = ([Ct] -> QCInst -> ([Ct], QCInst))
-> [Ct] -> [QCInst] -> ([Ct], [QCInst])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL [Ct] -> QCInst -> ([Ct], QCInst)
get_pending_inst [] [QCInst]
insts

    get_pending :: Ct -> [Ct] -> [Ct]  -- Get dicts with cc_pend_sc = True
                                       -- but flipping the flag
    get_pending :: Ct -> [Ct] -> [Ct]
get_pending Ct
dict [Ct]
dicts
        | Just Ct
dict' <- Ct -> Maybe Ct
isPendingScDict Ct
dict
        , CtEvidence -> Bool
belongs_to_this_level (Ct -> CtEvidence
ctEvidence Ct
dict)
        = Ct
dict' Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: [Ct]
dicts
        | Bool
otherwise
        = [Ct]
dicts

    add :: Ct -> DictMap Ct -> DictMap Ct
    add :: Ct -> DictMap Ct -> DictMap Ct
add ct :: Ct
ct@(CDictCan { cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [TcPredType]
cc_tyargs = [TcPredType]
tys }) DictMap Ct
dicts
        = DictMap Ct -> Class -> [TcPredType] -> Ct -> DictMap Ct
addDictCt DictMap Ct
dicts Class
cls [TcPredType]
tys Ct
ct
    add Ct
ct DictMap Ct
_ = String -> SDoc -> DictMap Ct
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"getPendingScDicts" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)

    get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
    get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
get_pending_inst [Ct]
cts qci :: QCInst
qci@(QCI { qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev })
       | Just QCInst
qci' <- QCInst -> Maybe QCInst
isPendingScInst QCInst
qci
       , CtEvidence -> Bool
belongs_to_this_level CtEvidence
ev
       = (QCInst -> Ct
CQuantCan QCInst
qci' Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: [Ct]
cts, QCInst
qci')
       | Bool
otherwise
       = ([Ct]
cts, QCInst
qci)

    belongs_to_this_level :: CtEvidence -> Bool
belongs_to_this_level CtEvidence
ev = CtLoc -> TcLevel
ctLocLevel (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) TcLevel -> TcLevel -> Bool
forall a. Eq a => a -> a -> Bool
== TcLevel
this_lvl
    -- We only want Givens from this level; see (3a) in
    -- Note [The superclass story] in GHC.Tc.Solver.Canonical

getUnsolvedInerts :: TcS ( Bag Implication
                         , Cts )   -- All simple constraints
-- Return all the unsolved [Wanted] or [Derived] constraints
--
-- Post-condition: the returned simple constraints are all fully zonked
--                     (because they come from the inert set)
--                 the unsolved implics may not be
getUnsolvedInerts :: TcS (Bag Implication, Cts)
getUnsolvedInerts
 = do { IC { inert_eqs :: InertCans -> InertEqs
inert_eqs    = InertEqs
tv_eqs
           , inert_funeqs :: InertCans -> FunEqMap EqualCtList
inert_funeqs = FunEqMap EqualCtList
fun_eqs
           , inert_irreds :: InertCans -> Cts
inert_irreds = Cts
irreds
           , inert_dicts :: InertCans -> DictMap Ct
inert_dicts  = DictMap Ct
idicts
           } <- TcS InertCans
getInertCans

      ; let unsolved_tv_eqs :: Cts
unsolved_tv_eqs  = (Ct -> Cts -> Cts) -> InertEqs -> Cts -> Cts
forall b. (Ct -> b -> b) -> InertEqs -> b -> b
foldTyEqs Ct -> Cts -> Cts
add_if_unsolved InertEqs
tv_eqs Cts
emptyCts
            unsolved_fun_eqs :: Cts
unsolved_fun_eqs = (EqualCtList -> Cts -> Cts) -> FunEqMap EqualCtList -> Cts -> Cts
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldFunEqs EqualCtList -> Cts -> Cts
add_if_unsolveds FunEqMap EqualCtList
fun_eqs Cts
emptyCts
            unsolved_irreds :: Cts
unsolved_irreds  = (Ct -> Bool) -> Cts -> Cts
forall a. (a -> Bool) -> Bag a -> Bag a
Bag.filterBag Ct -> Bool
is_unsolved Cts
irreds
            unsolved_dicts :: Cts
unsolved_dicts   = (Ct -> Cts -> Cts) -> DictMap Ct -> Cts -> Cts
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts Ct -> Cts -> Cts
add_if_unsolved DictMap Ct
idicts Cts
emptyCts
            unsolved_others :: Cts
unsolved_others  = Cts
unsolved_irreds Cts -> Cts -> Cts
forall a. Bag a -> Bag a -> Bag a
`unionBags` Cts
unsolved_dicts

      ; Bag Implication
implics <- TcS (Bag Implication)
getWorkListImplics

      ; String -> SDoc -> TcS ()
traceTcS String
"getUnsolvedInerts" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
        [SDoc] -> SDoc
vcat [ String -> SDoc
text String
" tv eqs =" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
unsolved_tv_eqs
             , String -> SDoc
text String
"fun eqs =" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
unsolved_fun_eqs
             , String -> SDoc
text String
"others =" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
unsolved_others
             , String -> SDoc
text String
"implics =" SDoc -> SDoc -> SDoc
<+> Bag Implication -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag Implication
implics ]

      ; (Bag Implication, Cts) -> TcS (Bag Implication, Cts)
forall (m :: * -> *) a. Monad m => a -> m a
return ( Bag Implication
implics, Cts
unsolved_tv_eqs Cts -> Cts -> Cts
forall a. Bag a -> Bag a -> Bag a
`unionBags`
                          Cts
unsolved_fun_eqs Cts -> Cts -> Cts
forall a. Bag a -> Bag a -> Bag a
`unionBags`
                          Cts
unsolved_others) }
  where
    add_if_unsolved :: Ct -> Cts -> Cts
    add_if_unsolved :: Ct -> Cts -> Cts
add_if_unsolved Ct
ct Cts
cts | Ct -> Bool
is_unsolved Ct
ct = Ct
ct Ct -> Cts -> Cts
`consCts` Cts
cts
                           | Bool
otherwise      = Cts
cts

    add_if_unsolveds :: EqualCtList -> Cts -> Cts
    add_if_unsolveds :: EqualCtList -> Cts -> Cts
add_if_unsolveds EqualCtList
new_cts Cts
old_cts = (Ct -> Cts -> Cts) -> Cts -> [Ct] -> Cts
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> Cts -> Cts
add_if_unsolved Cts
old_cts
                                             (EqualCtList -> [Ct]
equalCtListToList EqualCtList
new_cts)

    is_unsolved :: Ct -> Bool
is_unsolved Ct
ct = Bool -> Bool
not (Ct -> Bool
isGivenCt Ct
ct)   -- Wanted or Derived

getHasGivenEqs :: TcLevel           -- TcLevel of this implication
               -> TcS ( HasGivenEqs -- are there Given equalities?
                      , Cts )       -- Insoluble equalities arising from givens
-- See Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
getHasGivenEqs :: TcLevel -> TcS (HasGivenEqs, Cts)
getHasGivenEqs TcLevel
tclvl
  = do { inerts :: InertCans
inerts@(IC { inert_irreds :: InertCans -> Cts
inert_irreds       = Cts
irreds
                    , inert_given_eqs :: InertCans -> Bool
inert_given_eqs    = Bool
given_eqs
                    , inert_given_eq_lvl :: InertCans -> TcLevel
inert_given_eq_lvl = TcLevel
ge_lvl })
              <- TcS InertCans
getInertCans
       ; let insols :: Cts
insols = (Ct -> Bool) -> Cts -> Cts
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Ct -> Bool
insolubleEqCt Cts
irreds
                      -- Specifically includes ones that originated in some
                      -- outer context but were refined to an insoluble by
                      -- a local equality; so do /not/ add ct_given_here.

             -- See Note [HasGivenEqs] in GHC.Tc.Types.Constraint, and
             -- Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
             has_ge :: HasGivenEqs
has_ge | TcLevel
ge_lvl TcLevel -> TcLevel -> Bool
forall a. Eq a => a -> a -> Bool
== TcLevel
tclvl = HasGivenEqs
MaybeGivenEqs
                    | Bool
given_eqs       = HasGivenEqs
LocalGivenEqs
                    | Bool
otherwise       = HasGivenEqs
NoGivenEqs

       ; String -> SDoc -> TcS ()
traceTcS String
"getHasGivenEqs" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"given_eqs:" SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
given_eqs
              , String -> SDoc
text String
"ge_lvl:" SDoc -> SDoc -> SDoc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
ge_lvl
              , String -> SDoc
text String
"ambient level:" SDoc -> SDoc -> SDoc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl
              , String -> SDoc
text String
"Inerts:" SDoc -> SDoc -> SDoc
<+> InertCans -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertCans
inerts
              , String -> SDoc
text String
"Insols:" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
insols]
       ; (HasGivenEqs, Cts) -> TcS (HasGivenEqs, Cts)
forall (m :: * -> *) a. Monad m => a -> m a
return (HasGivenEqs
has_ge, Cts
insols) }

{- Note [Unsolved Derived equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In getUnsolvedInerts, we return a derived equality from the inert_eqs
because it is a candidate for floating out of this implication.  We
only float equalities with a meta-tyvar on the left, so we only pull
those out here.

Note [What might equal later?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We must determine whether a Given might later equal a Wanted. We
definitely need to account for the possibility that any metavariable
might be arbitrarily instantiated. Yet we do *not* want
to allow skolems in to be instantiated, as we've already rewritten
with respect to any Givens. (We're solving a Wanted here, and so
all Givens have already been processed.)

This is best understood by example.

1. C alpha  ~?  C Int

   That given certainly might match later.

2. C a  ~?  C Int

   No. No new givens are going to arise that will get the `a` to rewrite
   to Int.

3. C alpha[tv]   ~?  C Int

   That alpha[tv] is a TyVarTv, unifiable only with other type variables.
   It cannot equal later.

4. C (F alpha)   ~?   C Int

   Sure -- that can equal later, if we learn something useful about alpha.

5. C (F alpha[tv])  ~?  C Int

   This, too, might equal later. Perhaps we have [G] F b ~ Int elsewhere.
   Or maybe we have C (F alpha[tv] beta[tv]), these unify with each other,
   and F x x = Int. Remember: returning True doesn't commit ourselves to
   anything.

6. C (F a)  ~?  C a

   No, this won't match later. If we could rewrite (F a) or a, we would
   have by now.

7. C (Maybe alpha)  ~?  C alpha

   We say this cannot equal later, because it would require
   alpha := Maybe (Maybe (Maybe ...)). While such a type can be contrived,
   we choose not to worry about it. See Note [Infinitary substitution in lookup]
   in GHC.Core.InstEnv. Getting this wrong let to #19107, tested in
   typecheck/should_compile/T19107.

8. C cbv   ~?  C Int
   where cbv = F a

   The cbv is a cycle-breaker var which stands for F a. See
   Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical.
   This is just like case 6, and we say "no". Saying "no" here is
   essential in getting the parser to type-check, with its use of DisambECP.

9. C cbv   ~?   C Int
   where cbv = F alpha

   Here, we might indeed equal later. Distinguishing between
   this case and Example 8 is why we need the InertSet in mightEqualLater.

10. C (F alpha, Int)  ~?  C (Bool, F alpha)

   This cannot equal later, because F a would have to equal both Bool and
   Int.

To deal with type family applications, we use the Core flattener. See
Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.
The Core flattener replaces all type family applications with
fresh variables. The next question: should we allow these fresh
variables in the domain of a unifying substitution?

A type family application that mentions only skolems (example 6) is settled:
any skolems would have been rewritten w.r.t. Givens by now. These type family
applications match only themselves. A type family application that mentions
metavariables, on the other hand, can match anything. So, if the original type
family application contains a metavariable, we use BindMe to tell the unifier
to allow it in the substitution. On the other hand, a type family application
with only skolems is considered rigid.

This treatment fixes #18910 and is tested in
typecheck/should_compile/InstanceGivenOverlap{,2}
-}

removeInertCts :: [Ct] -> InertCans -> InertCans
-- ^ Remove inert constraints from the 'InertCans', for use when a
-- typechecker plugin wishes to discard a given.
removeInertCts :: [Ct] -> InertCans -> InertCans
removeInertCts [Ct]
cts InertCans
icans = (InertCans -> Ct -> InertCans) -> InertCans -> [Ct] -> InertCans
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' InertCans -> Ct -> InertCans
removeInertCt InertCans
icans [Ct]
cts

removeInertCt :: InertCans -> Ct -> InertCans
removeInertCt :: InertCans -> Ct -> InertCans
removeInertCt InertCans
is Ct
ct =
  case Ct
ct of

    CDictCan  { cc_class :: Ct -> Class
cc_class = Class
cl, cc_tyargs :: Ct -> [TcPredType]
cc_tyargs = [TcPredType]
tys } ->
      InertCans
is { inert_dicts :: DictMap Ct
inert_dicts = DictMap Ct -> Class -> [TcPredType] -> DictMap Ct
forall a. DictMap a -> Class -> [TcPredType] -> DictMap a
delDict (InertCans -> DictMap Ct
inert_dicts InertCans
is) Class
cl [TcPredType]
tys }

    CEqCan    { cc_lhs :: Ct -> CanEqLHS
cc_lhs  = CanEqLHS
lhs, cc_rhs :: Ct -> TcPredType
cc_rhs = TcPredType
rhs } -> InertCans -> CanEqLHS -> TcPredType -> InertCans
delEq InertCans
is CanEqLHS
lhs TcPredType
rhs

    CQuantCan {}     -> String -> InertCans
forall a. String -> a
panic String
"removeInertCt: CQuantCan"
    CIrredCan {}     -> String -> InertCans
forall a. String -> a
panic String
"removeInertCt: CIrredEvCan"
    CNonCanonical {} -> String -> InertCans
forall a. String -> a
panic String
"removeInertCt: CNonCanonical"

-- | Looks up a family application in the inerts; returned coercion
-- is oriented input ~ output
lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavourRole))
lookupFamAppInert :: TyCon
-> [TcPredType]
-> TcS (Maybe (Coercion, TcPredType, CtFlavourRole))
lookupFamAppInert TyCon
fam_tc [TcPredType]
tys
  = do { IS { inert_cans :: InertSet -> InertCans
inert_cans = IC { inert_funeqs :: InertCans -> FunEqMap EqualCtList
inert_funeqs = FunEqMap EqualCtList
inert_funeqs } } <- TcS InertSet
getTcSInerts
       ; Maybe (Coercion, TcPredType, CtFlavourRole)
-> TcS (Maybe (Coercion, TcPredType, CtFlavourRole))
forall (m :: * -> *) a. Monad m => a -> m a
return (FunEqMap EqualCtList -> Maybe (Coercion, TcPredType, CtFlavourRole)
lookup_inerts FunEqMap EqualCtList
inert_funeqs) }
  where
    lookup_inerts :: FunEqMap EqualCtList -> Maybe (Coercion, TcPredType, CtFlavourRole)
lookup_inerts FunEqMap EqualCtList
inert_funeqs
      | Just (EqualCtList (CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ctev, cc_rhs :: Ct -> TcPredType
cc_rhs = TcPredType
rhs } :| [Ct]
_))
          <- FunEqMap EqualCtList -> TyCon -> [TcPredType] -> Maybe EqualCtList
forall a. FunEqMap a -> TyCon -> [TcPredType] -> Maybe a
findFunEq FunEqMap EqualCtList
inert_funeqs TyCon
fam_tc [TcPredType]
tys
      = (Coercion, TcPredType, CtFlavourRole)
-> Maybe (Coercion, TcPredType, CtFlavourRole)
forall a. a -> Maybe a
Just (HasDebugCallStack => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion CtEvidence
ctev, TcPredType
rhs, CtEvidence -> CtFlavourRole
ctEvFlavourRole CtEvidence
ctev)
      | Bool
otherwise = Maybe (Coercion, TcPredType, CtFlavourRole)
forall a. Maybe a
Nothing

lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
-- Is this exact predicate type cached in the solved or canonicals of the InertSet?
lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
lookupInInerts CtLoc
loc TcPredType
pty
  | ClassPred Class
cls [TcPredType]
tys <- TcPredType -> Pred
classifyPredType TcPredType
pty
  = do { InertSet
inerts <- TcS InertSet
getTcSInerts
       ; Maybe CtEvidence -> TcS (Maybe CtEvidence)
forall (m :: * -> *) a. Monad m => a -> m a
return (InertSet -> CtLoc -> Class -> [TcPredType] -> Maybe CtEvidence
lookupSolvedDict InertSet
inerts CtLoc
loc Class
cls [TcPredType]
tys Maybe CtEvidence -> Maybe CtEvidence -> Maybe CtEvidence
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
                 (Ct -> CtEvidence) -> Maybe Ct -> Maybe CtEvidence
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Ct -> CtEvidence
ctEvidence (InertCans -> CtLoc -> Class -> [TcPredType] -> Maybe Ct
lookupInertDict (InertSet -> InertCans
inert_cans InertSet
inerts) CtLoc
loc Class
cls [TcPredType]
tys)) }
  | Bool
otherwise -- NB: No caching for equalities, IPs, holes, or errors
  = Maybe CtEvidence -> TcS (Maybe CtEvidence)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe CtEvidence
forall a. Maybe a
Nothing

-- | Look up a dictionary inert.
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe Ct
lookupInertDict :: InertCans -> CtLoc -> Class -> [TcPredType] -> Maybe Ct
lookupInertDict (IC { inert_dicts :: InertCans -> DictMap Ct
inert_dicts = DictMap Ct
dicts }) CtLoc
loc Class
cls [TcPredType]
tys
  = case DictMap Ct -> CtLoc -> Class -> [TcPredType] -> Maybe Ct
forall a. DictMap a -> CtLoc -> Class -> [TcPredType] -> Maybe a
findDict DictMap Ct
dicts CtLoc
loc Class
cls [TcPredType]
tys of
      Just Ct
ct -> Ct -> Maybe Ct
forall a. a -> Maybe a
Just Ct
ct
      Maybe Ct
_       -> Maybe Ct
forall a. Maybe a
Nothing

-- | Look up a solved inert.
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
-- Returns just if exactly this predicate type exists in the solved.
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [TcPredType] -> Maybe CtEvidence
lookupSolvedDict (IS { inert_solved_dicts :: InertSet -> DictMap CtEvidence
inert_solved_dicts = DictMap CtEvidence
solved }) CtLoc
loc Class
cls [TcPredType]
tys
  = case DictMap CtEvidence
-> CtLoc -> Class -> [TcPredType] -> Maybe CtEvidence
forall a. DictMap a -> CtLoc -> Class -> [TcPredType] -> Maybe a
findDict DictMap CtEvidence
solved CtLoc
loc Class
cls [TcPredType]
tys of
      Just CtEvidence
ev -> CtEvidence -> Maybe CtEvidence
forall a. a -> Maybe a
Just CtEvidence
ev
      Maybe CtEvidence
_       -> Maybe CtEvidence
forall a. Maybe a
Nothing

---------------------------
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
lookupFamAppCache :: TyCon -> [TcPredType] -> TcS (Maybe (Coercion, TcPredType))
lookupFamAppCache TyCon
fam_tc [TcPredType]
tys
  = do { IS { inert_famapp_cache :: InertSet -> FunEqMap (Coercion, TcPredType)
inert_famapp_cache = FunEqMap (Coercion, TcPredType)
famapp_cache } <- TcS InertSet
getTcSInerts
       ; case FunEqMap (Coercion, TcPredType)
-> TyCon -> [TcPredType] -> Maybe (Coercion, TcPredType)
forall a. FunEqMap a -> TyCon -> [TcPredType] -> Maybe a
findFunEq FunEqMap (Coercion, TcPredType)
famapp_cache TyCon
fam_tc [TcPredType]
tys of
           result :: Maybe (Coercion, TcPredType)
result@(Just (Coercion
co, TcPredType
ty)) ->
             do { String -> SDoc -> TcS ()
traceTcS String
"famapp_cache hit" ([SDoc] -> SDoc
vcat [ TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> [TcPredType] -> TcPredType
mkTyConApp TyCon
fam_tc [TcPredType]
tys)
                                                    , TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
ty
                                                    , Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co ])
                ; Maybe (Coercion, TcPredType) -> TcS (Maybe (Coercion, TcPredType))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Coercion, TcPredType)
result }
           Maybe (Coercion, TcPredType)
Nothing -> Maybe (Coercion, TcPredType) -> TcS (Maybe (Coercion, TcPredType))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Coercion, TcPredType)
forall a. Maybe a
Nothing }

extendFamAppCache :: TyCon -> [Type] -> (TcCoercion, TcType) -> TcS ()
-- NB: co :: rhs ~ F tys, to match expectations of rewriter
extendFamAppCache :: TyCon -> [TcPredType] -> (Coercion, TcPredType) -> TcS ()
extendFamAppCache TyCon
tc [TcPredType]
xi_args stuff :: (Coercion, TcPredType)
stuff@(Coercion
_, TcPredType
ty)
  = do { DynFlags
dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_FamAppCache DynFlags
dflags) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
    do { String -> SDoc -> TcS ()
traceTcS String
"extendFamAppCache" ([SDoc] -> SDoc
vcat [ TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
<+> [TcPredType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcPredType]
xi_args
                                            , TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
ty ])
            -- 'co' can be bottom, in the case of derived items
       ; (InertSet -> InertSet) -> TcS ()
updInertTcS ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ is :: InertSet
is@(IS { inert_famapp_cache :: InertSet -> FunEqMap (Coercion, TcPredType)
inert_famapp_cache = FunEqMap (Coercion, TcPredType)
fc }) ->
            InertSet
is { inert_famapp_cache :: FunEqMap (Coercion, TcPredType)
inert_famapp_cache = FunEqMap (Coercion, TcPredType)
-> TyCon
-> [TcPredType]
-> (Coercion, TcPredType)
-> FunEqMap (Coercion, TcPredType)
forall a. FunEqMap a -> TyCon -> [TcPredType] -> a -> FunEqMap a
insertFunEq FunEqMap (Coercion, TcPredType)
fc TyCon
tc [TcPredType]
xi_args (Coercion, TcPredType)
stuff } } }

-- Remove entries from the cache whose evidence mentions variables in the
-- supplied set
dropFromFamAppCache :: VarSet -> TcS ()
dropFromFamAppCache :: VarSet -> TcS ()
dropFromFamAppCache VarSet
varset
  = do { inerts :: InertSet
inerts@(IS { inert_famapp_cache :: InertSet -> FunEqMap (Coercion, TcPredType)
inert_famapp_cache = FunEqMap (Coercion, TcPredType)
famapp_cache }) <- TcS InertSet
getTcSInerts
       ; let filtered :: FunEqMap (Coercion, TcPredType)
filtered = ((Coercion, TcPredType) -> Bool)
-> FunEqMap (Coercion, TcPredType)
-> FunEqMap (Coercion, TcPredType)
forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
filterTcAppMap (Coercion, TcPredType) -> Bool
check FunEqMap (Coercion, TcPredType)
famapp_cache
       ; InertSet -> TcS ()
setTcSInerts (InertSet -> TcS ()) -> InertSet -> TcS ()
forall a b. (a -> b) -> a -> b
$ InertSet
inerts { inert_famapp_cache :: FunEqMap (Coercion, TcPredType)
inert_famapp_cache = FunEqMap (Coercion, TcPredType)
filtered } }
  where
    check :: (TcCoercion, TcType) -> Bool
    check :: (Coercion, TcPredType) -> Bool
check (Coercion
co, TcPredType
_) = Bool -> Bool
not ((TcTyVar -> Bool) -> Coercion -> Bool
anyFreeVarsOfCo (TcTyVar -> VarSet -> Bool
`elemVarSet` VarSet
varset) Coercion
co)

{- *********************************************************************
*                                                                      *
                   Irreds
*                                                                      *
********************************************************************* -}

foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b
foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b
foldIrreds Ct -> b -> b
k Cts
irreds b
z = (Ct -> b -> b) -> b -> Cts -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> b -> b
k b
z Cts
irreds

{-
************************************************************************
*                                                                      *
*              The TcS solver monad                                    *
*                                                                      *
************************************************************************

Note [The TcS monad]
~~~~~~~~~~~~~~~~~~~~
The TcS monad is a weak form of the main Tc monad

All you can do is
    * fail
    * allocate new variables
    * fill in evidence variables

Filling in a dictionary evidence variable means to create a binding
for it, so TcS carries a mutable location where the binding can be
added.  This is initialised from the innermost implication constraint.
-}

data TcSEnv
  = TcSEnv {
      TcSEnv -> EvBindsVar
tcs_ev_binds    :: EvBindsVar,

      TcSEnv -> IORef Int
tcs_unified     :: IORef Int,
         -- The number of unification variables we have filled
         -- The important thing is whether it is non-zero

      TcSEnv -> IORef (Maybe TcLevel)
tcs_unif_lvl  :: IORef (Maybe TcLevel),
         -- The Unification Level Flag
         -- Outermost level at which we have unified a meta tyvar
         -- Starts at Nothing, then (Just i), then (Just j) where j<i
         -- See Note [The Unification Level Flag]

      TcSEnv -> IORef Int
tcs_count     :: IORef Int, -- Global step count

      TcSEnv -> IORef InertSet
tcs_inerts    :: IORef InertSet, -- Current inert set

      -- See Note [WorkList priorities] in GHC.Tc.Solver.InertSet
      TcSEnv -> IORef WorkList
tcs_worklist  :: IORef WorkList -- Current worklist
    }

---------------
newtype TcS a = TcS { TcS a -> TcSEnv -> TcM a
unTcS :: TcSEnv -> TcM a } deriving (a -> TcS b -> TcS a
(a -> b) -> TcS a -> TcS b
(forall a b. (a -> b) -> TcS a -> TcS b)
-> (forall a b. a -> TcS b -> TcS a) -> Functor TcS
forall a b. a -> TcS b -> TcS a
forall a b. (a -> b) -> TcS a -> TcS b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> TcS b -> TcS a
$c<$ :: forall a b. a -> TcS b -> TcS a
fmap :: (a -> b) -> TcS a -> TcS b
$cfmap :: forall a b. (a -> b) -> TcS a -> TcS b
Functor)

-- | Smart constructor for 'TcS', as describe in Note [The one-shot state
-- monad trick] in "GHC.Utils.Monad".
mkTcS :: (TcSEnv -> TcM a) -> TcS a
mkTcS :: (TcSEnv -> TcM a) -> TcS a
mkTcS TcSEnv -> TcM a
f = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM a) -> TcSEnv -> TcM a
oneShot TcSEnv -> TcM a
f)

instance Applicative TcS where
  pure :: a -> TcS a
pure a
x = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \TcSEnv
_ -> a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
  <*> :: TcS (a -> b) -> TcS a -> TcS b
(<*>) = TcS (a -> b) -> TcS a -> TcS b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad TcS where
  TcS a
m >>= :: TcS a -> (a -> TcS b) -> TcS b
>>= a -> TcS b
k   = (TcSEnv -> TcM b) -> TcS b
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS ((TcSEnv -> TcM b) -> TcS b) -> (TcSEnv -> TcM b) -> TcS b
forall a b. (a -> b) -> a -> b
$ \TcSEnv
ebs -> do
    TcS a -> TcSEnv -> TcM a
forall a. TcS a -> TcSEnv -> TcM a
unTcS TcS a
m TcSEnv
ebs TcM a -> (a -> TcM b) -> TcM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\a
r -> TcS b -> TcSEnv -> TcM b
forall a. TcS a -> TcSEnv -> TcM a
unTcS (a -> TcS b
k a
r) TcSEnv
ebs)

instance MonadFail TcS where
  fail :: String -> TcS a
fail String
err  = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \TcSEnv
_ -> String -> TcM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err

instance MonadUnique TcS where
   getUniqueSupplyM :: TcS UniqSupply
getUniqueSupplyM = TcM UniqSupply -> TcS UniqSupply
forall a. TcM a -> TcS a
wrapTcS TcM UniqSupply
forall (m :: * -> *). MonadUnique m => m UniqSupply
getUniqueSupplyM

instance HasModule TcS where
   getModule :: TcS Module
getModule = TcM Module -> TcS Module
forall a. TcM a -> TcS a
wrapTcS TcM Module
forall (m :: * -> *). HasModule m => m Module
getModule

instance MonadThings TcS where
   lookupThing :: Name -> TcS TyThing
lookupThing Name
n = TcM TyThing -> TcS TyThing
forall a. TcM a -> TcS a
wrapTcS (Name -> TcM TyThing
forall (m :: * -> *). MonadThings m => Name -> m TyThing
lookupThing Name
n)

-- Basic functionality
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
wrapTcS :: TcM a -> TcS a
-- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
-- and TcS is supposed to have limited functionality
wrapTcS :: TcM a -> TcS a
wrapTcS TcM a
action = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \TcSEnv
_env -> TcM a
action -- a TcM action will not use the TcEvBinds

wrapErrTcS :: TcM a -> TcS a
-- The thing wrapped should just fail
-- There's no static check; it's up to the user
-- Having a variant for each error message is too painful
wrapErrTcS :: TcM a -> TcS a
wrapErrTcS = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS

wrapWarnTcS :: TcM a -> TcS a
-- The thing wrapped should just add a warning, or no-op
-- There's no static check; it's up to the user
wrapWarnTcS :: TcM a -> TcS a
wrapWarnTcS = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS

failTcS, panicTcS  :: SDoc -> TcS a
warnTcS   :: WarningFlag -> SDoc -> TcS ()
addErrTcS :: SDoc -> TcS ()
failTcS :: SDoc -> TcS a
failTcS      = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS (TcM a -> TcS a) -> (SDoc -> TcM a) -> SDoc -> TcS a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> TcM a
forall a. SDoc -> TcRn a
TcM.failWith
warnTcS :: WarningFlag -> SDoc -> TcS ()
warnTcS WarningFlag
flag = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> (SDoc -> TcM ()) -> SDoc -> TcS ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DiagnosticReason -> SDoc -> TcM ()
TcM.addDiagnostic (WarningFlag -> DiagnosticReason
WarningWithFlag WarningFlag
flag)
addErrTcS :: SDoc -> TcS ()
addErrTcS    = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> (SDoc -> TcM ()) -> SDoc -> TcS ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> TcM ()
TcM.addErr
panicTcS :: SDoc -> TcS a
panicTcS SDoc
doc = String -> SDoc -> TcS a
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"GHC.Tc.Solver.Canonical" SDoc
doc

traceTcS :: String -> SDoc -> TcS ()
traceTcS :: String -> SDoc -> TcS ()
traceTcS String
herald SDoc
doc = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (String -> SDoc -> TcM ()
TcM.traceTc String
herald SDoc
doc)
{-# INLINE traceTcS #-}  -- see Note [INLINE conditional tracing utilities]

runTcPluginTcS :: TcPluginM a -> TcS a
runTcPluginTcS :: TcPluginM a -> TcS a
runTcPluginTcS TcPluginM a
m = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS (TcM a -> TcS a) -> (EvBindsVar -> TcM a) -> EvBindsVar -> TcS a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPluginM a -> EvBindsVar -> TcM a
forall a. TcPluginM a -> EvBindsVar -> TcM a
runTcPluginM TcPluginM a
m (EvBindsVar -> TcS a) -> TcS EvBindsVar -> TcS a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TcS EvBindsVar
getTcEvBindsVar

instance HasDynFlags TcS where
    getDynFlags :: TcS DynFlags
getDynFlags = TcM DynFlags -> TcS DynFlags
forall a. TcM a -> TcS a
wrapTcS TcM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags

getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
getGlobalRdrEnvTcS = TcM GlobalRdrEnv -> TcS GlobalRdrEnv
forall a. TcM a -> TcS a
wrapTcS TcM GlobalRdrEnv
TcM.getGlobalRdrEnv

bumpStepCountTcS :: TcS ()
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = (TcSEnv -> TcM ()) -> TcS ()
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS ((TcSEnv -> TcM ()) -> TcS ()) -> (TcSEnv -> TcM ()) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \TcSEnv
env ->
  do { let ref :: IORef Int
ref = TcSEnv -> IORef Int
tcs_count TcSEnv
env
     ; Int
n <- IORef Int -> TcRnIf TcGblEnv TcLclEnv Int
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef Int
ref
     ; IORef Int -> Int -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef Int
ref (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) }

csTraceTcS :: SDoc -> TcS ()
csTraceTcS :: SDoc -> TcS ()
csTraceTcS SDoc
doc
  = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ TcM SDoc -> TcM ()
csTraceTcM (SDoc -> TcM SDoc
forall (m :: * -> *) a. Monad m => a -> m a
return SDoc
doc)
{-# INLINE csTraceTcS #-}  -- see Note [INLINE conditional tracing utilities]

traceFireTcS :: CtEvidence -> SDoc -> TcS ()
-- Dump a rule-firing trace
traceFireTcS :: CtEvidence -> SDoc -> TcS ()
traceFireTcS CtEvidence
ev SDoc
doc
  = (TcSEnv -> TcM ()) -> TcS ()
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS ((TcSEnv -> TcM ()) -> TcS ()) -> (TcSEnv -> TcM ()) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \TcSEnv
env -> TcM SDoc -> TcM ()
csTraceTcM (TcM SDoc -> TcM ()) -> TcM SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
    do { Int
n <- IORef Int -> TcRnIf TcGblEnv TcLclEnv Int
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef (TcSEnv -> IORef Int
tcs_count TcSEnv
env)
       ; TcLevel
tclvl <- TcM TcLevel
TcM.getTcLevel
       ; SDoc -> TcM SDoc
forall (m :: * -> *) a. Monad m => a -> m a
return (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Step" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
n
                       SDoc -> SDoc -> SDoc
<> SDoc -> SDoc
brackets (String -> SDoc
text String
"l:" SDoc -> SDoc -> SDoc
<> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl SDoc -> SDoc -> SDoc
<> SDoc
comma SDoc -> SDoc -> SDoc
<>
                                    String -> SDoc
text String
"d:" SDoc -> SDoc -> SDoc
<> SubGoalDepth -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> SubGoalDepth
ctLocDepth (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev)))
                       SDoc -> SDoc -> SDoc
<+> SDoc
doc SDoc -> SDoc -> SDoc
<> SDoc
colon)
                     Int
4 (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev)) }
{-# INLINE traceFireTcS #-}  -- see Note [INLINE conditional tracing utilities]

csTraceTcM :: TcM SDoc -> TcM ()
-- Constraint-solver tracing, -ddump-cs-trace
csTraceTcM :: TcM SDoc -> TcM ()
csTraceTcM TcM SDoc
mk_doc
  = do { DynFlags
dflags <- TcM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (  DumpFlag -> DynFlags -> Bool
dopt DumpFlag
Opt_D_dump_cs_trace DynFlags
dflags
                  Bool -> Bool -> Bool
|| DumpFlag -> DynFlags -> Bool
dopt DumpFlag
Opt_D_dump_tc_trace DynFlags
dflags )
              ( do { SDoc
msg <- TcM SDoc
mk_doc
                   ; Bool -> DumpFlag -> String -> DumpFormat -> SDoc -> TcM ()
TcM.dumpTcRn Bool
False
                       DumpFlag
Opt_D_dump_cs_trace
                       String
"" DumpFormat
FormatText
                       SDoc
msg }) }
{-# INLINE csTraceTcM #-}  -- see Note [INLINE conditional tracing utilities]

runTcS :: TcS a                -- What to run
       -> TcM (a, EvBindMap)
runTcS :: TcS a -> TcM (a, EvBindMap)
runTcS TcS a
tcs
  = do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
       ; a
res <- EvBindsVar -> TcS a -> TcM a
forall a. EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds EvBindsVar
ev_binds_var TcS a
tcs
       ; EvBindMap
ev_binds <- EvBindsVar -> TcM EvBindMap
TcM.getTcEvBindsMap EvBindsVar
ev_binds_var
       ; (a, EvBindMap) -> TcM (a, EvBindMap)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
res, EvBindMap
ev_binds) }
-- | This variant of 'runTcS' will keep solving, even when only Deriveds
-- are left around. It also doesn't return any evidence, as callers won't
-- need it.
runTcSDeriveds :: TcS a -> TcM a
runTcSDeriveds :: TcS a -> TcM a
runTcSDeriveds TcS a
tcs
  = do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
       ; EvBindsVar -> TcS a -> TcM a
forall a. EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds EvBindsVar
ev_binds_var TcS a
tcs }

-- | This can deal only with equality constraints.
runTcSEqualities :: TcS a -> TcM a
runTcSEqualities :: TcS a -> TcM a
runTcSEqualities TcS a
thing_inside
  = do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newNoTcEvBinds
       ; EvBindsVar -> TcS a -> TcM a
forall a. EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds EvBindsVar
ev_binds_var TcS a
thing_inside }

-- | A variant of 'runTcS' that takes and returns an 'InertSet' for
-- later resumption of the 'TcS' session.
runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet)
runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet)
runTcSInerts InertSet
inerts TcS a
tcs = do
  EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
  Bool -> EvBindsVar -> TcS (a, InertSet) -> TcM (a, InertSet)
forall a. Bool -> EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds' Bool
False EvBindsVar
ev_binds_var (TcS (a, InertSet) -> TcM (a, InertSet))
-> TcS (a, InertSet) -> TcM (a, InertSet)
forall a b. (a -> b) -> a -> b
$ do
    InertSet -> TcS ()
setTcSInerts InertSet
inerts
    a
a <- TcS a
tcs
    InertSet
new_inerts <- TcS InertSet
getTcSInerts
    (a, InertSet) -> TcS (a, InertSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, InertSet
new_inerts)

runTcSWithEvBinds :: EvBindsVar
                  -> TcS a
                  -> TcM a
runTcSWithEvBinds :: EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds = Bool -> EvBindsVar -> TcS a -> TcM a
forall a. Bool -> EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds' Bool
True

runTcSWithEvBinds' :: Bool -- ^ Restore type variable cycles afterwards?
                           -- Don't if you want to reuse the InertSet.
                           -- See also Note [Type variable cycles in Givens]
                           -- in GHC.Tc.Solver.Canonical
                   -> EvBindsVar
                   -> TcS a
                   -> TcM a
runTcSWithEvBinds' :: Bool -> EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds' Bool
restore_cycles EvBindsVar
ev_binds_var TcS a
tcs
  = do { IORef Int
unified_var <- Int -> TcRnIf TcGblEnv TcLclEnv (IORef Int)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef Int
0
       ; IORef Int
step_count <- Int -> TcRnIf TcGblEnv TcLclEnv (IORef Int)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef Int
0
       ; IORef InertSet
inert_var <- InertSet -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef InertSet
emptyInert
       ; IORef WorkList
wl_var <- WorkList -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef WorkList
emptyWorkList
       ; IORef (Maybe TcLevel)
unif_lvl_var <- Maybe TcLevel -> TcRnIf TcGblEnv TcLclEnv (IORef (Maybe TcLevel))
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef Maybe TcLevel
forall a. Maybe a
Nothing
       ; let env :: TcSEnv
env = TcSEnv :: EvBindsVar
-> IORef Int
-> IORef (Maybe TcLevel)
-> IORef Int
-> IORef InertSet
-> IORef WorkList
-> TcSEnv
TcSEnv { tcs_ev_binds :: EvBindsVar
tcs_ev_binds      = EvBindsVar
ev_binds_var
                          , tcs_unified :: IORef Int
tcs_unified       = IORef Int
unified_var
                          , tcs_unif_lvl :: IORef (Maybe TcLevel)
tcs_unif_lvl      = IORef (Maybe TcLevel)
unif_lvl_var
                          , tcs_count :: IORef Int
tcs_count         = IORef Int
step_count
                          , tcs_inerts :: IORef InertSet
tcs_inerts        = IORef InertSet
inert_var
                          , tcs_worklist :: IORef WorkList
tcs_worklist      = IORef WorkList
wl_var }

             -- Run the computation
       ; a
res <- TcS a -> TcSEnv -> TcM a
forall a. TcS a -> TcSEnv -> TcM a
unTcS TcS a
tcs TcSEnv
env

       ; Int
count <- IORef Int -> TcRnIf TcGblEnv TcLclEnv Int
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef Int
step_count
       ; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
count Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
         TcM SDoc -> TcM ()
csTraceTcM (TcM SDoc -> TcM ()) -> TcM SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$ SDoc -> TcM SDoc
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> SDoc
text String
"Constraint solver steps =" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
count)

       ; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
restore_cycles (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
         do { InertSet
inert_set <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
inert_var
            ; InertSet -> TcM ()
restoreTyVarCycles InertSet
inert_set }

#if defined(DEBUG)
       ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
       ; checkForCyclicBinds ev_binds
#endif

       ; a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res }

----------------------------
#if defined(DEBUG)
checkForCyclicBinds :: EvBindMap -> TcM ()
checkForCyclicBinds ev_binds_map
  | null cycles
  = return ()
  | null coercion_cycles
  = TcM.traceTc "Cycle in evidence binds" $ ppr cycles
  | otherwise
  = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
  where
    ev_binds = evBindMapBinds ev_binds_map

    cycles :: [[EvBind]]
    cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges]

    coercion_cycles = [c | c <- cycles, any is_co_bind c]
    is_co_bind (EvBind { eb_lhs = b }) = isEqPrimPred (varType b)

    edges :: [ Node EvVar EvBind ]
    edges = [ DigraphNode bind bndr (nonDetEltsUniqSet (evVarsOfTerm rhs))
            | bind@(EvBind { eb_lhs = bndr, eb_rhs = rhs}) <- bagToList ev_binds ]
            -- It's OK to use nonDetEltsUFM here as
            -- stronglyConnCompFromEdgedVertices is still deterministic even
            -- if the edges are in nondeterministic order as explained in
            -- Note [Deterministic SCC] in GHC.Data.Graph.Directed.
#endif

----------------------------
setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
setEvBindsTcS EvBindsVar
ref (TcS TcSEnv -> TcM a
thing_inside)
 = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \ TcSEnv
env -> TcSEnv -> TcM a
thing_inside (TcSEnv
env { tcs_ev_binds :: EvBindsVar
tcs_ev_binds = EvBindsVar
ref })

nestImplicTcS :: EvBindsVar
              -> TcLevel -> TcS a
              -> TcS a
nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a -> TcS a
nestImplicTcS EvBindsVar
ref TcLevel
inner_tclvl (TcS TcSEnv -> TcM a
thing_inside)
  = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \ TcSEnv { tcs_unified :: TcSEnv -> IORef Int
tcs_unified       = IORef Int
unified_var
                   , tcs_inerts :: TcSEnv -> IORef InertSet
tcs_inerts        = IORef InertSet
old_inert_var
                   , tcs_count :: TcSEnv -> IORef Int
tcs_count         = IORef Int
count
                   , tcs_unif_lvl :: TcSEnv -> IORef (Maybe TcLevel)
tcs_unif_lvl      = IORef (Maybe TcLevel)
unif_lvl
                   } ->
    do { InertSet
inerts <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
old_inert_var
       ; let nest_inert :: InertSet
nest_inert = InertSet
inerts { inert_cycle_breakers :: [(TcTyVar, TcPredType)]
inert_cycle_breakers = []
                                 , inert_cans :: InertCans
inert_cans = (InertSet -> InertCans
inert_cans InertSet
inerts)
                                                   { inert_given_eqs :: Bool
inert_given_eqs = Bool
False } }
                 -- All other InertSet fields are inherited
       ; IORef InertSet
new_inert_var <- InertSet -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef InertSet
nest_inert
       ; IORef WorkList
new_wl_var    <- WorkList -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef WorkList
emptyWorkList
       ; let nest_env :: TcSEnv
nest_env = TcSEnv :: EvBindsVar
-> IORef Int
-> IORef (Maybe TcLevel)
-> IORef Int
-> IORef InertSet
-> IORef WorkList
-> TcSEnv
TcSEnv { tcs_count :: IORef Int
tcs_count         = IORef Int
count     -- Inherited
                               , tcs_unif_lvl :: IORef (Maybe TcLevel)
tcs_unif_lvl      = IORef (Maybe TcLevel)
unif_lvl  -- Inherited
                               , tcs_ev_binds :: EvBindsVar
tcs_ev_binds      = EvBindsVar
ref
                               , tcs_unified :: IORef Int
tcs_unified       = IORef Int
unified_var
                               , tcs_inerts :: IORef InertSet
tcs_inerts        = IORef InertSet
new_inert_var
                               , tcs_worklist :: IORef WorkList
tcs_worklist      = IORef WorkList
new_wl_var }
       ; a
res <- TcLevel -> TcM a -> TcM a
forall a. TcLevel -> TcM a -> TcM a
TcM.setTcLevel TcLevel
inner_tclvl (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
                TcSEnv -> TcM a
thing_inside TcSEnv
nest_env

       ; InertSet
out_inert_set <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
new_inert_var
       ; InertSet -> TcM ()
restoreTyVarCycles InertSet
out_inert_set

#if defined(DEBUG)
       -- Perform a check that the thing_inside did not cause cycles
       ; ev_binds <- TcM.getTcEvBindsMap ref
       ; checkForCyclicBinds ev_binds
#endif
       ; a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res }

nestTcS ::  TcS a -> TcS a
-- Use the current untouchables, augmenting the current
-- evidence bindings, and solved dictionaries
-- But have no effect on the InertCans, or on the inert_famapp_cache
-- (we want to inherit the latter from processing the Givens)
nestTcS :: TcS a -> TcS a
nestTcS (TcS TcSEnv -> TcM a
thing_inside)
  = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \ env :: TcSEnv
env@(TcSEnv { tcs_inerts :: TcSEnv -> IORef InertSet
tcs_inerts = IORef InertSet
inerts_var }) ->
    do { InertSet
inerts <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
inerts_var
       ; IORef InertSet
new_inert_var <- InertSet -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef InertSet
inerts
       ; IORef WorkList
new_wl_var    <- WorkList -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef WorkList
emptyWorkList
       ; let nest_env :: TcSEnv
nest_env = TcSEnv
env { tcs_inerts :: IORef InertSet
tcs_inerts   = IORef InertSet
new_inert_var
                            , tcs_worklist :: IORef WorkList
tcs_worklist = IORef WorkList
new_wl_var }

       ; a
res <- TcSEnv -> TcM a
thing_inside TcSEnv
nest_env

       ; InertSet
new_inerts <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
new_inert_var

       -- we want to propagate the safe haskell failures
       ; let old_ic :: InertCans
old_ic = InertSet -> InertCans
inert_cans InertSet
inerts
             new_ic :: InertCans
new_ic = InertSet -> InertCans
inert_cans InertSet
new_inerts
             nxt_ic :: InertCans
nxt_ic = InertCans
old_ic { inert_safehask :: DictMap Ct
inert_safehask = InertCans -> DictMap Ct
inert_safehask InertCans
new_ic }

       ; IORef InertSet -> InertSet -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef InertSet
inerts_var  -- See Note [Propagate the solved dictionaries]
                        (InertSet
inerts { inert_solved_dicts :: DictMap CtEvidence
inert_solved_dicts = InertSet -> DictMap CtEvidence
inert_solved_dicts InertSet
new_inerts
                                , inert_cans :: InertCans
inert_cans = InertCans
nxt_ic })

       ; a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res }

emitImplicationTcS :: TcLevel -> SkolemInfo
                   -> [TcTyVar]        -- Skolems
                   -> [EvVar]          -- Givens
                   -> Cts              -- Wanteds
                   -> TcS TcEvBinds
-- Add an implication to the TcS monad work-list
emitImplicationTcS :: TcLevel
-> SkolemInfo -> [TcTyVar] -> [TcTyVar] -> Cts -> TcS TcEvBinds
emitImplicationTcS TcLevel
new_tclvl SkolemInfo
skol_info [TcTyVar]
skol_tvs [TcTyVar]
givens Cts
wanteds
  = do { let wc :: WantedConstraints
wc = WantedConstraints
emptyWC { wc_simple :: Cts
wc_simple = Cts
wanteds }
       ; Implication
imp <- TcM Implication -> TcS Implication
forall a. TcM a -> TcS a
wrapTcS (TcM Implication -> TcS Implication)
-> TcM Implication -> TcS Implication
forall a b. (a -> b) -> a -> b
$
                do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
                   ; Implication
imp <- TcM Implication
TcM.newImplication
                   ; Implication -> TcM Implication
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication
imp { ic_tclvl :: TcLevel
ic_tclvl  = TcLevel
new_tclvl
                                 , ic_skols :: [TcTyVar]
ic_skols  = [TcTyVar]
skol_tvs
                                 , ic_given :: [TcTyVar]
ic_given  = [TcTyVar]
givens
                                 , ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
wc
                                 , ic_binds :: EvBindsVar
ic_binds  = EvBindsVar
ev_binds_var
                                 , ic_info :: SkolemInfo
ic_info   = SkolemInfo
skol_info }) }

       ; Implication -> TcS ()
emitImplication Implication
imp
       ; TcEvBinds -> TcS TcEvBinds
forall (m :: * -> *) a. Monad m => a -> m a
return (EvBindsVar -> TcEvBinds
TcEvBinds (Implication -> EvBindsVar
ic_binds Implication
imp)) }

emitTvImplicationTcS :: TcLevel -> SkolemInfo
                     -> [TcTyVar]        -- Skolems
                     -> Cts              -- Wanteds
                     -> TcS ()
-- Just like emitImplicationTcS but no givens and no bindings
emitTvImplicationTcS :: TcLevel -> SkolemInfo -> [TcTyVar] -> Cts -> TcS ()
emitTvImplicationTcS TcLevel
new_tclvl SkolemInfo
skol_info [TcTyVar]
skol_tvs Cts
wanteds
  = do { let wc :: WantedConstraints
wc = WantedConstraints
emptyWC { wc_simple :: Cts
wc_simple = Cts
wanteds }
       ; Implication
imp <- TcM Implication -> TcS Implication
forall a. TcM a -> TcS a
wrapTcS (TcM Implication -> TcS Implication)
-> TcM Implication -> TcS Implication
forall a b. (a -> b) -> a -> b
$
                do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newNoTcEvBinds
                   ; Implication
imp <- TcM Implication
TcM.newImplication
                   ; Implication -> TcM Implication
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication
imp { ic_tclvl :: TcLevel
ic_tclvl  = TcLevel
new_tclvl
                                 , ic_skols :: [TcTyVar]
ic_skols  = [TcTyVar]
skol_tvs
                                 , ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
wc
                                 , ic_binds :: EvBindsVar
ic_binds  = EvBindsVar
ev_binds_var
                                 , ic_info :: SkolemInfo
ic_info   = SkolemInfo
skol_info }) }

       ; Implication -> TcS ()
emitImplication Implication
imp }


{- Note [Propagate the solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's really quite important that nestTcS does not discard the solved
dictionaries from the thing_inside.
Consider
   Eq [a]
   forall b. empty =>  Eq [a]
We solve the simple (Eq [a]), under nestTcS, and then turn our attention to
the implications.  It's definitely fine to use the solved dictionaries on
the inner implications, and it can make a significant performance difference
if you do so.
-}

-- Getters and setters of GHC.Tc.Utils.Env fields
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-- Getter of inerts and worklist
getTcSInertsRef :: TcS (IORef InertSet)
getTcSInertsRef :: TcS (IORef InertSet)
getTcSInertsRef = (TcSEnv -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet))
-> TcS (IORef InertSet)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (IORef InertSet -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (IORef InertSet -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet))
-> (TcSEnv -> IORef InertSet)
-> TcSEnv
-> TcRnIf TcGblEnv TcLclEnv (IORef InertSet)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> IORef InertSet
tcs_inerts)

getTcSWorkListRef :: TcS (IORef WorkList)
getTcSWorkListRef :: TcS (IORef WorkList)
getTcSWorkListRef = (TcSEnv -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList))
-> TcS (IORef WorkList)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (IORef WorkList -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList)
forall (m :: * -> *) a. Monad m => a -> m a
return (IORef WorkList -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList))
-> (TcSEnv -> IORef WorkList)
-> TcSEnv
-> TcRnIf TcGblEnv TcLclEnv (IORef WorkList)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> IORef WorkList
tcs_worklist)

getTcSInerts :: TcS InertSet
getTcSInerts :: TcS InertSet
getTcSInerts = TcS (IORef InertSet)
getTcSInertsRef TcS (IORef InertSet)
-> (IORef InertSet -> TcS InertSet) -> TcS InertSet
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IORef InertSet -> TcS InertSet
forall a. TcRef a -> TcS a
readTcRef

setTcSInerts :: InertSet -> TcS ()
setTcSInerts :: InertSet -> TcS ()
setTcSInerts InertSet
ics = do { IORef InertSet
r <- TcS (IORef InertSet)
getTcSInertsRef; IORef InertSet -> InertSet -> TcS ()
forall a. TcRef a -> a -> TcS ()
writeTcRef IORef InertSet
r InertSet
ics }

getWorkListImplics :: TcS (Bag Implication)
getWorkListImplics :: TcS (Bag Implication)
getWorkListImplics
  = do { IORef WorkList
wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
       ; WorkList
wl_curr <- IORef WorkList -> TcS WorkList
forall a. TcRef a -> TcS a
readTcRef IORef WorkList
wl_var
       ; Bag Implication -> TcS (Bag Implication)
forall (m :: * -> *) a. Monad m => a -> m a
return (WorkList -> Bag Implication
wl_implics WorkList
wl_curr) }

pushLevelNoWorkList :: SDoc -> TcS a -> TcS (TcLevel, a)
-- Push the level and run thing_inside
-- However, thing_inside should not generate any work items
#if defined(DEBUG)
pushLevelNoWorkList err_doc (TcS thing_inside)
  = TcS (\env -> TcM.pushTcLevelM $
                 thing_inside (env { tcs_worklist = wl_panic })
        )
  where
    wl_panic  = pprPanic "GHC.Tc.Solver.Monad.buildImplication" err_doc
                         -- This panic checks that the thing-inside
                         -- does not emit any work-list constraints
#else
pushLevelNoWorkList :: SDoc -> TcS a -> TcS (TcLevel, a)
pushLevelNoWorkList SDoc
_ (TcS TcSEnv -> TcM a
thing_inside)
  = (TcSEnv -> TcM (TcLevel, a)) -> TcS (TcLevel, a)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (\TcSEnv
env -> TcM a -> TcM (TcLevel, a)
forall a. TcM a -> TcM (TcLevel, a)
TcM.pushTcLevelM (TcSEnv -> TcM a
thing_inside TcSEnv
env))  -- Don't check
#endif

updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
updWorkListTcS WorkList -> WorkList
f
  = do { IORef WorkList
wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
       ; IORef WorkList -> (WorkList -> WorkList) -> TcS ()
forall a. TcRef a -> (a -> a) -> TcS ()
updTcRef IORef WorkList
wl_var WorkList -> WorkList
f }

emitWorkNC :: [CtEvidence] -> TcS ()
emitWorkNC :: [CtEvidence] -> TcS ()
emitWorkNC [CtEvidence]
evs
  | [CtEvidence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CtEvidence]
evs
  = () -> TcS ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = [Ct] -> TcS ()
emitWork ((CtEvidence -> Ct) -> [CtEvidence] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> Ct
mkNonCanonical [CtEvidence]
evs)

emitWork :: [Ct] -> TcS ()
emitWork :: [Ct] -> TcS ()
emitWork [] = () -> TcS ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()   -- avoid printing, among other work
emitWork [Ct]
cts
  = do { String -> SDoc -> TcS ()
traceTcS String
"Emitting fresh work" ([SDoc] -> SDoc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
cts))
       ; (WorkList -> WorkList) -> TcS ()
updWorkListTcS ([Ct] -> WorkList -> WorkList
extendWorkListCts [Ct]
cts) }

emitImplication :: Implication -> TcS ()
emitImplication :: Implication -> TcS ()
emitImplication Implication
implic
  = (WorkList -> WorkList) -> TcS ()
updWorkListTcS (Implication -> WorkList -> WorkList
extendWorkListImplic Implication
implic)

newTcRef :: a -> TcS (TcRef a)
newTcRef :: a -> TcS (TcRef a)
newTcRef a
x = TcM (TcRef a) -> TcS (TcRef a)
forall a. TcM a -> TcS a
wrapTcS (a -> TcM (TcRef a)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef a
x)

readTcRef :: TcRef a -> TcS a
readTcRef :: TcRef a -> TcS a
readTcRef TcRef a
ref = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS (TcRef a -> TcM a
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef TcRef a
ref)

writeTcRef :: TcRef a -> a -> TcS ()
writeTcRef :: TcRef a -> a -> TcS ()
writeTcRef TcRef a
ref a
val = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcRef a -> a -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef TcRef a
ref a
val)

updTcRef :: TcRef a -> (a->a) -> TcS ()
updTcRef :: TcRef a -> (a -> a) -> TcS ()
updTcRef TcRef a
ref a -> a
upd_fn = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcRef a -> (a -> a) -> TcM ()
forall a gbl lcl. TcRef a -> (a -> a) -> TcRnIf gbl lcl ()
TcM.updTcRef TcRef a
ref a -> a
upd_fn)

getTcEvBindsVar :: TcS EvBindsVar
getTcEvBindsVar :: TcS EvBindsVar
getTcEvBindsVar = (TcSEnv -> TcM EvBindsVar) -> TcS EvBindsVar
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (EvBindsVar -> TcM EvBindsVar
forall (m :: * -> *) a. Monad m => a -> m a
return (EvBindsVar -> TcM EvBindsVar)
-> (TcSEnv -> EvBindsVar) -> TcSEnv -> TcM EvBindsVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> EvBindsVar
tcs_ev_binds)

getTcLevel :: TcS TcLevel
getTcLevel :: TcS TcLevel
getTcLevel = TcM TcLevel -> TcS TcLevel
forall a. TcM a -> TcS a
wrapTcS TcM TcLevel
TcM.getTcLevel

getTcEvTyCoVars :: EvBindsVar -> TcS TyCoVarSet
getTcEvTyCoVars :: EvBindsVar -> TcS VarSet
getTcEvTyCoVars EvBindsVar
ev_binds_var
  = TcM VarSet -> TcS VarSet
forall a. TcM a -> TcS a
wrapTcS (TcM VarSet -> TcS VarSet) -> TcM VarSet -> TcS VarSet
forall a b. (a -> b) -> a -> b
$ EvBindsVar -> TcM VarSet
TcM.getTcEvTyCoVars EvBindsVar
ev_binds_var

getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap
getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap
getTcEvBindsMap EvBindsVar
ev_binds_var
  = TcM EvBindMap -> TcS EvBindMap
forall a. TcM a -> TcS a
wrapTcS (TcM EvBindMap -> TcS EvBindMap) -> TcM EvBindMap -> TcS EvBindMap
forall a b. (a -> b) -> a -> b
$ EvBindsVar -> TcM EvBindMap
TcM.getTcEvBindsMap EvBindsVar
ev_binds_var

setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS ()
setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS ()
setTcEvBindsMap EvBindsVar
ev_binds_var EvBindMap
binds
  = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ EvBindsVar -> EvBindMap -> TcM ()
TcM.setTcEvBindsMap EvBindsVar
ev_binds_var EvBindMap
binds

unifyTyVar :: TcTyVar -> TcType -> TcS ()
-- Unify a meta-tyvar with a type
-- We keep track of how many unifications have happened in tcs_unified,
--
-- We should never unify the same variable twice!
unifyTyVar :: TcTyVar -> TcPredType -> TcS ()
unifyTyVar TcTyVar
tv TcPredType
ty
  = Bool -> SDoc -> TcS () -> TcS ()
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcTyVar -> Bool
isMetaTyVar TcTyVar
tv) (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
    (TcSEnv -> TcM ()) -> TcS ()
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM ()) -> TcS ()) -> (TcSEnv -> TcM ()) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ TcSEnv
env ->
    do { String -> SDoc -> TcM ()
TcM.traceTc String
"unifyTyVar" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
":=" SDoc -> SDoc -> SDoc
<+> TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
ty)
       ; TcTyVar -> TcPredType -> TcM ()
TcM.writeMetaTyVar TcTyVar
tv TcPredType
ty
       ; IORef Int -> (Int -> Int) -> TcM ()
forall a gbl lcl. TcRef a -> (a -> a) -> TcRnIf gbl lcl ()
TcM.updTcRef (TcSEnv -> IORef Int
tcs_unified TcSEnv
env) (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) }

reportUnifications :: TcS a -> TcS (Int, a)
reportUnifications :: TcS a -> TcS (Int, a)
reportUnifications (TcS TcSEnv -> TcM a
thing_inside)
  = (TcSEnv -> TcM (Int, a)) -> TcS (Int, a)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM (Int, a)) -> TcS (Int, a))
-> (TcSEnv -> TcM (Int, a)) -> TcS (Int, a)
forall a b. (a -> b) -> a -> b
$ \ TcSEnv
env ->
    do { IORef Int
inner_unified <- Int -> TcRnIf TcGblEnv TcLclEnv (IORef Int)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef Int
0
       ; a
res <- TcSEnv -> TcM a
thing_inside (TcSEnv
env { tcs_unified :: IORef Int
tcs_unified = IORef Int
inner_unified })
       ; Int
n_unifs <- IORef Int -> TcRnIf TcGblEnv TcLclEnv Int
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef Int
inner_unified
       ; IORef Int -> (Int -> Int) -> TcM ()
forall a gbl lcl. TcRef a -> (a -> a) -> TcRnIf gbl lcl ()
TcM.updTcRef (TcSEnv -> IORef Int
tcs_unified TcSEnv
env) (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n_unifs)
       ; (Int, a) -> TcM (Int, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n_unifs, a
res) }

getDefaultInfo ::  TcS ([Type], (Bool, Bool))
getDefaultInfo :: TcS ([TcPredType], (Bool, Bool))
getDefaultInfo = TcM ([TcPredType], (Bool, Bool))
-> TcS ([TcPredType], (Bool, Bool))
forall a. TcM a -> TcS a
wrapTcS TcM ([TcPredType], (Bool, Bool))
TcM.tcGetDefaultTys

getWorkList :: TcS WorkList
getWorkList :: TcS WorkList
getWorkList = do { IORef WorkList
wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
                 ; TcM WorkList -> TcS WorkList
forall a. TcM a -> TcS a
wrapTcS (IORef WorkList -> TcM WorkList
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef WorkList
wl_var) }

selectNextWorkItem :: TcS (Maybe Ct)
-- Pick which work item to do next
-- See Note [Prioritise equalities]
selectNextWorkItem :: TcS (Maybe Ct)
selectNextWorkItem
  = do { IORef WorkList
wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
       ; WorkList
wl <- IORef WorkList -> TcS WorkList
forall a. TcRef a -> TcS a
readTcRef IORef WorkList
wl_var
       ; case WorkList -> Maybe (Ct, WorkList)
selectWorkItem WorkList
wl of {
           Maybe (Ct, WorkList)
Nothing -> Maybe Ct -> TcS (Maybe Ct)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Ct
forall a. Maybe a
Nothing ;
           Just (Ct
ct, WorkList
new_wl) ->
    do { -- checkReductionDepth (ctLoc ct) (ctPred ct)
         -- This is done by GHC.Tc.Solver.Interact.chooseInstance
       ; IORef WorkList -> WorkList -> TcS ()
forall a. TcRef a -> a -> TcS ()
writeTcRef IORef WorkList
wl_var WorkList
new_wl
       ; Maybe Ct -> TcS (Maybe Ct)
forall (m :: * -> *) a. Monad m => a -> m a
return (Ct -> Maybe Ct
forall a. a -> Maybe a
Just Ct
ct) } } }

-- Just get some environments needed for instance looking up and matching
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

getInstEnvs :: TcS InstEnvs
getInstEnvs :: TcS InstEnvs
getInstEnvs = TcM InstEnvs -> TcS InstEnvs
forall a. TcM a -> TcS a
wrapTcS (TcM InstEnvs -> TcS InstEnvs) -> TcM InstEnvs -> TcS InstEnvs
forall a b. (a -> b) -> a -> b
$ TcM InstEnvs
TcM.tcGetInstEnvs

getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
getFamInstEnvs = TcM (FamInstEnv, FamInstEnv) -> TcS (FamInstEnv, FamInstEnv)
forall a. TcM a -> TcS a
wrapTcS (TcM (FamInstEnv, FamInstEnv) -> TcS (FamInstEnv, FamInstEnv))
-> TcM (FamInstEnv, FamInstEnv) -> TcS (FamInstEnv, FamInstEnv)
forall a b. (a -> b) -> a -> b
$ TcM (FamInstEnv, FamInstEnv)
FamInst.tcGetFamInstEnvs

getTopEnv :: TcS HscEnv
getTopEnv :: TcS HscEnv
getTopEnv = TcM HscEnv -> TcS HscEnv
forall a. TcM a -> TcS a
wrapTcS (TcM HscEnv -> TcS HscEnv) -> TcM HscEnv -> TcS HscEnv
forall a b. (a -> b) -> a -> b
$ TcM HscEnv
forall gbl lcl. TcRnIf gbl lcl HscEnv
TcM.getTopEnv

getGblEnv :: TcS TcGblEnv
getGblEnv :: TcS TcGblEnv
getGblEnv = TcM TcGblEnv -> TcS TcGblEnv
forall a. TcM a -> TcS a
wrapTcS (TcM TcGblEnv -> TcS TcGblEnv) -> TcM TcGblEnv -> TcS TcGblEnv
forall a b. (a -> b) -> a -> b
$ TcM TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
TcM.getGblEnv

getLclEnv :: TcS TcLclEnv
getLclEnv :: TcS TcLclEnv
getLclEnv = TcM TcLclEnv -> TcS TcLclEnv
forall a. TcM a -> TcS a
wrapTcS (TcM TcLclEnv -> TcS TcLclEnv) -> TcM TcLclEnv -> TcS TcLclEnv
forall a b. (a -> b) -> a -> b
$ TcM TcLclEnv
forall gbl lcl. TcRnIf gbl lcl lcl
TcM.getLclEnv

tcLookupClass :: Name -> TcS Class
tcLookupClass :: Name -> TcS Class
tcLookupClass Name
c = TcM Class -> TcS Class
forall a. TcM a -> TcS a
wrapTcS (TcM Class -> TcS Class) -> TcM Class -> TcS Class
forall a b. (a -> b) -> a -> b
$ Name -> TcM Class
TcM.tcLookupClass Name
c

tcLookupId :: Name -> TcS Id
tcLookupId :: Name -> TcS TcTyVar
tcLookupId Name
n = TcM TcTyVar -> TcS TcTyVar
forall a. TcM a -> TcS a
wrapTcS (TcM TcTyVar -> TcS TcTyVar) -> TcM TcTyVar -> TcS TcTyVar
forall a b. (a -> b) -> a -> b
$ Name -> TcM TcTyVar
TcM.tcLookupId Name
n

-- Setting names as used (used in the deriving of Coercible evidence)
-- Too hackish to expose it to TcS? In that case somehow extract the used
-- constructors from the result of solveInteract
addUsedGREs :: [GlobalRdrElt] -> TcS ()
addUsedGREs :: [GlobalRdrElt] -> TcS ()
addUsedGREs [GlobalRdrElt]
gres = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS  (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ [GlobalRdrElt] -> TcM ()
TcM.addUsedGREs [GlobalRdrElt]
gres

addUsedGRE :: Bool -> GlobalRdrElt -> TcS ()
addUsedGRE :: Bool -> GlobalRdrElt -> TcS ()
addUsedGRE Bool
warn_if_deprec GlobalRdrElt
gre = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ Bool -> GlobalRdrElt -> TcM ()
TcM.addUsedGRE Bool
warn_if_deprec GlobalRdrElt
gre

keepAlive :: Name -> TcS ()
keepAlive :: Name -> TcS ()
keepAlive = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> (Name -> TcM ()) -> Name -> TcS ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> TcM ()
TcM.keepAlive

-- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

checkWellStagedDFun :: CtLoc -> InstanceWhat -> PredType -> TcS ()
-- Check that we do not try to use an instance before it is available.  E.g.
--    instance Eq T where ...
--    f x = $( ... (\(p::T) -> p == p)... )
-- Here we can't use the equality function from the instance in the splice

checkWellStagedDFun :: CtLoc -> InstanceWhat -> TcPredType -> TcS ()
checkWellStagedDFun CtLoc
loc InstanceWhat
what TcPredType
pred
  | TopLevInstance { iw_dfun_id :: InstanceWhat -> TcTyVar
iw_dfun_id = TcTyVar
dfun_id } <- InstanceWhat
what
  , let bind_lvl :: Int
bind_lvl = TcTyVar -> Int
TcM.topIdLvl TcTyVar
dfun_id
  , Int
bind_lvl Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
impLevel
  = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtLoc -> TcM () -> TcM ()
forall a. CtLoc -> TcM a -> TcM a
TcM.setCtLocM CtLoc
loc (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
    do { ThStage
use_stage <- TcM ThStage
TcM.getStage
       ; SDoc -> Int -> Int -> TcM ()
TcM.checkWellStaged SDoc
pp_thing Int
bind_lvl (ThStage -> Int
thLevel ThStage
use_stage) }

  | Bool
otherwise
  = () -> TcS ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()    -- Fast path for common case
  where
    pp_thing :: SDoc
pp_thing = String -> SDoc
text String
"instance for" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
pred)

pprEq :: TcType -> TcType -> SDoc
pprEq :: TcPredType -> TcPredType -> SDoc
pprEq TcPredType
ty1 TcPredType
ty2 = TcPredType -> SDoc
pprParendType TcPredType
ty1 SDoc -> SDoc -> SDoc
<+> Char -> SDoc
char Char
'~' SDoc -> SDoc -> SDoc
<+> TcPredType -> SDoc
pprParendType TcPredType
ty2

isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe TcPredType)
isFilledMetaTyVar_maybe TcTyVar
tv = TcM (Maybe TcPredType) -> TcS (Maybe TcPredType)
forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM (Maybe TcPredType)
TcM.isFilledMetaTyVar_maybe TcTyVar
tv)

isFilledMetaTyVar :: TcTyVar -> TcS Bool
isFilledMetaTyVar :: TcTyVar -> TcS Bool
isFilledMetaTyVar TcTyVar
tv = TcM Bool -> TcS Bool
forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM Bool
TcM.isFilledMetaTyVar TcTyVar
tv)

zonkTyCoVarsAndFV :: TcTyCoVarSet -> TcS TcTyCoVarSet
zonkTyCoVarsAndFV :: VarSet -> TcS VarSet
zonkTyCoVarsAndFV VarSet
tvs = TcM VarSet -> TcS VarSet
forall a. TcM a -> TcS a
wrapTcS (VarSet -> TcM VarSet
TcM.zonkTyCoVarsAndFV VarSet
tvs)

zonkTyCoVarsAndFVList :: [TcTyCoVar] -> TcS [TcTyCoVar]
zonkTyCoVarsAndFVList :: [TcTyVar] -> TcS [TcTyVar]
zonkTyCoVarsAndFVList [TcTyVar]
tvs = TcM [TcTyVar] -> TcS [TcTyVar]
forall a. TcM a -> TcS a
wrapTcS ([TcTyVar] -> TcM [TcTyVar]
TcM.zonkTyCoVarsAndFVList [TcTyVar]
tvs)

zonkCo :: Coercion -> TcS Coercion
zonkCo :: Coercion -> TcS Coercion
zonkCo = TcM Coercion -> TcS Coercion
forall a. TcM a -> TcS a
wrapTcS (TcM Coercion -> TcS Coercion)
-> (Coercion -> TcM Coercion) -> Coercion -> TcS Coercion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercion -> TcM Coercion
TcM.zonkCo

zonkTcType :: TcType -> TcS TcType
zonkTcType :: TcPredType -> TcS TcPredType
zonkTcType TcPredType
ty = TcM TcPredType -> TcS TcPredType
forall a. TcM a -> TcS a
wrapTcS (TcPredType -> TcM TcPredType
TcM.zonkTcType TcPredType
ty)

zonkTcTypes :: [TcType] -> TcS [TcType]
zonkTcTypes :: [TcPredType] -> TcS [TcPredType]
zonkTcTypes [TcPredType]
tys = TcM [TcPredType] -> TcS [TcPredType]
forall a. TcM a -> TcS a
wrapTcS ([TcPredType] -> TcM [TcPredType]
TcM.zonkTcTypes [TcPredType]
tys)

zonkTcTyVar :: TcTyVar -> TcS TcType
zonkTcTyVar :: TcTyVar -> TcS TcPredType
zonkTcTyVar TcTyVar
tv = TcM TcPredType -> TcS TcPredType
forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM TcPredType
TcM.zonkTcTyVar TcTyVar
tv)

zonkSimples :: Cts -> TcS Cts
zonkSimples :: Cts -> TcS Cts
zonkSimples Cts
cts = TcM Cts -> TcS Cts
forall a. TcM a -> TcS a
wrapTcS (Cts -> TcM Cts
TcM.zonkSimples Cts
cts)

zonkWC :: WantedConstraints -> TcS WantedConstraints
zonkWC :: WantedConstraints -> TcS WantedConstraints
zonkWC WantedConstraints
wc = TcM WantedConstraints -> TcS WantedConstraints
forall a. TcM a -> TcS a
wrapTcS (WantedConstraints -> TcM WantedConstraints
TcM.zonkWC WantedConstraints
wc)

zonkTyCoVarKind :: TcTyCoVar -> TcS TcTyCoVar
zonkTyCoVarKind :: TcTyVar -> TcS TcTyVar
zonkTyCoVarKind TcTyVar
tv = TcM TcTyVar -> TcS TcTyVar
forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM TcTyVar
TcM.zonkTyCoVarKind TcTyVar
tv)

----------------------------
pprKicked :: Int -> SDoc
pprKicked :: Int -> SDoc
pprKicked Int
0 = SDoc
empty
pprKicked Int
n = SDoc -> SDoc
parens (Int -> SDoc
int Int
n SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"kicked out")

{- *********************************************************************
*                                                                      *
*              The Unification Level Flag                              *
*                                                                      *
********************************************************************* -}

{- Note [The Unification Level Flag]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider a deep tree of implication constraints
   forall[1] a.                              -- Outer-implic
      C alpha[1]                               -- Simple
      forall[2] c. ....(C alpha[1])....        -- Implic-1
      forall[2] b. ....(alpha[1] ~ Int)....    -- Implic-2

The (C alpha) is insoluble until we know alpha.  We solve alpha
by unifying alpha:=Int somewhere deep inside Implic-2. But then we
must try to solve the Outer-implic all over again. This time we can
solve (C alpha) both in Outer-implic, and nested inside Implic-1.

When should we iterate solving a level-n implication?
Answer: if any unification of a tyvar at level n takes place
        in the ic_implics of that implication.

* What if a unification takes place at level n-1? Then don't iterate
  level n, because we'll iterate level n-1, and that will in turn iterate
  level n.

* What if a unification takes place at level n, in the ic_simples of
  level n?  No need to track this, because the kick-out mechanism deals
  with it.  (We can't drop kick-out in favour of iteration, because kick-out
  works for skolem-equalities, not just unifications.)

So the monad-global Unification Level Flag, kept in tcs_unif_lvl keeps
track of
  - Whether any unifications at all have taken place (Nothing => no unifications)
  - If so, what is the outermost level that has seen a unification (Just lvl)

The iteration done in the simplify_loop/maybe_simplify_again loop in GHC.Tc.Solver.

It helpful not to iterate unless there is a chance of progress.  #8474 is
an example:

  * There's a deeply-nested chain of implication constraints.
       ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int

  * From the innermost one we get a [D] alpha[1] ~ Int,
    so we can unify.

  * It's better not to iterate the inner implications, but go all the
    way out to level 1 before iterating -- because iterating level 1
    will iterate the inner levels anyway.

(In the olden days when we "floated" thse Derived constraints, this was
much, much more important -- we got exponential behaviour, as each iteration
produced the same Derived constraint.)
-}


resetUnificationFlag :: TcS Bool
-- We are at ambient level i
-- If the unification flag = Just i, reset it to Nothing and return True
-- Otherwise leave it unchanged and return False
resetUnificationFlag :: TcS Bool
resetUnificationFlag
  = (TcSEnv -> TcM Bool) -> TcS Bool
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM Bool) -> TcS Bool)
-> (TcSEnv -> TcM Bool) -> TcS Bool
forall a b. (a -> b) -> a -> b
$ \TcSEnv
env ->
    do { let ref :: IORef (Maybe TcLevel)
ref = TcSEnv -> IORef (Maybe TcLevel)
tcs_unif_lvl TcSEnv
env
       ; TcLevel
ambient_lvl <- TcM TcLevel
TcM.getTcLevel
       ; Maybe TcLevel
mb_lvl <- IORef (Maybe TcLevel) -> TcRnIf TcGblEnv TcLclEnv (Maybe TcLevel)
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef (Maybe TcLevel)
ref
       ; String -> SDoc -> TcM ()
TcM.traceTc String
"resetUnificationFlag" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"ambient:" SDoc -> SDoc -> SDoc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
ambient_lvl
              , String -> SDoc
text String
"unif_lvl:" SDoc -> SDoc -> SDoc
<+> Maybe TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe TcLevel
mb_lvl ]
       ; case Maybe TcLevel
mb_lvl of
           Maybe TcLevel
Nothing       -> Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
           Just TcLevel
unif_lvl | TcLevel
ambient_lvl TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
unif_lvl
                         -> Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                         | Bool
otherwise
                         -> do { IORef (Maybe TcLevel) -> Maybe TcLevel -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef (Maybe TcLevel)
ref Maybe TcLevel
forall a. Maybe a
Nothing
                               ; Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True } }

setUnificationFlag :: TcLevel -> TcS ()
-- (setUnificationFlag i) sets the unification level to (Just i)
-- unless it already is (Just j) where j <= i
setUnificationFlag :: TcLevel -> TcS ()
setUnificationFlag TcLevel
lvl
  = (TcSEnv -> TcM ()) -> TcS ()
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM ()) -> TcS ()) -> (TcSEnv -> TcM ()) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \TcSEnv
env ->
    do { let ref :: IORef (Maybe TcLevel)
ref = TcSEnv -> IORef (Maybe TcLevel)
tcs_unif_lvl TcSEnv
env
       ; Maybe TcLevel
mb_lvl <- IORef (Maybe TcLevel) -> TcRnIf TcGblEnv TcLclEnv (Maybe TcLevel)
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef (Maybe TcLevel)
ref
       ; case Maybe TcLevel
mb_lvl of
           Just TcLevel
unif_lvl | TcLevel
lvl TcLevel -> TcLevel -> Bool
`deeperThanOrSame` TcLevel
unif_lvl
                         -> () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           Maybe TcLevel
_ -> IORef (Maybe TcLevel) -> Maybe TcLevel -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef (Maybe TcLevel)
ref (TcLevel -> Maybe TcLevel
forall a. a -> Maybe a
Just TcLevel
lvl) }


{- *********************************************************************
*                                                                      *
*                Instantiation etc.
*                                                                      *
********************************************************************* -}

-- Instantiations
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
instDFunType :: TcTyVar -> [Maybe TcPredType] -> TcS ([TcPredType], [TcPredType])
instDFunType TcTyVar
dfun_id [Maybe TcPredType]
inst_tys
  = TcM ([TcPredType], [TcPredType])
-> TcS ([TcPredType], [TcPredType])
forall a. TcM a -> TcS a
wrapTcS (TcM ([TcPredType], [TcPredType])
 -> TcS ([TcPredType], [TcPredType]))
-> TcM ([TcPredType], [TcPredType])
-> TcS ([TcPredType], [TcPredType])
forall a b. (a -> b) -> a -> b
$ TcTyVar -> [Maybe TcPredType] -> TcM ([TcPredType], [TcPredType])
TcM.instDFunType TcTyVar
dfun_id [Maybe TcPredType]
inst_tys

newFlexiTcSTy :: Kind -> TcS TcType
newFlexiTcSTy :: TcPredType -> TcS TcPredType
newFlexiTcSTy TcPredType
knd = TcM TcPredType -> TcS TcPredType
forall a. TcM a -> TcS a
wrapTcS (TcPredType -> TcM TcPredType
TcM.newFlexiTyVarTy TcPredType
knd)

cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
cloneMetaTyVar TcTyVar
tv = TcM TcTyVar -> TcS TcTyVar
forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM TcTyVar
TcM.cloneMetaTyVar TcTyVar
tv)

instFlexi :: [TKVar] -> TcS TCvSubst
instFlexi :: [TcTyVar] -> TcS TCvSubst
instFlexi = TCvSubst -> [TcTyVar] -> TcS TCvSubst
instFlexiX TCvSubst
emptyTCvSubst

instFlexiX :: TCvSubst -> [TKVar] -> TcS TCvSubst
instFlexiX :: TCvSubst -> [TcTyVar] -> TcS TCvSubst
instFlexiX TCvSubst
subst [TcTyVar]
tvs
  = TcM TCvSubst -> TcS TCvSubst
forall a. TcM a -> TcS a
wrapTcS ((TCvSubst -> TcTyVar -> TcM TCvSubst)
-> TCvSubst -> [TcTyVar] -> TcM TCvSubst
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM TCvSubst -> TcTyVar -> TcM TCvSubst
instFlexiHelper TCvSubst
subst [TcTyVar]
tvs)

instFlexiHelper :: TCvSubst -> TKVar -> TcM TCvSubst
instFlexiHelper :: TCvSubst -> TcTyVar -> TcM TCvSubst
instFlexiHelper TCvSubst
subst TcTyVar
tv
  = do { Unique
uniq <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
TcM.newUnique
       ; TcTyVarDetails
details <- MetaInfo -> TcM TcTyVarDetails
TcM.newMetaDetails MetaInfo
TauTv
       ; let name :: Name
name = Name -> Unique -> Name
setNameUnique (TcTyVar -> Name
tyVarName TcTyVar
tv) Unique
uniq
             kind :: TcPredType
kind = TCvSubst -> TcPredType -> TcPredType
substTyUnchecked TCvSubst
subst (TcTyVar -> TcPredType
tyVarKind TcTyVar
tv)
             ty' :: TcPredType
ty'  = TcTyVar -> TcPredType
mkTyVarTy (Name -> TcPredType -> TcTyVarDetails -> TcTyVar
mkTcTyVar Name
name TcPredType
kind TcTyVarDetails
details)
       ; String -> SDoc -> TcM ()
TcM.traceTc String
"instFlexi" (TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
ty')
       ; TCvSubst -> TcM TCvSubst
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst -> TcTyVar -> TcPredType -> TCvSubst
extendTvSubst TCvSubst
subst TcTyVar
tv TcPredType
ty') }

matchGlobalInst :: DynFlags
                -> Bool      -- True <=> caller is the short-cut solver
                             -- See Note [Shortcut solving: overlap]
                -> Class -> [Type] -> TcS TcM.ClsInstResult
matchGlobalInst :: DynFlags -> Bool -> Class -> [TcPredType] -> TcS ClsInstResult
matchGlobalInst DynFlags
dflags Bool
short_cut Class
cls [TcPredType]
tys
  = TcM ClsInstResult -> TcS ClsInstResult
forall a. TcM a -> TcS a
wrapTcS (DynFlags -> Bool -> Class -> [TcPredType] -> TcM ClsInstResult
TcM.matchGlobalInst DynFlags
dflags Bool
short_cut Class
cls [TcPredType]
tys)

tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar])
tcInstSkolTyVarsX :: TCvSubst -> [TcTyVar] -> TcS (TCvSubst, [TcTyVar])
tcInstSkolTyVarsX TCvSubst
subst [TcTyVar]
tvs = TcM (TCvSubst, [TcTyVar]) -> TcS (TCvSubst, [TcTyVar])
forall a. TcM a -> TcS a
wrapTcS (TcM (TCvSubst, [TcTyVar]) -> TcS (TCvSubst, [TcTyVar]))
-> TcM (TCvSubst, [TcTyVar]) -> TcS (TCvSubst, [TcTyVar])
forall a b. (a -> b) -> a -> b
$ TCvSubst -> [TcTyVar] -> TcM (TCvSubst, [TcTyVar])
TcM.tcInstSkolTyVarsX TCvSubst
subst [TcTyVar]
tvs

-- Creating and setting evidence variables and CtFlavors
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

data MaybeNew = Fresh CtEvidence | Cached EvExpr

isFresh :: MaybeNew -> Bool
isFresh :: MaybeNew -> Bool
isFresh (Fresh {})  = Bool
True
isFresh (Cached {}) = Bool
False

freshGoals :: [MaybeNew] -> [CtEvidence]
freshGoals :: [MaybeNew] -> [CtEvidence]
freshGoals [MaybeNew]
mns = [ CtEvidence
ctev | Fresh CtEvidence
ctev <- [MaybeNew]
mns ]

getEvExpr :: MaybeNew -> EvExpr
getEvExpr :: MaybeNew -> EvExpr
getEvExpr (Fresh CtEvidence
ctev) = CtEvidence -> EvExpr
ctEvExpr CtEvidence
ctev
getEvExpr (Cached EvExpr
evt) = EvExpr
evt

setEvBind :: EvBind -> TcS ()
setEvBind :: EvBind -> TcS ()
setEvBind EvBind
ev_bind
  = do { EvBindsVar
evb <- TcS EvBindsVar
getTcEvBindsVar
       ; TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ EvBindsVar -> EvBind -> TcM ()
TcM.addTcEvBind EvBindsVar
evb EvBind
ev_bind }

-- | Mark variables as used filling a coercion hole
useVars :: CoVarSet -> TcS ()
useVars :: VarSet -> TcS ()
useVars VarSet
co_vars
  = do { EvBindsVar
ev_binds_var <- TcS EvBindsVar
getTcEvBindsVar
       ; let ref :: IORef VarSet
ref = EvBindsVar -> IORef VarSet
ebv_tcvs EvBindsVar
ev_binds_var
       ; TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$
         do { VarSet
tcvs <- IORef VarSet -> TcM VarSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef VarSet
ref
            ; let tcvs' :: VarSet
tcvs' = VarSet
tcvs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
co_vars
            ; IORef VarSet -> VarSet -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef VarSet
ref VarSet
tcvs' } }

-- | Equalities only
setWantedEq :: TcEvDest -> Coercion -> TcS ()
setWantedEq :: TcEvDest -> Coercion -> TcS ()
setWantedEq (HoleDest CoercionHole
hole) Coercion
co
  = do { VarSet -> TcS ()
useVars (Coercion -> VarSet
coVarsOfCo Coercion
co)
       ; CoercionHole -> Coercion -> TcS ()
fillCoercionHole CoercionHole
hole Coercion
co }
setWantedEq (EvVarDest TcTyVar
ev) Coercion
_ = String -> SDoc -> TcS ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"setWantedEq" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
ev)

-- | Good for both equalities and non-equalities
setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm (HoleDest CoercionHole
hole) EvTerm
tm
  | Just Coercion
co <- EvTerm -> Maybe Coercion
evTermCoercion_maybe EvTerm
tm
  = do { VarSet -> TcS ()
useVars (Coercion -> VarSet
coVarsOfCo Coercion
co)
       ; CoercionHole -> Coercion -> TcS ()
fillCoercionHole CoercionHole
hole Coercion
co }
  | Bool
otherwise
  = -- See Note [Yukky eq_sel for a HoleDest]
    do { let co_var :: TcTyVar
co_var = CoercionHole -> TcTyVar
coHoleCoVar CoercionHole
hole
       ; EvBind -> TcS ()
setEvBind (TcTyVar -> EvTerm -> EvBind
mkWantedEvBind TcTyVar
co_var EvTerm
tm)
       ; CoercionHole -> Coercion -> TcS ()
fillCoercionHole CoercionHole
hole (TcTyVar -> Coercion
mkTcCoVarCo TcTyVar
co_var) }

setWantedEvTerm (EvVarDest TcTyVar
ev_id) EvTerm
tm
  = EvBind -> TcS ()
setEvBind (TcTyVar -> EvTerm -> EvBind
mkWantedEvBind TcTyVar
ev_id EvTerm
tm)

{- Note [Yukky eq_sel for a HoleDest]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
How can it be that a Wanted with HoleDest gets evidence that isn't
just a coercion? i.e. evTermCoercion_maybe returns Nothing.

Consider [G] forall a. blah => a ~ T
         [W] S ~# T

Then doTopReactEqPred carefully looks up the (boxed) constraint (S ~
T) in the quantified constraints, and wraps the (boxed) evidence it
gets back in an eq_sel to extract the unboxed (S ~# T).  We can't put
that term into a coercion, so we add a value binding
    h = eq_sel (...)
and the coercion variable h to fill the coercion hole.
We even re-use the CoHole's Id for this binding!

Yuk!
-}

fillCoercionHole :: CoercionHole -> Coercion -> TcS ()
fillCoercionHole :: CoercionHole -> Coercion -> TcS ()
fillCoercionHole CoercionHole
hole Coercion
co
  = do { TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ CoercionHole -> Coercion -> TcM ()
TcM.fillCoercionHole CoercionHole
hole Coercion
co
       ; CoercionHole -> Coercion -> TcS ()
kickOutAfterFillingCoercionHole CoercionHole
hole Coercion
co }

setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev EvTerm
tm
  = case CtEvidence
ev of
      CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest } -> TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest EvTerm
tm
      CtEvidence
_                             -> () -> TcS ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

newTcEvBinds :: TcS EvBindsVar
newTcEvBinds :: TcS EvBindsVar
newTcEvBinds = TcM EvBindsVar -> TcS EvBindsVar
forall a. TcM a -> TcS a
wrapTcS TcM EvBindsVar
TcM.newTcEvBinds

newNoTcEvBinds :: TcS EvBindsVar
newNoTcEvBinds :: TcS EvBindsVar
newNoTcEvBinds = TcM EvBindsVar -> TcS EvBindsVar
forall a. TcM a -> TcS a
wrapTcS TcM EvBindsVar
TcM.newNoTcEvBinds

newEvVar :: TcPredType -> TcS EvVar
newEvVar :: TcPredType -> TcS TcTyVar
newEvVar TcPredType
pred = TcM TcTyVar -> TcS TcTyVar
forall a. TcM a -> TcS a
wrapTcS (TcPredType -> TcM TcTyVar
forall gbl lcl. TcPredType -> TcRnIf gbl lcl TcTyVar
TcM.newEvVar TcPredType
pred)

newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
-- Make a new variable of the given PredType,
-- immediately bind it to the given term
-- and return its CtEvidence
-- See Note [Bind new Givens immediately] in GHC.Tc.Types.Constraint
newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (TcPredType
pred, EvTerm
rhs)
  = do { TcTyVar
new_ev <- TcPredType -> EvTerm -> TcS TcTyVar
newBoundEvVarId TcPredType
pred EvTerm
rhs
       ; CtEvidence -> TcS CtEvidence
forall (m :: * -> *) a. Monad m => a -> m a
return (CtGiven :: TcPredType -> TcTyVar -> CtLoc -> CtEvidence
CtGiven { ctev_pred :: TcPredType
ctev_pred = TcPredType
pred, ctev_evar :: TcTyVar
ctev_evar = TcTyVar
new_ev, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc }) }

-- | Make a new 'Id' of the given type, bound (in the monad's EvBinds) to the
-- given term
newBoundEvVarId :: TcPredType -> EvTerm -> TcS EvVar
newBoundEvVarId :: TcPredType -> EvTerm -> TcS TcTyVar
newBoundEvVarId TcPredType
pred EvTerm
rhs
  = do { TcTyVar
new_ev <- TcPredType -> TcS TcTyVar
newEvVar TcPredType
pred
       ; EvBind -> TcS ()
setEvBind (TcTyVar -> EvTerm -> EvBind
mkGivenEvBind TcTyVar
new_ev EvTerm
rhs)
       ; TcTyVar -> TcS TcTyVar
forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
new_ev }

newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
newGivenEvVars CtLoc
loc [(TcPredType, EvTerm)]
pts = ((TcPredType, EvTerm) -> TcS CtEvidence)
-> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc) [(TcPredType, EvTerm)]
pts

emitNewWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS Coercion
-- | Emit a new Wanted equality into the work-list
emitNewWantedEq :: CtLoc -> Role -> TcPredType -> TcPredType -> TcS Coercion
emitNewWantedEq CtLoc
loc Role
role TcPredType
ty1 TcPredType
ty2
  = do { (CtEvidence
ev, Coercion
co) <- CtLoc
-> Role -> TcPredType -> TcPredType -> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc Role
role TcPredType
ty1 TcPredType
ty2
       ; (WorkList -> WorkList) -> TcS ()
updWorkListTcS (Ct -> WorkList -> WorkList
extendWorkListEq (CtEvidence -> Ct
mkNonCanonical CtEvidence
ev))
       ; Coercion -> TcS Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
co }

-- | Make a new equality CtEvidence
newWantedEq :: CtLoc -> Role -> TcType -> TcType
            -> TcS (CtEvidence, Coercion)
newWantedEq :: CtLoc
-> Role -> TcPredType -> TcPredType -> TcS (CtEvidence, Coercion)
newWantedEq = ShadowInfo
-> CtLoc
-> Role
-> TcPredType
-> TcPredType
-> TcS (CtEvidence, Coercion)
newWantedEq_SI ShadowInfo
WDeriv

newWantedEq_SI :: ShadowInfo -> CtLoc -> Role
               -> TcType -> TcType
               -> TcS (CtEvidence, Coercion)
newWantedEq_SI :: ShadowInfo
-> CtLoc
-> Role
-> TcPredType
-> TcPredType
-> TcS (CtEvidence, Coercion)
newWantedEq_SI ShadowInfo
si CtLoc
loc Role
role TcPredType
ty1 TcPredType
ty2
  = do { CoercionHole
hole <- TcM CoercionHole -> TcS CoercionHole
forall a. TcM a -> TcS a
wrapTcS (TcM CoercionHole -> TcS CoercionHole)
-> TcM CoercionHole -> TcS CoercionHole
forall a b. (a -> b) -> a -> b
$ TcPredType -> TcM CoercionHole
TcM.newCoercionHole TcPredType
pty
       ; String -> SDoc -> TcS ()
traceTcS String
"Emitting new coercion hole" (CoercionHole -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoercionHole
hole SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
pty)
       ; (CtEvidence, Coercion) -> TcS (CtEvidence, Coercion)
forall (m :: * -> *) a. Monad m => a -> m a
return ( CtWanted :: TcPredType -> TcEvDest -> ShadowInfo -> CtLoc -> CtEvidence
CtWanted { ctev_pred :: TcPredType
ctev_pred = TcPredType
pty, ctev_dest :: TcEvDest
ctev_dest = CoercionHole -> TcEvDest
HoleDest CoercionHole
hole
                           , ctev_nosh :: ShadowInfo
ctev_nosh = ShadowInfo
si
                           , ctev_loc :: CtLoc
ctev_loc = CtLoc
loc}
                , CoercionHole -> Coercion
mkHoleCo CoercionHole
hole ) }
  where
    pty :: TcPredType
pty = Role -> TcPredType -> TcPredType -> TcPredType
mkPrimEqPredRole Role
role TcPredType
ty1 TcPredType
ty2

-- no equalities here. Use newWantedEq instead
newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
newWantedEvVarNC = ShadowInfo -> CtLoc -> TcPredType -> TcS CtEvidence
newWantedEvVarNC_SI ShadowInfo
WDeriv

newWantedEvVarNC_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS CtEvidence
-- Don't look up in the solved/inerts; we know it's not there
newWantedEvVarNC_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS CtEvidence
newWantedEvVarNC_SI ShadowInfo
si CtLoc
loc TcPredType
pty
  = do { TcTyVar
new_ev <- TcPredType -> TcS TcTyVar
newEvVar TcPredType
pty
       ; String -> SDoc -> TcS ()
traceTcS String
"Emitting new wanted" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
new_ev SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
pty SDoc -> SDoc -> SDoc
$$
                                         CtLoc -> SDoc
pprCtLoc CtLoc
loc)
       ; CtEvidence -> TcS CtEvidence
forall (m :: * -> *) a. Monad m => a -> m a
return (CtWanted :: TcPredType -> TcEvDest -> ShadowInfo -> CtLoc -> CtEvidence
CtWanted { ctev_pred :: TcPredType
ctev_pred = TcPredType
pty, ctev_dest :: TcEvDest
ctev_dest = TcTyVar -> TcEvDest
EvVarDest TcTyVar
new_ev
                          , ctev_nosh :: ShadowInfo
ctev_nosh = ShadowInfo
si
                          , ctev_loc :: CtLoc
ctev_loc = CtLoc
loc })}

newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
newWantedEvVar = ShadowInfo -> CtLoc -> TcPredType -> TcS MaybeNew
newWantedEvVar_SI ShadowInfo
WDeriv

newWantedEvVar_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS MaybeNew
-- For anything except ClassPred, this is the same as newWantedEvVarNC
newWantedEvVar_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS MaybeNew
newWantedEvVar_SI ShadowInfo
si CtLoc
loc TcPredType
pty
  = do { Maybe CtEvidence
mb_ct <- CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
lookupInInerts CtLoc
loc TcPredType
pty
       ; case Maybe CtEvidence
mb_ct of
            Just CtEvidence
ctev
              | Bool -> Bool
not (CtEvidence -> Bool
isDerived CtEvidence
ctev)
              -> do { String -> SDoc -> TcS ()
traceTcS String
"newWantedEvVar/cache hit" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ctev
                    ; MaybeNew -> TcS MaybeNew
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeNew -> TcS MaybeNew) -> MaybeNew -> TcS MaybeNew
forall a b. (a -> b) -> a -> b
$ EvExpr -> MaybeNew
Cached (CtEvidence -> EvExpr
ctEvExpr CtEvidence
ctev) }
            Maybe CtEvidence
_ -> do { CtEvidence
ctev <- ShadowInfo -> CtLoc -> TcPredType -> TcS CtEvidence
newWantedEvVarNC_SI ShadowInfo
si CtLoc
loc TcPredType
pty
                    ; MaybeNew -> TcS MaybeNew
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> MaybeNew
Fresh CtEvidence
ctev) } }

newWanted :: CtLoc -> PredType -> TcS MaybeNew
-- Deals with both equalities and non equalities. Tries to look
-- up non-equalities in the cache
newWanted :: CtLoc -> TcPredType -> TcS MaybeNew
newWanted = ShadowInfo -> CtLoc -> TcPredType -> TcS MaybeNew
newWanted_SI ShadowInfo
WDeriv

newWanted_SI :: ShadowInfo -> CtLoc -> PredType -> TcS MaybeNew
newWanted_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS MaybeNew
newWanted_SI ShadowInfo
si CtLoc
loc TcPredType
pty
  | Just (Role
role, TcPredType
ty1, TcPredType
ty2) <- TcPredType -> Maybe (Role, TcPredType, TcPredType)
getEqPredTys_maybe TcPredType
pty
  = CtEvidence -> MaybeNew
Fresh (CtEvidence -> MaybeNew)
-> ((CtEvidence, Coercion) -> CtEvidence)
-> (CtEvidence, Coercion)
-> MaybeNew
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CtEvidence, Coercion) -> CtEvidence
forall a b. (a, b) -> a
fst ((CtEvidence, Coercion) -> MaybeNew)
-> TcS (CtEvidence, Coercion) -> TcS MaybeNew
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ShadowInfo
-> CtLoc
-> Role
-> TcPredType
-> TcPredType
-> TcS (CtEvidence, Coercion)
newWantedEq_SI ShadowInfo
si CtLoc
loc Role
role TcPredType
ty1 TcPredType
ty2
  | Bool
otherwise
  = ShadowInfo -> CtLoc -> TcPredType -> TcS MaybeNew
newWantedEvVar_SI ShadowInfo
si CtLoc
loc TcPredType
pty

-- deals with both equalities and non equalities. Doesn't do any cache lookups.
newWantedNC :: CtLoc -> PredType -> TcS CtEvidence
newWantedNC :: CtLoc -> TcPredType -> TcS CtEvidence
newWantedNC CtLoc
loc TcPredType
pty
  | Just (Role
role, TcPredType
ty1, TcPredType
ty2) <- TcPredType -> Maybe (Role, TcPredType, TcPredType)
getEqPredTys_maybe TcPredType
pty
  = (CtEvidence, Coercion) -> CtEvidence
forall a b. (a, b) -> a
fst ((CtEvidence, Coercion) -> CtEvidence)
-> TcS (CtEvidence, Coercion) -> TcS CtEvidence
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc
-> Role -> TcPredType -> TcPredType -> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc Role
role TcPredType
ty1 TcPredType
ty2
  | Bool
otherwise
  = CtLoc -> TcPredType -> TcS CtEvidence
newWantedEvVarNC CtLoc
loc TcPredType
pty

emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS ()
emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS ()
emitNewDeriveds CtLoc
loc [TcPredType]
preds
  | [TcPredType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcPredType]
preds
  = () -> TcS ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = do { [CtEvidence]
evs <- (TcPredType -> TcS CtEvidence) -> [TcPredType] -> TcS [CtEvidence]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CtLoc -> TcPredType -> TcS CtEvidence
newDerivedNC CtLoc
loc) [TcPredType]
preds
       ; String -> SDoc -> TcS ()
traceTcS String
"Emitting new deriveds" ([CtEvidence] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [CtEvidence]
evs)
       ; (WorkList -> WorkList) -> TcS ()
updWorkListTcS ([CtEvidence] -> WorkList -> WorkList
extendWorkListDeriveds [CtEvidence]
evs) }

emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS ()
-- Create new equality Derived and put it in the work list
-- There's no caching, no lookupInInerts
emitNewDerivedEq :: CtLoc -> Role -> TcPredType -> TcPredType -> TcS ()
emitNewDerivedEq CtLoc
loc Role
role TcPredType
ty1 TcPredType
ty2
  = do { CtEvidence
ev <- CtLoc -> TcPredType -> TcS CtEvidence
newDerivedNC CtLoc
loc (Role -> TcPredType -> TcPredType -> TcPredType
mkPrimEqPredRole Role
role TcPredType
ty1 TcPredType
ty2)
       ; String -> SDoc -> TcS ()
traceTcS String
"Emitting new derived equality" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev SDoc -> SDoc -> SDoc
$$ CtLoc -> SDoc
pprCtLoc CtLoc
loc)
       ; (WorkList -> WorkList) -> TcS ()
updWorkListTcS (Ct -> WorkList -> WorkList
extendWorkListEq (CtEvidence -> Ct
mkNonCanonical CtEvidence
ev)) }
         -- Very important: put in the wl_eqs
         -- See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet
         -- (Avoiding fundep iteration)

newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence
newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence
newDerivedNC CtLoc
loc TcPredType
pred
  = CtEvidence -> TcS CtEvidence
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> TcS CtEvidence) -> CtEvidence -> TcS CtEvidence
forall a b. (a -> b) -> a -> b
$ CtDerived :: TcPredType -> CtLoc -> CtEvidence
CtDerived { ctev_pred :: TcPredType
ctev_pred = TcPredType
pred, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc }

-- --------- Check done in GHC.Tc.Solver.Interact.selectNewWorkItem???? ---------
-- | Checks if the depth of the given location is too much. Fails if
-- it's too big, with an appropriate error message.
checkReductionDepth :: CtLoc -> TcType   -- ^ type being reduced
                    -> TcS ()
checkReductionDepth :: CtLoc -> TcPredType -> TcS ()
checkReductionDepth CtLoc
loc TcPredType
ty
  = do { DynFlags
dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DynFlags -> SubGoalDepth -> Bool
subGoalDepthExceeded DynFlags
dflags (CtLoc -> SubGoalDepth
ctLocDepth CtLoc
loc)) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
         TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapErrTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$
         CtLoc -> TcPredType -> TcM ()
forall a. CtLoc -> TcPredType -> TcM a
solverDepthErrorTcS CtLoc
loc TcPredType
ty }

matchFam :: TyCon -> [Type] -> TcS (Maybe (CoercionN, TcType))
-- Given (F tys) return (ty, co), where co :: ty ~N F tys
matchFam :: TyCon -> [TcPredType] -> TcS (Maybe (Coercion, TcPredType))
matchFam TyCon
tycon [TcPredType]
args = (Maybe (Coercion, TcPredType) -> Maybe (Coercion, TcPredType))
-> TcS (Maybe (Coercion, TcPredType))
-> TcS (Maybe (Coercion, TcPredType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Coercion, TcPredType) -> (Coercion, TcPredType))
-> Maybe (Coercion, TcPredType) -> Maybe (Coercion, TcPredType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Coercion -> Coercion)
-> (Coercion, TcPredType) -> (Coercion, TcPredType)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Coercion -> Coercion
mkTcSymCo)) (TcS (Maybe (Coercion, TcPredType))
 -> TcS (Maybe (Coercion, TcPredType)))
-> TcS (Maybe (Coercion, TcPredType))
-> TcS (Maybe (Coercion, TcPredType))
forall a b. (a -> b) -> a -> b
$ TcM (Maybe (Coercion, TcPredType))
-> TcS (Maybe (Coercion, TcPredType))
forall a. TcM a -> TcS a
wrapTcS (TcM (Maybe (Coercion, TcPredType))
 -> TcS (Maybe (Coercion, TcPredType)))
-> TcM (Maybe (Coercion, TcPredType))
-> TcS (Maybe (Coercion, TcPredType))
forall a b. (a -> b) -> a -> b
$ TyCon -> [TcPredType] -> TcM (Maybe (Coercion, TcPredType))
matchFamTcM TyCon
tycon [TcPredType]
args

matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (CoercionN, TcType))
-- Given (F tys) return (ty, co), where co :: F tys ~N ty
matchFamTcM :: TyCon -> [TcPredType] -> TcM (Maybe (Coercion, TcPredType))
matchFamTcM TyCon
tycon [TcPredType]
args
  = do { (FamInstEnv, FamInstEnv)
fam_envs <- TcM (FamInstEnv, FamInstEnv)
FamInst.tcGetFamInstEnvs
       ; let match_fam_result :: Maybe (Coercion, TcPredType)
match_fam_result
              = (FamInstEnv, FamInstEnv)
-> Role -> TyCon -> [TcPredType] -> Maybe (Coercion, TcPredType)
reduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
fam_envs Role
Nominal TyCon
tycon [TcPredType]
args
       ; String -> SDoc -> TcM ()
TcM.traceTc String
"matchFamTcM" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Matching:" SDoc -> SDoc -> SDoc
<+> TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> [TcPredType] -> TcPredType
mkTyConApp TyCon
tycon [TcPredType]
args)
              , Maybe (Coercion, TcPredType) -> SDoc
forall a a. (Outputable a, Outputable a) => Maybe (a, a) -> SDoc
ppr_res Maybe (Coercion, TcPredType)
match_fam_result ]
       ; Maybe (Coercion, TcPredType) -> TcM (Maybe (Coercion, TcPredType))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Coercion, TcPredType)
match_fam_result }
  where
    ppr_res :: Maybe (a, a) -> SDoc
ppr_res Maybe (a, a)
Nothing        = String -> SDoc
text String
"Match failed"
    ppr_res (Just (a
co,a
ty)) = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Match succeeded:")
                                Int
2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Rewrites to:" SDoc -> SDoc -> SDoc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
ty
                                        , String -> SDoc
text String
"Coercion:" SDoc -> SDoc -> SDoc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
co ])

{-
************************************************************************
*                                                                      *
              Breaking type variable cycles
*                                                                      *
************************************************************************
-}

-- | Replace all type family applications in the RHS with fresh variables,
-- emitting givens that relate the type family application to the variable.
-- See Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical.
breakTyVarCycle :: CtLoc
                -> TcType      -- the RHS
                -> TcS TcType  -- new RHS that doesn't have any type families
-- This could be considerably more efficient. See Detail (5) of Note.
breakTyVarCycle :: CtLoc -> TcPredType -> TcS TcPredType
breakTyVarCycle CtLoc
loc = TcPredType -> TcS TcPredType
go
  where
    go :: TcPredType -> TcS TcPredType
go TcPredType
ty | Just TcPredType
ty' <- TcPredType -> Maybe TcPredType
rewriterView TcPredType
ty = TcPredType -> TcS TcPredType
go TcPredType
ty'
    go (Rep.TyConApp TyCon
tc [TcPredType]
tys)
      | TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
      = do { let ([TcPredType]
fun_args, [TcPredType]
extra_args) = Int -> [TcPredType] -> ([TcPredType], [TcPredType])
forall a. Int -> [a] -> ([a], [a])
splitAt (TyCon -> Int
tyConArity TyCon
tc) [TcPredType]
tys
                 fun_app :: TcPredType
fun_app                = TyCon -> [TcPredType] -> TcPredType
mkTyConApp TyCon
tc [TcPredType]
fun_args
                 fun_app_kind :: TcPredType
fun_app_kind           = HasDebugCallStack => TcPredType -> TcPredType
TcPredType -> TcPredType
tcTypeKind TcPredType
fun_app
           ; TcTyVar
new_tv <- TcM TcTyVar -> TcS TcTyVar
forall a. TcM a -> TcS a
wrapTcS (TcPredType -> TcM TcTyVar
TcM.newCycleBreakerTyVar TcPredType
fun_app_kind)
           ; let new_ty :: TcPredType
new_ty     = TcTyVar -> TcPredType
mkTyVarTy TcTyVar
new_tv
                 given_pred :: TcPredType
given_pred = TcPredType -> TcPredType -> TcPredType -> TcPredType -> TcPredType
mkHeteroPrimEqPred TcPredType
fun_app_kind TcPredType
fun_app_kind
                                                 TcPredType
fun_app TcPredType
new_ty
                 given_term :: EvTerm
given_term = Coercion -> EvTerm
evCoercion (Coercion -> EvTerm) -> Coercion -> EvTerm
forall a b. (a -> b) -> a -> b
$ TcPredType -> Coercion
mkNomReflCo TcPredType
new_ty  -- See Detail (4) of Note
           ; CtEvidence
new_given <- CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (TcPredType
given_pred, EvTerm
given_term)
           ; String -> SDoc -> TcS ()
traceTcS String
"breakTyVarCycle replacing type family" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
new_given)
           ; [CtEvidence] -> TcS ()
emitWorkNC [CtEvidence
new_given]
           ; (InertSet -> InertSet) -> TcS ()
updInertTcS ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \InertSet
is ->
               InertSet
is { inert_cycle_breakers :: [(TcTyVar, TcPredType)]
inert_cycle_breakers = (TcTyVar
new_tv, TcPredType
fun_app) (TcTyVar, TcPredType)
-> [(TcTyVar, TcPredType)] -> [(TcTyVar, TcPredType)]
forall a. a -> [a] -> [a]
:
                                           InertSet -> [(TcTyVar, TcPredType)]
inert_cycle_breakers InertSet
is }
           ; [TcPredType]
extra_args' <- (TcPredType -> TcS TcPredType) -> [TcPredType] -> TcS [TcPredType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TcPredType -> TcS TcPredType
go [TcPredType]
extra_args
           ; TcPredType -> TcS TcPredType
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPredType -> [TcPredType] -> TcPredType
mkAppTys TcPredType
new_ty [TcPredType]
extra_args') }
              -- Worried that this substitution will change kinds?
              -- See Detail (3) of Note

      | Bool
otherwise
      = TyCon -> [TcPredType] -> TcPredType
mkTyConApp TyCon
tc ([TcPredType] -> TcPredType) -> TcS [TcPredType] -> TcS TcPredType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TcPredType -> TcS TcPredType) -> [TcPredType] -> TcS [TcPredType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TcPredType -> TcS TcPredType
go [TcPredType]
tys

    go (Rep.AppTy TcPredType
ty1 TcPredType
ty2)       = TcPredType -> TcPredType -> TcPredType
mkAppTy (TcPredType -> TcPredType -> TcPredType)
-> TcS TcPredType -> TcS (TcPredType -> TcPredType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> TcS TcPredType
go TcPredType
ty1 TcS (TcPredType -> TcPredType) -> TcS TcPredType -> TcS TcPredType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> TcS TcPredType
go TcPredType
ty2
    go (Rep.FunTy AnonArgFlag
vis TcPredType
w TcPredType
arg TcPredType
res) = AnonArgFlag -> TcPredType -> TcPredType -> TcPredType -> TcPredType
mkFunTy AnonArgFlag
vis (TcPredType -> TcPredType -> TcPredType -> TcPredType)
-> TcS TcPredType -> TcS (TcPredType -> TcPredType -> TcPredType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> TcS TcPredType
go TcPredType
w TcS (TcPredType -> TcPredType -> TcPredType)
-> TcS TcPredType -> TcS (TcPredType -> TcPredType)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> TcS TcPredType
go TcPredType
arg TcS (TcPredType -> TcPredType) -> TcS TcPredType -> TcS TcPredType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> TcS TcPredType
go TcPredType
res
    go (Rep.CastTy TcPredType
ty Coercion
co)        = TcPredType -> Coercion -> TcPredType
mkCastTy (TcPredType -> Coercion -> TcPredType)
-> TcS TcPredType -> TcS (Coercion -> TcPredType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> TcS TcPredType
go TcPredType
ty TcS (Coercion -> TcPredType) -> TcS Coercion -> TcS TcPredType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coercion -> TcS Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
co

    go ty :: TcPredType
ty@(Rep.TyVarTy {})    = TcPredType -> TcS TcPredType
forall (m :: * -> *) a. Monad m => a -> m a
return TcPredType
ty
    go ty :: TcPredType
ty@(Rep.LitTy {})      = TcPredType -> TcS TcPredType
forall (m :: * -> *) a. Monad m => a -> m a
return TcPredType
ty
    go ty :: TcPredType
ty@(Rep.ForAllTy {})   = TcPredType -> TcS TcPredType
forall (m :: * -> *) a. Monad m => a -> m a
return TcPredType
ty  -- See Detail (1) of Note
    go ty :: TcPredType
ty@(Rep.CoercionTy {}) = TcPredType -> TcS TcPredType
forall (m :: * -> *) a. Monad m => a -> m a
return TcPredType
ty  -- See Detail (2) of Note

-- | Fill in CycleBreakerTvs with the variables they stand for.
-- See Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical.
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles InertSet
is
  = [(TcTyVar, TcPredType)]
-> ((TcTyVar, TcPredType) -> TcM ()) -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (InertSet -> [(TcTyVar, TcPredType)]
inert_cycle_breakers InertSet
is) (((TcTyVar, TcPredType) -> TcM ()) -> TcM ())
-> ((TcTyVar, TcPredType) -> TcM ()) -> TcM ()
forall a b. (a -> b) -> a -> b
$ \ (TcTyVar
cycle_breaker_tv, TcPredType
orig_ty) ->
    TcTyVar -> TcPredType -> TcM ()
TcM.writeMetaTyVar TcTyVar
cycle_breaker_tv TcPredType
orig_ty

-- Unwrap a type synonym only when either:
--   The type synonym is forgetful, or
--   the type synonym mentions a type family in its expansion
-- See Note [Rewriting synonyms] in GHC.Tc.Solver.Rewrite.
rewriterView :: TcType -> Maybe TcType
rewriterView :: TcPredType -> Maybe TcPredType
rewriterView ty :: TcPredType
ty@(Rep.TyConApp TyCon
tc [TcPredType]
_)
  | TyCon -> Bool
isForgetfulSynTyCon TyCon
tc Bool -> Bool -> Bool
|| (TyCon -> Bool
isTypeSynonymTyCon TyCon
tc Bool -> Bool -> Bool
&& Bool -> Bool
not (TyCon -> Bool
isFamFreeTyCon TyCon
tc))
  = TcPredType -> Maybe TcPredType
tcView TcPredType
ty
rewriterView TcPredType
_other = Maybe TcPredType
forall a. Maybe a
Nothing