{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}

{-# OPTIONS_GHC -Wno-orphans #-}

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

    -- The TcS monad
    TcS(..), TcSEnv(..),
    runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts,
    failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS,
    runTcSEqualities,
    nestTcS, nestImplicTcS, tryShortCutTcS, nestFunDepsTcS,
    setEvBindsTcS, setTcLevelTcS, updTcEvBinds,

    selectNextWorkItem,
    getWorkList,
    updWorkListTcS,
    pushLevelNoWorkList,

    runTcPluginTcS, recordUsedGREs,
    matchGlobalInst, TcM.ClsInstResult(..),

    QCInst(..),

    -- TcSMode
    TcSMode(..), getTcSMode, setTcSMode, vanillaTcSMode,

    -- The pipeline
    StopOrContinue(..), continueWith, stopWith,
    startAgainWith, SolverStage(Stage, runSolverStage), simpleStage,
    stopWithStage, nopStage,

    -- Tracing etc
    panicTcS, traceTcS, tryEarlyAbortTcS,
    traceFireTcS, bumpStepCountTcS, csTraceTcS,
    wrapErrTcS, wrapWarnTcS,

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

    newTcEvBinds, newNoTcEvBinds,
    newWantedEq,
    newWanted,
    newWantedNC, newWantedEvVarNC,
    newBoundEvVarId,
    unifyTyVar, reportFineGrainUnifications, reportCoarseGrainUnifications,
    setEvBind, setWantedEq, setWantedDict, setEqIfWanted, setDictIfWanted,
    fillCoercionHole,
    newEvVar, newGivenEv, emitNewGivens,
    emitChildEqs, checkReductionDepth,

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

    -- Inerts
    updInertSet, updInertCans,
    getHasGivenEqs, setInertCans,
    getInertEqs, getInertCans, getInertGivens,
    getInertInsols, getInnermostGivenEqLevel,
    getInertSet, setInertSet,
    getUnsolvedInerts,
    removeInertCts, getPendingGivenScs,
    insertFunEq, addInertQCI,
    updInertDicts, updInertIrreds,
    emitWorkNC, emitWork,
    lookupInertDict,

    -- The Model
    recordUnification, kickOutRewritable, kickOutAfterUnification,

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

    -- Inert solved dictionaries
    getSolvedDicts, setSolvedDicts,
    updSolvedDicts, lookupSolvedDict,

    -- Irreds
    foldIrreds,

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

    -- Instantiation
    instDFunType,

    -- Unification
    wrapUnifier, wrapUnifierAndEmit, uPairsTcM,

    -- MetaTyVars
    newFlexiTcSTy, instFlexiX, instFlexiXTcM,
    cloneMetaTyVar,
    tcInstSkolTyVarsX,

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

    -- References
    newTcRef, readTcRef, writeTcRef, updTcRef,

    -- Misc
    getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
    matchFam, matchFamTcM,
    checkWellLevelledDFun,
    pprEq,

    -- Enforcing invariants for type equalities
    checkTypeEq
) 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
       ( tcGetDefaultTys
       , tcLookupClass, tcLookupId, tcLookupTyCon
       )
import GHC.Tc.Zonk.Monad ( ZonkM )
import qualified GHC.Tc.Zonk.TcType  as TcM

import GHC.Driver.DynFlags

import GHC.Tc.Instance.Class( safeOverlap, instanceReturnsDictCon )
import GHC.Utils.Misc


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

import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Unify

import GHC.Tc.Types.Evidence
import GHC.Tc.Types
import GHC.Tc.Types.Origin
import GHC.Tc.Types.CtLoc
import GHC.Tc.Types.Constraint

import GHC.Builtin.Names ( callStackTyConName, exceptionContextTyConName )

import GHC.Core.Type
import GHC.Core.TyCo.Rep as Rep
import GHC.Core.TyCo.Tidy
import GHC.Core.Coercion
import GHC.Core.Coercion.Axiom( TypeEqn )
import GHC.Core.Predicate
import GHC.Core.Reduction
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Core.Unify (typesAreApart)

import GHC.LanguageExtensions as LangExt
import GHC.Rename.Env
import qualified GHC.Rename.Env as TcM

import GHC.Types.Name
import GHC.Types.TyThing
import GHC.Types.Name.Reader
import GHC.Types.DefaultEnv ( DefaultEnv )
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Unique.Supply
import GHC.Types.Id
import GHC.Types.Basic (allImportLevels)
import GHC.Types.ThLevelIndex (thLevelIndexFromImportLevel)
import GHC.Types.SrcLoc

import GHC.Unit.Module
import GHC.Unit.Module.Graph

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

import GHC.Data.Bag as Bag
import GHC.Data.Pair

import GHC.Utils.Monad

import GHC.Exts (oneShot)

import Control.Monad
import Data.Foldable hiding ( foldr1 )
import Data.IORef
import qualified Data.Set as Set
import Data.Maybe( catMaybes )
import Data.List ( mapAccumL )

#if defined(DEBUG)
import GHC.Types.Unique.Set (nonDetEltsUniqSet)
import GHC.Data.Graph.Directed
#endif


{- *********************************************************************
*                                                                      *
               SolverStage and StopOrContinue
*                                                                      *
********************************************************************* -}

{- Note [The SolverStage monad]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The SolverStage monad allows us to write simple code like that in
GHC.Tc.Solver.solveEquality.   At the time of writing it looked like
this (may get out of date but the idea is clear):

solveEquality :: ... -> SolverStage Void
solveEquality ev eq_rel ty1 ty2
  = do { Pair ty1' ty2' <- zonkEqTypes ev eq_rel ty1 ty2
       ; mb_canon <- canonicaliseEquality ev' eq_rel ty1' ty2'
       ; case mb_canon of {
            Left irred_ct -> do { tryQCsIrredEqCt irred_ct
                                ; solveIrred irred_ct } ;
            Right eq_ct   -> do { tryInertEqs eq_ct
                                ; tryFunDeps  eq_ct
                                ; tryQCsEqCt  eq_ct
                                ; simpleStage (updInertEqs eq_ct)
                                ; stopWithStage (eqCtEvidence eq_ct) ".." }}}

Each sub-stage can elect to
  (a) ContinueWith: continue to the next stasge
  (b) StartAgain:   start again at the beginning of the pipeline
  (c) Stop:         stop altogether; constraint is solved

These three possiblities are described by the `StopOrContinue` data type.
The `SolverStage` monad does the plumbing.

Notes:

(SM1) Each individual stage pretty quickly drops down into
         TcS (StopOrContinue a)
    because the monadic plumbing of `SolverStage` is relatively ineffienct,
    with that three-way split.

(SM2) We use `SolverStage Void` to express the idea that ContinueWith is
    impossible; we don't need to pattern match on it as a possible outcome:A
    see GHC.Tc.Solver.Solve.solveOne.   To that end, ContinueWith is strict.
-}

data StopOrContinue a
  = StartAgain Ct     -- Constraint is not solved, but some unifications
                      --   happened, so go back to the beginning of the pipeline

  | ContinueWith !a   -- The constraint was not solved, although it may have
                      --   been rewritten.  It is strict so that
                      --   ContinueWith Void can't happen; see (SM2) in
                      --   Note [The SolverStage monad]

  | Stop CtEvidence   -- The (rewritten) constraint was solved
         SDoc         -- Tells how it was solved
                      -- Any new sub-goals have been put on the work list
  deriving ((forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b)
-> (forall a b. a -> StopOrContinue b -> StopOrContinue a)
-> Functor StopOrContinue
forall a b. a -> StopOrContinue b -> StopOrContinue a
forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b
fmap :: forall a b. (a -> b) -> StopOrContinue a -> StopOrContinue b
$c<$ :: forall a b. a -> StopOrContinue b -> StopOrContinue a
<$ :: forall a b. a -> StopOrContinue b -> StopOrContinue a
Functor)

instance Outputable a => Outputable (StopOrContinue a) where
  ppr :: StopOrContinue a -> SDoc
ppr (Stop CtEvidence
ev SDoc
s)      = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Stop" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (SDoc
s SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ev:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev)
  ppr (ContinueWith a
w) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ContinueWith" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
w
  ppr (StartAgain Ct
w)   = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"StartAgain" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
w

newtype SolverStage a = Stage { forall a. SolverStage a -> TcS (StopOrContinue a)
runSolverStage :: TcS (StopOrContinue a) }
  deriving( (forall a b. (a -> b) -> SolverStage a -> SolverStage b)
-> (forall a b. a -> SolverStage b -> SolverStage a)
-> Functor SolverStage
forall a b. a -> SolverStage b -> SolverStage a
forall a b. (a -> b) -> SolverStage a -> SolverStage b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> SolverStage a -> SolverStage b
fmap :: forall a b. (a -> b) -> SolverStage a -> SolverStage b
$c<$ :: forall a b. a -> SolverStage b -> SolverStage a
<$ :: forall a b. a -> SolverStage b -> SolverStage a
Functor )

instance Applicative SolverStage where
  pure :: forall a. a -> SolverStage a
pure a
x = TcS (StopOrContinue a) -> SolverStage a
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (StopOrContinue a -> TcS (StopOrContinue a)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> StopOrContinue a
forall a. a -> StopOrContinue a
ContinueWith a
x))
  <*> :: forall a b. SolverStage (a -> b) -> SolverStage a -> SolverStage b
(<*>)  = SolverStage (a -> b) -> SolverStage a -> SolverStage b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad SolverStage where
  return :: forall a. a -> SolverStage a
return          = a -> SolverStage a
forall a. a -> SolverStage a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  (Stage TcS (StopOrContinue a)
m) >>= :: forall a b. SolverStage a -> (a -> SolverStage b) -> SolverStage b
>>= a -> SolverStage b
k = TcS (StopOrContinue b) -> SolverStage b
TcS (StopOrContinue b) -> SolverStage b
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue b) -> SolverStage b)
-> TcS (StopOrContinue b) -> SolverStage b
forall a b. (a -> b) -> a -> b
$
                    do { soc <- TcS (StopOrContinue a)
m
                       ; case soc of
                           StartAgain Ct
x   -> StopOrContinue b -> TcS (StopOrContinue b)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ct -> StopOrContinue b
forall a. Ct -> StopOrContinue a
StartAgain Ct
x)
                           Stop CtEvidence
ev SDoc
d      -> StopOrContinue b -> TcS (StopOrContinue b)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> SDoc -> StopOrContinue b
forall a. CtEvidence -> SDoc -> StopOrContinue a
Stop CtEvidence
ev SDoc
d)
                           ContinueWith a
x -> SolverStage b -> TcS (StopOrContinue b)
forall a. SolverStage a -> TcS (StopOrContinue a)
runSolverStage (a -> SolverStage b
k a
x) }

nopStage :: a -> SolverStage a
nopStage :: forall a. a -> SolverStage a
nopStage a
res = TcS (StopOrContinue a) -> SolverStage a
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (a -> TcS (StopOrContinue a)
forall a. a -> TcS (StopOrContinue a)
continueWith a
res)

simpleStage :: TcS a -> SolverStage a
-- Always does a ContinueWith; no Stop or StartAgain
simpleStage :: forall a. TcS a -> SolverStage a
simpleStage TcS a
thing = TcS (StopOrContinue a) -> SolverStage a
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (do { res <- TcS a
thing; continueWith res })

startAgainWith :: Ct -> TcS (StopOrContinue a)
startAgainWith :: forall a. Ct -> TcS (StopOrContinue a)
startAgainWith Ct
ct = StopOrContinue a -> TcS (StopOrContinue a)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ct -> StopOrContinue a
forall a. Ct -> StopOrContinue a
StartAgain Ct
ct)

continueWith :: a -> TcS (StopOrContinue a)
continueWith :: forall a. a -> TcS (StopOrContinue a)
continueWith a
ct = StopOrContinue a -> TcS (StopOrContinue a)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> StopOrContinue a
forall a. a -> StopOrContinue a
ContinueWith a
ct)

stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
stopWith :: forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
s = StopOrContinue a -> TcS (StopOrContinue a)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> SDoc -> StopOrContinue a
forall a. CtEvidence -> SDoc -> StopOrContinue a
Stop CtEvidence
ev (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
s))

stopWithStage :: CtEvidence -> String -> SolverStage a
stopWithStage :: forall a. CtEvidence -> String -> SolverStage a
stopWithStage CtEvidence
ev String
s = TcS (StopOrContinue a) -> SolverStage a
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (CtEvidence -> String -> TcS (StopOrContinue a)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
s)


{- *********************************************************************
*                                                                      *
                   Inert instances: inert_qcis
*                                                                      *
********************************************************************* -}

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

       -- Update given equalities. C.f updateGivenEqs
       ; tclvl <- getTcLevel
       ; let body_pred    = QCInst -> Type
qci_body QCInst
new_qci
             not_equality = Type -> Bool
isClassPred Type
body_pred Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isEqClassPred Type
body_pred)
                  -- True <=> definitely not an equality
                  -- A qci_body like (f a) might be an equality

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

       ; setInertCans 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_qcis :: InertCans -> [QCInst]
inert_qcis = [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 a. a -> TcS a
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 a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (InertCans
ics { inert_qcis = new_qci : qcis }) }

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

{- Note [Do not add duplicate quantified instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As an optimisation, we avoid adding duplicate quantified instances to the
inert set; we use a simple duplicate check using tcEqType for simplicity,
even though it doesn't account for superficial differences, e.g. it will count
the following two constraints as different (#22223):

  - forall a b. C a b
  - forall b a. C a b

The main logic that allows us to pick local instances, even in the presence of
duplicates, is explained in Note [Use only the best matching quantified constraint]
in GHC.Tc.Solver.Dict.
-}

updInertDicts :: DictCt -> TcS ()
updInertDicts :: DictCt -> TcS ()
updInertDicts DictCt
dict_ct
  = do { String -> SDoc -> TcS ()
traceTcS String
"Adding inert dict" (DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_ct)

       -- For Given implicit parameters (only), delete any existing
       -- Givens for the same implicit parameter.
       -- See Note [Shadowing of implicit parameters]
       ; DictCt -> TcS ()
deleteGivenIPs DictCt
dict_ct

       -- Add the new constraint to the inert set
       ; (InertCans -> InertCans) -> TcS ()
updInertCans ((DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans
updDicts (DictCt -> DictMap DictCt -> DictMap DictCt
addDict DictCt
dict_ct)) }

deleteGivenIPs :: DictCt -> TcS ()
-- Special magic when adding a Given implicit parameter to the inert set
-- For [G] ?x::ty, remove any existing /Givens/ mentioning ?x,
--    from /both/ inert_cans /and/ inert_solved_dicts (#23761)
-- See Note [Shadowing of implicit parameters]
deleteGivenIPs :: DictCt -> TcS ()
deleteGivenIPs (DictCt { di_cls :: DictCt -> Class
di_cls = Class
cls, di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys })
  | CtEvidence -> Bool
isGiven CtEvidence
ev
  , Just (Type
str_ty, Type
_) <- Class -> [Type] -> Maybe (Type, Type)
isIPPred_maybe Class
cls [Type]
tys
  = (InertSet -> InertSet) -> TcS ()
updInertSet ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ inerts :: InertSet
inerts@(IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
ics, inert_solved_dicts :: InertSet -> DictMap DictCt
inert_solved_dicts = DictMap DictCt
solved }) ->
    InertSet
inerts { inert_cans         = updDicts (filterDicts (keep_can str_ty)) ics
           , inert_solved_dicts = filterDicts (keep_solved str_ty) solved }
  | Bool
otherwise
  = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    keep_can, keep_solved :: Type -> DictCt -> Bool
    -- keep_can: we keep an inert dictionary UNLESS
    --   (1) it is a Given
    --   (2) it binds an implicit parameter (?str :: ty) for the given 'str'
    --       regardless of 'ty', possibly via its superclasses
    -- The test is a bit conservative, hence `mightMentionIP` and `typesAreApart`
    -- See Note [Using typesAreApart when calling mightMentionIP]
    -- in GHC.Core.Predicate
    --
    -- keep_solved: same as keep_can, but for /all/ constraints not just Givens
    --
    -- Why two functions?  See (SIP3) in Note [Shadowing of implicit parameters]
    keep_can :: Type -> DictCt -> Bool
keep_can Type
str (DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev, di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys })
      = Bool -> Bool
not (CtEvidence -> Bool
isGiven CtEvidence
ev                -- (1)
          Bool -> Bool -> Bool
&& Type -> Class -> [Type] -> Bool
mentions_ip Type
str Class
cls [Type]
tys)  -- (2)
    keep_solved :: Type -> DictCt -> Bool
keep_solved Type
str (DictCt { di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys })
      = Bool -> Bool
not (Type -> Class -> [Type] -> Bool
mentions_ip Type
str Class
cls [Type]
tys)

    -- mentions_ip: the inert constraint might provide evidence
    -- for an implicit parameter (?str :: ty) for the given 'str'
    mentions_ip :: Type -> Class -> [Type] -> Bool
mentions_ip Type
str Class
cls [Type]
tys
      = (Type -> Bool) -> (Type -> Bool) -> Class -> [Type] -> Bool
mightMentionIP (Bool -> Bool
not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type -> Bool
typesAreApart Type
str) (Bool -> Type -> Bool
forall a b. a -> b -> a
const Bool
True) Class
cls [Type]
tys

updInertIrreds :: IrredCt -> TcS ()
updInertIrreds :: IrredCt -> TcS ()
updInertIrreds IrredCt
irred
  = do { tc_lvl <- TcS TcLevel
getTcLevel
       ; updInertCans $ addIrredToCans tc_lvl irred }

{- *********************************************************************
*                                                                      *
                  Kicking out
*                                                                      *
************************************************************************
-}

{- Note [Kick out after filling a coercion hole]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we solve `kco` and have `co` in the inert set whose rewriter-set includes `kco`,
we should kick out `co` so that we can now unify it, which might unlock other stuff.
See Note [Unify only if the rewriter set is empty] in GHC.Tc.Solver.Equality for
why solving `kco` might unlock `co`, especially (URW2).

Hence `kickOutAfterFillingCoercionHole`.  It looks at inert constraints that are
  * Wanted
  * Of the form  alpha ~ rhs, where alpha is a unification variable
and kicks out any that will have an empty rewriter set after filling the hole.

Wrinkles:
(KOC1) If co's rewriter-set is {kco, xco}, there is no point in kicking it out,
       because it still can't be unified.  So we only kick out if the co's
       rewriter-set becomes empty.

(KOC2) `kco` might itself have a rewriter set.  This is fairly common.  E.g.
               kco : a[sk] ~ beta[tau]
       Assuming we can't unify it for some reason, we may swap that over to give
               kco2 : beta[tau] ~ a[sk]      kco := sym kco2
       So `kco` is "solved" but the coercion that solves it has free coercion holes!
       So rather than kick out `co`, we should just change its rewriter-set to depend
       on `kco2` instead of `kco`.  Hence the `new_holes` passed to
       `kickOutAfterFillingCoercionHole`

(KOC3) It's possible that this could just go ahead and unify, but could there
       be occurs-check problems? Seems simpler just to kick out.

(KOC4) Kick-out is undesirable, so it'd be better to solve `kco` before `co`.  So
       the solver prioritises equalities with an empty rewriter set, to try to
       avoid unnecessary kick-out.  See GHC.Tc.Types.Constraint
       Note [Prioritise Wanteds with empty CoHoleSet] esp (PER1)
-}

kickOutRewritable  :: KickOutSpec -> CtFlavourRole -> TcS ()
kickOutRewritable :: KickOutSpec -> CtFlavourRole -> TcS ()
kickOutRewritable KickOutSpec
ko_spec CtFlavourRole
new_fr
  = do { ics <- TcS InertCans
getInertCans
       ; let (kicked_out, ics') = kickOutRewritableLHS ko_spec new_fr ics
             n_kicked = Cts -> Int
forall a. Bag a -> Int
lengthBag Cts
kicked_out
       ; setInertCans ics'

       ; unless (isEmptyBag kicked_out) $
         do { emitWork 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 = (Ct -> VarSet -> VarSet) -> VarSet -> Cts -> VarSet
forall a b. (a -> b -> b) -> b -> Bag a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> VarSet -> VarSet
add_one VarSet
emptyVarSet Cts
kicked_out
                  add_one :: Ct -> VarSet -> VarSet
                  add_one Ct
ct VarSet
vs | CtGiven (GivenCt { ctev_evar :: GivenCtEvidence -> TcTyVar
ctev_evar = TcTyVar
ev_var }) <- Ct -> CtEvidence
ctEvidence Ct
ct
                                = VarSet
vs VarSet -> TcTyVar -> VarSet
`extendVarSet` TcTyVar
ev_var
                                | Bool
otherwise = VarSet
vs

            ; when (new_fr `eqCanRewriteFR` (Given, NomEq) &&
                   -- if this isn't true, no use looking through the constraints
                    not (isEmptyVarSet kicked_given_ev_vars)) $
              do { traceTcS "Given(s) have been kicked out; drop from famapp-cache"
                            (ppr kicked_given_ev_vars)
                 ; dropFromFamAppCache kicked_given_ev_vars }

            ; csTraceTcS $
              hang (text "Kick out")
                 2 (vcat [ text "n-kicked =" <+> int n_kicked
                         , text "kicked_out =" <+> ppr kicked_out
                         , text "Residual inerts =" <+> ppr ics' ]) } }

kickOutAfterUnification :: TcTyVarSet -> TcS ()
kickOutAfterUnification :: VarSet -> TcS ()
kickOutAfterUnification VarSet
tv_set
  | VarSet -> Bool
isEmptyVarSet VarSet
tv_set
  = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = do { n_kicked <- KickOutSpec -> CtFlavourRole -> TcS ()
kickOutRewritable (VarSet -> KickOutSpec
KOAfterUnify VarSet
tv_set) (CtFlavour
Given, EqRel
NomEq)
                     -- Given because the tv := xi is given; NomEq because
                     -- only nominal equalities are solved by unification
       ; traceTcS "kickOutAfterUnification" (ppr tv_set $$ text "n_kicked =" <+> ppr n_kicked)
       ; return n_kicked }

kickOutAfterFillingCoercionHole :: CoercionHole -> CoercionPlusHoles -> TcS ()
-- See Note [Kick out after filling a coercion hole]
kickOutAfterFillingCoercionHole :: CoercionHole -> CoercionPlusHoles -> TcS ()
kickOutAfterFillingCoercionHole CoercionHole
hole (CPH { cph_holes :: CoercionPlusHoles -> CoHoleSet
cph_holes = CoHoleSet
new_holes })
  = do { ics <- TcS InertCans
getInertCans
       ; let (kicked_out, ics') = kick_out ics
             n_kicked           = [EqCt] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [EqCt]
kicked_out

       ; unless (n_kicked == 0) $
         do { updWorkListTcS (extendWorkListRewrittenEqs kicked_out)
            ; csTraceTcS $
              hang (text "Kick out, hole =" <+> ppr hole)
                 2 (vcat [ text "n-kicked =" <+> int n_kicked
                         , text "kicked_out =" <+> ppr kicked_out
                         , text "Residual inerts =" <+> ppr ics' ]) }

       ; setInertCans ics' }
  where
    kick_out :: InertCans -> ([EqCt], InertCans)
    kick_out :: InertCans -> ([EqCt], InertCans)
kick_out ics :: InertCans
ics@(IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs })
      = ([EqCt]
eqs_to_kick, InertCans
ics { inert_eqs = eqs_to_keep })
      where
        ([EqCt]
eqs_to_kick, InertEqs
eqs_to_keep) = (EqCt -> Either EqCt EqCt) -> InertEqs -> ([EqCt], InertEqs)
transformAndPartitionTyVarEqs EqCt -> Either EqCt EqCt
kick_out_eq InertEqs
eqs

    kick_out_eq :: EqCt -> Either EqCt EqCt
    kick_out_eq :: EqCt -> Either EqCt EqCt
kick_out_eq eq_ct :: EqCt
eq_ct@(EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ev, eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs })
      | CtWanted (wev :: WantedCtEvidence
wev@(WantedCt { ctev_rewriters :: WantedCtEvidence -> CoHoleSet
ctev_rewriters = CoHoleSet
rewriters })) <- CtEvidence
ev
      , TyVarLHS TcTyVar
tv <- CanEqLHS
lhs
      , TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
      , CoercionHole
hole CoercionHole -> CoHoleSet -> Bool
`elemCoHoleSet` CoHoleSet
rewriters
      , let holes' :: CoHoleSet
holes' = (CoHoleSet
rewriters CoHoleSet -> CoercionHole -> CoHoleSet
`delCoHoleSet` CoercionHole
hole) CoHoleSet -> CoHoleSet -> CoHoleSet
forall a. Monoid a => a -> a -> a
`mappend` CoHoleSet
new_holes
                     -- Adding new_holes and deleting hole: see (KOC2)
            eq_ct' :: EqCt
eq_ct' = EqCt
eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = holes' }) }
      = if CoHoleSet -> Bool
isEmptyCoHoleSet CoHoleSet
holes'
        then EqCt -> Either EqCt EqCt
forall a b. a -> Either a b
Left EqCt
eq_ct'    -- Kick out, if new rewriter set is empty (KOC1)
        else EqCt -> Either EqCt EqCt
forall a b. b -> Either a b
Right EqCt
eq_ct'   -- Keep, but with trimmed holes see (KOC2)
      | Bool
otherwise
      = EqCt -> Either EqCt EqCt
forall a b. b -> Either a b
Right EqCt
eq_ct

--------------
insertSafeOverlapFailureTcS :: InstanceWhat -> DictCt -> TcS ()
-- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
insertSafeOverlapFailureTcS :: InstanceWhat -> DictCt -> TcS ()
insertSafeOverlapFailureTcS InstanceWhat
what DictCt
item
  | InstanceWhat -> Bool
safeOverlap InstanceWhat
what
  = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = (InertSet -> InertSet) -> TcS ()
updInertSet (\InertSet
is -> InertSet
is { inert_safehask = addDict item (inert_safehask is) })

getSafeOverlapFailures :: TcS (Bag DictCt)
-- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
getSafeOverlapFailures :: TcS (Bag DictCt)
getSafeOverlapFailures
 = do { IS { inert_safehask = safehask } <- TcS InertSet
getInertSet
      ; return $ foldDicts consBag safehask emptyBag }

--------------
updSolvedDicts :: InstanceWhat -> DictCt -> TcS ()
-- Conditionally add a new item in the solved set of the monad
-- See Note [Solved dictionaries] in GHC.Tc.Solver.InertSet
updSolvedDicts :: InstanceWhat -> DictCt -> TcS ()
updSolvedDicts InstanceWhat
what dict_ct :: DictCt
dict_ct@(DictCt { di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys, di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev })
  | CtEvidence -> Bool
isWanted CtEvidence
ev
  , InstanceWhat -> Bool
instanceReturnsDictCon InstanceWhat
what
  = do { is_callstack    <- (Type -> Bool) -> Name -> TcS (Type -> Bool)
is_tyConTy Type -> Bool
isCallStackTy        Name
callStackTyConName
       ; is_exceptionCtx <- is_tyConTy isExceptionContextTy exceptionContextTyConName
       ; let contains_callstack_or_exceptionCtx =
               (Type -> Bool) -> (Type -> Bool) -> Class -> [Type] -> Bool
mightMentionIP
                 (Bool -> Type -> Bool
forall a b. a -> b -> a
const Bool
True)
                    -- NB: the name of the call-stack IP is irrelevant
                    -- e.g (?foo :: CallStack) counts!
                 (Type -> Bool
is_callstack (Type -> Bool) -> (Type -> Bool) -> Type -> Bool
forall (f :: * -> *). Applicative f => f Bool -> f Bool -> f Bool
<||> Type -> Bool
is_exceptionCtx)
                 Class
cls [Type]
tys
       -- See Note [Don't add HasCallStack constraints to the solved set]
       ; unless contains_callstack_or_exceptionCtx $
    do { traceTcS "updSolvedDicts:" $ ppr dict_ct
       ; updInertSet $ \ InertSet
ics ->
           InertSet
ics { inert_solved_dicts = addSolvedDict dict_ct (inert_solved_dicts ics) }
       } }
  | Bool
otherwise
  = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where

    -- Return a predicate that decides whether a type is CallStack
    -- or ExceptionContext, accounting for e.g. type family reduction, as
    -- per Note [Using typesAreApart when calling mightMentionIP].
    --
    -- See Note [Using isCallStackTy in mightMentionIP].
    is_tyConTy :: (Type -> Bool) -> Name -> TcS (Type -> Bool)
    is_tyConTy :: (Type -> Bool) -> Name -> TcS (Type -> Bool)
is_tyConTy Type -> Bool
is_eq Name
tc_name
      = do { (mb_tc, _) <- TcM (Maybe TyCon, Messages TcRnMessage)
-> TcS (Maybe TyCon, Messages TcRnMessage)
forall a. TcM a -> TcS a
wrapTcS (TcM (Maybe TyCon, Messages TcRnMessage)
 -> TcS (Maybe TyCon, Messages TcRnMessage))
-> TcM (Maybe TyCon, Messages TcRnMessage)
-> TcS (Maybe TyCon, Messages TcRnMessage)
forall a b. (a -> b) -> a -> b
$ TcRn TyCon -> TcM (Maybe TyCon, Messages TcRnMessage)
forall a. TcRn a -> TcRn (Maybe a, Messages TcRnMessage)
TcM.tryTc (TcRn TyCon -> TcM (Maybe TyCon, Messages TcRnMessage))
-> TcRn TyCon -> TcM (Maybe TyCon, Messages TcRnMessage)
forall a b. (a -> b) -> a -> b
$ Name -> TcRn TyCon
TcM.tcLookupTyCon Name
tc_name
           ; case mb_tc of
              Just TyCon
tc ->
                (Type -> Bool) -> TcS (Type -> Bool)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type -> Bool) -> TcS (Type -> Bool))
-> (Type -> Bool) -> TcS (Type -> Bool)
forall a b. (a -> b) -> a -> b
$ \ Type
ty -> Bool -> Bool
not (Type -> Type -> Bool
typesAreApart Type
ty (TyCon -> Type
mkTyConTy TyCon
tc))
              Maybe TyCon
Nothing ->
                (Type -> Bool) -> TcS (Type -> Bool)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Type -> Bool
is_eq
           }

{- Note [Don't add HasCallStack constraints to the solved set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We must not add solved Wanted dictionaries that mention HasCallStack constraints
to the solved set, or we might fail to accumulate the proper call stack, as was
reported in #25529.

Recall that HasCallStack constraints (and the related HasExceptionContext
constraints) are implicit parameter constraints, and are accumulated as per
Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence.

When we solve a Wanted that contains a HasCallStack constraint, we don't want
to cache the result, because re-using that solution means re-using the call-stack
in a different context!

See also Note [Shadowing of implicit parameters], which deals with a similar
problem with Given implicit parameter constraints.

Note [Using isCallStackTy in mightMentionIP]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
To implement Note [Don't add HasCallStack constraints to the solved set],
we need to check whether a constraint contains a HasCallStack or HasExceptionContext
constraint. We do this using the 'mentionsIP' function, but as per
Note [Using typesAreApart when calling mightMentionIP] we don't want to simply do:

  mightMentionIP
    (const True) -- (ignore the implicit parameter string)
    (isCallStackTy <||> isExceptionContextTy)

because this does not account for e.g. a type family that reduces to CallStack.
The predicate we want to use instead is:

    \ ty -> not (typesAreApart ty callStackTy && typesAreApart ty exceptionContextTy)

However, this is made difficult by the fact that CallStack and ExceptionContext
are not wired-in types; they are only known-key. This means we must look them
up using 'tcLookupTyCon'. However, this might fail, e.g. if we are in the middle
of typechecking ghc-internal and these data-types have not been typechecked yet!

In that case, we simply fall back to the naive 'isCallStackTy'/'isExceptionContextTy'
logic.

Note that it would be somewhat painful to wire-in ExceptionContext: at the time
of writing (March 2025), this would require wiring in the ExceptionAnnotation
class, as well as SomeExceptionAnnotation, which is a data type with existentials.
-}

getSolvedDicts :: TcS (DictMap DictCt)
getSolvedDicts :: TcS (DictMap DictCt)
getSolvedDicts = do { ics <- TcS InertSet
getInertSet; return (inert_solved_dicts ics) }

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

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

updInertSet :: (InertSet -> InertSet) -> TcS ()
-- Modify the inert set with the supplied function
updInertSet :: (InertSet -> InertSet) -> TcS ()
updInertSet InertSet -> InertSet
upd_fn
  = do { is_var <- TcS (IORef InertSet)
getInertSetRef
       ; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
                     ; TcM.writeTcRef is_var (upd_fn curr_inert) }) }

getInertCans :: TcS InertCans
getInertCans :: TcS InertCans
getInertCans = do { inerts <- TcS InertSet
getInertSet; return (inert_cans inerts) }

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

updRetInertCans :: (InertCans -> (a, InertCans)) -> TcS a
-- Modify the inert set with the supplied function
updRetInertCans :: forall a. (InertCans -> (a, InertCans)) -> TcS a
updRetInertCans InertCans -> (a, InertCans)
upd_fn
  = do { is_var <- TcS (IORef InertSet)
getInertSetRef
       ; wrapTcS (do { inerts <- TcM.readTcRef is_var
                     ; let (res, cans') = upd_fn (inert_cans inerts)
                     ; TcM.writeTcRef is_var (inerts { inert_cans = cans' })
                     ; return 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 ()
updInertSet ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ InertSet
inerts -> InertSet
inerts { inert_cans = upd_fn (inert_cans inerts) }

getInertEqs :: TcS InertEqs
getInertEqs :: TcS InertEqs
getInertEqs = do { inert <- TcS InertCans
getInertCans; return (inert_eqs inert) }

getInnermostGivenEqLevel :: TcS TcLevel
getInnermostGivenEqLevel :: TcS TcLevel
getInnermostGivenEqLevel = do { inert <- TcS InertCans
getInertCans
                              ; return (inert_given_eq_lvl inert) }

-- | Retrieves all insoluble constraints from the inert set,
-- specifically including Given constraints.
--
-- This consists of:
--
--  - insoluble equalities, such as @Int ~# Bool@;
--  - constraints that are custom type errors, of the form
--    @TypeError msg@ or @Maybe (TypeError msg)@, but not constraints such as
--    @F x (TypeError msg)@ in which the type error is nested under
--    a type family application,
--  - unsatisfiable constraints, of the form @Unsatisfiable msg@.
--
-- The inclusion of Givens is important for pattern match warnings, as we
-- want to consider a pattern match that introduces insoluble Givens to be
-- redundant (see Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver).
getInertInsols :: TcS Cts
getInertInsols :: TcS Cts
getInertInsols
  -- See Note [When is a constraint insoluble?]
  = do { inert_cts <- TcS Cts
getInertCts
       ; return $ filterBag insolubleCt inert_cts }

getInertCts :: TcS Cts
getInertCts :: TcS Cts
getInertCts
  = do { inerts <- TcS InertCans
getInertCans
       ; return $
          unionManyBags
            [ fmap CIrredCan $ inert_irreds inerts
            , foldDicts  (consBag . CDictCan) (inert_dicts  inerts) emptyBag
            , foldFunEqs (consBag . CEqCan  ) (inert_funeqs inerts) emptyBag
            , foldTyEqs  (consBag . CEqCan  ) (inert_eqs    inerts) emptyBag
            ] }

getInertGivens :: TcS [Ct]
-- Returns the Given constraints in the inert set
getInertGivens :: TcS [Ct]
getInertGivens
  = do { all_cts <- TcS Cts
getInertCts
       ; return (filter isGivenCt $ bagToList all_cts) }

getPendingGivenScs :: TcS [Ct]
-- Find all inert Given dictionaries, or quantified constraints, such that
--     1. cc_pend_sc flag has fuel strictly > 0
--     2. belongs to the current level
-- For each such dictionary:
-- * Return it (with unmodified cc_pend_sc) in sc_pending
-- * Modify the dict in the inert set to have cc_pend_sc = doNotExpand
--   to record that we have expanded superclasses for this dict
getPendingGivenScs :: TcS [Ct]
getPendingGivenScs = do { lvl <- TcS TcLevel
getTcLevel
                        ; updRetInertCans (get_sc_pending 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 DictCt
inert_dicts = DictMap DictCt
dicts, inert_qcis :: InertCans -> [QCInst]
inert_qcis = [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 = dicts', inert_qcis = insts' })
  where
    sc_pending :: [Ct]
sc_pending = [Ct]
sc_pend_insts [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ (DictCt -> Ct) -> [DictCt] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map DictCt -> Ct
DictCt -> Ct
CDictCan [DictCt]
sc_pend_dicts

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

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

    exhaustAndAdd :: DictCt -> DictMap DictCt -> DictMap DictCt
    exhaustAndAdd :: DictCt -> DictMap DictCt -> DictMap DictCt
exhaustAndAdd DictCt
ct DictMap DictCt
dicts = DictCt -> DictMap DictCt -> DictMap DictCt
addDict (DictCt
ct {di_pend_sc = doNotExpand}) DictMap DictCt
dicts
    -- Exhaust the fuel for this constraint before adding it as
    -- we don't want to expand these constraints again

    get_pending :: DictCt -> [DictCt] -> [DictCt]  -- Get dicts with cc_pend_sc > 0
    get_pending :: DictCt -> [DictCt] -> [DictCt]
get_pending DictCt
dict [DictCt]
dicts
        | DictCt -> Bool
isPendingScDictCt DictCt
dict
        , CtEvidence -> Bool
belongs_to_this_level (DictCt -> CtEvidence
dictCtEvidence DictCt
dict)
        = DictCt
dict DictCt -> [DictCt] -> [DictCt]
forall a. a -> [a] -> [a]
: [DictCt]
dicts
        | Bool
otherwise
        = [DictCt]
dicts

    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
pendingScInst_maybe 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')
       -- qci' have their fuel exhausted
       -- we don't want to expand these constraints again
       -- qci is expanded
       | 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
`sameDepthAs` TcLevel
this_lvl
    -- We only want Givens from this level; see (3a) in
    -- Note [The superclass story] in GHC.Tc.Solver.Dict

getUnsolvedInerts :: TcS Cts    -- All simple constraints
-- Return all the unsolved [Wanted] 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 Cts
getUnsolvedInerts
 = do { IC { inert_eqs    = tv_eqs
           , inert_funeqs = fun_eqs
           , inert_irreds = irreds
           , inert_dicts  = idicts
           , inert_qcis   = qcis
           } <- TcS InertCans
getInertCans

      ; let unsolved_tv_eqs  = (EqCt -> Cts -> Cts) -> InertEqs -> Cts -> Cts
forall b. (EqCt -> b -> b) -> InertEqs -> b -> b
foldTyEqs  ((EqCt -> Ct) -> EqCt -> Cts -> Cts
forall a. (a -> Ct) -> a -> Cts -> Cts
add_if_unsolved EqCt -> Ct
EqCt -> Ct
CEqCan)    InertEqs
tv_eqs Cts
emptyCts
            unsolved_fun_eqs = (EqCt -> Cts -> Cts) -> FunEqMap [EqCt] -> Cts -> Cts
forall b. (EqCt -> b -> b) -> FunEqMap [EqCt] -> b -> b
foldFunEqs ((EqCt -> Ct) -> EqCt -> Cts -> Cts
forall a. (a -> Ct) -> a -> Cts -> Cts
add_if_unsolved EqCt -> Ct
EqCt -> Ct
CEqCan)    FunEqMap [EqCt]
fun_eqs Cts
emptyCts
            unsolved_irreds  = (IrredCt -> Cts -> Cts) -> Cts -> Bag IrredCt -> Cts
forall a b. (a -> b -> b) -> b -> Bag a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr      ((IrredCt -> Ct) -> IrredCt -> Cts -> Cts
forall a. (a -> Ct) -> a -> Cts -> Cts
add_if_unsolved IrredCt -> Ct
IrredCt -> Ct
CIrredCan) Cts
emptyCts Bag IrredCt
irreds
            unsolved_dicts   = (DictCt -> Cts -> Cts) -> DictMap DictCt -> Cts -> Cts
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts  ((DictCt -> Ct) -> DictCt -> Cts -> Cts
forall a. (a -> Ct) -> a -> Cts -> Cts
add_if_unsolved DictCt -> Ct
DictCt -> Ct
CDictCan)  DictMap DictCt
idicts Cts
emptyCts
            unsolved_qcis    = (QCInst -> Cts -> Cts) -> Cts -> [QCInst] -> Cts
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr      ((QCInst -> Ct) -> QCInst -> Cts -> Cts
forall a. (a -> Ct) -> a -> Cts -> Cts
add_if_unsolved QCInst -> Ct
QCInst -> Ct
CQuantCan) Cts
emptyCts [QCInst]
qcis

      ; traceTcS "getUnsolvedInerts" $
        vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs
             , text "fun eqs =" <+> ppr unsolved_fun_eqs
             , text "dicts =" <+> ppr unsolved_dicts
             , text "irreds =" <+> ppr unsolved_irreds ]

      ; return ( unsolved_tv_eqs  `unionBags`
                 unsolved_fun_eqs `unionBags`
                 unsolved_irreds  `unionBags`
                 unsolved_dicts   `unionBags`
                 unsolved_qcis ) }
  where
    add_if_unsolved :: (a -> Ct) -> a -> Cts -> Cts
    add_if_unsolved :: forall a. (a -> Ct) -> a -> Cts -> Cts
add_if_unsolved a -> Ct
mk_ct a
thing Cts
cts
      | Ct -> Bool
isWantedCt Ct
ct = Ct
ct Ct -> Cts -> Cts
`consCts` Cts
cts
      | Bool
otherwise     = Cts
cts
      where
        ct :: Ct
ct = a -> Ct
mk_ct a
thing


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

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

       ; traceTcS "getHasGivenEqs" $
         vcat [ text "given_eqs:" <+> ppr given_eqs
              , text "ge_lvl:" <+> ppr ge_lvl
              , text "ambient level:" <+> ppr tclvl
              , text "Inerts:" <+> ppr inerts
              , text "Insols:" <+> ppr given_insols]
       ; return (has_ge, given_insols) }
  where
    insoluble_given_equality :: IrredCt -> Bool
    -- Check for unreachability; specifically do not include UserError/Unsatisfiable
    insoluble_given_equality :: IrredCt -> Bool
insoluble_given_equality (IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev, ir_reason :: IrredCt -> CtIrredReason
ir_reason = CtIrredReason
reason })
       = CtIrredReason -> Bool
isInsolubleReason CtIrredReason
reason Bool -> Bool -> Bool
&& CtEvidence -> Bool
isGiven CtEvidence
ev

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 b a. (b -> a -> b) -> b -> [a] -> b
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 DictCt
dict_ct -> InertCans
is { inert_dicts = delDict dict_ct (inert_dicts is) }
      CEqCan    EqCt
eq_ct  -> EqCt -> InertCans -> InertCans
delEq    EqCt
eq_ct InertCans
is
      CIrredCan IrredCt
ir_ct  -> IrredCt -> InertCans -> InertCans
delIrred IrredCt
ir_ct InertCans
is
      CQuantCan {}     -> String -> InertCans
forall a. HasCallStack => String -> a
panic String
"removeInertCt: CQuantCan"
      CNonCanonical {} -> String -> InertCans
forall a. HasCallStack => String -> a
panic String
"removeInertCt: CNonCanonical"

-- | Looks up a family application in the inerts.
lookupFamAppInert :: (CtFlavourRole -> Bool)  -- can it rewrite the target?
                  -> TyCon -> [Type] -> TcS (Maybe EqCt)
lookupFamAppInert :: (CtFlavourRole -> Bool) -> TyCon -> [Type] -> TcS (Maybe EqCt)
lookupFamAppInert CtFlavourRole -> Bool
rewrite_pred TyCon
fam_tc [Type]
tys
  = do { IS { inert_cans = IC { inert_funeqs = inert_funeqs } } <- TcS InertSet
getInertSet
       ; return (lookup_inerts inert_funeqs) }
  where
    lookup_inerts :: FunEqMap [EqCt] -> Maybe EqCt
lookup_inerts FunEqMap [EqCt]
inert_funeqs
      = case FunEqMap [EqCt] -> TyCon -> [Type] -> Maybe [EqCt]
forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq FunEqMap [EqCt]
inert_funeqs TyCon
fam_tc [Type]
tys of
          Maybe [EqCt]
Nothing              -> Maybe EqCt
forall a. Maybe a
Nothing
          Just ([EqCt]
ecl :: [EqCt]) -> (EqCt -> Bool) -> [EqCt] -> Maybe EqCt
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (CtFlavourRole -> Bool
rewrite_pred (CtFlavourRole -> Bool) -> (EqCt -> CtFlavourRole) -> EqCt -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EqCt -> CtFlavourRole
eqCtFlavourRole) [EqCt]
ecl

---------------------------
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe Reduction)
lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe Reduction)
lookupFamAppCache TyCon
fam_tc [Type]
tys
  = do { IS { inert_famapp_cache = famapp_cache } <- TcS InertSet
getInertSet
       ; case findFunEq famapp_cache fam_tc tys of
           result :: Maybe Reduction
result@(Just Reduction
redn) ->
             do { String -> SDoc -> TcS ()
traceTcS String
"famapp_cache hit" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
tys)
                                                    , Reduction -> SDoc
forall a. Outputable a => a -> SDoc
ppr Reduction
redn ])
                ; Maybe Reduction -> TcS (Maybe Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Reduction
result }
           Maybe Reduction
Nothing -> Maybe Reduction -> TcS (Maybe Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Reduction
forall a. Maybe a
Nothing }

extendFamAppCache :: TyCon -> [Type] -> Reduction -> TcS ()
-- NB: co :: rhs ~ F tys, to match expectations of rewriter
extendFamAppCache :: TyCon -> [Type] -> Reduction -> TcS ()
extendFamAppCache TyCon
tc [Type]
xi_args stuff :: Reduction
stuff@(Reduction Coercion
_ Type
ty)
  = do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; when (gopt Opt_FamAppCache dflags) $
    do { traceTcS "extendFamAppCache" (vcat [ ppr tc <+> ppr xi_args
                                            , ppr ty ])
       ; updInertSet $ \ is :: InertSet
is@(IS { inert_famapp_cache :: InertSet -> FunEqMap Reduction
inert_famapp_cache = FunEqMap Reduction
fc }) ->
            InertSet
is { inert_famapp_cache = insertFunEq fc tc xi_args stuff } } }

-- Remove entries from the cache whose evidence mentions variables in the
-- supplied set
dropFromFamAppCache :: VarSet -> TcS ()
dropFromFamAppCache :: VarSet -> TcS ()
dropFromFamAppCache VarSet
varset
  = (InertSet -> InertSet) -> TcS ()
updInertSet (\inerts :: InertSet
inerts@(IS { inert_famapp_cache :: InertSet -> FunEqMap Reduction
inert_famapp_cache = FunEqMap Reduction
famapp_cache }) ->
                   InertSet
inerts { inert_famapp_cache = filterTcAppMap check famapp_cache })
  where
    check :: Reduction -> Bool
    check :: Reduction -> Bool
check Reduction
redn
      = Bool -> Bool
not ((TcTyVar -> Bool) -> Coercion -> Bool
anyFreeVarsOfCo (TcTyVar -> VarSet -> Bool
`elemVarSet` VarSet
varset) (Coercion -> Bool) -> Coercion -> Bool
forall a b. (a -> b) -> a -> b
$ Reduction -> Coercion
reductionCoercion Reduction
redn)

{-
************************************************************************
*                                                                      *
*              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.
-}

-- | The mode for the constraint solving monad.
data TcSMode
  = TcSMode -- See Note [TcSMode], where each field is documented
            { TcSMode -> Bool
tcsmResumable        :: Bool
                   -- ^ Do not restore type-equality cycles
            , TcSMode -> Bool
tcsmEarlyAbort       :: Bool
                   -- ^ Abort early on insoluble constraints
            , TcSMode -> Bool
tcsmSkipOverlappable :: Bool
                   -- ^ Do not select an OVERLAPPABLE instance
            , TcSMode -> Bool
tcsmFullySolveQCIs   :: Bool
                   -- ^ Fully solve quantified constraints
            }

vanillaTcSMode :: TcSMode
vanillaTcSMode :: TcSMode
vanillaTcSMode = TcSMode { tcsmResumable :: Bool
tcsmResumable        = Bool
False
                         , tcsmEarlyAbort :: Bool
tcsmEarlyAbort       = Bool
False
                         , tcsmSkipOverlappable :: Bool
tcsmSkipOverlappable = Bool
False
                         , tcsmFullySolveQCIs :: Bool
tcsmFullySolveQCIs   = Bool
False }

instance Outputable TcSMode where
  ppr :: TcSMode -> SDoc
ppr (TcSMode { tcsmResumable :: TcSMode -> Bool
tcsmResumable = Bool
pm, tcsmEarlyAbort :: TcSMode -> Bool
tcsmEarlyAbort = Bool
ea
               , tcsmSkipOverlappable :: TcSMode -> Bool
tcsmSkipOverlappable = Bool
so, tcsmFullySolveQCIs :: TcSMode -> Bool
tcsmFullySolveQCIs = Bool
fs })
    = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"TcSMode" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> (SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
cat ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate SDoc
forall doc. IsLine doc => doc
comma ([SDoc] -> [SDoc]) -> [SDoc] -> [SDoc]
forall a b. (a -> b) -> a -> b
$ [Maybe SDoc] -> [SDoc]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe SDoc] -> [SDoc]) -> [Maybe SDoc] -> [SDoc]
forall a b. (a -> b) -> a -> b
$
                         [ Bool -> String -> Maybe SDoc
forall {a}. IsLine a => Bool -> String -> Maybe a
pp_one Bool
pm String
"Resumable", Bool -> String -> Maybe SDoc
forall {a}. IsLine a => Bool -> String -> Maybe a
pp_one Bool
ea String
"EarlyAbort"
                         , Bool -> String -> Maybe SDoc
forall {a}. IsLine a => Bool -> String -> Maybe a
pp_one Bool
so String
"SkipOverlappable", Bool -> String -> Maybe SDoc
forall {a}. IsLine a => Bool -> String -> Maybe a
pp_one Bool
fs String
"FullySolveQCIs" ])
      -- We get something like TcSMode{EarlyAbort,FullySolveQCIs},
      -- mentioning just the flags that are on
    where
      pp_one :: Bool -> String -> Maybe a
pp_one Bool
True String
s  = a -> Maybe a
forall a. a -> Maybe a
Just (String -> a
forall doc. IsLine doc => String -> doc
text String
s)
      pp_one Bool
False String
_ = Maybe a
forall a. Maybe a
Nothing

{- Note [TcSMode]
~~~~~~~~~~~~~~~~~
The constraint solver can operate in different modes:

* `tcsmResumable`: Used by the pattern match overlap checker.  The idea is that
  the returned InertSet will later be resumed, so we do not want to restore
  type-equality cycles See also Note [Type equality cycles] in GHC.Tc.Solver.Equality

* `tcsmEarlyAbort`: Abort (fail in the monad) as soon as we come across an
  insoluble constraint. This is used to fail-fast when checking for hole-fits.
  See Note [Speeding up valid hole-fits].

* `tcsmSkipOverlappable`: don't use OVERLAPPABLE instances.  Used by the
  short-cut solver.  See Note [Shortcut solving] in GHC.Tc.Solver.Dict

* `tcsmFullSolveQCIs`: fully solve quantified constraints, or leave them alone.
  Used (only) for SPECIALISE pragmas;
  see (NFS1) in Note [Handling new-form SPECIALISE pragmas] in GHC.Tc.Gen.Sig
-}

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

      TcSEnv -> WhatUnifications
tcs_what  :: WhatUnifications,
         -- Level of the outermost meta-tyvar that we have unified
         -- See Note [WhatUnifications] in GHC.Tc.Utils.Unify

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

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

      -- | The mode of operation for the constraint solver.
      -- See Note [TcSMode]
      TcSEnv -> TcSMode
tcs_mode :: TcSMode,

      TcSEnv -> TcRef WorkList
tcs_worklist :: TcRef WorkList
    }

---------------
newtype TcS a = TcS { forall a. TcS a -> TcSEnv -> TcM a
unTcS :: TcSEnv -> TcM a }
  deriving ((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
$cfmap :: forall a b. (a -> b) -> TcS a -> TcS b
fmap :: forall a b. (a -> b) -> TcS a -> TcS b
$c<$ :: forall a b. a -> TcS b -> TcS a
<$ :: forall a b. a -> TcS b -> TcS a
Functor)

instance MonadFix TcS where
  mfix :: forall a. (a -> TcS a) -> TcS a
mfix a -> TcS a
k = (TcSEnv -> TcM a) -> TcS a
(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 -> (a -> TcM a) -> TcM a
forall a.
(a -> IOEnv (Env TcGblEnv TcLclEnv) a)
-> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (\a
x -> TcS a -> TcSEnv -> TcM a
forall a. TcS a -> TcSEnv -> TcM a
unTcS (a -> TcS a
k a
x) TcSEnv
env)

-- | 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 :: forall a. (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
forall a b. (a -> b) -> a -> b
oneShot TcSEnv -> TcM a
f)

instance Applicative TcS where
  pure :: forall a. 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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
  <*> :: forall a b. 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 >>= :: forall a b. 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 a b.
IOEnv (Env TcGblEnv TcLclEnv) a
-> (a -> IOEnv (Env TcGblEnv TcLclEnv) b)
-> IOEnv (Env TcGblEnv TcLclEnv) 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 MonadIO TcS where
  liftIO :: forall a. IO a -> TcS a
liftIO IO a
act = (TcSEnv -> TcM a) -> TcS a
(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 -> IO a -> TcM a
forall a. IO a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO a
act

instance MonadFail TcS where
  fail :: forall a. HasCallStack => 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 a. HasCallStack => String -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a.
(MonadFail m, HasCallStack) =>
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 :: forall a. 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

liftZonkTcS :: ZonkM a -> TcS a
liftZonkTcS :: forall a. ZonkM a -> TcS a
liftZonkTcS = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS (TcM a -> TcS a) -> (ZonkM a -> TcM a) -> ZonkM a -> TcS a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ZonkM a -> TcM a
forall a. ZonkM a -> TcM a
TcM.liftZonkM

wrap2TcS :: (TcM a -> TcM a) -> TcS a -> TcS a
wrap2TcS :: forall a. (TcM a -> TcM a) -> TcS a -> TcS a
wrap2TcS TcM a -> TcM a
fn (TcS TcSEnv -> TcM a
thing) = (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 -> TcM a
fn (TcSEnv -> TcM a
thing TcSEnv
env)

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 :: forall a. 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 :: forall a. TcM a -> TcS a
wrapWarnTcS = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS

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

tryEarlyAbortTcS :: TcS ()
-- Abort (fail in the monad) if the mode is TcSEarlyAbort
tryEarlyAbortTcS :: TcS ()
tryEarlyAbortTcS
  = (TcSEnv -> TcM ()) -> TcS ()
forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS (\TcSEnv
env -> Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TcSMode -> Bool
tcsmEarlyAbort (TcSEnv -> TcSMode
tcs_mode TcSEnv
env)) TcM ()
forall env a. IOEnv env a
TcM.failM)

-- | Emit a warning within the 'TcS' monad at the location given by the 'CtLoc'.
ctLocWarnTcS :: CtLoc -> TcRnMessage -> TcS ()
ctLocWarnTcS :: CtLoc -> TcRnMessage -> TcS ()
ctLocWarnTcS CtLoc
loc TcRnMessage
msg = 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
$ TcRnMessage -> TcM ()
TcM.addDiagnostic TcRnMessage
msg

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 :: forall a. TcPluginM a -> TcS a
runTcPluginTcS = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS (TcM a -> TcS a) -> (TcPluginM a -> TcM a) -> TcPluginM a -> TcS a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPluginM a -> TcM a
forall a. TcPluginM a -> TcM a
runTcPluginM

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 :: TcRef Int
ref = TcSEnv -> TcRef Int
tcs_count TcSEnv
env
     ; n <- TcRef Int -> IOEnv (Env TcGblEnv TcLclEnv) Int
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef TcRef Int
ref
     ; TcM.writeTcRef ref (n+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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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 { n <- TcRef Int -> IOEnv (Env TcGblEnv TcLclEnv) Int
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef (TcSEnv -> TcRef Int
tcs_count TcSEnv
env)
       ; tclvl <- TcM.getTcLevel
       ; return (hang (text "Step" <+> int n
                       <> brackets (text "l:" <> ppr tclvl <> comma <>
                                    text "d:" <> ppr (ctLocDepth (ctEvLoc ev)))
                       <+> doc <> colon)
                     4 (ppr 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 { logger <- IOEnv (Env TcGblEnv TcLclEnv) Logger
forall (m :: * -> *). HasLogger m => m Logger
getLogger
       ; when (  logHasDumpFlag logger Opt_D_dump_cs_trace
                  || logHasDumpFlag logger Opt_D_dump_tc_trace)
              ( do { msg <- mk_doc
                   ; TcM.dumpTcRn False
                       Opt_D_dump_cs_trace
                       "" FormatText
                       msg }) }
{-# INLINE csTraceTcM #-}  -- see Note [INLINE conditional tracing utilities]

runTcS :: TcS a                -- What to run
       -> TcM (a, EvBindMap)
runTcS :: forall a. TcS a -> TcM (a, EvBindMap)
runTcS TcS a
tcs
  = do { ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
       ; res <- runTcSWithEvBinds ev_binds_var tcs
       ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
       ; return (res, ev_binds) }

-- | This variant of 'runTcS' will immediately fail upon encountering an
-- insoluble ct. See Note [Speeding up valid hole-fits]. Its one usage
-- site does not need the ev_binds, so we do not return them.
runTcSEarlyAbort :: TcS a -> TcM a
runTcSEarlyAbort :: forall a. TcS a -> TcM a
runTcSEarlyAbort TcS a
tcs
  = do { ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
       ; runTcSWithEvBinds' mode ev_binds_var tcs }
  where
    mode :: TcSMode
mode = TcSMode
vanillaTcSMode { tcsmEarlyAbort = True }

-- | This can deal only with equality constraints.
runTcSEqualities :: TcS a -> TcM a
runTcSEqualities :: forall a. TcS a -> TcM a
runTcSEqualities TcS a
thing_inside
  = do { ev_binds_var <- TcM EvBindsVar
TcM.newNoTcEvBinds
       ; runTcSWithEvBinds ev_binds_var 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 :: forall a. InertSet -> TcS a -> TcM (a, InertSet)
runTcSInerts InertSet
inerts TcS a
tcs
  = do { ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
       ; runTcSWithEvBinds' (vanillaTcSMode { tcsmResumable = True })
                             ev_binds_var $
         do { setInertSet inerts
            ; a <- tcs
            ; new_inerts <- getInertSet
            ; return (a, new_inerts) } }

runTcSWithEvBinds :: EvBindsVar
                  -> TcS a
                  -> TcM a
runTcSWithEvBinds :: forall a. EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds = TcSMode -> EvBindsVar -> TcS a -> TcM a
forall a. TcSMode -> EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds' TcSMode
vanillaTcSMode

runTcSWithEvBinds' :: TcSMode
                   -> EvBindsVar
                   -> TcS a
                   -> TcM a
runTcSWithEvBinds' :: forall a. TcSMode -> EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds' TcSMode
mode EvBindsVar
ev_binds_var TcS a
thing_inside
  = do { step_count  <- Int -> IOEnv (Env TcGblEnv TcLclEnv) (TcRef Int)
forall (m :: * -> *) a. MonadIO m => a -> m (TcRef a)
TcM.newTcRef Int
0

       -- Make a fresh, empty inert set
       -- Subtle point: see (TGE6) in Note [Tracking Given equalities]
       --               in GHC.Tc.Solver.InertSet
       ; tc_lvl      <- TcM.getTcLevel
       ; inert_var   <- TcM.newTcRef (emptyInertSet tc_lvl)

       ; wl_var      <- TcM.newTcRef emptyWorkList
       ; unif_lvl_var <- TcM.newTcRef infiniteTcLevel
       ; let env = TcSEnv { tcs_ev_binds :: EvBindsVar
tcs_ev_binds = EvBindsVar
ev_binds_var
                          , tcs_what :: WhatUnifications
tcs_what     = TcRef TcLevel -> WhatUnifications
WU_Coarse TcRef TcLevel
unif_lvl_var
                          , tcs_count :: TcRef Int
tcs_count    = TcRef Int
step_count
                          , tcs_inerts :: IORef InertSet
tcs_inerts   = IORef InertSet
inert_var
                          , tcs_mode :: TcSMode
tcs_mode     = TcSMode
mode
                          , tcs_worklist :: TcRef WorkList
tcs_worklist = TcRef WorkList
wl_var }

             -- Run the computation
       ; res <- unTcS thing_inside env

       ; count <- TcM.readTcRef step_count
       ; when (count > 0) $
         csTraceTcM $ return (text "Constraint solver steps =" <+> int count)

       -- Restore tyvar cycles: see Note [Type equality cycles] in
       --                       GHC.Tc.Solver.Equality
       -- But /not/ when tcsmResumable is set: see Note [TcSMode]
       ; unless (tcsmResumable mode) $
         do { inert_set <- TcM.readTcRef inert_var
            ; restoreTyVarCycles inert_set }

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

       ; return 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 }) = isEqPred (varType b)

    edges :: [ Node EvVar EvBind ]
    edges = [ DigraphNode bind bndr (nonDetEltsUniqSet (nestedEvIdsOfTerm 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 :: forall a. EvBindsVar -> TcS a -> TcS a
setEvBindsTcS EvBindsVar
ref (TcS TcSEnv -> TcM a
thing_inside)
 = (TcSEnv -> TcM a) -> TcS a
(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 = ref })

setTcLevelTcS :: TcLevel -> TcS a -> TcS a
setTcLevelTcS :: forall a. TcLevel -> TcS a -> TcS a
setTcLevelTcS TcLevel
lvl (TcS TcSEnv -> TcM a
thing_inside)
 = (TcSEnv -> TcM a) -> TcS a
(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 -> TcLevel -> TcM a -> TcM a
forall a. TcLevel -> TcM a -> TcM a
TcM.setTcLevel TcLevel
lvl (TcSEnv -> TcM a
thing_inside TcSEnv
env)

{- Note [nestImplicTcS]
~~~~~~~~~~~~~~~~~~~~~~~
`nestImplicTcS` is used to build a nested scope when we begin solving an implication.

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

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

nestImplicTcS :: SkolemInfoAnon -> EvBindsVar
              -> TcLevel -> TcS a
              -> TcS a
-- See Note [nestImplicTcS]
nestImplicTcS :: forall a. SkolemInfoAnon -> EvBindsVar -> TcLevel -> TcS a -> TcS a
nestImplicTcS SkolemInfoAnon
skol_info EvBindsVar
ev_binds_var TcLevel
inner_tclvl (TcS TcSEnv -> TcM a
thing_inside)
  = (TcSEnv -> TcM a) -> TcS a
(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
old_inert_var }) ->
    do { old_inerts <- IORef InertSet -> IOEnv (Env TcGblEnv TcLclEnv) InertSet
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef IORef InertSet
old_inert_var
       ; let nest_inert = InertSet -> InertSet
mk_nested_inerts InertSet
old_inerts
       ; new_inert_var <- TcM.newTcRef nest_inert
       ; new_wl_var    <- TcM.newTcRef emptyWorkList
       ; let nest_env = TcSEnv
env { tcs_ev_binds = ev_binds_var
                            , tcs_inerts   = new_inert_var
                            , tcs_worklist = new_wl_var }
       ; res <- TcM.setTcLevel inner_tclvl $
                thing_inside nest_env

       ; out_inert_set <- TcM.readTcRef new_inert_var
       ; restoreTyVarCycles out_inert_set

#if defined(DEBUG)
       -- Perform a check that the thing_inside did not cause cycles
       ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
       ; checkForCyclicBinds ev_binds
#endif
       ; return res }
  where
    mk_nested_inerts :: InertSet -> InertSet
mk_nested_inerts InertSet
old_inerts
      -- For an implication that comes from a static form (static e),
      -- start with a completely empty inert set; in particular, no Givens
      -- See (SF3) in Note [Grand plan for static forms]
      -- in GHC.Iface.Tidy.StaticPtrTable
      | SkolemInfoAnon
StaticFormSkol <- SkolemInfoAnon
skol_info
      = TcLevel -> InertSet
emptyInertSet TcLevel
inner_tclvl

      | Bool
otherwise
      = InertSet -> InertSet
pushCycleBreakerVarStack (InertSet -> InertSet) -> InertSet -> InertSet
forall a b. (a -> b) -> a -> b
$
        InertSet -> InertSet
resetInertCans           (InertSet -> InertSet) -> InertSet -> InertSet
forall a b. (a -> b) -> a -> b
$  -- See (NI1) in Note [nestImplicTcS]
        InertSet
old_inerts

nestFunDepsTcS :: TcS a -> TcS a
nestFunDepsTcS :: forall a. TcS a -> TcS a
nestFunDepsTcS (TcS TcSEnv -> TcM a
thing_inside)
  = (TcSEnv -> TcM a) -> TcS a
(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 }) ->
    TcM a -> TcM a
forall a. TcM a -> TcM a
TcM.pushTcLevelM_  (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
         -- pushTcLevelTcM: increase the level so that unification variables
         -- allocated by the fundep-creation itself don't count as useful unifications
         -- See Note [Deeper TcLevel for partial improvement unification variables]
         --     in GHC.Tc.Solver.FunDeps
    do { inerts <- IORef InertSet -> IOEnv (Env TcGblEnv TcLclEnv) InertSet
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef IORef InertSet
inerts_var
       ; let nest_inerts = InertSet -> InertSet
resetInertCans InertSet
inerts
                 -- resetInertCans: like nestImplicTcS
       ; new_inert_var <- TcM.newTcRef nest_inerts
       ; new_wl_var    <- TcM.newTcRef emptyWorkList
       ; let nest_env = TcSEnv
env { tcs_inerts   = new_inert_var
                            , tcs_worklist = new_wl_var }

       ; TcM.traceTc "nestFunDepsTcS {" empty
       ; res <- thing_inside nest_env
       ; TcM.traceTc "nestFunDepsTcS }" empty

       -- Unlike nestTcS, do /not/ do `updateInertsWith`; we are going to
       -- abandon everything about this sub-computation except its unifications

       ; return 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 :: forall a. TcS a -> TcS a
nestTcS (TcS TcSEnv -> TcM a
thing_inside)
  = (TcSEnv -> TcM a) -> TcS a
(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 { inerts <- IORef InertSet -> IOEnv (Env TcGblEnv TcLclEnv) InertSet
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef IORef InertSet
inerts_var
       ; new_inert_var <- TcM.newTcRef inerts
       ; new_wl_var    <- TcM.newTcRef emptyWorkList
       ; let nest_env = TcSEnv
env { tcs_inerts   = new_inert_var
                            , tcs_worklist = new_wl_var }
                        -- Inherit tcs_ev_binds from caller

       ; res <- thing_inside nest_env

       ; new_inerts <- TcM.readTcRef new_inert_var
       ; TcM.updTcRef inerts_var (`updateInertsWith` new_inerts)

       ; return res }

tryShortCutTcS :: TcS Bool -> TcS Bool
-- Like nestTcS, but
--   (a) be a no-op if the nested computation returns False
--   (b) if (but only if) success, propagate nested bindings to the caller
-- Use only by the short-cut solver;
--   see Note [Shortcut solving] in GHC.Tc.Solver.Dict
tryShortCutTcS :: TcS Bool -> TcS Bool
tryShortCutTcS (TcS TcSEnv -> TcM Bool
thing_inside)
  = (TcSEnv -> TcM Bool) -> TcS Bool
(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
$ \ env :: TcSEnv
env@(TcSEnv { tcs_mode :: TcSEnv -> TcSMode
tcs_mode = TcSMode
mode
                        , tcs_inerts :: TcSEnv -> IORef InertSet
tcs_inerts = IORef InertSet
inerts_var
                        , tcs_ev_binds :: TcSEnv -> EvBindsVar
tcs_ev_binds = EvBindsVar
old_ev_binds_var }) ->
    do { -- Initialise a fresh inert set, with no Givens and no Wanteds
         --    (i.e. empty `inert_cans`)
         -- But inherit all the InertSet cache fields; in particular
         --  * the given_eq_lvl, so we don't accidentally unify a
         --    unification variable from outside a GADT match
         --  * the `solved_dicts`; see wrinkle (SCS3) of Note [Shortcut solving]
         --  * the `famapp_cache`; similarly
         old_inerts <- IORef InertSet -> IOEnv (Env TcGblEnv TcLclEnv) InertSet
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef IORef InertSet
inerts_var
       ; let given_eq_lvl = InertCans -> TcLevel
inert_given_eq_lvl (InertSet -> InertCans
inert_cans InertSet
old_inerts)
             new_inerts   = InertSet
old_inerts { inert_cans = emptyInertCans given_eq_lvl }
       ; new_inert_var <- TcM.newTcRef new_inerts

       ; new_wl_var       <- TcM.newTcRef emptyWorkList
       ; new_ev_binds_var <- TcM.cloneEvBindsVar old_ev_binds_var
       ; let nest_env = TcSEnv
env { tcs_mode     = mode { tcsmSkipOverlappable = True }
                            , tcs_ev_binds = new_ev_binds_var
                            , tcs_inerts   = new_inert_var
                            , tcs_worklist = new_wl_var }

       ; TcM.traceTc "tryTcS {" $
         vcat [ text "old_ev_binds:" <+> ppr old_ev_binds_var
              , text "new_ev_binds:" <+> ppr new_ev_binds_var
              , ppr old_inerts ]
       ; solved <- thing_inside nest_env
       ; TcM.traceTc "tryTcS }" (ppr solved)

       ; if not solved
         then return False
         else do {  -- Successfully solved
                   -- Add the new bindings to the existing ones
                 ; TcM.updTcEvBinds old_ev_binds_var new_ev_binds_var

                 -- Update the existing inert set
                 ; new_inerts <- TcM.readTcRef new_inert_var
                 ; TcM.updTcRef inerts_var (`updateInertsWith` new_inerts)

                 ; TcM.traceTc "tryTcS update" (ppr (inert_solved_dicts new_inerts))

                 ; return True } }

updateInertsWith :: InertSet -> InertSet -> InertSet
-- Update the current inert set with bits from a nested solve,
-- that finished with a new inert set
-- In particular, propagate:
--    - solved dictionaires; see Note [Propagate the solved dictionaries]
--    - Safe Haskell failures
updateInertsWith :: InertSet -> InertSet -> InertSet
updateInertsWith InertSet
current_inerts
                 (IS { inert_solved_dicts :: InertSet -> DictMap DictCt
inert_solved_dicts = DictMap DictCt
new_solved
                     , inert_safehask :: InertSet -> DictMap DictCt
inert_safehask     = DictMap DictCt
new_safehask })
  = InertSet
current_inerts { inert_solved_dicts = new_solved
                   , inert_safehask     = new_safehask }

{- 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
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

getTcSMode :: TcS TcSMode
getTcSMode :: TcS TcSMode
getTcSMode = (TcSEnv -> TcM TcSMode) -> TcS TcSMode
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (TcSMode -> TcM TcSMode
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcSMode -> TcM TcSMode)
-> (TcSEnv -> TcSMode) -> TcSEnv -> TcM TcSMode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> TcSMode
tcs_mode)

setTcSMode :: TcSMode -> TcS a -> TcS a
setTcSMode :: forall a. TcSMode -> TcS a -> TcS a
setTcSMode TcSMode
mode TcS a
thing_inside
  = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (\TcSEnv
env -> TcS a -> TcSEnv -> TcM a
forall a. TcS a -> TcSEnv -> TcM a
unTcS TcS a
thing_inside (TcSEnv
env { tcs_mode = mode }))

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

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

setInertSet :: InertSet -> TcS ()
setInertSet :: InertSet -> TcS ()
setInertSet InertSet
is = do { r <- TcS (IORef InertSet)
getInertSetRef; writeTcRef r is }


newTcRef :: a -> TcS (TcRef a)
newTcRef :: forall a. 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 (m :: * -> *) a. MonadIO m => a -> m (TcRef a)
TcM.newTcRef a
x)

readTcRef :: TcRef a -> TcS a
readTcRef :: forall a. TcRef a -> TcS a
readTcRef TcRef a
ref = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS (TcRef a -> TcM a
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef TcRef a
ref)

writeTcRef :: TcRef a -> a -> TcS ()
writeTcRef :: forall a. TcRef a -> a -> TcS ()
writeTcRef TcRef a
ref a
val = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcRef a -> a -> TcM ()
forall (m :: * -> *) a. MonadIO m => TcRef a -> a -> m ()
TcM.writeTcRef TcRef a
ref a
val)

updTcRef :: TcRef a -> (a->a) -> TcS ()
updTcRef :: forall a. 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 (m :: * -> *) a. MonadIO m => TcRef a -> (a -> a) -> m ()
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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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 [TcCoercion]
getTcEvTyCoVars :: EvBindsVar -> TcS [Coercion]
getTcEvTyCoVars EvBindsVar
ev_binds_var
  = TcM [Coercion] -> TcS [Coercion]
forall a. TcM a -> TcS a
wrapTcS (TcM [Coercion] -> TcS [Coercion])
-> TcM [Coercion] -> TcS [Coercion]
forall a b. (a -> b) -> a -> b
$ EvBindsVar -> TcM [Coercion]
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

updTcEvBinds :: EvBindsVar -> EvBindsVar -> TcS ()
updTcEvBinds :: EvBindsVar -> EvBindsVar -> TcS ()
updTcEvBinds EvBindsVar
evb EvBindsVar
nested_evb
  = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ EvBindsVar -> EvBindsVar -> TcM ()
TcM.updTcEvBinds EvBindsVar
evb EvBindsVar
nested_evb

getDefaultInfo ::  TcS (DefaultEnv, Bool)
getDefaultInfo :: TcS (DefaultEnv, Bool)
getDefaultInfo = TcM (DefaultEnv, Bool) -> TcS (DefaultEnv, Bool)
forall a. TcM a -> TcS a
wrapTcS TcM (DefaultEnv, Bool)
TcM.tcGetDefaultTys


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

setSrcSpan :: RealSrcSpan -> TcS a -> TcS a
setSrcSpan :: forall a. RealSrcSpan -> TcS a -> TcS a
setSrcSpan RealSrcSpan
ss = (TcM a -> TcM a) -> TcS a -> TcS a
forall a. (TcM a -> TcM a) -> TcS a -> TcS a
wrap2TcS (SrcSpan -> TcM a -> TcM a
forall a. SrcSpan -> TcRn a -> TcRn a
TcM.setSrcSpan (RealSrcSpan -> Maybe BufSpan -> SrcSpan
RealSrcSpan RealSrcSpan
ss Maybe BufSpan
forall a. Monoid a => a
mempty))

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

tcLookupTyCon :: Name -> TcS TyCon
tcLookupTyCon :: Name -> TcS TyCon
tcLookupTyCon Name
n = TcRn TyCon -> TcS TyCon
forall a. TcM a -> TcS a
wrapTcS (TcRn TyCon -> TcS TyCon) -> TcRn TyCon -> TcS TyCon
forall a b. (a -> b) -> a -> b
$ Name -> TcRn TyCon
TcM.tcLookupTyCon Name
n

-- Any use of this function is a bit suspect, because it violates the
-- pure veneer of TcS. But it's just about warnings around unused imports
-- and local constructors (GHC will issue fewer warnings than it otherwise
-- might), so it's not worth losing sleep over.
recordUsedGREs :: Bag GlobalRdrElt -> TcS ()
recordUsedGREs :: Bag GlobalRdrElt -> TcS ()
recordUsedGREs Bag GlobalRdrElt
gres
  = do { TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ DeprecationWarnings -> [GlobalRdrElt] -> TcM ()
TcM.addUsedGREs DeprecationWarnings
NoDeprecationWarnings [GlobalRdrElt]
gre_list
         -- If a newtype constructor was imported, don't warn about not
         -- importing it...
       ; TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ (GlobalRdrElt -> TcM ()) -> [GlobalRdrElt] -> TcM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (Name -> TcM ()
TcM.keepAlive (Name -> TcM ())
-> (GlobalRdrElt -> Name) -> GlobalRdrElt -> TcM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalRdrElt -> Name
forall info. GlobalRdrEltX info -> Name
greName) [GlobalRdrElt]
gre_list }
         -- ...and similarly, if a newtype constructor was defined in the same
         -- module, don't warn about it being unused.
         -- See Note [Tracking unused binding and imports] in GHC.Tc.Utils.

  where
    gre_list :: [GlobalRdrElt]
gre_list = Bag GlobalRdrElt -> [GlobalRdrElt]
forall a. Bag a -> [a]
bagToList Bag GlobalRdrElt
gres

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

checkWellLevelledDFun :: 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

checkWellLevelledDFun :: CtLoc -> InstanceWhat -> Type -> TcS ()
checkWellLevelledDFun CtLoc
loc InstanceWhat
what Type
pred
  = do
      mbind_lvl <- HasCallStack =>
InstanceWhat -> TcS (Maybe (Set ThLevelIndex, Bool))
InstanceWhat -> TcS (Maybe (Set ThLevelIndex, Bool))
checkWellLevelledInstanceWhat InstanceWhat
what
      case mbind_lvl of
        Just (Set ThLevelIndex
bind_lvls, Bool
is_local) ->
          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
              { use_lvl <- ThLevel -> ThLevelIndex
thLevelIndex (ThLevel -> ThLevelIndex)
-> IOEnv (Env TcGblEnv TcLclEnv) ThLevel
-> IOEnv (Env TcGblEnv TcLclEnv) ThLevelIndex
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env TcGblEnv TcLclEnv) ThLevel
TcM.getThLevel
              ; dflags <- getDynFlags
              ; checkCrossLevelClsInst dflags (LevelCheckInstance what pred) bind_lvls use_lvl is_local  }
        -- If no level information is returned for an InstanceWhat, then it's safe to use
        -- at any level.
        Maybe (Set ThLevelIndex, Bool)
Nothing -> () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()


-- TODO: Unify this with checkCrossLevelLifting function
checkCrossLevelClsInst :: DynFlags -> LevelCheckReason
                       -> Set.Set ThLevelIndex -> ThLevelIndex
                       -> Bool -> TcM ()
checkCrossLevelClsInst :: DynFlags
-> LevelCheckReason
-> Set ThLevelIndex
-> ThLevelIndex
-> Bool
-> TcM ()
checkCrossLevelClsInst DynFlags
dflags LevelCheckReason
reason Set ThLevelIndex
bind_lvls ThLevelIndex
use_lvl_idx Bool
is_local
  -- If the Id is imported, then allow with ImplicitStagePersistence
  | Bool -> Bool
not Bool
is_local
  , Extension -> DynFlags -> Bool
xopt Extension
LangExt.ImplicitStagePersistence DynFlags
dflags
  = () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  -- NB: Do this check after the ImplicitStagePersistence check, because
  -- it will do some computation to work out the levels of instances.
  | ThLevelIndex
use_lvl_idx ThLevelIndex -> Set ThLevelIndex -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set ThLevelIndex
bind_lvls = () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  -- With ImplicitStagePersistence, using later than bound is fine
  | Extension -> DynFlags -> Bool
xopt Extension
LangExt.ImplicitStagePersistence DynFlags
dflags
  , (ThLevelIndex -> Bool) -> Set ThLevelIndex -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (ThLevelIndex
use_lvl_idx ThLevelIndex -> ThLevelIndex -> Bool
forall a. Ord a => a -> a -> Bool
>=) Set ThLevelIndex
bind_lvls  = () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise = TcRnMessage -> TcM ()
TcM.addErrTc (LevelCheckReason
-> Set ThLevelIndex
-> ThLevelIndex
-> Maybe ErrorItem
-> DiagnosticReason
-> TcRnMessage
TcRnBadlyLevelled LevelCheckReason
reason Set ThLevelIndex
bind_lvls ThLevelIndex
use_lvl_idx Maybe ErrorItem
forall a. Maybe a
Nothing DiagnosticReason
ErrorWithoutFlag)



-- | Returns the ThLevel of evidence for the solved constraint (if it has evidence)
-- See Note [Well-levelled instance evidence]
checkWellLevelledInstanceWhat :: HasCallStack => InstanceWhat -> TcS (Maybe (Set.Set ThLevelIndex, Bool))
checkWellLevelledInstanceWhat :: HasCallStack =>
InstanceWhat -> TcS (Maybe (Set ThLevelIndex, Bool))
checkWellLevelledInstanceWhat InstanceWhat
what
  | TopLevInstance { iw_dfun_id :: InstanceWhat -> TcTyVar
iw_dfun_id = TcTyVar
dfun_id } <- InstanceWhat
what
    = (Set ThLevelIndex, Bool) -> Maybe (Set ThLevelIndex, Bool)
(Set ThLevelIndex, Bool) -> Maybe (Set ThLevelIndex, Bool)
forall a. a -> Maybe a
Just ((Set ThLevelIndex, Bool) -> Maybe (Set ThLevelIndex, Bool))
-> TcS (Set ThLevelIndex, Bool)
-> TcS (Maybe (Set ThLevelIndex, Bool))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TcS (Set ThLevelIndex, Bool)
checkNameVisibleLevels (TcTyVar -> Name
idName TcTyVar
dfun_id)
  | BuiltinTypeableInstance TyCon
tc <- InstanceWhat
what
    -- The typeable instance is always defined in the same module as the TyCon.
    = (Set ThLevelIndex, Bool) -> Maybe (Set ThLevelIndex, Bool)
(Set ThLevelIndex, Bool) -> Maybe (Set ThLevelIndex, Bool)
forall a. a -> Maybe a
Just ((Set ThLevelIndex, Bool) -> Maybe (Set ThLevelIndex, Bool))
-> TcS (Set ThLevelIndex, Bool)
-> TcS (Maybe (Set ThLevelIndex, Bool))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TcS (Set ThLevelIndex, Bool)
checkNameVisibleLevels (TyCon -> Name
tyConName TyCon
tc)
  | Bool
otherwise = Maybe (Set ThLevelIndex, Bool)
-> TcS (Maybe (Set ThLevelIndex, Bool))
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Set ThLevelIndex, Bool)
forall a. Maybe a
Nothing

-- | Check the levels at which the given name is visible, including a boolean
-- indicating if the name is local or not.
checkNameVisibleLevels :: Name -> TcS (Set.Set ThLevelIndex, Bool)
checkNameVisibleLevels :: Name -> TcS (Set ThLevelIndex, Bool)
checkNameVisibleLevels Name
name = do
  cur_mod <- TcGblEnv -> Module
forall t. ContainsModule t => t -> Module
extractModule (TcGblEnv -> Module) -> TcS TcGblEnv -> TcS Module
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcS TcGblEnv
getGblEnv
  if nameIsLocalOrFrom cur_mod name
    then return (Set.singleton topLevelIndex, True)
    else do
      lvls <- checkModuleVisibleLevels (nameModule name)
      return (lvls, False)

{- Note [Using the module graph to compute TH level visiblities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When typechecking a module M, in order to implement GHC proposal #682
(see Note [Explicit Level Imports] in GHC.Tc.Gen.Head), we need to be able to
compute the Template Haskell levels that typeclass instances are visible at in M.

To do this, we use the "level 0 imports" module graph, which we query via
GHC.Unit.Module.Graph.mgQueryZero. For example, if we want all modules that are
visible at level -1 from M, we do the following:

  1. start with all the direct of M imports at level -1, i.e. the "splice imports"
  2. then look at all modules that are reachable from these using only level 0
     normal imports, using 'mgQueryZero'.

This works precisely because, as specified in the proposal, with -XNoImplicitStagePersistence,
modules only export items at level 0. In particular, instances are only exported
at level 0.

See the SI36 test for an illustration.
-}

-- | Check which TH levels a module is visable at
--
-- Used to check visibility of instances (do not use this for normal identifiers).
checkModuleVisibleLevels :: Module -> TcS (Set.Set ThLevelIndex)
checkModuleVisibleLevels :: Module -> TcS (Set ThLevelIndex)
checkModuleVisibleLevels Module
check_mod = do
  cur_mod <- TcGblEnv -> Module
forall t. ContainsModule t => t -> Module
extractModule (TcGblEnv -> Module) -> TcS TcGblEnv -> TcS Module
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcS TcGblEnv
getGblEnv
  hsc_env <- getTopEnv

  -- 0. The keys for the scope of the current module.
  let mkKey ImportLevel
s Module
m = (ModNodeKeyWithUid -> ImportLevel -> ZeroScopeKey
ModuleScope (Module -> IsBootInterface -> ModNodeKeyWithUid
moduleToMnk Module
m IsBootInterface
NotBoot) ImportLevel
s)
      cur_mod_scope_key ImportLevel
s = ImportLevel -> Module -> ZeroScopeKey
mkKey ImportLevel
s Module
cur_mod

  -- 1. is_visible checks that a specific key is visible from the given level in the
  -- current module.
  let is_visible :: ImportLevel -> ZeroScopeKey -> Bool
      is_visible ImportLevel
s ZeroScopeKey
k = ModuleGraph -> ZeroScopeKey -> ZeroScopeKey -> Bool
mgQueryZero (HscEnv -> ModuleGraph
hsc_mod_graph HscEnv
hsc_env) (ImportLevel -> ZeroScopeKey
cur_mod_scope_key ImportLevel
s) ZeroScopeKey
k

  -- 2. The key we are looking for, either the module itself in the home package or the
  -- module unit id of the module we are checking.
  let instance_key = if Module -> UnitId
moduleUnitId Module
check_mod UnitId -> Set UnitId -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` HscEnv -> Set UnitId
hsc_all_home_unit_ids HscEnv
hsc_env
                       then ImportLevel -> Module -> ZeroScopeKey
mkKey ImportLevel
NormalLevel Module
check_mod
                       else UnitId -> ZeroScopeKey
UnitScope (Module -> UnitId
moduleUnitId Module
check_mod)

  -- 3. For each level, check if the key is visible from that level.
  let lvls = [ ImportLevel -> ThLevelIndex
thLevelIndexFromImportLevel ImportLevel
lvl | ImportLevel
lvl <- [ImportLevel]
allImportLevels, ImportLevel -> ZeroScopeKey -> Bool
is_visible ImportLevel
lvl ZeroScopeKey
instance_key]
  return $ Set.fromList lvls

{-
Note [Well-levelled instance evidence]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Evidence for instances must obey the same level restrictions as normal bindings.
In particular, it is forbidden to use an instance in a top-level splice in the
module which the instance is defined. This is because the evidence is bound at
the top-level and top-level definitions are forbidden from being using in top-level splices in
the same module.

For example, suppose you have a function..  foo :: Show a => Code Q a -> Code Q ()
then the following program is disallowed,

```
data T a = T a deriving (Show)

main :: IO ()
main =
  let x = $$(foo [|| T () ||])
  in return ()
```

because the `foo` function (used in a top-level splice) requires `Show T` evidence,
which is defined at the top-level and therefore fails with an error that we have violated
the stage restriction.

```
Main.hs:12:14: error:
    • GHC stage restriction:
        instance for ‘Show
                        (T ())’ is used in a top-level splice, quasi-quote, or annotation,
        and must be imported, not defined locally
    • In the expression: foo [|| T () ||]
      In the Template Haskell splice $$(foo [|| T () ||])
      In the expression: $$(foo [|| T () ||])
   |
12 |   let x = $$(foo [|| T () ||])
   |
```

Solving a `Typeable (T t1 ...tn)` constraint generates code that relies on
`$tcT`, the `TypeRep` for `T`; and we must check that this reference to `$tcT`
is well levelled.  It's easy to know the level of `$tcT`: for imported TyCons it
will be the level of the imported TyCon Name, and for local TyCons it will be `toplevel`.

Therefore the `InstanceWhat` type had to be extended with
a special case for `Typeable`, which recorded the TyCon the evidence was for and
could them be used to check that we were not attempting to evidence in a level incorrect
manner.

-}

pprEq :: TcType -> TcType -> SDoc
pprEq :: Type -> Type -> SDoc
pprEq Type
ty1 Type
ty2 = Type -> SDoc
pprParendType Type
ty1 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'~' SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
pprParendType Type
ty2

isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
isFilledMetaTyVar_maybe TcTyVar
tv = TcM (Maybe Type) -> TcS (Maybe Type)
forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM (Maybe Type)
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)

isUnfilledMetaTyVar :: TcTyVar -> TcS Bool
isUnfilledMetaTyVar :: TcTyVar -> TcS Bool
isUnfilledMetaTyVar TcTyVar
tv = TcM Bool -> TcS Bool
forall a. TcM a -> TcS a
wrapTcS (TcM Bool -> TcS Bool) -> TcM Bool -> TcS Bool
forall a b. (a -> b) -> a -> b
$ TcTyVar -> TcM Bool
TcM.isUnfilledMetaTyVar TcTyVar
tv

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

zonkTyCoVarsAndFVList :: [TcTyCoVar] -> TcS [TcTyCoVar]
zonkTyCoVarsAndFVList :: [TcTyVar] -> TcS [TcTyVar]
zonkTyCoVarsAndFVList [TcTyVar]
tvs = ZonkM [TcTyVar] -> TcS [TcTyVar]
forall a. ZonkM a -> TcS a
liftZonkTcS ([TcTyVar] -> ZonkM [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
. (ZonkM Coercion -> TcM Coercion)
-> (Coercion -> ZonkM Coercion) -> Coercion -> TcM Coercion
forall a b. (a -> b) -> (Coercion -> a) -> Coercion -> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ZonkM Coercion -> TcM Coercion
forall a. ZonkM a -> TcM a
TcM.liftZonkM Coercion -> ZonkM Coercion
TcM.zonkCo

zonkTcType :: TcType -> TcS TcType
zonkTcType :: Type -> TcS Type
zonkTcType Type
ty = ZonkM Type -> TcS Type
forall a. ZonkM a -> TcS a
liftZonkTcS (Type -> ZonkM Type
TcM.zonkTcType Type
ty)

zonkTcTypes :: [TcType] -> TcS [TcType]
zonkTcTypes :: [Type] -> TcS [Type]
zonkTcTypes [Type]
tys = ZonkM [Type] -> TcS [Type]
forall a. ZonkM a -> TcS a
liftZonkTcS ([Type] -> ZonkM [Type]
TcM.zonkTcTypes [Type]
tys)

zonkTcTyVar :: TcTyVar -> TcS TcType
zonkTcTyVar :: TcTyVar -> TcS Type
zonkTcTyVar TcTyVar
tv = ZonkM Type -> TcS Type
forall a. ZonkM a -> TcS a
liftZonkTcS (TcTyVar -> ZonkM Type
TcM.zonkTcTyVar TcTyVar
tv)

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

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

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

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


{- *********************************************************************
*                                                                      *
*              The work list
*                                                                      *
********************************************************************* -}


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

getWorkList :: TcS WorkList
getWorkList :: TcS WorkList
getWorkList = do { wl_var <- TcS (TcRef WorkList)
getTcSWorkListRef
                 ; readTcRef wl_var }

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

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

emitWork :: Cts -> TcS ()
emitWork :: Cts -> TcS ()
emitWork Cts
cts
  | Cts -> Bool
forall a. Bag a -> Bool
isEmptyBag Cts
cts    -- Avoid printing, among other work
  = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = do { String -> SDoc -> TcS ()
traceTcS String
"Emitting fresh work" (Cts -> SDoc
forall a. Outputable a => Bag a -> SDoc
pprBag Cts
cts)
       ; (WorkList -> WorkList) -> TcS ()
updWorkListTcS (Cts -> WorkList -> WorkList
extendWorkListCts Cts
cts) }

selectNextWorkItem :: TcS (Maybe Ct)
-- Pick which work item to do next
-- See Note [Prioritise equalities]
--
-- Postcondition: if the returned item is a Wanted equality,
--                then its rewriter set is fully zonked.
--
-- Suppose a constraint c1 is rewritten by another, c2.  When c2
-- gets solved, c1 has no rewriters, and can be prioritised; see
-- Note [Prioritise Wanteds with empty CoHoleSet] in
-- GHC.Tc.Types.Constraint wrinkle (PER1)

-- ToDo: if wl_rw_eqs is long, we'll re-zonk it each time we pick
--       a new item from wl_rest.  Bad.
selectNextWorkItem :: TcS (Maybe Ct)
selectNextWorkItem
  = do { wl_var <- TcS (TcRef WorkList)
getTcSWorkListRef
       ; wl     <- readTcRef wl_var

       ; case wl of { WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs_X
                         , wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest }
           | Ct
ct:[Ct]
cts <- [Ct]
eqs_N  -> Ct -> WorkList -> TcS (Maybe Ct)
pick_me Ct
ct (WorkList
wl { wl_eqs_N  = cts })
           | Ct
ct:[Ct]
cts <- [Ct]
eqs_X  -> Ct -> WorkList -> TcS (Maybe Ct)
pick_me Ct
ct (WorkList
wl { wl_eqs_X  = cts })
           | Bool
otherwise        -> [Ct] -> [Ct] -> TcS (Maybe Ct)
try_rws [] [Ct]
rw_eqs
           where
             pick_me :: Ct -> WorkList -> TcS (Maybe Ct)
             pick_me :: Ct -> WorkList -> TcS (Maybe Ct)
pick_me Ct
ct WorkList
new_wl
               = do { TcRef WorkList -> WorkList -> TcS ()
forall a. TcRef a -> a -> TcS ()
writeTcRef TcRef WorkList
wl_var WorkList
new_wl
                    ; Maybe Ct -> TcS (Maybe Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ct -> Maybe Ct
forall a. a -> Maybe a
Just Ct
ct) }
                 -- NB: no need for checkReductionDepth (ctLoc ct) (ctPred ct)
                 -- This is done by GHC.Tc.Solver.Dict.chooseInstance

             -- try_rws looks through rw_eqs to find one that has an empty
             -- rewriter set, after zonking.  If none such, call try_rest.
             try_rws :: [Ct] -> [Ct] -> TcS (Maybe Ct)
try_rws [Ct]
acc (Ct
ct:[Ct]
cts)
                = do { ct' <- ZonkM Ct -> TcS Ct
forall a. ZonkM a -> TcS a
liftZonkTcS (Ct -> ZonkM Ct
TcM.zonkCtCoHoleSet Ct
ct)
                     ; if ctHasNoRewriters ct'
                       then pick_me ct' (wl { wl_rw_eqs = cts ++ acc })
                       else try_rws (ct':acc) cts }
             try_rws [Ct]
acc [] = [Ct] -> TcS (Maybe Ct)
try_rest [Ct]
acc

             try_rest :: [Ct] -> TcS (Maybe Ct)
try_rest [Ct]
zonked_rws
               | Ct
ct:[Ct]
cts <- [Ct]
rest       = Ct -> WorkList -> TcS (Maybe Ct)
pick_me Ct
ct (WorkList
wl { wl_rw_eqs = zonked_rws, wl_rest = cts })
               | Ct
ct:[Ct]
cts <- [Ct]
zonked_rws = Ct -> WorkList -> TcS (Maybe Ct)
pick_me Ct
ct (WorkList
wl { wl_rw_eqs = cts })
               | Bool
otherwise            = Maybe Ct -> TcS (Maybe Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Ct
forall a. Maybe a
Nothing
     } }


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 :: forall a. 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


{- *********************************************************************
*                                                                      *
*              Tracking unifications in TcS
*                                                                      *
********************************************************************* -}

unifyTyVar :: TcTyVar -> TcType -> TcS ()
-- Unify a meta-tyvar with a type
-- We should never unify the same variable twice!
-- C.f. GHC.Tc.Utils.Unify.unifyTyVar
unifyTyVar :: TcTyVar -> Type -> TcS ()
unifyTyVar TcTyVar
tv Type
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
$
    do { ZonkM () -> TcS ()
forall a. ZonkM a -> TcS a
liftZonkTcS (HasDebugCallStack => TcTyVar -> Type -> ZonkM ()
TcTyVar -> Type -> ZonkM ()
TcM.writeMetaTyVar TcTyVar
tv Type
ty)  -- Produces a trace message
       ; what_uni <- TcS WhatUnifications
getWhatUnifications
       ; wrapTcS $ recordUnification what_uni tv }

reportFineGrainUnifications :: TcS a -> TcS (TcTyVarSet, a)
-- Record what unifications were done by thing_inside
-- Remember to propagate the information to the enclosing context
reportFineGrainUnifications :: forall a. TcS a -> TcS (VarSet, a)
reportFineGrainUnifications (TcS TcSEnv -> TcM a
thing_inside)
  = (TcSEnv -> TcM (VarSet, a)) -> TcS (VarSet, a)
(TcSEnv -> TcM (VarSet, a)) -> TcS (VarSet, a)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM (VarSet, a)) -> TcS (VarSet, a))
-> (TcSEnv -> TcM (VarSet, a)) -> TcS (VarSet, a)
forall a b. (a -> b) -> a -> b
$ \ env :: TcSEnv
env@(TcSEnv { tcs_what :: TcSEnv -> WhatUnifications
tcs_what = WhatUnifications
outer_wu }) ->
    do { (unif_tvs, res) <- TcSEnv -> (TcSEnv -> TcM a) -> TcM (VarSet, a)
forall a. TcSEnv -> (TcSEnv -> TcM a) -> TcM (VarSet, a)
report_fine_grain_unifs TcSEnv
env TcSEnv -> TcM a
thing_inside
       ; recordUnifications outer_wu unif_tvs
       ; return (unif_tvs, res) }

reportCoarseGrainUnifications :: TcS a -> TcS (TcLevel, a)
-- Record whether any useful unifications are done by thing_inside
-- Specifically: return the TcLevel of the outermost (smallest level)
--   unification variable that has been unified, or infiniteTcLevel if none
-- Remember to propagate the information to the enclosing context
reportCoarseGrainUnifications :: forall a. TcS a -> TcS (TcLevel, a)
reportCoarseGrainUnifications (TcS TcSEnv -> TcM a
thing_inside)
  = (TcSEnv -> TcM (TcLevel, a)) -> TcS (TcLevel, a)
(TcSEnv -> TcM (TcLevel, a)) -> TcS (TcLevel, a)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM (TcLevel, a)) -> TcS (TcLevel, a))
-> (TcSEnv -> TcM (TcLevel, a)) -> TcS (TcLevel, a)
forall a b. (a -> b) -> a -> b
$ \ env :: TcSEnv
env@(TcSEnv { tcs_what :: TcSEnv -> WhatUnifications
tcs_what = WhatUnifications
outer_what }) ->
    case WhatUnifications
outer_what of
      WhatUnifications
WU_None -> TcSEnv -> (TcSEnv -> TcM a) -> TcM (TcLevel, a)
forall a. TcSEnv -> (TcSEnv -> TcM a) -> TcM (TcLevel, a)
report_coarse_grain_unifs TcSEnv
env TcSEnv -> TcM a
thing_inside

      WU_Coarse TcRef TcLevel
outer_ul_ref
        -> do { (inner_ul, res) <- TcSEnv -> (TcSEnv -> TcM a) -> TcM (TcLevel, a)
forall a. TcSEnv -> (TcSEnv -> TcM a) -> TcM (TcLevel, a)
report_coarse_grain_unifs TcSEnv
env TcSEnv -> TcM a
thing_inside

              -- Propagate to outer_ul_ref
              ; outer_ul <- TcM.readTcRef outer_ul_ref
              ; unless (inner_ul `deeperThanOrSame` outer_ul) $
                TcM.writeTcRef outer_ul_ref inner_ul

              ; TcM.traceTc "reportCoarse(Coarse)" $
                vcat [ text "outer_ul" <+> ppr outer_ul
                     , text "inner_ul" <+> ppr inner_ul]
              ; return (inner_ul, res) }

      WU_Fine TcRef VarSet
outer_tvs_ref
        -> do { (unif_tvs,res) <- TcSEnv -> (TcSEnv -> TcM a) -> TcM (VarSet, a)
forall a. TcSEnv -> (TcSEnv -> TcM a) -> TcM (VarSet, a)
report_fine_grain_unifs TcSEnv
env TcSEnv -> TcM a
thing_inside

              -- Propagate to outer_tvs_rev
              ; TcM.updTcRef outer_tvs_ref (`unionVarSet` unif_tvs)

              ; let outermost_unif_lvl = VarSet -> TcLevel
minTcTyVarSetLevel VarSet
unif_tvs
              ; TcM.traceTc "reportCoarse(Fine)" $
                vcat [ text "unif_tvs" <+> ppr unif_tvs
                     , text "unif_happened" <+> ppr outermost_unif_lvl ]
              ; return (outermost_unif_lvl, res) }

report_coarse_grain_unifs :: TcSEnv -> (TcSEnv -> TcM a)
                          -> TcM (TcLevel, a)
-- Returns the level number of the outermost
-- unification variable that is unified
report_coarse_grain_unifs :: forall a. TcSEnv -> (TcSEnv -> TcM a) -> TcM (TcLevel, a)
report_coarse_grain_unifs TcSEnv
env TcSEnv -> TcM a
thing_inside
  = do { inner_ul_ref <- TcLevel -> IOEnv (Env TcGblEnv TcLclEnv) (TcRef TcLevel)
forall (m :: * -> *) a. MonadIO m => a -> m (TcRef a)
TcM.newTcRef TcLevel
infiniteTcLevel
       ; res <- thing_inside (env { tcs_what = WU_Coarse inner_ul_ref })
       ; inner_ul <- TcM.readTcRef inner_ul_ref
       ; TcM.traceTc "report_coarse" $
         text "inner_lvl ="   <+> ppr inner_ul
       ; return (inner_ul, res) }

report_fine_grain_unifs :: TcSEnv -> (TcSEnv -> TcM a)
                        -> TcM (TcTyVarSet, a)
report_fine_grain_unifs :: forall a. TcSEnv -> (TcSEnv -> TcM a) -> TcM (VarSet, a)
report_fine_grain_unifs TcSEnv
env TcSEnv -> TcM a
thing_inside
  = do { unif_tvs_ref <- VarSet -> IOEnv (Env TcGblEnv TcLclEnv) (TcRef VarSet)
forall (m :: * -> *) a. MonadIO m => a -> m (TcRef a)
TcM.newTcRef VarSet
emptyVarSet

       ; res <- thing_inside (env { tcs_what = WU_Fine unif_tvs_ref })

       ; unif_tvs    <- TcM.readTcRef unif_tvs_ref
       ; ambient_lvl <- TcM.getTcLevel

       -- Keep only variables from this or outer levels
       ; let is_interesting TcTyVar
unif_tv
                = TcLevel
ambient_lvl TcLevel -> TcLevel -> Bool
`deeperThanOrSame` TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
unif_tv
             interesting_tvs = (TcTyVar -> Bool) -> VarSet -> VarSet
filterVarSet TcTyVar -> Bool
is_interesting VarSet
unif_tvs
       ; TcM.traceTc "report_fine" (ppr unif_tvs $$ ppr interesting_tvs)
       ; return (interesting_tvs, res) }

getWhatUnifications :: TcS WhatUnifications
getWhatUnifications :: TcS WhatUnifications
getWhatUnifications
  = (TcSEnv -> TcM WhatUnifications) -> TcS WhatUnifications
(TcSEnv -> TcM WhatUnifications) -> TcS WhatUnifications
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM WhatUnifications) -> TcS WhatUnifications)
-> (TcSEnv -> TcM WhatUnifications) -> TcS WhatUnifications
forall a b. (a -> b) -> a -> b
$ \TcSEnv
env -> WhatUnifications -> TcM WhatUnifications
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcSEnv -> WhatUnifications
tcs_what TcSEnv
env)


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

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

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

newFlexiTcSTy :: Kind -> TcS TcType
newFlexiTcSTy :: Type -> TcS Type
newFlexiTcSTy Type
knd = TcM Type -> TcS Type
forall a. TcM a -> TcS a
wrapTcS (Type -> TcM Type
TcM.newFlexiTyVarTy Type
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)

instFlexiX :: Subst -> [TKVar] -> TcS ([TcTyVar], Subst)
instFlexiX :: Subst -> [TcTyVar] -> TcS ([TcTyVar], Subst)
instFlexiX Subst
subst [TcTyVar]
tvs = TcM ([TcTyVar], Subst) -> TcS ([TcTyVar], Subst)
forall a. TcM a -> TcS a
wrapTcS (Subst -> [TcTyVar] -> TcM ([TcTyVar], Subst)
instFlexiXTcM Subst
subst [TcTyVar]
tvs)

instFlexiXTcM :: Subst -> [TKVar] -> TcM ([TcTyVar], Subst)
-- Makes fresh tyvar, extends the substitution, and the in-scope set
-- Takes account of the case [k::Type, a::k, ...],
-- where we must substitute for k in a's kind
instFlexiXTcM :: Subst -> [TcTyVar] -> TcM ([TcTyVar], Subst)
instFlexiXTcM Subst
subst []
  = ([TcTyVar], Subst) -> TcM ([TcTyVar], Subst)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Subst
subst)
instFlexiXTcM Subst
subst (TcTyVar
tv:[TcTyVar]
tvs)
  = do { uniq <- TcRnIf TcGblEnv TcLclEnv Unique
forall gbl lcl. TcRnIf gbl lcl Unique
TcM.newUnique
       ; details <- TcM.newMetaDetails TauTv
       ; let name   = Name -> Unique -> Name
setNameUnique (TcTyVar -> Name
tyVarName TcTyVar
tv) Unique
uniq
             kind   = Subst -> Type -> Type
substTyUnchecked Subst
subst (TcTyVar -> Type
tyVarKind TcTyVar
tv)
             tv'    = Name -> Type -> TcTyVarDetails -> TcTyVar
mkTcTyVar Name
name Type
kind TcTyVarDetails
details
             subst' = Subst -> TcTyVar -> TcTyVar -> Subst
extendTvSubstWithClone Subst
subst TcTyVar
tv TcTyVar
tv'
       ; (tvs', subst'') <- instFlexiXTcM subst' tvs
       ; return (tv':tvs', subst'') }

matchGlobalInst :: DynFlags -> Class -> [Type] -> CtLoc -> TcS TcM.ClsInstResult
matchGlobalInst :: DynFlags -> Class -> [Type] -> CtLoc -> TcS ClsInstResult
matchGlobalInst DynFlags
dflags Class
cls [Type]
tys CtLoc
loc
  = do { mode <- TcS TcSMode
getTcSMode
       ; let skip_overlappable = TcSMode -> Bool
tcsmSkipOverlappable TcSMode
mode
       ; wrapTcS $ TcM.matchGlobalInst dflags skip_overlappable cls tys (Just loc) }

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

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

data MaybeNew = Fresh WantedCtEvidence | Cached EvExpr

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

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

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

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

setEqIfWanted :: CtEvidence -> CoercionPlusHoles -> TcS ()
setEqIfWanted :: CtEvidence -> CoercionPlusHoles -> TcS ()
setEqIfWanted CtEvidence
ev CoercionPlusHoles
co_plus_holes
  = case CtEvidence
ev of
      CtWanted (WantedCt { ctev_dest :: WantedCtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest })
         -> HasDebugCallStack => TcEvDest -> CoercionPlusHoles -> TcS ()
TcEvDest -> CoercionPlusHoles -> TcS ()
setWantedEq TcEvDest
dest CoercionPlusHoles
co_plus_holes
      CtEvidence
_  -> () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

setWantedEq :: HasDebugCallStack => TcEvDest -> CoercionPlusHoles -> TcS ()
-- ^ Equalities only
setWantedEq :: HasDebugCallStack => TcEvDest -> CoercionPlusHoles -> TcS ()
setWantedEq TcEvDest
dest CoercionPlusHoles
co_plus_holes
  = case TcEvDest
dest of
      HoleDest CoercionHole
hole -> CoercionHole -> CoercionPlusHoles -> TcS ()
fillCoercionHole CoercionHole
hole CoercionPlusHoles
co_plus_holes
      EvVarDest TcTyVar
ev  -> String -> SDoc -> TcS ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"setWantedEq: EvVarDest" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
ev)

setDictIfWanted :: CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setDictIfWanted :: CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setDictIfWanted CtEvidence
ev CanonicalEvidence
canonical EvTerm
tm
  = case CtEvidence
ev of
      CtWanted (WantedCt { ctev_dest :: WantedCtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest })
         -> TcEvDest -> CanonicalEvidence -> EvTerm -> TcS ()
setWantedDict TcEvDest
dest CanonicalEvidence
canonical EvTerm
tm
      CtEvidence
_  -> () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

setWantedDict :: TcEvDest -> CanonicalEvidence -> EvTerm -> TcS ()
-- ^ Dictionaries only
setWantedDict :: TcEvDest -> CanonicalEvidence -> EvTerm -> TcS ()
setWantedDict TcEvDest
dest CanonicalEvidence
canonical EvTerm
tm
  = case TcEvDest
dest of
      EvVarDest TcTyVar
ev_id -> EvBind -> TcS ()
setEvBind (TcTyVar -> CanonicalEvidence -> EvTerm -> EvBind
mkWantedEvBind TcTyVar
ev_id CanonicalEvidence
canonical EvTerm
tm)
      HoleDest CoercionHole
h      -> String -> SDoc -> TcS ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"setWantedEq: HoleDest" (CoercionHole -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoercionHole
h)

fillCoercionHole :: CoercionHole -> CoercionPlusHoles -> TcS ()
fillCoercionHole :: CoercionHole -> CoercionPlusHoles -> TcS ()
fillCoercionHole CoercionHole
hole co_plus_holes :: CoercionPlusHoles
co_plus_holes@(CPH { cph_co :: CoercionPlusHoles -> Coercion
cph_co = Coercion
co })
  = do { ev_binds_var <- TcS EvBindsVar
getTcEvBindsVar
       ; wrapTcS $ do { -- Record usage of the free vars of this coercion
                        TcM.updTcRef (ebv_tcvs ev_binds_var) (co :)
                      ; -- Fill the hole
                        TcM.fillCoercionHole hole co_plus_holes }
       ; kickOutAfterFillingCoercionHole hole co_plus_holes }

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 :: Type -> TcS TcTyVar
newEvVar Type
pred = TcM TcTyVar -> TcS TcTyVar
forall a. TcM a -> TcS a
wrapTcS (Type -> TcM TcTyVar
forall gbl lcl. Type -> TcRnIf gbl lcl TcTyVar
TcM.newEvVar Type
pred)

newGivenEv :: CtLoc -> (TcPredType, EvTerm) -> TcS GivenCtEvidence
-- 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
--
-- The `pred` can be an /equality predicate/ t1 ~# t2;
--   see (EQC1) in Note [Solving equality classes] in GHC.Tc.Solver.Dict
newGivenEv :: CtLoc -> (Type, EvTerm) -> TcS GivenCtEvidence
newGivenEv CtLoc
loc (Type
pred, EvTerm
rhs)
  = do { new_ev <- Type -> EvTerm -> TcS TcTyVar
newBoundEvVarId Type
pred EvTerm
rhs
       ; return $ GivenCt { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = 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 :: Type -> EvTerm -> TcS TcTyVar
newBoundEvVarId Type
pred EvTerm
rhs
  = do { new_ev <- Type -> TcS TcTyVar
newEvVar Type
pred
       ; setEvBind (mkGivenEvBind new_ev rhs)
       ; return new_ev }

emitNewGivens :: CtLoc -> [(Role,TcCoercion)] -> TcS ()
emitNewGivens :: CtLoc -> [(Role, Coercion)] -> TcS ()
emitNewGivens CtLoc
loc [(Role, Coercion)]
pts
  = do { String -> SDoc -> TcS ()
traceTcS String
"emitNewGivens" ([(Role, Coercion)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Role, Coercion)]
pts)
       ; gs <- ((Type, EvTerm) -> TcS GivenCtEvidence)
-> [(Type, EvTerm)] -> TcS [GivenCtEvidence]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (CtLoc -> (Type, EvTerm) -> TcS GivenCtEvidence
newGivenEv CtLoc
loc) ([(Type, EvTerm)] -> TcS [GivenCtEvidence])
-> [(Type, EvTerm)] -> TcS [GivenCtEvidence]
forall a b. (a -> b) -> a -> b
$
                [ (Role -> Type -> Type -> Type
mkEqPredRole Role
role Type
ty1 Type
ty2, Coercion -> EvTerm
evCoercion Coercion
co)
                | (Role
role, Coercion
co) <- [(Role, Coercion)]
pts
                , let Pair Type
ty1 Type
ty2 = HasDebugCallStack => Coercion -> Pair Type
Coercion -> Pair Type
coercionKind Coercion
co
                , Bool -> Bool
not (Type
ty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty2) ] -- Kill reflexive Givens at birth
       ; emitWorkNC (map CtGiven gs) }

emitChildEqs :: CtEvidence -> Cts -> TcS ()
-- Emit a bunch of equalities into the work list
-- See Note [Work-list ordering] in GHC.Tc.Solver.Equality
--
-- All the constraints in `cts` share the same rewriter set so,
-- rather than looking at it one by one, we pass it to
-- extendWorkListChildEqs; just a small optimisation.
emitChildEqs :: CtEvidence -> Cts -> TcS ()
emitChildEqs CtEvidence
ev Cts
eqs
  | Cts -> Bool
forall a. Bag a -> Bool
isEmptyBag Cts
eqs
  = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = (WorkList -> WorkList) -> TcS ()
updWorkListTcS (CtEvidence -> Cts -> WorkList -> WorkList
extendWorkListChildEqs CtEvidence
ev Cts
eqs)

-- | Create a new Wanted constraint holding a coercion hole
-- for an equality between the two types at the given 'Role'.
newWantedEq :: CtLoc -> CoHoleSet -> Role -> TcType -> TcType
            -> TcS (WantedCtEvidence, CoercionHole)
newWantedEq :: CtLoc
-> CoHoleSet
-> Role
-> Type
-> Type
-> TcS (WantedCtEvidence, CoercionHole)
newWantedEq CtLoc
loc CoHoleSet
rewriters Role
role Type
ty1 Type
ty2
  = do { 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
$ Type -> TcM CoercionHole
TcM.newCoercionHole Type
pty
       ; let wtd = WantedCt { ctev_pred :: Type
ctev_pred      = Type
pty
                            , ctev_dest :: TcEvDest
ctev_dest      = CoercionHole -> TcEvDest
HoleDest CoercionHole
hole
                            , ctev_loc :: CtLoc
ctev_loc       = CtLoc
loc
                            , ctev_rewriters :: CoHoleSet
ctev_rewriters = CoHoleSet
rewriters }
       ; return (wtd, hole) }
  where
    pty :: Type
pty = Role -> Type -> Type -> Type
mkEqPredRole Role
role Type
ty1 Type
ty2

-- | Create a new Wanted constraint holding an evidence variable.
--
-- Don't use this for equality constraints: use 'newWantedEq' instead.
newWantedEvVarNC :: CtLoc -> CoHoleSet
                 -> TcPredType -> TcS WantedCtEvidence
-- Don't look up in the solved/inerts; we know it's not there
newWantedEvVarNC :: CtLoc -> CoHoleSet -> Type -> TcS WantedCtEvidence
newWantedEvVarNC CtLoc
loc CoHoleSet
rewriters Type
pty
  = Bool -> SDoc -> TcS WantedCtEvidence -> TcS WantedCtEvidence
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Bool -> Bool
not (Type -> Bool
isEqPred Type
pty)) (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pty) (TcS WantedCtEvidence -> TcS WantedCtEvidence)
-> TcS WantedCtEvidence -> TcS WantedCtEvidence
forall a b. (a -> b) -> a -> b
$
    do { new_ev <- Type -> TcS TcTyVar
newEvVar Type
pty
       ; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$
                                         pprCtLoc loc)
       ; return $ WantedCt { ctev_pred      = pty
                           , ctev_dest      = EvVarDest new_ev
                           , ctev_loc       = loc
                           , ctev_rewriters = rewriters }
       }

-- | `newWantedEvVar` makes up a fresh evidence variable for the given predicate.
-- For ClassPred, check if this exact predicate type is in the solved dicts
--      But do /not/ look in the inert_cans, because doing so bypasses all
--      all the careful tests in tryInertDicts, leading to
--      #20666 (prohibitedSuperClassSolve) and #26117 (short-cut solve)
-- We do no such caching forIPs, holes, or errors; so for anything
-- except ClassPred, this is the same as newWantedEvVarNC
--
-- Don't use this for equality constraints: this function is only for
-- constraints with 'EvVarDest'.
newWantedEvVar :: CtLoc -> CoHoleSet
               -> TcPredType -> TcS MaybeNew
newWantedEvVar :: CtLoc -> CoHoleSet -> Type -> TcS MaybeNew
newWantedEvVar CtLoc
loc CoHoleSet
rewriters Type
pty
  = case HasDebugCallStack => Type -> Pred
Type -> Pred
classifyPredType Type
pty of
      EqPred {} -> String -> SDoc -> TcS MaybeNew
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"newWantedEvVar: HoleDestPred" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pty)
      ClassPred Class
cls [Type]
tys
        -> do { inerts <- TcS InertSet
getInertSet
              ; case lookupSolvedDict inerts cls tys of
                 Just CtEvidence
ev -> 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
ev
                               ; MaybeNew -> TcS MaybeNew
forall a. a -> TcS a
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 (HasDebugCallStack => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
ev) }
                 Maybe CtEvidence
Nothing -> do { ev <- CtLoc -> CoHoleSet -> Type -> TcS WantedCtEvidence
newWantedEvVarNC CtLoc
loc CoHoleSet
rewriters Type
pty
                               ; return (Fresh ev) } }
      Pred
_other -> do { ev <- CtLoc -> CoHoleSet -> Type -> TcS WantedCtEvidence
newWantedEvVarNC CtLoc
loc CoHoleSet
rewriters Type
pty
                   ; return (Fresh ev) }

-- | Create a new Wanted constraint, potentially looking up
-- non-equality constraints in the cache instead of creating
-- a new one from scratch.
--
-- Deals with both equality and non-equality constraints.
newWanted :: CtLoc -> CoHoleSet -> PredType -> TcS MaybeNew
newWanted :: CtLoc -> CoHoleSet -> Type -> TcS MaybeNew
newWanted CtLoc
loc CoHoleSet
rewriters Type
pty
  | Just (Role
role, Type
ty1, Type
ty2) <- Type -> Maybe (Role, Type, Type)
getEqPredTys_maybe Type
pty
  = WantedCtEvidence -> MaybeNew
WantedCtEvidence -> MaybeNew
Fresh (WantedCtEvidence -> MaybeNew)
-> ((WantedCtEvidence, CoercionHole) -> WantedCtEvidence)
-> (WantedCtEvidence, CoercionHole)
-> MaybeNew
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WantedCtEvidence, CoercionHole) -> WantedCtEvidence
forall a b. (a, b) -> a
fst ((WantedCtEvidence, CoercionHole) -> MaybeNew)
-> TcS (WantedCtEvidence, CoercionHole) -> TcS MaybeNew
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc
-> CoHoleSet
-> Role
-> Type
-> Type
-> TcS (WantedCtEvidence, CoercionHole)
newWantedEq CtLoc
loc CoHoleSet
rewriters Role
role Type
ty1 Type
ty2
  | Bool
otherwise
  = CtLoc -> CoHoleSet -> Type -> TcS MaybeNew
newWantedEvVar CtLoc
loc CoHoleSet
rewriters Type
pty

-- | Create a new Wanted constraint.
--
-- Deals with both equality and non-equality constraints.
--
-- Does not attempt to re-use non-equality constraints that already
-- exist in the inert set.
newWantedNC :: CtLoc -> CoHoleSet -> PredType -> TcS WantedCtEvidence
newWantedNC :: CtLoc -> CoHoleSet -> Type -> TcS WantedCtEvidence
newWantedNC CtLoc
loc CoHoleSet
rewriters Type
pty
  | Just (Role
role, Type
ty1, Type
ty2) <- Type -> Maybe (Role, Type, Type)
getEqPredTys_maybe Type
pty
  = (WantedCtEvidence, CoercionHole) -> WantedCtEvidence
forall a b. (a, b) -> a
fst ((WantedCtEvidence, CoercionHole) -> WantedCtEvidence)
-> TcS (WantedCtEvidence, CoercionHole) -> TcS WantedCtEvidence
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc
-> CoHoleSet
-> Role
-> Type
-> Type
-> TcS (WantedCtEvidence, CoercionHole)
newWantedEq CtLoc
loc CoHoleSet
rewriters Role
role Type
ty1 Type
ty2
  | Bool
otherwise
  = CtLoc -> CoHoleSet -> Type -> TcS WantedCtEvidence
newWantedEvVarNC CtLoc
loc CoHoleSet
rewriters Type
pty

-- | 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 -> Type -> TcS ()
checkReductionDepth CtLoc
loc Type
ty
  = do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; when (subGoalDepthExceeded (reductionDepth dflags) (ctLocDepth loc)) $
         wrapErrTcS $ solverDepthError loc ty }

matchFam :: TyCon -> [Type] -> TcS (Maybe ReductionN)
matchFam :: TyCon -> [Type] -> TcS (Maybe Reduction)
matchFam TyCon
tycon [Type]
args = TcM (Maybe Reduction) -> TcS (Maybe Reduction)
forall a. TcM a -> TcS a
wrapTcS (TcM (Maybe Reduction) -> TcS (Maybe Reduction))
-> TcM (Maybe Reduction) -> TcS (Maybe Reduction)
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> TcM (Maybe Reduction)
matchFamTcM TyCon
tycon [Type]
args

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

solverDepthError :: CtLoc -> TcType -> TcM a
solverDepthError :: forall a. CtLoc -> Type -> TcM a
solverDepthError CtLoc
loc Type
ty
  = CtLoc -> TcM a -> TcM a
forall a. CtLoc -> TcM a -> TcM a
TcM.setCtLocM CtLoc
loc (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
    do { (ty, env0) <- ZonkM (Type, TidyEnv) -> TcM (Type, TidyEnv)
forall a. ZonkM a -> TcM a
TcM.liftZonkM (ZonkM (Type, TidyEnv) -> TcM (Type, TidyEnv))
-> ZonkM (Type, TidyEnv) -> TcM (Type, TidyEnv)
forall a b. (a -> b) -> a -> b
$
           do { ty   <- Type -> ZonkM Type
TcM.zonkTcType Type
ty
              ; env0 <- TcM.tcInitTidyEnv
              ; return (ty, env0) }
       ; let (tidy_env, tidy_ty)  = tidyOpenTypeX env0 ty
             msg = Type -> SubGoalDepth -> TcRnMessage
TcRnSolverDepthError Type
tidy_ty SubGoalDepth
depth
       ; TcM.failWithTcM (tidy_env, msg) }
  where
    depth :: SubGoalDepth
depth = CtLoc -> SubGoalDepth
ctLocDepth CtLoc
loc

{-
************************************************************************
*                                                                      *
              Unification
*                                                                      *
************************************************************************

Note [wrapUnifier]
~~~~~~~~~~~~~~~~~~
When decomposing equalities we often create new wanted constraints for
(s ~ t).  But what if s=t?  Then it'd be faster to return Refl right away.

Rather than making an equality test (which traverses the structure of the type,
perhaps fruitlessly), we call uType (via wrapUnifier) to traverse the common
structure, and bales out when it finds a difference by creating a new deferred
Wanted constraint.  But where it succeeds in finding common structure, it just
builds a coercion to reflect it.

This is all much faster than creating a new constraint, putting it in the
work list, picking it out, canonicalising it, etc etc.
-}

uPairsTcM :: UnifyEnv -> [TypeEqn] -> TcM ()
uPairsTcM :: UnifyEnv -> [Pair Type] -> TcM ()
uPairsTcM UnifyEnv
uenv [Pair Type]
eqns = (Pair Type -> TcM Coercion) -> [Pair Type] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Pair Type
ty1 Type
ty2) -> UnifyEnv -> Type -> Type -> TcM Coercion
uType UnifyEnv
uenv Type
ty1 Type
ty2) [Pair Type]
eqns

wrapUnifierAndEmit :: CtEvidence -> Role
                   -> (UnifyEnv -> TcM TcCoercion)  -- Some calls to uType
                   -> TcS CoercionPlusHoles
-- Like wrapUnifier, but
--    emits any unsolved equalities into the work-list
--    kicks out any inert constraints that mention unified variables
--    returns a CoHoleSet describing the new unsolved goals
wrapUnifierAndEmit :: CtEvidence
-> Role -> (UnifyEnv -> TcM Coercion) -> TcS CoercionPlusHoles
wrapUnifierAndEmit CtEvidence
ev Role
role UnifyEnv -> TcM Coercion
do_unifications
  = do { (unifs, (co, eqs)) <- TcS (Coercion, Cts) -> TcS (VarSet, (Coercion, Cts))
forall a. TcS a -> TcS (VarSet, a)
reportFineGrainUnifications (TcS (Coercion, Cts) -> TcS (VarSet, (Coercion, Cts)))
-> TcS (Coercion, Cts) -> TcS (VarSet, (Coercion, Cts))
forall a b. (a -> b) -> a -> b
$
                               CtEvidence
-> Role -> (UnifyEnv -> TcM Coercion) -> TcS (Coercion, Cts)
forall a. CtEvidence -> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts)
wrapUnifier CtEvidence
ev Role
role UnifyEnv -> TcM Coercion
do_unifications

       -- Emit the deferred constraints
       ; emitChildEqs ev eqs

       -- Kick out any inert constraints mentioning the unified variables
       ; kickOutAfterUnification unifs

       ; return (CPH { cph_co = co, cph_holes = rewriterSetFromCts eqs }) }

wrapUnifier :: CtEvidence -> Role
             -> (UnifyEnv -> TcM a)  -- Some calls to uType
             -> TcS (a, Bag Ct)
-- Invokes the do_unifications argument, with a suitable UnifyEnv.
-- Very good short-cut when the two types are equal, or nearly so
--    See Note [wrapUnifier]
-- The (Bag Ct) are the deferred constraints; we emit them but
-- also return them
wrapUnifier :: forall a. CtEvidence -> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts)
wrapUnifier CtEvidence
ev Role
role UnifyEnv -> TcM a
do_unifications
  = do { given_eq_lvl <- TcS TcLevel
getInnermostGivenEqLevel
       ; what_uni     <- getWhatUnifications

       ; wrapTcS $
         do { defer_ref    <- TcM.newTcRef emptyBag
            ; let env = UE { u_role :: Role
u_role         = Role
role
                           , u_given_eq_lvl :: TcLevel
u_given_eq_lvl = TcLevel
given_eq_lvl
                           , u_rewriters :: CoHoleSet
u_rewriters    = CtEvidence -> CoHoleSet
ctEvRewriters CtEvidence
ev
                           , u_loc :: CtLoc
u_loc          = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
                           , u_defer :: TcRef Cts
u_defer        = TcRef Cts
defer_ref
                           , u_what :: WhatUnifications
u_what         = WhatUnifications
what_uni }
              -- u_rewriters: the rewriter set and location from
              -- the parent constraint `ev` are inherited in any
              -- new constraints spat out by the unifier
              --
              -- u_what: likewise inherit the WhatUnifications flag,
              --         so that unifications done here are visible
              --         to the caller

            ; res <- do_unifications env

            ; cts     <- TcM.readTcRef defer_ref
            ; return (res, cts) } }


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

checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType
            -> TcS (PuResult Ct Reduction)
-- Used for general CanEqLHSs, ones that do
-- not have a touchable type variable on the LHS (i.e. not unifying)
checkTypeEq :: CtEvidence
-> EqRel -> CanEqLHS -> Type -> TcS (PuResult Ct Reduction)
checkTypeEq CtEvidence
ev EqRel
eq_rel CanEqLHS
lhs Type
rhs =
  case CtEvidence
ev of
    CtGiven {} ->
      do { String -> SDoc -> TcS ()
traceTcS String
"checkTypeEq {" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"lhs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs
                                          , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rhs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs ])
         ; check_result <- TcM (PuResult (TcTyVar, Type) Reduction)
-> TcS (PuResult (TcTyVar, Type) Reduction)
forall a. TcM a -> TcS a
wrapTcS (TyEqFlags (IOEnv (Env TcGblEnv TcLclEnv)) (TcTyVar, Type)
-> Type -> TcM (PuResult (TcTyVar, Type) Reduction)
forall (m :: * -> *) a.
Monad m =>
TyEqFlags m a -> Type -> m (PuResult a Reduction)
checkTyEqRhs TyEqFlags (IOEnv (Env TcGblEnv TcLclEnv)) (TcTyVar, Type)
given_flags Type
rhs)
         ; traceTcS "checkTypeEq }" (ppr check_result)
         ; case check_result of
              PuFail CheckTyEqResult
reason -> PuResult Ct Reduction -> TcS (PuResult Ct Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckTyEqResult -> PuResult Ct Reduction
forall a b. CheckTyEqResult -> PuResult a b
PuFail CheckTyEqResult
reason)
              PuOK Bag (TcTyVar, Type)
prs Reduction
redn -> do { new_givens <- ((TcTyVar, Type) -> TcS Ct) -> Bag (TcTyVar, Type) -> TcS Cts
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM (TcTyVar, Type) -> TcS Ct
mk_new_given Bag (TcTyVar, Type)
prs
                                  ; emitWork new_givens
                                  ; updInertSet (addCycleBreakerBindings prs)
                                  ; return (pure redn) } }
    CtWanted {} -> TcM (PuResult Ct Reduction) -> TcS (PuResult Ct Reduction)
forall a. TcM a -> TcS a
wrapTcS (TyEqFlags (IOEnv (Env TcGblEnv TcLclEnv)) Ct
-> Type -> TcM (PuResult Ct Reduction)
forall (m :: * -> *) a.
Monad m =>
TyEqFlags m a -> Type -> m (PuResult a Reduction)
checkTyEqRhs TyEqFlags (IOEnv (Env TcGblEnv TcLclEnv)) Ct
wanted_flags Type
rhs)
  where
    wanted_flags :: TyEqFlags TcM Ct
    wanted_flags :: TyEqFlags (IOEnv (Env TcGblEnv TcLclEnv)) Ct
wanted_flags = CheckTyEqProblem
-> CanEqLHS -> TyEqFlags (IOEnv (Env TcGblEnv TcLclEnv)) Ct
forall (m :: * -> *) a.
CheckTyEqProblem -> CanEqLHS -> TyEqFlags m a
notUnifying_TEFTask CheckTyEqProblem
occ_prob CanEqLHS
lhs
                   -- checkTypeEq deals only with the non-unifying case

    given_flags :: TyEqFlags TcM (TcTyVar, TcType)
    given_flags :: TyEqFlags (IOEnv (Env TcGblEnv TcLclEnv)) (TcTyVar, Type)
given_flags = TyEqFlags (IOEnv (Env TcGblEnv TcLclEnv)) Ct
wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven }
        -- TEFA_Break used for: [G] a ~ Maybe (F a)
        --                   or [W] F a ~ Maybe (F a)

    -- occ_prob: see Note [Occurs check and representational equality]
    occ_prob :: CheckTyEqProblem
occ_prob = case EqRel
eq_rel of
                 EqRel
NomEq  -> CheckTyEqProblem
cteInsolubleOccurs
                 EqRel
ReprEq -> CheckTyEqProblem
cteSolubleOccurs

    ---------------------------
    mk_new_given :: (TcTyVar, TcType) -> TcS Ct
    mk_new_given :: (TcTyVar, Type) -> TcS Ct
mk_new_given (TcTyVar
new_tv, Type
fam_app)
      = CtEvidence -> Ct
mkNonCanonical (CtEvidence -> Ct)
-> (GivenCtEvidence -> CtEvidence) -> GivenCtEvidence -> Ct
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GivenCtEvidence -> CtEvidence
GivenCtEvidence -> CtEvidence
CtGiven (GivenCtEvidence -> Ct) -> TcS GivenCtEvidence -> TcS Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> (Type, EvTerm) -> TcS GivenCtEvidence
newGivenEv CtLoc
cb_loc (Type
given_pred, EvTerm
given_term)
      where
        new_ty :: Type
new_ty     = TcTyVar -> Type
mkTyVarTy TcTyVar
new_tv
        given_pred :: Type
given_pred = Type -> Type -> Type
mkNomEqPred Type
fam_app Type
new_ty
        given_term :: EvTerm
given_term = Coercion -> EvTerm
evCoercion (Coercion -> EvTerm) -> Coercion -> EvTerm
forall a b. (a -> b) -> a -> b
$ Type -> Coercion
mkNomReflCo Type
new_ty  -- See Detail (4) of Note

    -- See Detail (7) of the Note
    cb_loc :: CtLoc
cb_loc = CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
updateCtLocOrigin (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) CtOrigin -> CtOrigin
CtOrigin -> CtOrigin
CycleBreakerOrigin

-------------------------
-- | Fill in CycleBreakerTvs with the variables they stand for.
-- See Note [Type equality cycles] in GHC.Tc.Solver.Equality
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles InertSet
is
  = ZonkM () -> TcM ()
forall a. ZonkM a -> TcM a
TcM.liftZonkM
  (ZonkM () -> TcM ()) -> ZonkM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ CycleBreakerVarStack -> (TcTyVar -> Type -> ZonkM ()) -> ZonkM ()
forall (m :: * -> *).
Monad m =>
CycleBreakerVarStack -> (TcTyVar -> Type -> m ()) -> m ()
forAllCycleBreakerBindings_ (InertSet -> CycleBreakerVarStack
inert_cycle_breakers InertSet
is) HasDebugCallStack => TcTyVar -> Type -> ZonkM ()
TcTyVar -> Type -> ZonkM ()
TcM.writeMetaTyVar
{-# SPECIALISE forAllCycleBreakerBindings_ ::
      CycleBreakerVarStack -> (TcTyVar -> TcType -> ZonkM ()) -> ZonkM () #-}


{- Note [Occurs check and representational equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(a ~R# b a) is soluble if b later turns out to be Identity
So we treat this as a "soluble occurs check".

Note [Don't cycle-break Wanteds when not unifying]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consdier
  [W] a[2] ~ Maybe (F a[2])

Should we cycle-break this Wanted, thus?

  [W] a[2] ~ Maybe delta[2]
  [W] delta[2] ~ F a[2]

For a start, this is dodgy because we might just unify delta, thus undoing
what we have done, and getting an infinite loop in the solver.  Even if we
somehow prevented ourselves from doing so, is there any merit in the split?
Maybe: perhaps we can use that equality on `a` to unlock other constraints?
Consider
  type instance F (Maybe _) = Bool

  [G] g1: a ~ Maybe Bool
  [W] w1: a ~ Maybe (F a)

If we loop-break w1 to get
  [W] w1': a ~ Maybe gamma
  [W] w3:  gamma ~ F a
Now rewrite w3 with w1'
  [W] w3':  gamma ~ F (Maybe gamma)
Now use the type instance to get
  gamma := Bool
Now we are left with
  [W] w1': a ~ Maybe Bool
which we can solve from the Given.

BUT in this situation we could have rewritten the
/original/ Wanted from the Given, like this:
  [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool))
and that is readily soluble.

In short: loop-breaking Wanteds, when we aren't unifying,
seems of no merit.  Hence TEFA_Recurse, rather than TEFA_Break,
in `wanted_flags` in `checkTypeEq`.
-}