{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# 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, runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts,
    failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS,
    runTcSEqualities,
    nestTcS, nestImplicTcS, setEvBindsTcS,
    emitImplicationTcS, emitTvImplicationTcS,
    emitFunDepWanteds,

    selectNextWorkItem,
    getWorkList,
    updWorkListTcS,
    pushLevelNoWorkList,

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

    QCInst(..),

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

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

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

    newTcEvBinds, newNoTcEvBinds,
    newWantedEq, emitNewWantedEq,
    newWanted,
    newWantedNC, newWantedEvVarNC,
    newBoundEvVarId,
    unifyTyVar, reportUnifications, touchabilityAndShapeTest,
    setEvBind, setWantedEq,
    setWantedEvTerm, setEvBindIfWanted,
    newEvVar, newGivenEvVar, emitNewGivens,
    checkReductionDepth,
    getSolvedDicts, setSolvedDicts,

    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, addInertForAll,
    emitWorkNC, emitWork,
    lookupInertDict,

    -- The Model
    kickOutAfterUnification, kickOutRewritable,

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

    -- Inert solved dictionaries
    updSolvedDicts, lookupSolvedDict,

    -- Irreds
    foldIrreds,

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

    -- Instantiation
    instDFunType,

    -- Unification
    wrapUnifierTcS, unifyFunDeps, uPairsTcM, unifyForAllBody,

    -- MetaTyVars
    newFlexiTcSTy, instFlexiX,
    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,
    checkWellStagedDFun,
    pprEq,

    -- Enforcing invariants for type equalities
    checkTypeEq, checkTouchableTyVarEq
) where

import GHC.Prelude

import GHC.Driver.Env

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

import qualified GHC.Tc.Utils.Monad    as TcM
import qualified GHC.Tc.Utils.TcMType  as TcM
import qualified GHC.Tc.Instance.Class as TcM( matchGlobalInst, ClsInstResult(..) )
import qualified GHC.Tc.Utils.Env      as TcM
       ( checkWellStaged, tcGetDefaultTys
       , tcLookupClass, tcLookupId, tcLookupTyCon
       , topIdLvl )
import GHC.Tc.Zonk.Monad ( ZonkM )
import qualified GHC.Tc.Zonk.TcType  as TcM
import qualified GHC.Tc.Zonk.Type as TcM

import GHC.Driver.DynFlags

import GHC.Tc.Instance.Class( safeOverlap, instanceReturnsDictCon )
import GHC.Tc.Instance.FunDeps( FunDepEqn(..) )
import GHC.Tc.Utils.TcType
import GHC.Tc.Solver.Types
import GHC.Tc.Solver.InertSet
import GHC.Tc.Types.Evidence
import GHC.Tc.Errors.Types
import GHC.Tc.Types
import GHC.Tc.Types.Origin
import GHC.Tc.Types.Constraint
import GHC.Tc.Utils.Unify

import GHC.Builtin.Names ( unsatisfiableClassNameKey )

import GHC.Core.Type
import GHC.Core.TyCo.Rep as Rep
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.Types.Name
import GHC.Types.TyThing
import GHC.Types.Name.Reader
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Unique.Supply
import GHC.Types.Unique.Set( elementOfUniqSet )

import GHC.Unit.Module ( HasModule, getModule, extractModule )
import qualified GHC.Rename.Env as TcM

import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Logger
import GHC.Utils.Misc (HasDebugCallStack)

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

import GHC.Utils.Monad

import GHC.Exts (oneShot)
import Control.Monad
import Data.IORef
import Data.List ( mapAccumL )
import Data.Foldable
import qualified Data.Semigroup as S
import GHC.Types.SrcLoc
import GHC.Rename.Env

#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
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) }

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

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

       -- Update given equalities. C.f updateGivenEqs
       ; tclvl <- getTcLevel
       ; let pred         = QCInst -> Type
qci_pred QCInst
new_qci
             not_equality = Type -> Bool
isClassPred Type
pred Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isEqPred Type
pred)
                  -- True <=> definitely not an equality
                  -- A qci_pred 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_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
qcis })
      | (QCInst -> Bool) -> [QCInst] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any QCInst -> Bool
same_qci [QCInst]
qcis
      = do { String -> SDoc -> TcS ()
traceTcS String
"skipping duplicate quantified instance" (QCInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr QCInst
new_qci)
           ; InertCans -> TcS InertCans
forall 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_insts = 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.
-}

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


-----------------------------------------
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 { ctev_evar :: CtEvidence -> 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 :: [TcTyVar] -> TcS ()
kickOutAfterUnification :: [TcTyVar] -> TcS ()
kickOutAfterUnification [TcTyVar]
tvs
  | [TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs
  = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = do { let tv_set :: VarSet
tv_set = [TcTyVar] -> VarSet
mkVarSet [TcTyVar]
tvs

       ; 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

       -- Set the unification flag if we have done outer unifications
       -- that might affect an earlier implication constraint
       ; let min_tv_lvl = (TcLevel -> TcLevel -> TcLevel) -> [TcLevel] -> TcLevel
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 TcLevel -> TcLevel -> TcLevel
minTcLevel ((TcTyVar -> TcLevel) -> [TcTyVar] -> [TcLevel]
forall a b. (a -> b) -> [a] -> [b]
map TcTyVar -> TcLevel
tcTyVarLevel [TcTyVar]
tvs)
       ; ambient_lvl <- getTcLevel
       ; when (ambient_lvl `strictlyDeeperThan` min_tv_lvl) $
         setUnificationFlag min_tv_lvl

       ; traceTcS "kickOutAfterUnification" (ppr tvs $$ text "n_kicked =" <+> ppr n_kicked)
       ; return n_kicked }

kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
-- See Wrinkle (EIK2a) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality
-- It's possible that this could just go ahead and unify, but could there be occurs-check
-- problems? Seems simpler just to kick out.
kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
kickOutAfterFillingCoercionHole CoercionHole
hole
  = do { ics <- TcS InertCans
getInertCans
       ; let (kicked_out, ics') = kick_out ics
             n_kicked           = Bag IrredCt -> Int
forall a. Bag a -> Int
lengthBag Bag IrredCt
kicked_out

       ; unless (n_kicked == 0) $
         do { updWorkListTcS (extendWorkListCts (fmap CIrredCan 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 -> (Bag IrredCt, InertCans)
    kick_out :: InertCans -> (Bag IrredCt, InertCans)
kick_out ics :: InertCans
ics@(IC { inert_irreds :: InertCans -> Bag IrredCt
inert_irreds = Bag IrredCt
irreds })
      = -- We only care about irreds here, because any constraint blocked
        -- by a coercion hole is an irred.  See wrinkle (EIK2a) in
        -- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
        (Bag IrredCt
irreds_to_kick, InertCans
ics { inert_irreds = irreds_to_keep })
      where
        (Bag IrredCt
irreds_to_kick, Bag IrredCt
irreds_to_keep) = (IrredCt -> Bool) -> Bag IrredCt -> (Bag IrredCt, Bag IrredCt)
forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag IrredCt -> Bool
kick_ct Bag IrredCt
irreds

    kick_ct :: IrredCt -> Bool
         -- True: kick out; False: keep.
    kick_ct :: IrredCt -> Bool
kick_ct IrredCt
ct
      | IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev, ir_reason :: IrredCt -> CtIrredReason
ir_reason = CtIrredReason
reason } <- IrredCt
ct
      , CtWanted { ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet UniqSet CoercionHole
rewriters } <- CtEvidence
ev
      , NonCanonicalReason CheckTyEqResult
ctyeq <- CtIrredReason
reason
      , CheckTyEqResult
ctyeq CheckTyEqResult -> CheckTyEqProblem -> Bool
`cterHasProblem` CheckTyEqProblem
cteCoercionHole
      , CoercionHole
hole CoercionHole -> UniqSet CoercionHole -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
`elementOfUniqSet` UniqSet CoercionHole
rewriters
      = Bool
True
      | Bool
otherwise
      = Bool
False

--------------
addInertSafehask :: InertCans -> DictCt -> InertCans
addInertSafehask :: InertCans -> DictCt -> InertCans
addInertSafehask InertCans
ics DictCt
item
  = InertCans
ics { inert_safehask = addDict item (inert_dicts ics) }

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        = (InertCans -> InertCans) -> TcS ()
updInertCans (\InertCans
ics -> InertCans -> DictCt -> InertCans
addInertSafehask InertCans
ics DictCt
item)

getSafeOverlapFailures :: TcS (Bag DictCt)
-- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
getSafeOverlapFailures :: TcS (Bag DictCt)
getSafeOverlapFailures
 = do { IC { inert_safehask = safehask } <- TcS InertCans
getInertCans
      ; 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_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev })
  | CtEvidence -> Bool
isWanted CtEvidence
ev
  , InstanceWhat -> Bool
instanceReturnsDictCon InstanceWhat
what
  = do { String -> SDoc -> TcS ()
traceTcS String
"updSolvedDicts:" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_ct
       ; (InertSet -> InertSet) -> TcS ()
updInertSet ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ 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 ()

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

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

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 top-level custom type errors, of the form
--    @TypeError msg@, but not constraints such as @Eq (TypeError msg)@
--    in which the type error is nested;
--  - 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
  = do { inert <- TcS InertCans
getInertCans
       ; let insols = (IrredCt -> Bool) -> Bag IrredCt -> Bag IrredCt
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag IrredCt -> Bool
insolubleIrredCt (InertCans -> Bag IrredCt
inert_irreds InertCans
inert)
             unsats = DictMap DictCt -> Unique -> Bag DictCt
forall a. DictMap a -> Unique -> Bag a
findDictsByTyConKey (InertCans -> DictMap DictCt
inert_dicts InertCans
inert) Unique
unsatisfiableClassNameKey
       ; return $ fmap CDictCan unsats `unionBags` fmap CIrredCan insols }

getInertGivens :: TcS [Ct]
-- Returns the Given constraints in the inert set
getInertGivens :: TcS [Ct]
getInertGivens
  = do { inerts <- TcS InertCans
getInertCans
       ; let all_cts = (IrredCt -> [Ct] -> [Ct]) -> Bag IrredCt -> [Ct] -> [Ct]
forall b. (IrredCt -> b -> b) -> Bag IrredCt -> b -> b
foldIrreds ((:) (Ct -> [Ct] -> [Ct]) -> (IrredCt -> Ct) -> IrredCt -> [Ct] -> [Ct]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IrredCt -> Ct
CIrredCan) (InertCans -> Bag IrredCt
inert_irreds InertCans
inerts)
                     ([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ (DictCt -> [Ct] -> [Ct]) -> DictMap DictCt -> [Ct] -> [Ct]
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts  ((:) (Ct -> [Ct] -> [Ct]) -> (DictCt -> Ct) -> DictCt -> [Ct] -> [Ct]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DictCt -> Ct
CDictCan) (InertCans -> DictMap DictCt
inert_dicts InertCans
inerts)
                     ([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ (EqCt -> [Ct] -> [Ct]) -> FunEqMap EqualCtList -> [Ct] -> [Ct]
forall b. (EqCt -> b -> b) -> FunEqMap EqualCtList -> b -> b
foldFunEqs ((:) (Ct -> [Ct] -> [Ct]) -> (EqCt -> Ct) -> EqCt -> [Ct] -> [Ct]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EqCt -> Ct
CEqCan)    (InertCans -> FunEqMap EqualCtList
inert_funeqs InertCans
inerts)
                     ([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ (EqCt -> [Ct] -> [Ct]) -> InertEqs -> [Ct] -> [Ct]
forall b. (EqCt -> b -> b) -> InertEqs -> b -> b
foldTyEqs  ((:) (Ct -> [Ct] -> [Ct]) -> (EqCt -> Ct) -> EqCt -> [Ct] -> [Ct]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EqCt -> Ct
CEqCan)    (InertCans -> InertEqs
inert_eqs InertCans
inerts)
                     ([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ []
       ; return (filter isGivenCt 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_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
insts })
  = Bool -> SDoc -> ([Ct], InertCans) -> ([Ct], InertCans)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ((Ct -> Bool) -> [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Ct -> Bool
isGivenCt [Ct]
sc_pending) ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
sc_pending)
       -- When getPendingScDics is called,
       -- there are never any Wanteds in the inert set
    ([Ct]
sc_pending, InertCans
ic { inert_dicts = dicts', inert_insts = 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
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
forall a. Eq a => a -> a -> Bool
== TcLevel
this_lvl
    -- We only want Givens from this level; see (3a) in
    -- Note [The superclass story] in GHC.Tc.Solver.Dict

getUnsolvedInerts :: TcS ( Bag Implication
                         , 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 (Bag Implication, Cts)
getUnsolvedInerts
 = do { IC { inert_eqs     = tv_eqs
           , inert_funeqs  = fun_eqs
           , inert_irreds  = irreds
           , inert_dicts   = idicts
           } <- 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
CEqCan)    InertEqs
tv_eqs Cts
emptyCts
            unsolved_fun_eqs = (EqCt -> Cts -> Cts) -> FunEqMap EqualCtList -> Cts -> Cts
forall b. (EqCt -> b -> b) -> FunEqMap EqualCtList -> b -> b
foldFunEqs ((EqCt -> Ct) -> EqCt -> Cts -> Cts
forall a. (a -> Ct) -> a -> Cts -> Cts
add_if_unsolved EqCt -> Ct
CEqCan)    FunEqMap EqualCtList
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
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
CDictCan)  DictMap DictCt
idicts Cts
emptyCts

      ; implics <- getWorkListImplics

      ; 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
             , text "implics =" <+> ppr implics ]

      ; return ( implics, unsolved_tv_eqs `unionBags`
                          unsolved_fun_eqs `unionBags`
                          unsolved_irreds `unionBags`
                          unsolved_dicts ) }
  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
forall a. Eq a => a -> a -> Bool
== 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 (Reduction, CtFlavourRole))
lookupFamAppInert :: (CtFlavourRole -> Bool)
-> TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole))
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 EqualCtList -> Maybe (Reduction, CtFlavourRole)
lookup_inerts FunEqMap EqualCtList
inert_funeqs
      | Just EqualCtList
ecl <- FunEqMap EqualCtList -> TyCon -> [Type] -> Maybe EqualCtList
forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq FunEqMap EqualCtList
inert_funeqs TyCon
fam_tc [Type]
tys
      , Just (EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ctev, eq_rhs :: EqCt -> Type
eq_rhs = Type
rhs })
          <- (EqCt -> Bool) -> EqualCtList -> 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) EqualCtList
ecl
      = (Reduction, CtFlavourRole) -> Maybe (Reduction, CtFlavourRole)
forall a. a -> Maybe a
Just (Coercion -> Type -> Reduction
mkReduction (HasDebugCallStack => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion CtEvidence
ctev) Type
rhs, CtEvidence -> CtFlavourRole
ctEvFlavourRole CtEvidence
ctev)
      | Bool
otherwise = Maybe (Reduction, CtFlavourRole)
forall a. Maybe a
Nothing

lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
-- Is this exact predicate type cached in the solved or canonicals of the InertSet?
lookupInInerts :: CtLoc -> Type -> TcS (Maybe CtEvidence)
lookupInInerts CtLoc
loc Type
pty
  | ClassPred Class
cls [Type]
tys <- Type -> Pred
classifyPredType Type
pty
  = do { inerts <- TcS InertSet
getInertSet
       ; let mb_solved = InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict InertSet
inerts CtLoc
loc Class
cls [Type]
tys
             mb_inert  = (DictCt -> CtEvidence) -> Maybe DictCt -> Maybe CtEvidence
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DictCt -> CtEvidence
dictCtEvidence (InertCans -> CtLoc -> Class -> [Type] -> Maybe DictCt
lookupInertDict (InertSet -> InertCans
inert_cans InertSet
inerts) CtLoc
loc Class
cls [Type]
tys)
       ; return $ do -- Maybe monad
            found_ev <- mb_solved `mplus` mb_inert

            -- We're about to "solve" the wanted we're looking up, so we
            -- must make sure doing so wouldn't run afoul of
            -- Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance.
            -- Forgetting this led to #20666.
            guard $ not (prohibitedSuperClassSolve (ctEvLoc found_ev) loc)

            return found_ev }
  | Bool
otherwise -- NB: No caching for equalities, IPs, holes, or errors
  = Maybe CtEvidence -> TcS (Maybe CtEvidence)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe CtEvidence
forall a. Maybe a
Nothing

-- | Look up a dictionary inert.
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe DictCt
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe DictCt
lookupInertDict (IC { inert_dicts :: InertCans -> DictMap DictCt
inert_dicts = DictMap DictCt
dicts }) CtLoc
loc Class
cls [Type]
tys
  = DictMap DictCt -> CtLoc -> Class -> [Type] -> Maybe DictCt
forall a. DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict DictMap DictCt
dicts CtLoc
loc Class
cls [Type]
tys

-- | Look up a solved inert.
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
-- Returns just if exactly this predicate type exists in the solved.
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict (IS { inert_solved_dicts :: InertSet -> DictMap DictCt
inert_solved_dicts = DictMap DictCt
solved }) CtLoc
loc Class
cls [Type]
tys
  = (DictCt -> CtEvidence) -> Maybe DictCt -> Maybe CtEvidence
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DictCt -> CtEvidence
dictCtEvidence (DictMap DictCt -> CtLoc -> Class -> [Type] -> Maybe DictCt
forall a. DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict DictMap DictCt
solved CtLoc
loc Class
cls [Type]
tys)

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

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

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

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

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

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

      -- Whether to throw an exception if we come across an insoluble constraint.
      -- Used to fail-fast when checking for hole-fits. See Note [Speeding up
      -- valid hole-fits].
      TcSEnv -> Bool
tcs_abort_on_insoluble :: Bool,

      -- See Note [WorkList priorities] in GHC.Tc.Solver.InertSet
      TcSEnv -> IORef WorkList
tcs_worklist  :: IORef WorkList -- Current 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
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
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. 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. String -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
err

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

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

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

-- Basic functionality
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
wrapTcS :: TcM a -> TcS a
-- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
-- and TcS is supposed to have limited functionality
wrapTcS :: 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 abort_on_insoluble flag is on
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 (TcSEnv -> Bool
tcs_abort_on_insoluble 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 :: IORef Int
ref = TcSEnv -> IORef Int
tcs_count TcSEnv
env
     ; n <- IORef Int -> IOEnv (Env TcGblEnv TcLclEnv) Int
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef IORef 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 <- IORef Int -> IOEnv (Env TcGblEnv TcLclEnv) Int
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
TcM.readTcRef (TcSEnv -> IORef 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' True True ev_binds_var tcs }

-- | 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' False False 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 = Bool -> Bool -> EvBindsVar -> TcS a -> TcM a
forall a. Bool -> Bool -> EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds' Bool
True Bool
False

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

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

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

       ; when restore_cycles $
         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 }) = isEqPrimPred (varType b)

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

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

nestImplicTcS :: EvBindsVar
              -> TcLevel -> TcS a
              -> TcS a
nestImplicTcS :: forall a. EvBindsVar -> TcLevel -> TcS a -> TcS a
nestImplicTcS EvBindsVar
ref TcLevel
inner_tclvl (TcS TcSEnv -> TcM a
thing_inside)
  = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \ TcSEnv { tcs_unified :: TcSEnv -> IORef Int
tcs_unified            = IORef Int
unified_var
                   , tcs_inerts :: TcSEnv -> IORef InertSet
tcs_inerts             = IORef InertSet
old_inert_var
                   , tcs_count :: TcSEnv -> IORef Int
tcs_count              = IORef Int
count
                   , tcs_unif_lvl :: TcSEnv -> IORef (Maybe TcLevel)
tcs_unif_lvl           = IORef (Maybe TcLevel)
unif_lvl
                   , tcs_abort_on_insoluble :: TcSEnv -> Bool
tcs_abort_on_insoluble = Bool
abort_on_insoluble
                   } ->
    do { 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
inerts { inert_cycle_breakers = pushCycleBreakerVarStack
                                                            (inert_cycle_breakers inerts)
                                 , inert_cans = (inert_cans inerts)
                                                   { inert_given_eqs = False } }
                 -- All other InertSet fields are inherited
       ; new_inert_var <- TcM.newTcRef nest_inert
       ; new_wl_var    <- TcM.newTcRef emptyWorkList
       ; let nest_env = TcSEnv { tcs_count :: IORef Int
tcs_count              = IORef Int
count     -- Inherited
                               , tcs_unif_lvl :: IORef (Maybe TcLevel)
tcs_unif_lvl           = IORef (Maybe TcLevel)
unif_lvl  -- Inherited
                               , tcs_ev_binds :: EvBindsVar
tcs_ev_binds           = EvBindsVar
ref
                               , tcs_unified :: IORef Int
tcs_unified            = IORef Int
unified_var
                               , tcs_inerts :: IORef InertSet
tcs_inerts             = IORef InertSet
new_inert_var
                               , tcs_abort_on_insoluble :: Bool
tcs_abort_on_insoluble = Bool
abort_on_insoluble
                               , tcs_worklist :: IORef WorkList
tcs_worklist           = IORef 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 ref
       ; checkForCyclicBinds ev_binds
#endif
       ; 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
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 }

       ; res <- thing_inside nest_env

       ; new_inerts <- TcM.readTcRef new_inert_var

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

       ; TcM.writeTcRef inerts_var  -- See Note [Propagate the solved dictionaries]
                        (inerts { inert_solved_dicts = inert_solved_dicts new_inerts
                                , inert_cans = nxt_ic })

       ; return res }

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

       ; emitImplication imp
       ; return (TcEvBinds (ic_binds imp)) }

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

       ; emitImplication imp }


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

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

getUnifiedRef :: TcS (IORef Int)
getUnifiedRef :: TcS (IORef Int)
getUnifiedRef = (TcSEnv -> IOEnv (Env TcGblEnv TcLclEnv) (IORef Int))
-> TcS (IORef Int)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (IORef Int -> IOEnv (Env TcGblEnv TcLclEnv) (IORef Int)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (IORef Int -> IOEnv (Env TcGblEnv TcLclEnv) (IORef Int))
-> (TcSEnv -> IORef Int)
-> TcSEnv
-> IOEnv (Env TcGblEnv TcLclEnv) (IORef Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> IORef Int
tcs_unified)

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

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

getWorkListImplics :: TcS (Bag Implication)
getWorkListImplics :: TcS (Bag Implication)
getWorkListImplics
  = do { wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
       ; wl_curr <- readTcRef wl_var
       ; return (wl_implics wl_curr) }

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

updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
updWorkListTcS WorkList -> WorkList
f
  = do { wl_var <- TcS (IORef 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)
         -- Zonk the rewriter set of Wanteds, because that affects
         -- the prioritisation of the work-list. 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 RewriterSet]
         -- in GHC.Tc.Types.Constraint wrinkle (WRW1)
       ; cts <- TcM Cts -> TcS Cts
forall a. TcM a -> TcS a
wrapTcS (TcM Cts -> TcS Cts) -> TcM Cts -> TcS Cts
forall a b. (a -> b) -> a -> b
$ (Ct -> IOEnv (Env TcGblEnv TcLclEnv) Ct) -> Cts -> TcM Cts
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Ct -> IOEnv (Env TcGblEnv TcLclEnv) Ct
TcM.zonkCtRewriterSet Cts
cts
       ; updWorkListTcS (extendWorkListCts cts) }

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

newTcRef :: a -> TcS (TcRef a)
newTcRef :: 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 TyCoVarSet
getTcEvTyCoVars :: EvBindsVar -> TcS VarSet
getTcEvTyCoVars EvBindsVar
ev_binds_var
  = TcM VarSet -> TcS VarSet
forall a. TcM a -> TcS a
wrapTcS (TcM VarSet -> TcS VarSet) -> TcM VarSet -> TcS VarSet
forall a b. (a -> b) -> a -> b
$ EvBindsVar -> TcM VarSet
TcM.getTcEvTyCoVars EvBindsVar
ev_binds_var

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

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

unifyTyVar :: TcTyVar -> TcType -> TcS ()
-- Unify a meta-tyvar with a type
-- We keep track of how many unifications have happened in tcs_unified,
--
-- We should never unify the same variable twice!
unifyTyVar :: TcTyVar -> 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
$
    (TcSEnv -> TcM ()) -> TcS ()
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM ()) -> TcS ()) -> (TcSEnv -> TcM ()) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ TcSEnv
env ->
    do { String -> SDoc -> TcM ()
TcM.traceTc String
"unifyTyVar" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
       ; ZonkM () -> TcM ()
forall a. ZonkM a -> TcM a
TcM.liftZonkM (ZonkM () -> TcM ()) -> ZonkM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => TcTyVar -> Type -> ZonkM ()
TcTyVar -> Type -> ZonkM ()
TcM.writeMetaTyVar TcTyVar
tv Type
ty
       ; IORef Int -> (Int -> Int) -> TcM ()
forall (m :: * -> *) a. MonadIO m => TcRef a -> (a -> a) -> m ()
TcM.updTcRef (TcSEnv -> IORef Int
tcs_unified TcSEnv
env) (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) }

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

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

getWorkList :: TcS WorkList
getWorkList :: TcS WorkList
getWorkList = do { wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
                 ; wrapTcS (TcM.readTcRef wl_var) }

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

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

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

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

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

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

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

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 = TcM TyCon -> TcS TyCon
forall a. TcM a -> TcS a
wrapTcS (TcM TyCon -> TcS TyCon) -> TcM TyCon -> TcS TyCon
forall a b. (a -> b) -> a -> b
$ Name -> TcM 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]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

checkWellStagedDFun :: CtLoc -> InstanceWhat -> Type -> TcS ()
checkWellStagedDFun CtLoc
loc InstanceWhat
what Type
pred
  = do
      mbind_lvl <- InstanceWhat -> TcS (Maybe Int)
checkWellStagedInstanceWhat InstanceWhat
what
      case mbind_lvl of
        Just Int
bind_lvl | Int
bind_lvl Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
impLevel ->
          TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtLoc -> TcM () -> TcM ()
forall a. CtLoc -> TcM a -> TcM a
TcM.setCtLocM CtLoc
loc (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$ do
              { use_stage <- TcM ThStage
TcM.getStage
              ; TcM.checkWellStaged (StageCheckInstance what pred) bind_lvl (thLevel use_stage) }
        Maybe Int
_ ->
          () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Returns the ThLevel of evidence for the solved constraint (if it has evidence)
-- See Note [Well-staged instance evidence]
checkWellStagedInstanceWhat :: InstanceWhat -> TcS (Maybe ThLevel)
checkWellStagedInstanceWhat :: InstanceWhat -> TcS (Maybe Int)
checkWellStagedInstanceWhat InstanceWhat
what
  | TopLevInstance { iw_dfun_id :: InstanceWhat -> TcTyVar
iw_dfun_id = TcTyVar
dfun_id } <- InstanceWhat
what
    = Maybe Int -> TcS (Maybe Int)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> TcS (Maybe Int)) -> Maybe Int -> TcS (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just (TcTyVar -> Int
TcM.topIdLvl TcTyVar
dfun_id)
  | BuiltinTypeableInstance TyCon
tc <- InstanceWhat
what
    = 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
        return $ Just (if nameIsLocalOrFrom cur_mod (tyConName tc)
                        then outerLevel
                        else impLevel)
  | Bool
otherwise = Maybe Int -> TcS (Maybe Int)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing

{-
Note [Well-staged 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 staged.  It's easy to know the stage of `$tcT`: for imported TyCons it
will be `impLevel`, 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 stage 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 Unification Level Flag                              *
*                                                                      *
********************************************************************* -}

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

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

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

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

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

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

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

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

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

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

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

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


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

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


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

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

instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
instDFunType :: TcTyVar -> [Maybe 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 Subst
instFlexiX :: Subst -> [TcTyVar] -> TcS Subst
instFlexiX Subst
subst [TcTyVar]
tvs = TcM Subst -> TcS Subst
forall a. TcM a -> TcS a
wrapTcS (Subst -> [TcTyVar] -> TcM Subst
instFlexiXTcM Subst
subst [TcTyVar]
tvs)

instFlexiXTcM :: Subst -> [TKVar] -> TcM 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 Subst
instFlexiXTcM Subst
subst []
  = Subst -> TcM 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'
       ; instFlexiXTcM subst' tvs  }

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

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 CtEvidence | Cached EvExpr

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

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

getEvExpr :: MaybeNew -> EvExpr
getEvExpr :: MaybeNew -> EvExpr
getEvExpr (Fresh CtEvidence
ctev) = HasDebugCallStack => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
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 }

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

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

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

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

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

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

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

Yuk!
-}

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

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

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

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

newEvVar :: TcPredType -> TcS EvVar
newEvVar :: 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)

newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
-- Make a new variable of the given PredType,
-- immediately bind it to the given term
-- and return its CtEvidence
-- See Note [Bind new Givens immediately] in GHC.Tc.Types.Constraint
newGivenEvVar :: CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (Type
pred, EvTerm
rhs)
  = do { new_ev <- Type -> EvTerm -> TcS TcTyVar
newBoundEvVarId Type
pred EvTerm
rhs
       ; return (CtGiven { 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,TcType,TcType,TcCoercion)] -> TcS ()
emitNewGivens :: CtLoc -> [(Role, Type, Type, Coercion)] -> TcS ()
emitNewGivens CtLoc
loc [(Role, Type, Type, Coercion)]
pts
  = do { evs <- ((Type, EvTerm) -> TcS CtEvidence)
-> [(Type, EvTerm)] -> TcS [CtEvidence]
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 CtEvidence
newGivenEvVar CtLoc
loc) ([(Type, EvTerm)] -> TcS [CtEvidence])
-> [(Type, EvTerm)] -> TcS [CtEvidence]
forall a b. (a -> b) -> a -> b
$
                [ (Role -> Type -> Type -> Type
mkPrimEqPredRole Role
role Type
ty1 Type
ty2, Coercion -> EvTerm
evCoercion Coercion
co)
                | (Role
role, Type
ty1, Type
ty2, Coercion
co) <- [(Role, Type, Type, Coercion)]
pts
                , Bool -> Bool
not (Type
ty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty2) ] -- Kill reflexive Givens at birth
       ; emitWorkNC evs }

emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS Coercion
-- | Emit a new Wanted equality into the work-list
emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> Type -> Type -> TcS Coercion
emitNewWantedEq CtLoc
loc RewriterSet
rewriters Role
role Type
ty1 Type
ty2
  = do { (ev, co) <- CtLoc
-> RewriterSet
-> Role
-> Type
-> Type
-> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc RewriterSet
rewriters Role
role Type
ty1 Type
ty2
       ; updWorkListTcS (extendWorkListEq rewriters (mkNonCanonical ev))
       ; return co }

-- | Create a new Wanted constraint holding a coercion hole
-- for an equality between the two types at the given 'Role'.
newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType
            -> TcS (CtEvidence, Coercion)
newWantedEq :: CtLoc
-> RewriterSet
-> Role
-> Type
-> Type
-> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc RewriterSet
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
$ CtLoc -> Type -> TcM CoercionHole
TcM.newCoercionHole CtLoc
loc Type
pty
       ; return ( CtWanted { ctev_pred      = pty
                           , ctev_dest      = HoleDest hole
                           , ctev_loc       = loc
                           , ctev_rewriters = rewriters }
                , mkHoleCo hole ) }
  where
    pty :: Type
pty = Role -> Type -> Type -> Type
mkPrimEqPredRole 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 -> RewriterSet
                 -> TcPredType -> TcS CtEvidence
-- Don't look up in the solved/inerts; we know it's not there
newWantedEvVarNC :: CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedEvVarNC CtLoc
loc RewriterSet
rewriters Type
pty
  = do { new_ev <- Type -> TcS TcTyVar
newEvVar Type
pty
       ; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$
                                         pprCtLoc loc)
       ; return (CtWanted { ctev_pred      = pty
                          , ctev_dest      = EvVarDest new_ev
                          , ctev_loc       = loc
                          , ctev_rewriters = rewriters })}

-- | Like 'newWantedEvVarNC', except it might look up in the inert set
-- to see if an inert already exists, and uses that instead of creating
-- a new Wanted constraint.
--
-- Don't use this for equality constraints: this function is only for
-- constraints with 'EvVarDest'.
newWantedEvVar :: CtLoc -> RewriterSet
               -> TcPredType -> TcS MaybeNew
-- For anything except ClassPred, this is the same as newWantedEvVarNC
newWantedEvVar :: CtLoc -> RewriterSet -> Type -> TcS MaybeNew
newWantedEvVar CtLoc
loc RewriterSet
rewriters Type
pty
  = Bool -> SDoc -> TcS MaybeNew -> TcS MaybeNew
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Bool -> Bool
not (Type -> Bool
isEqPrimPred Type
pty))
      ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"newWantedEvVar: HoleDestPred"
            , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"pty:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pty ]) (TcS MaybeNew -> TcS MaybeNew) -> TcS MaybeNew -> TcS MaybeNew
forall a b. (a -> b) -> a -> b
$
    do { mb_ct <- CtLoc -> Type -> TcS (Maybe CtEvidence)
lookupInInerts CtLoc
loc Type
pty
       ; case mb_ct of
            Just CtEvidence
ctev
              -> do { String -> SDoc -> TcS ()
traceTcS String
"newWantedEvVar/cache hit" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ctev
                    ; MaybeNew -> TcS MaybeNew
forall 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
ctev) }
            Maybe CtEvidence
_ -> do { ctev <- CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedEvVarNC CtLoc
loc RewriterSet
rewriters Type
pty
                    ; return (Fresh ctev) } }

-- | 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 -> RewriterSet -> PredType -> TcS MaybeNew
newWanted :: CtLoc -> RewriterSet -> Type -> TcS MaybeNew
newWanted CtLoc
loc RewriterSet
rewriters Type
pty
  | Just (Role
role, Type
ty1, Type
ty2) <- Type -> Maybe (Role, Type, Type)
getEqPredTys_maybe Type
pty
  = CtEvidence -> MaybeNew
Fresh (CtEvidence -> MaybeNew)
-> ((CtEvidence, Coercion) -> CtEvidence)
-> (CtEvidence, Coercion)
-> MaybeNew
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CtEvidence, Coercion) -> CtEvidence
forall a b. (a, b) -> a
fst ((CtEvidence, Coercion) -> MaybeNew)
-> TcS (CtEvidence, Coercion) -> TcS MaybeNew
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc
-> RewriterSet
-> Role
-> Type
-> Type
-> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc RewriterSet
rewriters Role
role Type
ty1 Type
ty2
  | Bool
otherwise
  = CtLoc -> RewriterSet -> Type -> TcS MaybeNew
newWantedEvVar CtLoc
loc RewriterSet
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 -> RewriterSet -> PredType -> TcS CtEvidence
newWantedNC :: CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedNC CtLoc
loc RewriterSet
rewriters Type
pty
  | Just (Role
role, Type
ty1, Type
ty2) <- Type -> Maybe (Role, Type, Type)
getEqPredTys_maybe Type
pty
  = (CtEvidence, Coercion) -> CtEvidence
forall a b. (a, b) -> a
fst ((CtEvidence, Coercion) -> CtEvidence)
-> TcS (CtEvidence, Coercion) -> TcS CtEvidence
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc
-> RewriterSet
-> Role
-> Type
-> Type
-> TcS (CtEvidence, Coercion)
newWantedEq CtLoc
loc RewriterSet
rewriters Role
role Type
ty1 Type
ty2
  | Bool
otherwise
  = CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedEvVarNC CtLoc
loc RewriterSet
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     = TidyEnv -> [TcTyVar] -> TidyEnv
tidyFreeTyCoVars TidyEnv
env0 (Type -> [TcTyVar]
tyCoVarsOfTypeList Type
ty)
             tidy_ty      = TidyEnv -> Type -> Type
tidyType TidyEnv
tidy_env Type
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

{-
************************************************************************
*                                                                      *
              Emitting equalities arising from fundeps
*                                                                      *
************************************************************************
-}

emitFunDepWanteds :: CtEvidence  -- The work item
                  -> [FunDepEqn (CtLoc, RewriterSet)]
                  -> TcS Bool  -- True <=> some unification happened

emitFunDepWanteds :: CtEvidence -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS Bool
emitFunDepWanteds CtEvidence
_ [] = Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False -- common case noop
-- See Note [FunDep and implicit parameter reactions]

emitFunDepWanteds CtEvidence
ev [FunDepEqn (CtLoc, RewriterSet)]
fd_eqns
  = CtEvidence -> Role -> (UnifyEnv -> TcM ()) -> TcS Bool
unifyFunDeps CtEvidence
ev Role
Nominal UnifyEnv -> TcM ()
do_fundeps
  where
    do_fundeps :: UnifyEnv -> TcM ()
    do_fundeps :: UnifyEnv -> TcM ()
do_fundeps UnifyEnv
env = (FunDepEqn (CtLoc, RewriterSet) -> TcM ())
-> [FunDepEqn (CtLoc, RewriterSet)] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (UnifyEnv -> FunDepEqn (CtLoc, RewriterSet) -> TcM ()
do_one UnifyEnv
env) [FunDepEqn (CtLoc, RewriterSet)]
fd_eqns

    do_one :: UnifyEnv -> FunDepEqn (CtLoc, RewriterSet) -> TcM ()
    do_one :: UnifyEnv -> FunDepEqn (CtLoc, RewriterSet) -> TcM ()
do_one UnifyEnv
uenv (FDEqn { fd_qtvs :: forall loc. FunDepEqn loc -> [TcTyVar]
fd_qtvs = [TcTyVar]
tvs, fd_eqs :: forall loc. FunDepEqn loc -> [TypeEqn]
fd_eqs = [TypeEqn]
eqs, fd_loc :: forall loc. FunDepEqn loc -> loc
fd_loc = (CtLoc
loc, RewriterSet
rewriters) })
      = do { eqs' <- [TcTyVar] -> [TypeEqn] -> TcM [TypeEqn]
instantiate_eqs [TcTyVar]
tvs ([TypeEqn] -> [TypeEqn]
forall a. [a] -> [a]
reverse [TypeEqn]
eqs)
                     -- (reverse eqs): See Note [Reverse order of fundep equations]
           ; uPairsTcM env_one eqs' }
      where
        env_one :: UnifyEnv
env_one = UnifyEnv
uenv { u_rewriters = u_rewriters uenv S.<> rewriters
                       , u_loc       = loc }

    instantiate_eqs :: [TyVar] -> [TypeEqn] -> TcM [TypeEqn]
    instantiate_eqs :: [TcTyVar] -> [TypeEqn] -> TcM [TypeEqn]
instantiate_eqs [TcTyVar]
tvs [TypeEqn]
eqs
      | [TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs
      = [TypeEqn] -> TcM [TypeEqn]
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return [TypeEqn]
eqs
      | Bool
otherwise
      = do { String -> SDoc -> TcM ()
TcM.traceTc String
"emitFunDepWanteds 2" ([TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
tvs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TypeEqn] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TypeEqn]
eqs)
           ; subst <- Subst -> [TcTyVar] -> TcM Subst
instFlexiXTcM Subst
emptySubst [TcTyVar]
tvs  -- Takes account of kind substitution
           ; return [ Pair (substTyUnchecked subst' ty1) ty2
                           -- ty2 does not mention fd_qtvs, so no need to subst it.
                           -- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
                           --     Wrinkle (1)
                    | Pair ty1 ty2 <- eqs
                    , let subst' = Subst -> VarSet -> Subst
extendSubstInScopeSet Subst
subst (Type -> VarSet
tyCoVarsOfType Type
ty1) ]
                          -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result
                          -- of matching with the [W] constraint. So we add its free
                          -- vars to InScopeSet, to satisfy substTy's invariants, even
                          -- though ty1 will never (currently) be a poytype, so this
                          -- InScopeSet will never be looked at.
           }

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

Note [wrapUnifierTcS]
~~~~~~~~~~~~~~~~~~~
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 wrapUnifierTcS) 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.

Note [unifyFunDeps]
~~~~~~~~~~~~~~~~~~~
The Bool returned by `unifyFunDeps` is True if we have unified a variable
that occurs in the constraint we are trying to solve; it is not in the
inert set so `wrapUnifierTcS` won't kick it out.  Instead we want to send it
back to the start of the pipeline.  Hence the Bool.

It's vital that we don't return (not (null unified)) because the fundeps
may create fresh variables; unifying them (alone) should not make us send
the constraint back to the start, or we'll get an infinite loop.  See
Note [Fundeps with instances, and equality orientation] in GHC.Tc.Solver.Dict
and Note [Improvement orientation] in GHC.Tc.Solver.Equality.
-}

uPairsTcM :: UnifyEnv -> [TypeEqn] -> TcM ()
uPairsTcM :: UnifyEnv -> [TypeEqn] -> TcM ()
uPairsTcM UnifyEnv
uenv [TypeEqn]
eqns = (TypeEqn -> TcM Coercion) -> [TypeEqn] -> 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) [TypeEqn]
eqns

unifyFunDeps :: CtEvidence -> Role
             -> (UnifyEnv -> TcM ())
             -> TcS Bool
unifyFunDeps :: CtEvidence -> Role -> (UnifyEnv -> TcM ()) -> TcS Bool
unifyFunDeps CtEvidence
ev Role
role UnifyEnv -> TcM ()
do_unifications
  = do { (_, _, unified) <- CtEvidence
-> Role -> (UnifyEnv -> TcM ()) -> TcS ((), Cts, [TcTyVar])
forall a.
CtEvidence
-> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts, [TcTyVar])
wrapUnifierTcS CtEvidence
ev Role
role UnifyEnv -> TcM ()
do_unifications
       ; return (any (`elemVarSet` fvs) unified) }
         -- See Note [unifyFunDeps]
  where
    fvs :: VarSet
fvs = Type -> VarSet
tyCoVarsOfType (CtEvidence -> Type
ctEvPred CtEvidence
ev)

unifyForAllBody :: CtEvidence -> Role -> (UnifyEnv -> TcM a)
                -> TcS (a, Cts)
-- We /return/ the equality constraints we generate,
-- rather than emitting them into the monad.
-- See See (SF5) in Note [Solving forall equalities] in GHC.Tc.Solver.Equality
unifyForAllBody :: forall a. CtEvidence -> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts)
unifyForAllBody CtEvidence
ev Role
role UnifyEnv -> TcM a
unify_body
  = do { (res, cts, unified, _rewriters) <- CtEvidence
-> Role
-> (UnifyEnv -> TcM a)
-> TcS (a, Cts, [TcTyVar], RewriterSet)
forall a.
CtEvidence
-> Role
-> (UnifyEnv -> TcM a)
-> TcS (a, Cts, [TcTyVar], RewriterSet)
wrapUnifierX CtEvidence
ev Role
role UnifyEnv -> TcM a
unify_body
         -- Ignore the rewriters. They are used in wrapUnifierTcS only
         -- as an optimistion to prioritise the work list; but they are
         -- /also/ stored in each individual constraint we return.

       -- Kick out any inert constraint that we have unified
       ; _ <- kickOutAfterUnification unified

       ; return (res, cts) }

wrapUnifierTcS :: CtEvidence -> Role
               -> (UnifyEnv -> TcM a)  -- Some calls to uType
               -> TcS (a, Bag Ct, [TcTyVar])
-- Invokes the do_unifications argument, with a suitable UnifyEnv.
-- Emit deferred equalities and kick-out from the inert set as a
-- result of any unifications.
-- Very good short-cut when the two types are equal, or nearly so
-- See Note [wrapUnifierTcS]
--
-- The [TcTyVar] is the list of unification variables that were
-- unified the process; the (Bag Ct) are the deferred constraints.

wrapUnifierTcS :: forall a.
CtEvidence
-> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts, [TcTyVar])
wrapUnifierTcS CtEvidence
ev Role
role UnifyEnv -> TcM a
do_unifications
  = do { (res, cts, unified, rewriters) <- CtEvidence
-> Role
-> (UnifyEnv -> TcM a)
-> TcS (a, Cts, [TcTyVar], RewriterSet)
forall a.
CtEvidence
-> Role
-> (UnifyEnv -> TcM a)
-> TcS (a, Cts, [TcTyVar], RewriterSet)
wrapUnifierX CtEvidence
ev Role
role UnifyEnv -> TcM a
do_unifications

       -- Emit the deferred constraints
       -- See Note [Work-list ordering] in GHC.Tc.Solved.Equality
       --
       -- All the constraints in `cts` share the same rewriter set so,
       -- rather than looking at it one by one, we pass it to
       -- extendWorkListEqs; just a small optimisation.
       ; unless (isEmptyBag cts) $
         updWorkListTcS (extendWorkListEqs rewriters cts)

       -- And kick out any inert constraint that we have unified
       ; _ <- kickOutAfterUnification unified

       ; return (res, cts, unified) }

wrapUnifierX :: CtEvidence -> Role
             -> (UnifyEnv -> TcM a)  -- Some calls to uType
             -> TcS (a, Bag Ct, [TcTyVar], RewriterSet)
wrapUnifierX :: forall a.
CtEvidence
-> Role
-> (UnifyEnv -> TcM a)
-> TcS (a, Cts, [TcTyVar], RewriterSet)
wrapUnifierX CtEvidence
ev Role
role UnifyEnv -> TcM a
do_unifications
  = do { unif_count_ref <- TcS (IORef Int)
getUnifiedRef
       ; wrapTcS $
         do { defer_ref   <- TcM.newTcRef emptyBag
            ; unified_ref <- TcM.newTcRef []
            ; rewriters   <- TcM.zonkRewriterSet (ctEvRewriters ev)
            ; let env = UE { u_role :: Role
u_role      = Role
role
                           , u_rewriters :: RewriterSet
u_rewriters = RewriterSet
rewriters
                           , u_loc :: CtLoc
u_loc       = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
                           , u_defer :: TcRef Cts
u_defer     = TcRef Cts
defer_ref
                           , u_unified :: Maybe (TcRef [TcTyVar])
u_unified   = TcRef [TcTyVar] -> Maybe (TcRef [TcTyVar])
forall a. a -> Maybe a
Just TcRef [TcTyVar]
unified_ref}

            ; res <- do_unifications env

            ; cts     <- TcM.readTcRef defer_ref
            ; unified <- TcM.readTcRef unified_ref

            -- Don't forget to update the count of variables
            -- unified, lest we forget to iterate (#24146)
            ; unless (null unified) $
              TcM.updTcRef unif_count_ref (+ (length unified))

            ; return (res, cts, unified, rewriters) } }


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

checkTouchableTyVarEq
   :: CtEvidence
   -> TcTyVar    -- A touchable meta-tyvar
   -> TcType     -- The RHS
   -> TcS (PuResult () Reduction)
-- Used for Nominal, Wanted equalities, with a touchable meta-tyvar on LHS
-- If checkTouchableTyVarEq tv ty = PuOK cts redn
--   then we can unify
--       tv := ty |> redn
--   with extra wanteds 'cts'
-- If it returns (PuFail reason) we can't unify, and the reason explains why.
checkTouchableTyVarEq :: CtEvidence -> TcTyVar -> Type -> TcS (PuResult () Reduction)
checkTouchableTyVarEq CtEvidence
ev TcTyVar
lhs_tv Type
rhs
  | Bool -> TcTyVar -> Type -> Bool
simpleUnifyCheck Bool
True TcTyVar
lhs_tv Type
rhs
    -- True <=> type families are ok on the RHS
  = do { String -> SDoc -> TcS ()
traceTcS String
"checkTouchableTyVarEq: simple-check wins" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
lhs_tv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs)
       ; PuResult () Reduction -> TcS (PuResult () Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> PuResult () Reduction
forall a. a -> PuResult () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Role -> Type -> Reduction
mkReflRedn Role
Nominal Type
rhs)) }

  | Bool
otherwise
  = do { String -> SDoc -> TcS ()
traceTcS String
"checkTouchableTyVarEq {" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
lhs_tv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs)
       ; check_result <- TcM (PuResult Ct Reduction) -> TcS (PuResult Ct Reduction)
forall a. TcM a -> TcS a
wrapTcS (Type -> TcM (PuResult Ct Reduction)
check_rhs Type
rhs)
       ; traceTcS "checkTouchableTyVarEq }" (ppr lhs_tv $$ ppr check_result)
       ; case check_result of
            PuFail CheckTyEqResult
reason -> PuResult () Reduction -> TcS (PuResult () Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckTyEqResult -> PuResult () Reduction
forall a b. CheckTyEqResult -> PuResult a b
PuFail CheckTyEqResult
reason)
            PuOK Cts
cts Reduction
redn -> do { Cts -> TcS ()
emitWork Cts
cts
                                ; PuResult () Reduction -> TcS (PuResult () Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> PuResult () Reduction
forall a. a -> PuResult () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Reduction
redn) } }

  where
    (MetaInfo
lhs_tv_info, TcLevel
lhs_tv_lvl) = case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
lhs_tv of
       MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info, mtv_tclvl :: TcTyVarDetails -> TcLevel
mtv_tclvl = TcLevel
lvl } -> (MetaInfo
info,TcLevel
lvl)
       TcTyVarDetails
_ -> String -> SDoc -> (MetaInfo, TcLevel)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"checkTouchableTyVarEq" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
lhs_tv)
            -- lhs_tv should be a meta-tyvar

    is_concrete_lhs_tv :: Bool
is_concrete_lhs_tv = MetaInfo -> Bool
isConcreteInfo MetaInfo
lhs_tv_info

    check_rhs :: Type -> TcM (PuResult Ct Reduction)
check_rhs Type
rhs
       -- Crucial special case for  alpha ~ F tys
       -- We don't want to flatten that (F tys)!
       | Just (TyFamLHS TyCon
tc [Type]
tys) <- Type -> Maybe CanEqLHS
canTyFamEqLHS_maybe Type
rhs
       = if Bool
is_concrete_lhs_tv
         then CheckTyEqResult -> TcM (PuResult Ct Reduction)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteConcrete)
         else TyEqFlags Ct -> TyCon -> [Type] -> TcM (PuResult Ct Reduction)
forall a.
TyEqFlags a -> TyCon -> [Type] -> TcM (PuResult a Reduction)
recurseIntoTyConApp TyEqFlags Ct
arg_flags TyCon
tc [Type]
tys
       | Bool
otherwise
       = TyEqFlags Ct -> Type -> TcM (PuResult Ct Reduction)
forall a. TyEqFlags a -> Type -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags Ct
flags Type
rhs

    flags :: TyEqFlags Ct
flags = TEF { tef_foralls :: Bool
tef_foralls  = Bool
False -- isRuntimeUnkSkol lhs_tv
                , tef_fam_app :: TyEqFamApp Ct
tef_fam_app  = CtEvidence
-> EqRel -> (Type -> TcM (PuResult Ct Reduction)) -> TyEqFamApp Ct
forall a. CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp a
mkTEFA_Break CtEvidence
ev EqRel
NomEq Type -> TcM (PuResult Ct Reduction)
break_wanted
                , tef_unifying :: AreUnifying
tef_unifying = MetaInfo -> TcLevel -> LevelCheck -> AreUnifying
Unifying MetaInfo
lhs_tv_info TcLevel
lhs_tv_lvl LevelCheck
LC_Promote
                , tef_lhs :: CanEqLHS
tef_lhs      = TcTyVar -> CanEqLHS
TyVarLHS TcTyVar
lhs_tv
                , tef_occurs :: CheckTyEqProblem
tef_occurs   = CheckTyEqProblem
cteInsolubleOccurs }

    arg_flags :: TyEqFlags Ct
arg_flags = TyEqFlags Ct -> TyEqFlags Ct
forall a. TyEqFlags a -> TyEqFlags a
famAppArgFlags TyEqFlags Ct
flags

    break_wanted :: Type -> TcM (PuResult Ct Reduction)
break_wanted Type
fam_app
      -- Occurs check or skolem escape; so flatten
      = do { let fam_app_kind :: Type
fam_app_kind = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
fam_app
           ; reason <- CheckTyEqProblem
-> TcTyVar -> TcLevel -> VarSet -> TcM CheckTyEqResult
checkPromoteFreeVars CheckTyEqProblem
cteInsolubleOccurs
                            TcTyVar
lhs_tv TcLevel
lhs_tv_lvl (Type -> VarSet
tyCoVarsOfType Type
fam_app_kind)
           ; if not (cterHasNoProblem reason)  -- Failed to promote free vars
             then failCheckWith reason
             else
        do { new_tv_ty <-
              case lhs_tv_info of
                ConcreteTv ConcreteTvOrigin
conc_info ->
                  -- Make a concrete tyvar if lhs_tv is concrete
                  -- e.g.  alpha[2,conc] ~ Maybe (F beta[4])
                  --       We want to flatten to
                  --       alpha[2,conc] ~ Maybe gamma[2,conc]
                  --       gamma[2,conc] ~ F beta[4]
                  ConcreteTvOrigin -> TcLevel -> Type -> TcM Type
TcM.newConcreteTyVarTyAtLevel ConcreteTvOrigin
conc_info TcLevel
lhs_tv_lvl Type
fam_app_kind
                MetaInfo
_ -> TcLevel -> Type -> TcM Type
TcM.newMetaTyVarTyAtLevel TcLevel
lhs_tv_lvl Type
fam_app_kind

           ; let pty = Role -> Type -> Type -> Type
mkPrimEqPredRole Role
Nominal Type
fam_app Type
new_tv_ty
           ; hole <- TcM.newVanillaCoercionHole pty
           ; let new_ev = CtWanted { ctev_pred :: Type
ctev_pred      = Type
pty
                                   , ctev_dest :: TcEvDest
ctev_dest      = CoercionHole -> TcEvDest
HoleDest CoercionHole
hole
                                   , ctev_loc :: CtLoc
ctev_loc       = CtLoc
cb_loc
                                   , ctev_rewriters :: RewriterSet
ctev_rewriters = CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
ev }
           ; return (PuOK (singleCt (mkNonCanonical new_ev))
                          (mkReduction (HoleCo hole) new_tv_ty)) } }

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

------------------------
checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType
            -> TcS (PuResult () 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 () Reduction)
checkTypeEq CtEvidence
ev EqRel
eq_rel CanEqLHS
lhs Type
rhs
  | CtEvidence -> Bool
isGiven CtEvidence
ev
  = 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 (Type -> TcM (PuResult (TcTyVar, Type) Reduction)
check_given_rhs Type
rhs)
       ; traceTcS "checkTypeEq }" (ppr check_result)
       ; case check_result of
            PuFail CheckTyEqResult
reason -> PuResult () Reduction -> TcS (PuResult () Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckTyEqResult -> PuResult () 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) } }

  | Bool
otherwise  -- Wanted
  = do { check_result <- TcM (PuResult Ct Reduction) -> TcS (PuResult Ct Reduction)
forall a. TcM a -> TcS a
wrapTcS (TyEqFlags Ct -> Type -> TcM (PuResult Ct Reduction)
forall a. TyEqFlags a -> Type -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags Ct
wanted_flags Type
rhs)
       ; case check_result of
            PuFail CheckTyEqResult
reason -> PuResult () Reduction -> TcS (PuResult () Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckTyEqResult -> PuResult () Reduction
forall a b. CheckTyEqResult -> PuResult a b
PuFail CheckTyEqResult
reason)
            PuOK Cts
cts Reduction
redn -> do { Cts -> TcS ()
emitWork Cts
cts
                                ; PuResult () Reduction -> TcS (PuResult () Reduction)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reduction -> PuResult () Reduction
forall a. a -> PuResult () a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Reduction
redn) } }
  where
    check_given_rhs :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
    check_given_rhs :: Type -> TcM (PuResult (TcTyVar, Type) Reduction)
check_given_rhs Type
rhs
       -- See Note [Special case for top-level of Given equality]
       | Just (TyFamLHS TyCon
tc [Type]
tys) <- Type -> Maybe CanEqLHS
canTyFamEqLHS_maybe Type
rhs
       = TyEqFlags (TcTyVar, Type)
-> TyCon -> [Type] -> TcM (PuResult (TcTyVar, Type) Reduction)
forall a.
TyEqFlags a -> TyCon -> [Type] -> TcM (PuResult a Reduction)
recurseIntoTyConApp TyEqFlags (TcTyVar, Type)
arg_flags TyCon
tc [Type]
tys
       | Bool
otherwise
       = TyEqFlags (TcTyVar, Type)
-> Type -> TcM (PuResult (TcTyVar, Type) Reduction)
forall a. TyEqFlags a -> Type -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags (TcTyVar, Type)
given_flags Type
rhs

    arg_flags :: TyEqFlags (TcTyVar, Type)
arg_flags = TyEqFlags (TcTyVar, Type) -> TyEqFlags (TcTyVar, Type)
forall a. TyEqFlags a -> TyEqFlags a
famAppArgFlags TyEqFlags (TcTyVar, Type)
given_flags

    given_flags :: TyEqFlags (TcTyVar,TcType)
    given_flags :: TyEqFlags (TcTyVar, Type)
given_flags = TEF { tef_lhs :: CanEqLHS
tef_lhs      = CanEqLHS
lhs
                      , tef_foralls :: Bool
tef_foralls  = Bool
False
                      , tef_unifying :: AreUnifying
tef_unifying = AreUnifying
NotUnifying
                      , tef_fam_app :: TyEqFamApp (TcTyVar, Type)
tef_fam_app  = CtEvidence
-> EqRel
-> (Type -> TcM (PuResult (TcTyVar, Type) Reduction))
-> TyEqFamApp (TcTyVar, Type)
forall a. CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp a
mkTEFA_Break CtEvidence
ev EqRel
eq_rel Type -> TcM (PuResult (TcTyVar, Type) Reduction)
break_given
                      , tef_occurs :: CheckTyEqProblem
tef_occurs   = CheckTyEqProblem
occ_prob }
        -- TEFA_Break used for: [G] a ~ Maybe (F a)
        --                   or [W] F a ~ Maybe (F a)

    wanted_flags :: TyEqFlags Ct
wanted_flags = TEF { tef_lhs :: CanEqLHS
tef_lhs      = CanEqLHS
lhs
                       , tef_foralls :: Bool
tef_foralls  = Bool
False
                       , tef_unifying :: AreUnifying
tef_unifying = AreUnifying
NotUnifying
                       , tef_fam_app :: TyEqFamApp Ct
tef_fam_app  = TyEqFamApp Ct
forall a. TyEqFamApp a
TEFA_Recurse
                       , tef_occurs :: CheckTyEqProblem
tef_occurs   = CheckTyEqProblem
occ_prob }
        -- TEFA_Recurse: see Note [Don't cycle-break Wanteds when not unifying]

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

    break_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
    break_given :: Type -> TcM (PuResult (TcTyVar, Type) Reduction)
break_given Type
fam_app
      = do { new_tv <- Type -> TcM TcTyVar
TcM.newCycleBreakerTyVar (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
fam_app)
           ; return (PuOK (unitBag (new_tv, fam_app))
                          (mkReflRedn Nominal (mkTyVarTy new_tv))) }
                    -- Why reflexive? See Detail (4) of the Note

    ---------------------------
    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) -> TcS CtEvidence -> TcS Ct
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar 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
mkPrimEqPred 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
CycleBreakerOrigin

mkTEFA_Break :: CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp a
mkTEFA_Break :: forall a. CtEvidence -> EqRel -> FamAppBreaker a -> TyEqFamApp a
mkTEFA_Break CtEvidence
ev EqRel
eq_rel FamAppBreaker a
breaker
  | EqRel
NomEq <- EqRel
eq_rel
  , Bool -> Bool
not Bool
cycle_breaker_origin
  = FamAppBreaker a -> TyEqFamApp a
forall a. FamAppBreaker a -> TyEqFamApp a
TEFA_Break FamAppBreaker a
breaker
  | Bool
otherwise
  = TyEqFamApp a
forall a. TyEqFamApp a
TEFA_Recurse
  where
    -- cycle_breaker_origin: see Detail (7) of Note [Type equality cycles]
    -- in GHC.Tc.Solver.Equality
    cycle_breaker_origin :: Bool
cycle_breaker_origin = case CtLoc -> CtOrigin
ctLocOrigin (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) of
                              CycleBreakerOrigin {} -> Bool
True
                              CtOrigin
_                     -> Bool
False

-------------------------
-- | 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 [Special case for top-level of Given equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We take care when examining
    [G] F ty ~ G (...(F ty)...)
where both sides are TyFamLHSs.  We don't want to flatten that RHS to
    [G] F ty ~ cbv
    [G] G (...(F ty)...) ~ cbv
Instead we'd like to say "occurs-check" and swap LHS and RHS, which yields a
canonical constraint
    [G] G (...(F ty)...) ~ F ty
That tents to rewrite a big type to smaller one. This happens in T15703,
where we had:
    [G] Pure g ~ From1 (To1 (Pure g))
Making a loop breaker and rewriting left to right just makes much bigger
types than swapping it over.

(We might hope to have swapped it over before getting to checkTypeEq,
but better safe than sorry.)

NB: We never see a TyVarLHS here, such as
    [G] a ~ F tys here
because we'd have swapped it to
   [G] F tys ~ a
in canEqCanLHS2, before getting to checkTypeEq.

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`.
-}