{-# LANGUAGE CPP, DeriveFunctor, TypeFamilies #-}

-- Type definitions for the constraint solver
module TcSMonad (

    -- The work list
    WorkList(..), isEmptyWorkList, emptyWorkList,
    extendWorkListNonEq, extendWorkListCt,
    extendWorkListCts, extendWorkListEq, extendWorkListFunEq,
    appendWorkList, extendWorkListImplic,
    selectNextWorkItem,
    workListSize, workListWantedCount,
    getWorkList, updWorkListTcS,

    -- The TcS monad
    TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
    failTcS, warnTcS, addErrTcS,
    runTcSEqualities,
    nestTcS, nestImplicTcS, setEvBindsTcS,
    checkConstraintsTcS, checkTvConstraintsTcS,

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

    QCInst(..),

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

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

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

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

    -- Inerts
    InertSet(..), InertCans(..),
    updInertTcS, updInertCans, updInertDicts, updInertIrreds,
    getNoGivenEqs, setInertCans,
    getInertEqs, getInertCans, getInertGivens,
    getInertInsols,
    getTcSInerts, setTcSInerts,
    matchableGivens, prohibitedSuperClassSolve, mightMatchLater,
    getUnsolvedInerts,
    removeInertCts, getPendingGivenScs,
    addInertCan, insertFunEq, addInertForAll,
    emitWorkNC, emitWork,
    isImprovable,

    -- The Model
    kickOutAfterUnification,

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

    -- Inert CDictCans
    DictMap, emptyDictMap, lookupInertDict, findDictsByClass, addDict,
    addDictsByClass, delDict, foldDicts, filterDicts, findDict,

    -- Inert CTyEqCans
    EqualCtList, findTyEqs, foldTyEqs, isInInertEqs,
    lookupInertTyVar,

    -- Inert solved dictionaries
    addSolvedDict, lookupSolvedDict,

    -- Irreds
    foldIrreds,

    -- The flattening cache
    lookupFlatCache, extendFlatCache, newFlattenSkolem,            -- Flatten skolems
    dischargeFunEq, pprKicked,

    -- Inert CFunEqCans
    updInertFunEqs, findFunEq,
    findFunEqsByTyCon,

    instDFunType,                              -- Instantiation

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

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

    -- References
    newTcRef, readTcRef, writeTcRef, updTcRef,

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

#include "HsVersions.h"

import GhcPrelude

import HscTypes

import qualified Inst as TcM
import InstEnv
import FamInst
import FamInstEnv

import qualified TcRnMonad as TcM
import qualified TcMType as TcM
import qualified ClsInst as TcM( matchGlobalInst, ClsInstResult(..) )
import qualified TcEnv as TcM
       ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl )
import ClsInst( InstanceWhat(..), safeOverlap, instanceReturnsDictCon )
import TcType
import DynFlags
import Type
import Coercion
import Unify

import TcEvidence
import Class
import TyCon
import TcErrors   ( solverDepthErrorTcS )

import Name
import Module ( HasModule, getModule )
import RdrName ( GlobalRdrEnv, GlobalRdrElt )
import qualified RnEnv as TcM
import Var
import VarEnv
import VarSet
import Outputable
import Bag
import UniqSupply
import Util
import TcRnTypes
import TcOrigin
import Constraint
import Predicate

import Unique
import UniqFM
import UniqDFM
import Maybes

import CoreMap
import Control.Monad
import qualified Control.Monad.Fail as MonadFail
import MonadUtils
import Data.IORef
import Data.List ( partition, mapAccumL )

#if defined(DEBUG)
import Digraph
import UniqSet
#endif

{-
************************************************************************
*                                                                      *
*                            Worklists                                *
*  Canonical and non-canonical constraints that the simplifier has to  *
*  work on. Including their simplification depths.                     *
*                                                                      *
*                                                                      *
************************************************************************

Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
A WorkList contains canonical and non-canonical items (of all flavors).
Notice that each Ct now has a simplification depth. We may
consider using this depth for prioritization as well in the future.

As a simple form of priority queue, our worklist separates out

* equalities (wl_eqs); see Note [Prioritise equalities]
* type-function equalities (wl_funeqs)
* all the rest (wl_rest)

Note [Prioritise equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's very important to process equalities /first/:

* (Efficiency)  The general reason to do so is that if we process a
  class constraint first, we may end up putting it into the inert set
  and then kicking it out later.  That's extra work compared to just
  doing the equality first.

* (Avoiding fundep iteration) As #14723 showed, it's possible to
  get non-termination if we
      - Emit the Derived fundep equalities for a class constraint,
        generating some fresh unification variables.
      - That leads to some unification
      - Which kicks out the class constraint
      - Which isn't solved (because there are still some more Derived
        equalities in the work-list), but generates yet more fundeps
  Solution: prioritise derived equalities over class constraints

* (Class equalities) We need to prioritise equalities even if they
  are hidden inside a class constraint;
  see Note [Prioritise class equalities]

* (Kick-out) We want to apply this priority scheme to kicked-out
  constraints too (see the call to extendWorkListCt in kick_out_rewritable
  E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
  homo-kinded when kicked out, and hence we want to prioritise it.

* (Derived equalities) Originally we tried to postpone processing
  Derived equalities, in the hope that we might never need to deal
  with them at all; but in fact we must process Derived equalities
  eagerly, partly for the (Efficiency) reason, and more importantly
  for (Avoiding fundep iteration).

Note [Prioritise class equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We prioritise equalities in the solver (see selectWorkItem). But class
constraints like (a ~ b) and (a ~~ b) are actually equalities too;
see Note [The equality types story] in TysPrim.

Failing to prioritise these is inefficient (more kick-outs etc).
But, worse, it can prevent us spotting a "recursive knot" among
Wanted constraints.  See comment:10 of #12734 for a worked-out
example.

So we arrange to put these particular class constraints in the wl_eqs.

  NB: since we do not currently apply the substitution to the
  inert_solved_dicts, the knot-tying still seems a bit fragile.
  But this makes it better.

-}

-- See Note [WorkList priorities]
data WorkList
  = WL { WorkList -> [Ct]
wl_eqs     :: [Ct]  -- CTyEqCan, CDictCan, CIrredCan
                             -- Given, Wanted, and Derived
                       -- Contains both equality constraints and their
                       -- class-level variants (a~b) and (a~~b);
                       -- See Note [Prioritise equalities]
                       -- See Note [Prioritise class equalities]

       , WorkList -> [Ct]
wl_funeqs  :: [Ct]

       , WorkList -> [Ct]
wl_rest    :: [Ct]

       , WorkList -> Bag Implication
wl_implics :: Bag Implication  -- See Note [Residual implications]
    }

appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList
    (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs1, wl_funeqs :: WorkList -> [Ct]
wl_funeqs = [Ct]
funeqs1, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest1
        , wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics1 })
    (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs2, wl_funeqs :: WorkList -> [Ct]
wl_funeqs = [Ct]
funeqs2, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest2
        , wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics2 })
   = WL :: [Ct] -> [Ct] -> [Ct] -> Bag Implication -> WorkList
WL { wl_eqs :: [Ct]
wl_eqs     = [Ct]
eqs1     [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
eqs2
        , wl_funeqs :: [Ct]
wl_funeqs  = [Ct]
funeqs1  [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
funeqs2
        , wl_rest :: [Ct]
wl_rest    = [Ct]
rest1    [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
rest2
        , wl_implics :: Bag Implication
wl_implics = Bag Implication
implics1 Bag Implication -> Bag Implication -> Bag Implication
forall a. Bag a -> Bag a -> Bag a
`unionBags`   Bag Implication
implics2 }

workListSize :: WorkList -> Int
workListSize :: WorkList -> Int
workListSize (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_funeqs :: WorkList -> [Ct]
wl_funeqs = [Ct]
funeqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
  = [Ct] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ct]
eqs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Ct] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ct]
funeqs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Ct] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ct]
rest

workListWantedCount :: WorkList -> Int
-- Count the things we need to solve
-- excluding the insolubles (c.f. inert_count)
workListWantedCount :: WorkList -> Int
workListWantedCount (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
  = (Ct -> Bool) -> [Ct] -> Int
forall a. (a -> Bool) -> [a] -> Int
count Ct -> Bool
isWantedCt [Ct]
eqs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Ct -> Bool) -> [Ct] -> Int
forall a. (a -> Bool) -> [a] -> Int
count Ct -> Bool
is_wanted [Ct]
rest
  where
    is_wanted :: Ct -> Bool
is_wanted Ct
ct
     | CIrredCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_insol :: Ct -> Bool
cc_insol = Bool
insol } <- Ct
ct
     = Bool -> Bool
not Bool
insol Bool -> Bool -> Bool
&& CtEvidence -> Bool
isWanted CtEvidence
ev
     | Bool
otherwise
     = Ct -> Bool
isWantedCt Ct
ct

extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl = WorkList
wl { wl_eqs :: [Ct]
wl_eqs = Ct
ct Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: WorkList -> [Ct]
wl_eqs WorkList
wl }

extendWorkListFunEq :: Ct -> WorkList -> WorkList
extendWorkListFunEq :: Ct -> WorkList -> WorkList
extendWorkListFunEq Ct
ct WorkList
wl = WorkList
wl { wl_funeqs :: [Ct]
wl_funeqs = Ct
ct Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: WorkList -> [Ct]
wl_funeqs WorkList
wl }

extendWorkListNonEq :: Ct -> WorkList -> WorkList
-- Extension by non equality
extendWorkListNonEq :: Ct -> WorkList -> WorkList
extendWorkListNonEq Ct
ct WorkList
wl = WorkList
wl { wl_rest :: [Ct]
wl_rest = Ct
ct Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: WorkList -> [Ct]
wl_rest WorkList
wl }

extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList
extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList
extendWorkListDeriveds [CtEvidence]
evs WorkList
wl
  = [Ct] -> WorkList -> WorkList
extendWorkListCts ((CtEvidence -> Ct) -> [CtEvidence] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> Ct
mkNonCanonical [CtEvidence]
evs) WorkList
wl

extendWorkListImplic :: Bag Implication -> WorkList -> WorkList
extendWorkListImplic :: Bag Implication -> WorkList -> WorkList
extendWorkListImplic Bag Implication
implics WorkList
wl = WorkList
wl { wl_implics :: Bag Implication
wl_implics = Bag Implication
implics Bag Implication -> Bag Implication -> Bag Implication
forall a. Bag a -> Bag a -> Bag a
`unionBags` WorkList -> Bag Implication
wl_implics WorkList
wl }

extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt :: Ct -> WorkList -> WorkList
extendWorkListCt Ct
ct WorkList
wl
 = case PredType -> Pred
classifyPredType (Ct -> PredType
ctPred Ct
ct) of
     EqPred EqRel
NomEq PredType
ty1 PredType
_
       | Just TyCon
tc <- PredType -> Maybe TyCon
tcTyConAppTyCon_maybe PredType
ty1
       , TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
       -> Ct -> WorkList -> WorkList
extendWorkListFunEq Ct
ct WorkList
wl

     EqPred {}
       -> Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl

     ClassPred Class
cls [PredType]
_  -- See Note [Prioritise class equalities]
       |  Class -> Bool
isEqPredClass Class
cls
       -> Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl

     Pred
_ -> Ct -> WorkList -> WorkList
extendWorkListNonEq Ct
ct WorkList
wl

extendWorkListCts :: [Ct] -> WorkList -> WorkList
-- Agnostic
extendWorkListCts :: [Ct] -> WorkList -> WorkList
extendWorkListCts [Ct]
cts WorkList
wl = (Ct -> WorkList -> WorkList) -> WorkList -> [Ct] -> WorkList
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> WorkList -> WorkList
extendWorkListCt WorkList
wl [Ct]
cts

isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_funeqs :: WorkList -> [Ct]
wl_funeqs = [Ct]
funeqs
                    , wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics })
  = [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs Bool -> Bool -> Bool
&& [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
rest Bool -> Bool -> Bool
&& [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
funeqs Bool -> Bool -> Bool
&& Bag Implication -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Implication
implics

emptyWorkList :: WorkList
emptyWorkList :: WorkList
emptyWorkList = WL :: [Ct] -> [Ct] -> [Ct] -> Bag Implication -> WorkList
WL { wl_eqs :: [Ct]
wl_eqs  = [], wl_rest :: [Ct]
wl_rest = []
                   , wl_funeqs :: [Ct]
wl_funeqs = [], wl_implics :: Bag Implication
wl_implics = Bag Implication
forall a. Bag a
emptyBag }

selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
-- See Note [Prioritise equalities]
selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
selectWorkItem wl :: WorkList
wl@(WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_funeqs :: WorkList -> [Ct]
wl_funeqs = [Ct]
feqs
                      , wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
  | Ct
ct:[Ct]
cts <- [Ct]
eqs  = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_eqs :: [Ct]
wl_eqs    = [Ct]
cts })
  | Ct
ct:[Ct]
fes <- [Ct]
feqs = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_funeqs :: [Ct]
wl_funeqs = [Ct]
fes })
  | Ct
ct:[Ct]
cts <- [Ct]
rest = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_rest :: [Ct]
wl_rest   = [Ct]
cts })
  | Bool
otherwise      = Maybe (Ct, WorkList)
forall a. Maybe a
Nothing

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

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

-- Pretty printing
instance Outputable WorkList where
  ppr :: WorkList -> SDoc
ppr (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_funeqs :: WorkList -> [Ct]
wl_funeqs = [Ct]
feqs
          , wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics })
   = String -> SDoc
text String
"WL" SDoc -> SDoc -> SDoc
<+> (SDoc -> SDoc
braces (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
     [SDoc] -> SDoc
vcat [ Bool -> SDoc -> SDoc
ppUnless ([Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
            String -> SDoc
text String
"Eqs =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
eqs)
          , Bool -> SDoc -> SDoc
ppUnless ([Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
feqs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
            String -> SDoc
text String
"Funeqs =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
feqs)
          , Bool -> SDoc -> SDoc
ppUnless ([Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
rest) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
            String -> SDoc
text String
"Non-eqs =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
rest)
          , Bool -> SDoc -> SDoc
ppUnless (Bag Implication -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Implication
implics) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
            SDoc -> SDoc -> SDoc
ifPprDebug (String -> SDoc
text String
"Implics =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat ((Implication -> SDoc) -> [Implication] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Implication -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Bag Implication -> [Implication]
forall a. Bag a -> [a]
bagToList Bag Implication
implics)))
                       (String -> SDoc
text String
"(Implics omitted)")
          ])


{- *********************************************************************
*                                                                      *
                InertSet: the inert set
*                                                                      *
*                                                                      *
********************************************************************* -}

data InertSet
  = IS { InertSet -> InertCans
inert_cans :: InertCans
              -- Canonical Given, Wanted, Derived
              -- Sometimes called "the inert set"

       , InertSet -> [(TcTyVar, PredType)]
inert_fsks :: [(TcTyVar, TcType)]
              -- A list of (fsk, ty) pairs; we add one element when we flatten
              -- a function application in a Given constraint, creating
              -- a new fsk in newFlattenSkolem.  When leaving a nested scope,
              -- unflattenGivens unifies fsk := ty
              --
              -- We could also get this info from inert_funeqs, filtered by
              -- level, but it seems simpler and more direct to capture the
              -- fsk as we generate them.

       , InertSet -> ExactFunEqMap (TcCoercion, PredType, CtFlavour)
inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
              -- See Note [Type family equations]
              -- If    F tys :-> (co, rhs, flav),
              -- then  co :: F tys ~ rhs
              --       flav is [G] or [WD]
              --
              -- Just a hash-cons cache for use when flattening only
              -- These include entirely un-processed goals, so don't use
              -- them to solve a top-level goal, else you may end up solving
              -- (w:F ty ~ a) by setting w:=w!  We just use the flat-cache
              -- when allocating a new flatten-skolem.
              -- Not necessarily inert wrt top-level equations (or inert_cans)

              -- NB: An ExactFunEqMap -- this doesn't match via loose types!

       , InertSet -> DictMap CtEvidence
inert_solved_dicts   :: DictMap CtEvidence
              -- All Wanteds, of form ev :: C t1 .. tn
              -- See Note [Solved dictionaries]
              -- and Note [Do not add superclasses of solved dictionaries]
       }

instance Outputable InertSet where
  ppr :: InertSet -> SDoc
ppr (IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
ics
          , inert_fsks :: InertSet -> [(TcTyVar, PredType)]
inert_fsks = [(TcTyVar, PredType)]
ifsks
          , inert_solved_dicts :: InertSet -> DictMap CtEvidence
inert_solved_dicts = DictMap CtEvidence
solved_dicts })
      = [SDoc] -> SDoc
vcat [ InertCans -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertCans
ics
             , String -> SDoc
text String
"Inert fsks =" SDoc -> SDoc -> SDoc
<+> [(TcTyVar, PredType)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(TcTyVar, PredType)]
ifsks
             , Bool -> SDoc -> SDoc
ppUnless ([CtEvidence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CtEvidence]
dicts) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
               String -> SDoc
text String
"Solved dicts =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat ((CtEvidence -> SDoc) -> [CtEvidence] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr [CtEvidence]
dicts) ]
         where
           dicts :: [CtEvidence]
dicts = Bag CtEvidence -> [CtEvidence]
forall a. Bag a -> [a]
bagToList (DictMap CtEvidence -> Bag CtEvidence
forall a. DictMap a -> Bag a
dictsToBag DictMap CtEvidence
solved_dicts)

emptyInertCans :: InertCans
emptyInertCans :: InertCans
emptyInertCans
  = IC :: InertEqs
-> FunEqMap Ct
-> FunEqMap Ct
-> [QCInst]
-> FunEqMap Ct
-> Cts
-> Int
-> InertCans
IC { inert_count :: Int
inert_count    = Int
0
       , inert_eqs :: InertEqs
inert_eqs      = InertEqs
forall a. DVarEnv a
emptyDVarEnv
       , inert_dicts :: FunEqMap Ct
inert_dicts    = FunEqMap Ct
forall a. DictMap a
emptyDicts
       , inert_safehask :: FunEqMap Ct
inert_safehask = FunEqMap Ct
forall a. DictMap a
emptyDicts
       , inert_funeqs :: FunEqMap Ct
inert_funeqs   = FunEqMap Ct
forall a. DictMap a
emptyFunEqs
       , inert_insts :: [QCInst]
inert_insts    = []
       , inert_irreds :: Cts
inert_irreds   = Cts
emptyCts }

emptyInert :: InertSet
emptyInert :: InertSet
emptyInert
  = IS :: InertCans
-> [(TcTyVar, PredType)]
-> ExactFunEqMap (TcCoercion, PredType, CtFlavour)
-> DictMap CtEvidence
-> InertSet
IS { inert_cans :: InertCans
inert_cans         = InertCans
emptyInertCans
       , inert_fsks :: [(TcTyVar, PredType)]
inert_fsks         = []
       , inert_flat_cache :: ExactFunEqMap (TcCoercion, PredType, CtFlavour)
inert_flat_cache   = ExactFunEqMap (TcCoercion, PredType, CtFlavour)
forall a. ExactFunEqMap a
emptyExactFunEqs
       , inert_solved_dicts :: DictMap CtEvidence
inert_solved_dicts = DictMap CtEvidence
forall a. DictMap a
emptyDictMap }


{- Note [Solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we apply a top-level instance declaration, we add the "solved"
dictionary to the inert_solved_dicts.  In general, we use it to avoid
creating a new EvVar when we have a new goal that we have solved in
the past.

But in particular, we can use it to create *recursive* dictionaries.
The simplest, degnerate case is
    instance C [a] => C [a] where ...
If we have
    [W] d1 :: C [x]
then we can apply the instance to get
    d1 = $dfCList d
    [W] d2 :: C [x]
Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1.
    d1 = $dfCList d
    d2 = d1

See Note [Example of recursive dictionaries]

VERY IMPORTANT INVARIANT:

 (Solved Dictionary Invariant)
    Every member of the inert_solved_dicts is the result
    of applying an instance declaration that "takes a step"

    An instance "takes a step" if it has the form
        dfunDList d1 d2 = MkD (...) (...) (...)
    That is, the dfun is lazy in its arguments, and guarantees to
    immediately return a dictionary constructor.  NB: all dictionary
    data constructors are lazy in their arguments.

    This property is crucial to ensure that all dictionaries are
    non-bottom, which in turn ensures that the whole "recursive
    dictionary" idea works at all, even if we get something like
        rec { d = dfunDList d dx }
    See Note [Recursive superclasses] in TcInstDcls.

 Reason:
   - All instances, except two exceptions listed below, "take a step"
     in the above sense

   - Exception 1: local quantified constraints have no such guarantee;
     indeed, adding a "solved dictionary" when appling a quantified
     constraint led to the ability to define unsafeCoerce
     in #17267.

   - Exception 2: the magic built-in instace for (~) has no
     such guarantee.  It behaves as if we had
         class    (a ~# b) => (a ~ b) where {}
         instance (a ~# b) => (a ~ b) where {}
     The "dfun" for the instance is strict in the coercion.
     Anyway there's no point in recording a "solved dict" for
     (t1 ~ t2); it's not going to allow a recursive dictionary
     to be constructed.  Ditto (~~) and Coercible.

THEREFORE we only add a "solved dictionary"
  - when applying an instance declaration
  - subject to Exceptions 1 and 2 above

In implementation terms
  - TcSMonad.addSolvedDict adds a new solved dictionary,
    conditional on the kind of instance

  - It is only called when applying an instance decl,
    in TcInteract.doTopReactDict

  - ClsInst.InstanceWhat says what kind of instance was
    used to solve the constraint.  In particular
      * LocalInstance identifies quantified constraints
      * BuiltinEqInstance identifies the strange built-in
        instances for equality.

  - ClsInst.instanceReturnsDictCon says which kind of
    instance guarantees to return a dictionary constructor

Other notes about solved dictionaries

* See also Note [Do not add superclasses of solved dictionaries]

* The inert_solved_dicts field is not rewritten by equalities,
  so it may get out of date.

* The inert_solved_dicts are all Wanteds, never givens

* We only cache dictionaries from top-level instances, not from
  local quantified constraints.  Reason: if we cached the latter
  we'd need to purge the cache when bringing new quantified
  constraints into scope, because quantified constraints "shadow"
  top-level instances.

Note [Do not add superclasses of solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Every member of inert_solved_dicts is the result of applying a
dictionary function, NOT of applying superclass selection to anything.
Consider

        class Ord a => C a where
        instance Ord [a] => C [a] where ...

Suppose we are trying to solve
  [G] d1 : Ord a
  [W] d2 : C [a]

Then we'll use the instance decl to give

  [G] d1 : Ord a     Solved: d2 : C [a] = $dfCList d3
  [W] d3 : Ord [a]

We must not add d4 : Ord [a] to the 'solved' set (by taking the
superclass of d2), otherwise we'll use it to solve d3, without ever
using d1, which would be a catastrophe.

Solution: when extending the solved dictionaries, do not add superclasses.
That's why each element of the inert_solved_dicts is the result of applying
a dictionary function.

Note [Example of recursive dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--- Example 1

    data D r = ZeroD | SuccD (r (D r));

    instance (Eq (r (D r))) => Eq (D r) where
        ZeroD     == ZeroD     = True
        (SuccD a) == (SuccD b) = a == b
        _         == _         = False;

    equalDC :: D [] -> D [] -> Bool;
    equalDC = (==);

We need to prove (Eq (D [])). Here's how we go:

   [W] d1 : Eq (D [])
By instance decl of Eq (D r):
   [W] d2 : Eq [D []]      where   d1 = dfEqD d2
By instance decl of Eq [a]:
   [W] d3 : Eq (D [])      where   d2 = dfEqList d3
                                   d1 = dfEqD d2
Now this wanted can interact with our "solved" d1 to get:
    d3 = d1

-- Example 2:
This code arises in the context of "Scrap Your Boilerplate with Class"

    class Sat a
    class Data ctx a
    instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2

    class Data Maybe a => Foo a

    instance Foo t => Sat (Maybe t)                             -- dfunSat

    instance Data Maybe a => Foo a                              -- dfunFoo1
    instance Foo a        => Foo [a]                            -- dfunFoo2
    instance                 Foo [Char]                         -- dfunFoo3

Consider generating the superclasses of the instance declaration
         instance Foo a => Foo [a]

So our problem is this
    [G] d0 : Foo t
    [W] d1 : Data Maybe [t]   -- Desired superclass

We may add the given in the inert set, along with its superclasses
  Inert:
    [G] d0 : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  WorkList
    [W] d1 : Data Maybe [t]

Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
  Inert:
    [G] d0 : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  Solved:
        d1 : Data Maybe [t]
  WorkList:
    [W] d2 : Sat (Maybe [t])
    [W] d3 : Data Maybe t

Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
  Inert:
    [G] d0 : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  Solved:
        d1 : Data Maybe [t]
        d2 : Sat (Maybe [t])
  WorkList:
    [W] d3 : Data Maybe t
    [W] d4 : Foo [t]

Now, we can just solve d3 from d01; d3 := d01
  Inert
    [G] d0 : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  Solved:
        d1 : Data Maybe [t]
        d2 : Sat (Maybe [t])
  WorkList
    [W] d4 : Foo [t]

Now, solve d4 using dfunFoo2;  d4 := dfunFoo2 d5
  Inert
    [G] d0  : Foo t
    [G] d01 : Data Maybe t   -- Superclass of d0
  Solved:
        d1 : Data Maybe [t]
        d2 : Sat (Maybe [t])
        d4 : Foo [t]
  WorkList:
    [W] d5 : Foo t

Now, d5 can be solved! d5 := d0

Result
   d1 := dfunData2 d2 d3
   d2 := dfunSat d4
   d3 := d01
   d4 := dfunFoo2 d5
   d5 := d0
-}

{- *********************************************************************
*                                                                      *
                InertCans: the canonical inerts
*                                                                      *
*                                                                      *
********************************************************************* -}

data InertCans   -- See Note [Detailed InertCans Invariants] for more
  = IC { InertCans -> InertEqs
inert_eqs :: InertEqs
              -- See Note [inert_eqs: the inert equalities]
              -- All CTyEqCans; index is the LHS tyvar
              -- Domain = skolems and untouchables; a touchable would be unified

       , InertCans -> FunEqMap Ct
inert_funeqs :: FunEqMap Ct
              -- All CFunEqCans; index is the whole family head type.
              -- All Nominal (that's an invarint of all CFunEqCans)
              -- LHS is fully rewritten (modulo eqCanRewrite constraints)
              --     wrt inert_eqs
              -- Can include all flavours, [G], [W], [WD], [D]
              -- See Note [Type family equations]

       , InertCans -> FunEqMap Ct
inert_dicts :: DictMap Ct
              -- Dictionaries only
              -- All fully rewritten (modulo flavour constraints)
              --     wrt inert_eqs

       , InertCans -> [QCInst]
inert_insts :: [QCInst]

       , InertCans -> FunEqMap Ct
inert_safehask :: DictMap Ct
              -- Failed dictionary resolution due to Safe Haskell overlapping
              -- instances restriction. We keep this separate from inert_dicts
              -- as it doesn't cause compilation failure, just safe inference
              -- failure.
              --
              -- ^ See Note [Safe Haskell Overlapping Instances Implementation]
              -- in TcSimplify

       , InertCans -> Cts
inert_irreds :: Cts
              -- Irreducible predicates that cannot be made canonical,
              --     and which don't interact with others (e.g.  (c a))
              -- and insoluble predicates (e.g.  Int ~ Bool, or a ~ [a])

       , InertCans -> Int
inert_count :: Int
              -- Number of Wanted goals in
              --     inert_eqs, inert_dicts, inert_safehask, inert_irreds
              -- Does not include insolubles
              -- When non-zero, keep trying to solve
       }

type InertEqs    = DTyVarEnv EqualCtList
type EqualCtList = [Ct]  -- See Note [EqualCtList invariants]

{- Note [Detailed InertCans Invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The InertCans represents a collection of constraints with the following properties:

  * All canonical

  * No two dictionaries with the same head
  * No two CIrreds with the same type

  * Family equations inert wrt top-level family axioms

  * Dictionaries have no matching top-level instance

  * Given family or dictionary constraints don't mention touchable
    unification variables

  * Non-CTyEqCan constraints are fully rewritten with respect
    to the CTyEqCan equalities (modulo canRewrite of course;
    eg a wanted cannot rewrite a given)

  * CTyEqCan equalities: see Note [inert_eqs: the inert equalities]

Note [EqualCtList invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    * All are equalities
    * All these equalities have the same LHS
    * The list is never empty
    * No element of the list can rewrite any other
    * Derived before Wanted

From the fourth invariant it follows that the list is
   - A single [G], or
   - Zero or one [D] or [WD], followd by any number of [W]

The Wanteds can't rewrite anything which is why we put them last

Note [Type family equations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Type-family equations, CFunEqCans, of form (ev : F tys ~ ty),
live in three places

  * The work-list, of course

  * The inert_funeqs are un-solved but fully processed, and in
    the InertCans. They can be [G], [W], [WD], or [D].

  * The inert_flat_cache.  This is used when flattening, to get maximal
    sharing. Everthing in the inert_flat_cache is [G] or [WD]

    It contains lots of things that are still in the work-list.
    E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
        work list.  Then we flatten w1, dumping (w3: G a ~ f1) in the work
        list.  Now if we flatten w2 before we get to w3, we still want to
        share that (G a).
    Because it contains work-list things, DO NOT use the flat cache to solve
    a top-level goal.  Eg in the above example we don't want to solve w3
    using w3 itself!

The CFunEqCan Ownership Invariant:

  * Each [G/W/WD] CFunEqCan has a distinct fsk or fmv
    It "owns" that fsk/fmv, in the sense that:
      - reducing a [W/WD] CFunEqCan fills in the fmv
      - unflattening a [W/WD] CFunEqCan fills in the fmv
      (in both cases unless an occurs-check would result)

  * In contrast a [D] CFunEqCan does not "own" its fmv:
      - reducing a [D] CFunEqCan does not fill in the fmv;
        it just generates an equality
      - unflattening ignores [D] CFunEqCans altogether


Note [inert_eqs: the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Definition [Can-rewrite relation]
A "can-rewrite" relation between flavours, written f1 >= f2, is a
binary relation with the following properties

  (R1) >= is transitive
  (R2) If f1 >= f, and f2 >= f,
       then either f1 >= f2 or f2 >= f1

Lemma.  If f1 >= f then f1 >= f1
Proof.  By property (R2), with f1=f2

Definition [Generalised substitution]
A "generalised substitution" S is a set of triples (a -f-> t), where
  a is a type variable
  t is a type
  f is a flavour
such that
  (WF1) if (a -f1-> t1) in S
           (a -f2-> t2) in S
        then neither (f1 >= f2) nor (f2 >= f1) hold
  (WF2) if (a -f-> t) is in S, then t /= a

Definition [Applying a generalised substitution]
If S is a generalised substitution
   S(f,a) = t,  if (a -fs-> t) in S, and fs >= f
          = a,  otherwise
Application extends naturally to types S(f,t), modulo roles.
See Note [Flavours with roles].

Theorem: S(f,a) is well defined as a function.
Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S,
               and  f1 >= f and f2 >= f
       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)

Notation: repeated application.
  S^0(f,t)     = t
  S^(n+1)(f,t) = S(f, S^n(t))

Definition: inert generalised substitution
A generalised substitution S is "inert" iff

  (IG1) there is an n such that
        for every f,t, S^n(f,t) = S^(n+1)(f,t)

By (IG1) we define S*(f,t) to be the result of exahaustively
applying S(f,_) to t.

----------------------------------------------------------------
Our main invariant:
   the inert CTyEqCans should be an inert generalised substitution
----------------------------------------------------------------

Note that inertness is not the same as idempotence.  To apply S to a
type, you may have to apply it recursive.  But inertness does
guarantee that this recursive use will terminate.

Note [Extending the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main Theorem [Stability under extension]
   Suppose we have a "work item"
       a -fw-> t
   and an inert generalised substitution S,
   THEN the extended substitution T = S+(a -fw-> t)
        is an inert generalised substitution
   PROVIDED
      (T1) S(fw,a) = a     -- LHS of work-item is a fixpoint of S(fw,_)
      (T2) S(fw,t) = t     -- RHS of work-item is a fixpoint of S(fw,_)
      (T3) a not in t      -- No occurs check in the work item

      AND, for every (b -fs-> s) in S:
           (K0) not (fw >= fs)
                Reason: suppose we kick out (a -fs-> s),
                        and add (a -fw-> t) to the inert set.
                        The latter can't rewrite the former,
                        so the kick-out achieved nothing

           OR { (K1) not (a = b)
                     Reason: if fw >= fs, WF1 says we can't have both
                             a -fw-> t  and  a -fs-> s

                AND (K2): guarantees inertness of the new substitution
                    {  (K2a) not (fs >= fs)
                    OR (K2b) fs >= fw
                    OR (K2d) a not in s }

                AND (K3) See Note [K3: completeness of solving]
                    { (K3a) If the role of fs is nominal: s /= a
                      (K3b) If the role of fs is representational:
                            s is not of form (a t1 .. tn) } }


Conditions (T1-T3) are established by the canonicaliser
Conditions (K1-K3) are established by TcSMonad.kickOutRewritable

The idea is that
* (T1-2) are guaranteed by exhaustively rewriting the work-item
  with S(fw,_).

* T3 is guaranteed by a simple occurs-check on the work item.
  This is done during canonicalisation, in canEqTyVar;
  (invariant: a CTyEqCan never has an occurs check).

* (K1-3) are the "kick-out" criteria.  (As stated, they are really the
  "keep" criteria.) If the current inert S contains a triple that does
  not satisfy (K1-3), then we remove it from S by "kicking it out",
  and re-processing it.

* Note that kicking out is a Bad Thing, because it means we have to
  re-process a constraint.  The less we kick out, the better.
  TODO: Make sure that kicking out really *is* a Bad Thing. We've assumed
  this but haven't done the empirical study to check.

* Assume we have  G>=G, G>=W and that's all.  Then, when performing
  a unification we add a new given  a -G-> ty.  But doing so does NOT require
  us to kick out an inert wanted that mentions a, because of (K2a).  This
  is a common case, hence good not to kick out.

* Lemma (L2): if not (fw >= fw), then K0 holds and we kick out nothing
  Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
         and so K0 holds.  Intuitively, since fw can't rewrite anything,
         adding it cannot cause any loops
  This is a common case, because Wanteds cannot rewrite Wanteds.
  It's used to avoid even looking for constraint to kick out.

* Lemma (L1): The conditions of the Main Theorem imply that there is no
              (a -fs-> t) in S, s.t.  (fs >= fw).
  Proof. Suppose the contrary (fs >= fw).  Then because of (T1),
  S(fw,a)=a.  But since fs>=fw, S(fw,a) = s, hence s=a.  But now we
  have (a -fs-> a) in S, which contradicts (WF2).

* The extended substitution satisfies (WF1) and (WF2)
  - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
  - (T3) guarantees (WF2).

* (K2) is about inertness.  Intuitively, any infinite chain T^0(f,t),
  T^1(f,t), T^2(f,T).... must pass through the new work item infinitely
  often, since the substitution without the work item is inert; and must
  pass through at least one of the triples in S infinitely often.

  - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f),
    and hence this triple never plays a role in application S(f,a).
    It is always safe to extend S with such a triple.

    (NB: we could strengten K1) in this way too, but see K3.

  - (K2b): If this holds then, by (T2), b is not in t.  So applying the
    work item does not generate any new opportunities for applying S

  - (K2c): If this holds, we can't pass through this triple infinitely
    often, because if we did then fs>=f, fw>=f, hence by (R2)
      * either fw>=fs, contradicting K2c
      * or fs>=fw; so by the argument in K2b we can't have a loop

  - (K2d): if a not in s, we hae no further opportunity to apply the
    work item, similar to (K2b)

  NB: Dimitrios has a PDF that does this in more detail

Key lemma to make it watertight.
  Under the conditions of the Main Theorem,
  forall f st fw >= f, a is not in S^k(f,t), for any k

Also, consider roles more carefully. See Note [Flavours with roles]

Note [K3: completeness of solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(K3) is not necessary for the extended substitution
to be inert.  In fact K1 could be made stronger by saying
   ... then (not (fw >= fs) or not (fs >= fs))
But it's not enough for S to be inert; we also want completeness.
That is, we want to be able to solve all soluble wanted equalities.
Suppose we have

   work-item   b -G-> a
   inert-item  a -W-> b

Assuming (G >= W) but not (W >= W), this fulfills all the conditions,
so we could extend the inerts, thus:

   inert-items   b -G-> a
                 a -W-> b

But if we kicked-out the inert item, we'd get

   work-item     a -W-> b
   inert-item    b -G-> a

Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl.
So we add one more clause to the kick-out criteria

Another way to understand (K3) is that we treat an inert item
        a -f-> b
in the same way as
        b -f-> a
So if we kick out one, we should kick out the other.  The orientation
is somewhat accidental.

When considering roles, we also need the second clause (K3b). Consider

  work-item    c -G/N-> a
  inert-item   a -W/R-> b c

The work-item doesn't get rewritten by the inert, because (>=) doesn't hold.
But we don't kick out the inert item because not (W/R >= W/R).  So we just
add the work item. But then, consider if we hit the following:

  work-item    b -G/N-> Id
  inert-items  a -W/R-> b c
               c -G/N-> a
where
  newtype Id x = Id x

For similar reasons, if we only had (K3a), we wouldn't kick the
representational inert out. And then, we'd miss solving the inert, which
now reduced to reflexivity.

The solution here is to kick out representational inerts whenever the
tyvar of a work item is "exposed", where exposed means being at the
head of the top-level application chain (a t1 .. tn).  See
TcType.isTyVarHead. This is encoded in (K3b).

Beware: if we make this test succeed too often, we kick out too much,
and the solver might loop.  Consider (#14363)
  work item:   [G] a ~R f b
  inert item:  [G] b ~R f a
In GHC 8.2 the completeness tests more aggressive, and kicked out
the inert item; but no rewriting happened and there was an infinite
loop.  All we need is to have the tyvar at the head.

Note [Flavours with roles]
~~~~~~~~~~~~~~~~~~~~~~~~~~
The system described in Note [inert_eqs: the inert equalities]
discusses an abstract
set of flavours. In GHC, flavours have two components: the flavour proper,
taken from {Wanted, Derived, Given} and the equality relation (often called
role), taken from {NomEq, ReprEq}.
When substituting w.r.t. the inert set,
as described in Note [inert_eqs: the inert equalities],
we must be careful to respect all components of a flavour.
For example, if we have

  inert set: a -G/R-> Int
             b -G/R-> Bool

  type role T nominal representational

and we wish to compute S(W/R, T a b), the correct answer is T a Bool, NOT
T Int Bool. The reason is that T's first parameter has a nominal role, and
thus rewriting a to Int in T a b is wrong. Indeed, this non-congruence of
substitution means that the proof in Note [The inert equalities] may need
to be revisited, but we don't think that the end conclusion is wrong.
-}

instance Outputable InertCans where
  ppr :: InertCans -> SDoc
ppr (IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs
          , inert_funeqs :: InertCans -> FunEqMap Ct
inert_funeqs = FunEqMap Ct
funeqs, inert_dicts :: InertCans -> FunEqMap Ct
inert_dicts = FunEqMap Ct
dicts
          , inert_safehask :: InertCans -> FunEqMap Ct
inert_safehask = FunEqMap Ct
safehask, inert_irreds :: InertCans -> Cts
inert_irreds = Cts
irreds
          , inert_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
insts
          , inert_count :: InertCans -> Int
inert_count = Int
count })
    = SDoc -> SDoc
braces (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
      [ Bool -> SDoc -> SDoc
ppUnless (InertEqs -> Bool
forall a. DVarEnv a -> Bool
isEmptyDVarEnv InertEqs
eqs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Equalities:"
          SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
pprCts (([Ct] -> Cts -> Cts) -> Cts -> InertEqs -> Cts
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv (\[Ct]
eqs Cts
rest -> [Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
eqs Cts -> Cts -> Cts
`andCts` Cts
rest) Cts
emptyCts InertEqs
eqs)
      , Bool -> SDoc -> SDoc
ppUnless (FunEqMap Ct -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap FunEqMap Ct
funeqs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Type-function equalities =" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
pprCts (FunEqMap Ct -> Cts
forall a. DictMap a -> Bag a
funEqsToBag FunEqMap Ct
funeqs)
      , Bool -> SDoc -> SDoc
ppUnless (FunEqMap Ct -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap FunEqMap Ct
dicts) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Dictionaries =" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
pprCts (FunEqMap Ct -> Cts
forall a. DictMap a -> Bag a
dictsToBag FunEqMap Ct
dicts)
      , Bool -> SDoc -> SDoc
ppUnless (FunEqMap Ct -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap FunEqMap Ct
safehask) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Safe Haskell unsafe overlap =" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
pprCts (FunEqMap Ct -> Cts
forall a. DictMap a -> Bag a
dictsToBag FunEqMap Ct
safehask)
      , Bool -> SDoc -> SDoc
ppUnless (Cts -> Bool
isEmptyCts Cts
irreds) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Irreds =" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
pprCts Cts
irreds
      , Bool -> SDoc -> SDoc
ppUnless ([QCInst] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QCInst]
insts) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Given instances =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat ((QCInst -> SDoc) -> [QCInst] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map QCInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr [QCInst]
insts)
      , String -> SDoc
text String
"Unsolved goals =" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
count
      ]

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

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

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

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

    Flatten: [G] Foo e ~ fsk
             [G] fsk ~ Maybe e   -- (A)

             [W] Foo ee ~ fmv
             [W] fmv ~ fsk       -- (B) From Foo e ~ Foo ee
             [W] fmv ~ Maybe ee

    --> rewrite (B) with (A)
             [W] Foo ee ~ fmv
             [W] fmv ~ Maybe e
             [W] fmv ~ Maybe ee

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

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

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

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

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

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

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

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

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

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

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

Additional notes:

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

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

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

  * This splitting business applies to CFunEqCans too; and then
    we do apply type-function reductions to the [D] CFunEqCan.
    See Note [Reduction for Derived CFunEqCans]

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

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

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

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

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

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

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

* Others: nothing is gained by splitting.

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

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

  work item: [WD] a ~ beta

This is heterogeneous, so we try flattening the kinds.

  co :: F v ~ fmv
  [WD] (a |> co) ~ beta

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

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

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

  work item: [WD] (a |> co) ~ beta
  inert: [D] fmv ~ alpha (CTyEqCan)

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

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

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

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

We decompose the cast, yielding

  [D] a ~ beta

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

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

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

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

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

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

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

Note [Examples of how Derived shadows helps completeness]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
#10009, a very nasty example:

    f :: (UnF (F b) ~ b) => F b -> ()

    g :: forall a. (UnF (F a) ~ a) => a -> ()
    g _ = f (undefined :: F a)

  For g we get [G] UnF (F a) ~ a
               [WD] UnF (F beta) ~ beta
               [WD] F a ~ F beta
  Flatten:
      [G] g1: F a ~ fsk1         fsk1 := F a
      [G] g2: UnF fsk1 ~ fsk2    fsk2 := UnF fsk1
      [G] g3: fsk2 ~ a

      [WD] w1: F beta ~ fmv1
      [WD] w2: UnF fmv1 ~ fmv2
      [WD] w3: fmv2 ~ beta
      [WD] w4: fmv1 ~ fsk1   -- From F a ~ F beta using flat-cache
                             -- and re-orient to put meta-var on left

Rewrite w2 with w4: [D] d1: UnF fsk1 ~ fmv2
React that with g2: [D] d2: fmv2 ~ fsk2
React that with w3: [D] beta ~ fsk2
            and g3: [D] beta ~ a -- Hooray beta := a
And that is enough to solve everything

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

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

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

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

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

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

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

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

See #11379 for a case of this.

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

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

Reasons:

* It's less work: fewer pairs to compare

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

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

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

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

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

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

shouldSplitWD :: InertEqs -> Ct -> Bool
shouldSplitWD InertEqs
inert_eqs (CFunEqCan { cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType]
tys })
  = InertEqs -> [PredType] -> Bool
should_split_match_args InertEqs
inert_eqs [PredType]
tys
    -- We don't need to split if the tv is the RHS fsk

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

shouldSplitWD InertEqs
inert_eqs (CTyEqCan { cc_tyvar :: Ct -> TcTyVar
cc_tyvar = TcTyVar
tv, cc_rhs :: Ct -> PredType
cc_rhs = PredType
ty
                                  , cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
  =  TcTyVar
tv TcTyVar -> InertEqs -> Bool
forall a. TcTyVar -> DVarEnv a -> Bool
`elemDVarEnv` InertEqs
inert_eqs
  Bool -> Bool -> Bool
|| Bool -> EqRel -> (EqRel -> TcTyVar -> Bool) -> PredType -> Bool
anyRewritableTyVar Bool
False EqRel
eq_rel (InertEqs -> EqRel -> TcTyVar -> Bool
canRewriteTv InertEqs
inert_eqs) PredType
ty
  -- NB False: do not ignore casts and coercions
  -- See Note [Splitting WD constraints]

shouldSplitWD InertEqs
inert_eqs (CIrredCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev })
  = Bool -> EqRel -> (EqRel -> TcTyVar -> Bool) -> PredType -> Bool
anyRewritableTyVar Bool
False (CtEvidence -> EqRel
ctEvEqRel CtEvidence
ev) (InertEqs -> EqRel -> TcTyVar -> Bool
canRewriteTv InertEqs
inert_eqs) (CtEvidence -> PredType
ctEvPred CtEvidence
ev)

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

should_split_match_args :: InertEqs -> [TcType] -> Bool
-- True if the inert_eqs can rewrite anything in the argument
-- types, ignoring casts and coercions
should_split_match_args :: InertEqs -> [PredType] -> Bool
should_split_match_args InertEqs
inert_eqs [PredType]
tys
  = (PredType -> Bool) -> [PredType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> EqRel -> (EqRel -> TcTyVar -> Bool) -> PredType -> Bool
anyRewritableTyVar Bool
True EqRel
NomEq (InertEqs -> EqRel -> TcTyVar -> Bool
canRewriteTv InertEqs
inert_eqs)) [PredType]
tys
    -- NB True: ignore casts coercions
    -- See Note [Splitting WD constraints]

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

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


{- *********************************************************************
*                                                                      *
                   Inert equalities
*                                                                      *
********************************************************************* -}

addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
addTyEq InertEqs
old_eqs TcTyVar
tv Ct
ct
  = ([Ct] -> [Ct] -> [Ct]) -> InertEqs -> TcTyVar -> [Ct] -> InertEqs
forall a. (a -> a -> a) -> DVarEnv a -> TcTyVar -> a -> DVarEnv a
extendDVarEnv_C [Ct] -> [Ct] -> [Ct]
add_eq InertEqs
old_eqs TcTyVar
tv [Ct
ct]
  where
    add_eq :: [Ct] -> [Ct] -> [Ct]
add_eq [Ct]
old_eqs [Ct]
_
      | Ct -> Bool
isWantedCt Ct
ct
      , (Ct
eq1 : [Ct]
eqs) <- [Ct]
old_eqs
      = Ct
eq1 Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: Ct
ct Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: [Ct]
eqs
      | Bool
otherwise
      = Ct
ct Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: [Ct]
old_eqs

foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b
foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b
foldTyEqs Ct -> b -> b
k InertEqs
eqs b
z
  = ([Ct] -> b -> b) -> b -> InertEqs -> b
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv (\[Ct]
cts b
z -> (Ct -> b -> b) -> b -> [Ct] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> b -> b
k b
z [Ct]
cts) b
z InertEqs
eqs

findTyEqs :: InertCans -> TyVar -> EqualCtList
findTyEqs :: InertCans -> TcTyVar -> [Ct]
findTyEqs InertCans
icans TcTyVar
tv = InertEqs -> TcTyVar -> Maybe [Ct]
forall a. DVarEnv a -> TcTyVar -> Maybe a
lookupDVarEnv (InertCans -> InertEqs
inert_eqs InertCans
icans) TcTyVar
tv Maybe [Ct] -> [Ct] -> [Ct]
forall a. Maybe a -> a -> a
`orElse` []

delTyEq :: InertEqs -> TcTyVar -> TcType -> InertEqs
delTyEq :: InertEqs -> TcTyVar -> PredType -> InertEqs
delTyEq InertEqs
m TcTyVar
tv PredType
t = ([Ct] -> [Ct]) -> InertEqs -> TcTyVar -> InertEqs
forall a. (a -> a) -> DVarEnv a -> TcTyVar -> DVarEnv a
modifyDVarEnv ((Ct -> Bool) -> [Ct] -> [Ct]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Ct -> Bool) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> Bool
isThisOne)) InertEqs
m TcTyVar
tv
  where isThisOne :: Ct -> Bool
isThisOne (CTyEqCan { cc_rhs :: Ct -> PredType
cc_rhs = PredType
t1 }) = PredType -> PredType -> Bool
eqType PredType
t PredType
t1
        isThisOne Ct
_                          = Bool
False

lookupInertTyVar :: InertEqs -> TcTyVar -> Maybe TcType
lookupInertTyVar :: InertEqs -> TcTyVar -> Maybe PredType
lookupInertTyVar InertEqs
ieqs TcTyVar
tv
  = case InertEqs -> TcTyVar -> Maybe [Ct]
forall a. DVarEnv a -> TcTyVar -> Maybe a
lookupDVarEnv InertEqs
ieqs TcTyVar
tv of
      Just (CTyEqCan { cc_rhs :: Ct -> PredType
cc_rhs = PredType
rhs, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
NomEq } : [Ct]
_ ) -> PredType -> Maybe PredType
forall a. a -> Maybe a
Just PredType
rhs
      Maybe [Ct]
_                                                        -> Maybe PredType
forall a. Maybe a
Nothing

{- *********************************************************************
*                                                                      *
                   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
  = (InertCans -> InertCans) -> TcS ()
updInertCans ((InertCans -> InertCans) -> TcS ())
-> (InertCans -> InertCans) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \InertCans
ics ->
    InertCans
ics { inert_insts :: [QCInst]
inert_insts = [QCInst] -> [QCInst]
add_qci (InertCans -> [QCInst]
inert_insts InertCans
ics) }
  where
    add_qci :: [QCInst] -> [QCInst]
    -- See Note [Do not add duplicate quantified instances]
    add_qci :: [QCInst] -> [QCInst]
add_qci [QCInst]
qcis | (QCInst -> Bool) -> [QCInst] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any QCInst -> Bool
same_qci [QCInst]
qcis = [QCInst]
qcis
                 | Bool
otherwise         = QCInst
new_qci QCInst -> [QCInst] -> [QCInst]
forall a. a -> [a] -> [a]
: [QCInst]
qcis

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

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

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

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

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

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

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

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

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

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

Note [Kicking out CFunEqCan for fundeps]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider:
   New:    [D] fmv1 ~ fmv2
   Inert:  [W] F alpha ~ fmv1
           [W] F beta  ~ fmv2

where F is injective. The new (derived) equality certainly can't
rewrite the inerts. But we *must* kick out the first one, to get:

   New:   [W] F alpha ~ fmv1
   Inert: [W] F beta ~ fmv2
          [D] fmv1 ~ fmv2

and now improvement will discover [D] alpha ~ beta. This is important;
eg in #9587.

So in kickOutRewritable we look at all the tyvars of the
CFunEqCan, including the fsk.
-}

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

       ; InertCans
ics <- TcS InertCans
getInertCans
       ; Ct
ct  <- InertCans -> Ct -> TcS Ct
maybeEmitShadow InertCans
ics Ct
ct
       ; InertCans
ics <- InertCans -> Ct -> TcS InertCans
maybeKickOut InertCans
ics Ct
ct
       ; InertCans -> TcS ()
setInertCans (InertCans -> Ct -> InertCans
add_item InertCans
ics Ct
ct)

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

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

add_item :: InertCans -> Ct -> InertCans
add_item :: InertCans -> Ct -> InertCans
add_item InertCans
ics item :: Ct
item@(CFunEqCan { cc_fun :: Ct -> TyCon
cc_fun = TyCon
tc, cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType]
tys })
  = InertCans
ics { inert_funeqs :: FunEqMap Ct
inert_funeqs = FunEqMap Ct -> TyCon -> [PredType] -> Ct -> FunEqMap Ct
forall a. FunEqMap a -> TyCon -> [PredType] -> a -> FunEqMap a
insertFunEq (InertCans -> FunEqMap Ct
inert_funeqs InertCans
ics) TyCon
tc [PredType]
tys Ct
item }

add_item InertCans
ics item :: Ct
item@(CTyEqCan { cc_tyvar :: Ct -> TcTyVar
cc_tyvar = TcTyVar
tv, cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev })
  = InertCans
ics { inert_eqs :: InertEqs
inert_eqs   = InertEqs -> TcTyVar -> Ct -> InertEqs
addTyEq (InertCans -> InertEqs
inert_eqs InertCans
ics) TcTyVar
tv Ct
item
        , inert_count :: Int
inert_count = CtEvidence -> Int -> Int
bumpUnsolvedCount CtEvidence
ev (InertCans -> Int
inert_count InertCans
ics) }

add_item ics :: InertCans
ics@(IC { inert_irreds :: InertCans -> Cts
inert_irreds = Cts
irreds, inert_count :: InertCans -> Int
inert_count = Int
count })
         item :: Ct
item@(CIrredCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_insol :: Ct -> Bool
cc_insol = Bool
insoluble })
  = InertCans
ics { inert_irreds :: Cts
inert_irreds = Cts
irreds Cts -> Ct -> Cts
forall a. Bag a -> a -> Bag a
`Bag.snocBag` Ct
item
        , inert_count :: Int
inert_count  = if Bool
insoluble
                         then Int
count  -- inert_count does not include insolubles
                         else CtEvidence -> Int -> Int
bumpUnsolvedCount CtEvidence
ev Int
count }

add_item InertCans
ics item :: Ct
item@(CDictCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType]
tys })
  = InertCans
ics { inert_dicts :: FunEqMap Ct
inert_dicts = FunEqMap Ct -> Class -> [PredType] -> Ct -> FunEqMap Ct
forall a. DictMap a -> Class -> [PredType] -> a -> DictMap a
addDict (InertCans -> FunEqMap Ct
inert_dicts InertCans
ics) Class
cls [PredType]
tys Ct
item
        , inert_count :: Int
inert_count = CtEvidence -> Int -> Int
bumpUnsolvedCount CtEvidence
ev (InertCans -> Int
inert_count InertCans
ics) }

add_item InertCans
_ Ct
item
  = String -> SDoc -> InertCans
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"upd_inert set: can't happen! Inserting " (SDoc -> InertCans) -> SDoc -> InertCans
forall a b. (a -> b) -> a -> b
$
    Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
item   -- Can't be CNonCanonical, CHoleCan,
               -- because they only land in inert_irreds

bumpUnsolvedCount :: CtEvidence -> Int -> Int
bumpUnsolvedCount :: CtEvidence -> Int -> Int
bumpUnsolvedCount CtEvidence
ev Int
n | CtEvidence -> Bool
isWanted CtEvidence
ev = Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1
                       | Bool
otherwise   = Int
n


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

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

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

kick_out_rewritable :: CtFlavourRole  -- Flavour/role of the equality that
                                      -- is being added to the inert set
                    -> TcTyVar        -- The new equality is tv ~ ty
                    -> InertCans
                    -> (WorkList, InertCans)
-- See Note [kickOutRewritable]
kick_out_rewritable :: CtFlavourRole -> TcTyVar -> InertCans -> (WorkList, InertCans)
kick_out_rewritable CtFlavourRole
new_fr TcTyVar
new_tv
                    ics :: InertCans
ics@(IC { inert_eqs :: InertCans -> InertEqs
inert_eqs      = InertEqs
tv_eqs
                            , inert_dicts :: InertCans -> FunEqMap Ct
inert_dicts    = FunEqMap Ct
dictmap
                            , inert_safehask :: InertCans -> FunEqMap Ct
inert_safehask = FunEqMap Ct
safehask
                            , inert_funeqs :: InertCans -> FunEqMap Ct
inert_funeqs   = FunEqMap Ct
funeqmap
                            , inert_irreds :: InertCans -> Cts
inert_irreds   = Cts
irreds
                            , inert_insts :: InertCans -> [QCInst]
inert_insts    = [QCInst]
old_insts
                            , inert_count :: InertCans -> Int
inert_count    = Int
n })
  | Bool -> Bool
not (CtFlavourRole
new_fr CtFlavourRole -> CtFlavourRole -> Bool
`eqMayRewriteFR` CtFlavourRole
new_fr)
  = (WorkList
emptyWorkList, InertCans
ics)
        -- If new_fr can't rewrite itself, it can't rewrite
        -- anything else, so no need to kick out anything.
        -- (This is a common case: wanteds can't rewrite wanteds)
        -- Lemma (L2) in Note [Extending the inert equalities]

  | Bool
otherwise
  = (WorkList
kicked_out, InertCans
inert_cans_in)
  where
    inert_cans_in :: InertCans
inert_cans_in = IC :: InertEqs
-> FunEqMap Ct
-> FunEqMap Ct
-> [QCInst]
-> FunEqMap Ct
-> Cts
-> Int
-> InertCans
IC { inert_eqs :: InertEqs
inert_eqs      = InertEqs
tv_eqs_in
                       , inert_dicts :: FunEqMap Ct
inert_dicts    = FunEqMap Ct
dicts_in
                       , inert_safehask :: FunEqMap Ct
inert_safehask = FunEqMap Ct
safehask   -- ??
                       , inert_funeqs :: FunEqMap Ct
inert_funeqs   = FunEqMap Ct
feqs_in
                       , inert_irreds :: Cts
inert_irreds   = Cts
irs_in
                       , inert_insts :: [QCInst]
inert_insts    = [QCInst]
insts_in
                       , inert_count :: Int
inert_count    = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- WorkList -> Int
workListWantedCount WorkList
kicked_out }

    kicked_out :: WorkList
    -- NB: use extendWorkList to ensure that kicked-out equalities get priority
    -- See Note [Prioritise equalities] (Kick-out).
    -- The irreds may include non-canonical (hetero-kinded) equality
    -- constraints, which perhaps may have become soluble after new_tv
    -- is substituted; ditto the dictionaries, which may include (a~b)
    -- or (a~~b) constraints.
    kicked_out :: WorkList
kicked_out = (Ct -> WorkList -> WorkList) -> WorkList -> Cts -> WorkList
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> WorkList -> WorkList
extendWorkListCt
                          (WorkList
emptyWorkList { wl_eqs :: [Ct]
wl_eqs    = [Ct]
tv_eqs_out
                                         , wl_funeqs :: [Ct]
wl_funeqs = [Ct]
feqs_out })
                          ((Cts
dicts_out Cts -> Cts -> Cts
`andCts` Cts
irs_out)
                            Cts -> [Ct] -> Cts
`extendCtsList` [Ct]
insts_out)

    ([Ct]
tv_eqs_out, InertEqs
tv_eqs_in) = ([Ct] -> ([Ct], InertEqs) -> ([Ct], InertEqs))
-> ([Ct], InertEqs) -> InertEqs -> ([Ct], InertEqs)
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv [Ct] -> ([Ct], InertEqs) -> ([Ct], InertEqs)
kick_out_eqs ([], InertEqs
forall a. DVarEnv a
emptyDVarEnv) InertEqs
tv_eqs
    ([Ct]
feqs_out,   FunEqMap Ct
feqs_in)   = (Ct -> Bool) -> FunEqMap Ct -> ([Ct], FunEqMap Ct)
partitionFunEqs  Ct -> Bool
kick_out_ct FunEqMap Ct
funeqmap
           -- See Note [Kicking out CFunEqCan for fundeps]
    (Cts
dicts_out,  FunEqMap Ct
dicts_in)  = (Ct -> Bool) -> FunEqMap Ct -> (Cts, FunEqMap Ct)
partitionDicts   Ct -> Bool
kick_out_ct FunEqMap Ct
dictmap
    (Cts
irs_out,    Cts
irs_in)    = (Ct -> Bool) -> Cts -> (Cts, Cts)
forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag     Ct -> Bool
kick_out_ct Cts
irreds
      -- Kick out even insolubles: See Note [Rewrite insolubles]
      -- Of course we must kick out irreducibles like (c a), in case
      -- we can rewrite 'c' to something more useful

    -- Kick-out for inert instances
    -- See Note [Quantified constraints] in TcCanonical
    insts_out :: [Ct]
    insts_in  :: [QCInst]
    ([Ct]
insts_out, [QCInst]
insts_in)
       | CtFlavourRole -> Bool
fr_may_rewrite (CtFlavour
Given, EqRel
NomEq)  -- All the insts are Givens
       = (QCInst -> Either Ct QCInst) -> [QCInst] -> ([Ct], [QCInst])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith QCInst -> Either Ct QCInst
kick_out_qci [QCInst]
old_insts
       | Bool
otherwise
       = ([], [QCInst]
old_insts)
    kick_out_qci :: QCInst -> Either Ct QCInst
kick_out_qci QCInst
qci
      | let ev :: CtEvidence
ev = QCInst -> CtEvidence
qci_ev QCInst
qci
      , EqRel -> PredType -> Bool
fr_can_rewrite_ty EqRel
NomEq (CtEvidence -> PredType
ctEvPred (QCInst -> CtEvidence
qci_ev QCInst
qci))
      = Ct -> Either Ct QCInst
forall a b. a -> Either a b
Left (CtEvidence -> Ct
mkNonCanonical CtEvidence
ev)
      | Bool
otherwise
      = QCInst -> Either Ct QCInst
forall a b. b -> Either a b
Right QCInst
qci

    (CtFlavour
_, EqRel
new_role) = CtFlavourRole
new_fr

    fr_can_rewrite_ty :: EqRel -> Type -> Bool
    fr_can_rewrite_ty :: EqRel -> PredType -> Bool
fr_can_rewrite_ty EqRel
role PredType
ty = Bool -> EqRel -> (EqRel -> TcTyVar -> Bool) -> PredType -> Bool
anyRewritableTyVar Bool
False EqRel
role
                                                   EqRel -> TcTyVar -> Bool
fr_can_rewrite_tv PredType
ty
    fr_can_rewrite_tv :: EqRel -> TyVar -> Bool
    fr_can_rewrite_tv :: EqRel -> TcTyVar -> Bool
fr_can_rewrite_tv EqRel
role TcTyVar
tv = EqRel
new_role EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
role
                             Bool -> Bool -> Bool
&& TcTyVar
tv TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
new_tv

    fr_may_rewrite :: CtFlavourRole -> Bool
    fr_may_rewrite :: CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs = CtFlavourRole
new_fr CtFlavourRole -> CtFlavourRole -> Bool
`eqMayRewriteFR` CtFlavourRole
fs
        -- Can the new item rewrite the inert item?

    kick_out_ct :: Ct -> Bool
    -- Kick it out if the new CTyEqCan can rewrite the inert one
    -- See Note [kickOutRewritable]
    kick_out_ct :: Ct -> Bool
kick_out_ct Ct
ct | let fs :: CtFlavourRole
fs@(CtFlavour
_,EqRel
role) = Ct -> CtFlavourRole
ctFlavourRole Ct
ct
                   = CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs
                   Bool -> Bool -> Bool
&& EqRel -> PredType -> Bool
fr_can_rewrite_ty EqRel
role (Ct -> PredType
ctPred Ct
ct)
                  -- False: ignore casts and coercions
                  -- NB: this includes the fsk of a CFunEqCan.  It can't
                  --     actually be rewritten, but we need to kick it out
                  --     so we get to take advantage of injectivity
                  -- See Note [Kicking out CFunEqCan for fundeps]

    kick_out_eqs :: EqualCtList -> ([Ct], DTyVarEnv EqualCtList)
                 -> ([Ct], DTyVarEnv EqualCtList)
    kick_out_eqs :: [Ct] -> ([Ct], InertEqs) -> ([Ct], InertEqs)
kick_out_eqs [Ct]
eqs ([Ct]
acc_out, InertEqs
acc_in)
      = ([Ct]
eqs_out [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
acc_out, case [Ct]
eqs_in of
                               []      -> InertEqs
acc_in
                               (Ct
eq1:[Ct]
_) -> InertEqs -> TcTyVar -> [Ct] -> InertEqs
forall a. DVarEnv a -> TcTyVar -> a -> DVarEnv a
extendDVarEnv InertEqs
acc_in (Ct -> TcTyVar
cc_tyvar Ct
eq1) [Ct]
eqs_in)
      where
        ([Ct]
eqs_out, [Ct]
eqs_in) = (Ct -> Bool) -> [Ct] -> ([Ct], [Ct])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Ct -> Bool
kick_out_eq [Ct]
eqs

    -- Implements criteria K1-K3 in Note [Extending the inert equalities]
    kick_out_eq :: Ct -> Bool
kick_out_eq (CTyEqCan { cc_tyvar :: Ct -> TcTyVar
cc_tyvar = TcTyVar
tv, cc_rhs :: Ct -> PredType
cc_rhs = PredType
rhs_ty
                          , cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
      | Bool -> Bool
not (CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs)
      = Bool
False  -- Keep it in the inert set if the new thing can't rewrite it

      -- Below here (fr_may_rewrite fs) is True
      | TcTyVar
tv TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
new_tv              = Bool
True        -- (K1)
      | Bool
kick_out_for_inertness    = Bool
True
      | Bool
kick_out_for_completeness = Bool
True
      | Bool
otherwise                 = Bool
False

      where
        fs :: CtFlavourRole
fs = (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
eq_rel)
        kick_out_for_inertness :: Bool
kick_out_for_inertness
          =        (CtFlavourRole
fs CtFlavourRole -> CtFlavourRole -> Bool
`eqMayRewriteFR` CtFlavourRole
fs)       -- (K2a)
            Bool -> Bool -> Bool
&& Bool -> Bool
not (CtFlavourRole
fs CtFlavourRole -> CtFlavourRole -> Bool
`eqMayRewriteFR` CtFlavourRole
new_fr)   -- (K2b)
            Bool -> Bool -> Bool
&& EqRel -> PredType -> Bool
fr_can_rewrite_ty EqRel
eq_rel PredType
rhs_ty    -- (K2d)
            -- (K2c) is guaranteed by the first guard of keep_eq

        kick_out_for_completeness :: Bool
kick_out_for_completeness
          = case EqRel
eq_rel of
              EqRel
NomEq  -> PredType
rhs_ty PredType -> PredType -> Bool
`eqType` TcTyVar -> PredType
mkTyVarTy TcTyVar
new_tv
              EqRel
ReprEq -> TcTyVar -> PredType -> Bool
isTyVarHead TcTyVar
new_tv PredType
rhs_ty

    kick_out_eq Ct
ct = String -> SDoc -> Bool
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"keep_eq" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)

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

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

{- Note [kickOutRewritable]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
See also Note [inert_eqs: the inert equalities].

When we add a new inert equality (a ~N ty) to the inert set,
we must kick out any inert items that could be rewritten by the
new equality, to maintain the inert-set invariants.

  - We want to kick out an existing inert constraint if
    a) the new constraint can rewrite the inert one
    b) 'a' is free in the inert constraint (so that it *will*)
       rewrite it if we kick it out.

    For (b) we use tyCoVarsOfCt, which returns the type variables /and
    the kind variables/ that are directly visible in the type. Hence
    we will have exposed all the rewriting we care about to make the
    most precise kinds visible for matching classes etc. No need to
    kick out constraints that mention type variables whose kinds
    contain this variable!

  - A Derived equality can kick out [D] constraints in inert_eqs,
    inert_dicts, inert_irreds etc.

  - We don't kick out constraints from inert_solved_dicts, and
    inert_solved_funeqs optimistically. But when we lookup we have to
    take the substitution into account


Note [Rewrite insolubles]
~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have an insoluble alpha ~ [alpha], which is insoluble
because an occurs check.  And then we unify alpha := [Int].  Then we
really want to rewrite the insoluble to [Int] ~ [[Int]].  Now it can
be decomposed.  Otherwise we end up with a "Can't match [Int] ~
[[Int]]" which is true, but a bit confusing because the outer type
constructors match.

Similarly, if we have a CHoleCan, we'd like to rewrite it with any
Givens, to give as informative an error messasge as possible
(#12468, #11325).

Hence:
 * In the main simlifier loops in TcSimplify (solveWanteds,
   simpl_loop), we feed the insolubles in solveSimpleWanteds,
   so that they get rewritten (albeit not solved).

 * We kick insolubles out of the inert set, if they can be
   rewritten (see TcSMonad.kick_out_rewritable)

 * We rewrite those insolubles in TcCanonical.
   See Note [Make sure that insolubles are fully rewritten]
-}



--------------
addInertSafehask :: InertCans -> Ct -> InertCans
addInertSafehask :: InertCans -> Ct -> InertCans
addInertSafehask InertCans
ics item :: Ct
item@(CDictCan { cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType]
tys })
  = InertCans
ics { inert_safehask :: FunEqMap Ct
inert_safehask = FunEqMap Ct -> Class -> [PredType] -> Ct -> FunEqMap Ct
forall a. DictMap a -> Class -> [PredType] -> a -> DictMap a
addDict (InertCans -> FunEqMap Ct
inert_dicts InertCans
ics) Class
cls [PredType]
tys Ct
item }

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

getInertGivens :: TcS [Ct]
-- Returns the Given constraints in the inert set,
-- with type functions *not* unflattened
getInertGivens :: TcS [Ct]
getInertGivens
  = do { InertCans
inerts <- TcS InertCans
getInertCans
       ; let all_cts :: [Ct]
all_cts = (Ct -> [Ct] -> [Ct]) -> FunEqMap Ct -> [Ct] -> [Ct]
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldDicts (:) (InertCans -> FunEqMap Ct
inert_dicts InertCans
inerts)
                     ([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ (Ct -> [Ct] -> [Ct]) -> FunEqMap Ct -> [Ct] -> [Ct]
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldFunEqs (:) (InertCans -> FunEqMap Ct
inert_funeqs InertCans
inerts)
                     ([Ct] -> [Ct]) -> [Ct] -> [Ct]
forall a b. (a -> b) -> a -> b
$ [[Ct]] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (InertEqs -> [[Ct]]
forall a. DVarEnv a -> [a]
dVarEnvElts (InertCans -> InertEqs
inert_eqs InertCans
inerts))
       ; [Ct] -> TcS [Ct]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Ct -> Bool) -> [Ct] -> [Ct]
forall a. (a -> Bool) -> [a] -> [a]
filter Ct -> Bool
isGivenCt [Ct]
all_cts) }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    -- For CFunEqCans we ignore the Derived ones, and keep
    -- only the Wanteds for flattening.  The Derived ones
    -- share a unification variable with the corresponding
    -- Wanted, so we definitely don't want to participate
    -- in unflattening
    -- See Note [Type family equations]
    add_if_wanted :: Ct -> Cts -> Cts
add_if_wanted Ct
ct Cts
cts | Ct -> Bool
isWantedCt Ct
ct = Ct
ct Ct -> Cts -> Cts
`consCts` Cts
cts
                         | Bool
otherwise     = Cts
cts

isInInertEqs :: DTyVarEnv EqualCtList -> TcTyVar -> TcType -> Bool
-- True if (a ~N ty) is in the inert set, in either Given or Wanted
isInInertEqs :: InertEqs -> TcTyVar -> PredType -> Bool
isInInertEqs InertEqs
eqs TcTyVar
tv PredType
rhs
  = case InertEqs -> TcTyVar -> Maybe [Ct]
forall a. DVarEnv a -> TcTyVar -> Maybe a
lookupDVarEnv InertEqs
eqs TcTyVar
tv of
      Maybe [Ct]
Nothing  -> Bool
False
      Just [Ct]
cts -> (Ct -> Bool) -> [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PredType -> Ct -> Bool
same_pred PredType
rhs) [Ct]
cts
  where
    same_pred :: PredType -> Ct -> Bool
same_pred PredType
rhs Ct
ct
      | CTyEqCan { cc_rhs :: Ct -> PredType
cc_rhs = PredType
rhs2, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel } <- Ct
ct
      , EqRel
NomEq <- EqRel
eq_rel
      , PredType
rhs PredType -> PredType -> Bool
`eqType` PredType
rhs2 = Bool
True
      | Bool
otherwise         = Bool
False

getNoGivenEqs :: TcLevel          -- TcLevel of this implication
               -> [TcTyVar]       -- Skolems of this implication
               -> TcS ( Bool      -- True <=> definitely no residual given equalities
                      , Cts )     -- Insoluble equalities arising from givens
-- See Note [When does an implication have given equalities?]
getNoGivenEqs :: TcLevel -> [TcTyVar] -> TcS (Bool, Cts)
getNoGivenEqs TcLevel
tclvl [TcTyVar]
skol_tvs
  = do { inerts :: InertCans
inerts@(IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
ieqs, inert_irreds :: InertCans -> Cts
inert_irreds = Cts
irreds })
              <- TcS InertCans
getInertCans
       ; let has_given_eqs :: Bool
has_given_eqs = (Ct -> Bool -> Bool) -> Bool -> Cts -> Bool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Bool -> Bool -> Bool
(||) (Bool -> Bool -> Bool) -> (Ct -> Bool) -> Ct -> Bool -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> Bool
ct_given_here) Bool
False Cts
irreds
                          Bool -> Bool -> Bool
|| ([Ct] -> Bool) -> InertEqs -> Bool
forall a. (a -> Bool) -> DVarEnv a -> Bool
anyDVarEnv [Ct] -> Bool
eqs_given_here InertEqs
ieqs
             insols :: Cts
insols = (Ct -> Bool) -> Cts -> Cts
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Ct -> Bool
insolubleEqCt Cts
irreds
                      -- Specifically includes ones that originated in some
                      -- outer context but were refined to an insoluble by
                      -- a local equality; so do /not/ add ct_given_here.

       ; String -> SDoc -> TcS ()
traceTcS String
"getNoGivenEqs" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
vcat [ if Bool
has_given_eqs then String -> SDoc
text String
"May have given equalities"
                                 else String -> SDoc
text String
"No given equalities"
              , String -> SDoc
text String
"Skols:" SDoc -> SDoc -> SDoc
<+> [TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
skol_tvs
              , String -> SDoc
text String
"Inerts:" SDoc -> SDoc -> SDoc
<+> InertCans -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertCans
inerts
              , String -> SDoc
text String
"Insols:" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
insols]
       ; (Bool, Cts) -> TcS (Bool, Cts)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Bool
not Bool
has_given_eqs, Cts
insols) }
  where
    eqs_given_here :: EqualCtList -> Bool
    eqs_given_here :: [Ct] -> Bool
eqs_given_here [ct :: Ct
ct@(CTyEqCan { cc_tyvar :: Ct -> TcTyVar
cc_tyvar = TcTyVar
tv })]
                              -- Givens are always a sigleton
      = Bool -> Bool
not (TcTyVar -> Bool
skolem_bound_here TcTyVar
tv) Bool -> Bool -> Bool
&& Ct -> Bool
ct_given_here Ct
ct
    eqs_given_here [Ct]
_ = Bool
False

    ct_given_here :: Ct -> Bool
    -- True for a Given bound by the current implication,
    -- i.e. the current level
    ct_given_here :: Ct -> Bool
ct_given_here Ct
ct =  CtEvidence -> Bool
isGiven CtEvidence
ev
                     Bool -> Bool -> Bool
&& TcLevel
tclvl TcLevel -> TcLevel -> Bool
forall a. Eq a => a -> a -> Bool
== CtLoc -> TcLevel
ctLocLevel (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev)
        where
          ev :: CtEvidence
ev = Ct -> CtEvidence
ctEvidence Ct
ct

    skol_tv_set :: VarSet
skol_tv_set = [TcTyVar] -> VarSet
mkVarSet [TcTyVar]
skol_tvs
    skolem_bound_here :: TcTyVar -> Bool
skolem_bound_here TcTyVar
tv -- See Note [Let-bound skolems]
      = case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
tv of
          SkolemTv {} -> TcTyVar
tv TcTyVar -> VarSet -> Bool
`elemVarSet` VarSet
skol_tv_set
          TcTyVarDetails
_           -> Bool
False

-- | Returns Given constraints that might,
-- potentially, match the given pred. This is used when checking to see if a
-- Given might overlap with an instance. See Note [Instance and Given overlap]
-- in TcInteract.
matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
matchableGivens CtLoc
loc_w PredType
pred_w (IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
inert_cans })
  = (Ct -> Bool) -> Cts -> Cts
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Ct -> Bool
matchable_given Cts
all_relevant_givens
  where
    -- just look in class constraints and irreds. matchableGivens does get called
    -- for ~R constraints, but we don't need to look through equalities, because
    -- canonical equalities are used for rewriting. We'll only get caught by
    -- non-canonical -- that is, irreducible -- equalities.
    all_relevant_givens :: Cts
    all_relevant_givens :: Cts
all_relevant_givens
      | Just (Class
clas, [PredType]
_) <- PredType -> Maybe (Class, [PredType])
getClassPredTys_maybe PredType
pred_w
      = FunEqMap Ct -> Class -> Cts
forall a. DictMap a -> Class -> Bag a
findDictsByClass (InertCans -> FunEqMap Ct
inert_dicts InertCans
inert_cans) Class
clas
        Cts -> Cts -> Cts
forall a. Bag a -> Bag a -> Bag a
`unionBags` InertCans -> Cts
inert_irreds InertCans
inert_cans
      | Bool
otherwise
      = InertCans -> Cts
inert_irreds InertCans
inert_cans

    matchable_given :: Ct -> Bool
    matchable_given :: Ct -> Bool
matchable_given Ct
ct
      | CtGiven { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc_g, ctev_pred :: CtEvidence -> PredType
ctev_pred = PredType
pred_g } <- Ct -> CtEvidence
ctEvidence Ct
ct
      = PredType -> CtLoc -> PredType -> CtLoc -> Bool
mightMatchLater PredType
pred_g CtLoc
loc_g PredType
pred_w CtLoc
loc_w

      | Bool
otherwise
      = Bool
False

mightMatchLater :: TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
mightMatchLater :: PredType -> CtLoc -> PredType -> CtLoc -> Bool
mightMatchLater PredType
given_pred CtLoc
given_loc PredType
wanted_pred CtLoc
wanted_loc
  =  Bool -> Bool
not (CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
given_loc CtLoc
wanted_loc)
  Bool -> Bool -> Bool
&& Maybe TCvSubst -> Bool
forall a. Maybe a -> Bool
isJust ((TcTyVar -> BindFlag) -> [PredType] -> [PredType] -> Maybe TCvSubst
tcUnifyTys TcTyVar -> BindFlag
bind_meta_tv [PredType
given_pred] [PredType
wanted_pred])
  where
    bind_meta_tv :: TcTyVar -> BindFlag
    -- Any meta tyvar may be unified later, so we treat it as
    -- bindable when unifying with givens. That ensures that we
    -- conservatively assume that a meta tyvar might get unified with
    -- something that matches the 'given', until demonstrated
    -- otherwise.  More info in Note [Instance and Given overlap]
    -- in TcInteract
    bind_meta_tv :: TcTyVar -> BindFlag
bind_meta_tv TcTyVar
tv | TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
                    , Bool -> Bool
not (TcTyVar -> Bool
isFskTyVar TcTyVar
tv) = BindFlag
BindMe
                    | Bool
otherwise           = BindFlag
Skolem

prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
-- See Note [Solving superclass constraints] in TcInstDcls
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
from_loc CtLoc
solve_loc
  | GivenOrigin (InstSC TypeSize
given_size) <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
from_loc
  , ScOrigin TypeSize
wanted_size <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
solve_loc
  = TypeSize
given_size TypeSize -> TypeSize -> Bool
forall a. Ord a => a -> a -> Bool
>= TypeSize
wanted_size
  | Bool
otherwise
  = Bool
False

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

Note [When does an implication have given equalities?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider an implication
   beta => alpha ~ Int
where beta is a unification variable that has already been unified
to () in an outer scope.  Then we can float the (alpha ~ Int) out
just fine. So when deciding whether the givens contain an equality,
we should canonicalise first, rather than just looking at the original
givens (#8644).

So we simply look at the inert, canonical Givens and see if there are
any equalities among them, the calculation of has_given_eqs.  There
are some wrinkles:

 * We must know which ones are bound in *this* implication and which
   are bound further out.  We can find that out from the TcLevel
   of the Given, which is itself recorded in the tcl_tclvl field
   of the TcLclEnv stored in the Given (ev_given_here).

   What about interactions between inner and outer givens?
      - Outer given is rewritten by an inner given, then there must
        have been an inner given equality, hence the “given-eq” flag
        will be true anyway.

      - Inner given rewritten by outer, retains its level (ie. The inner one)

 * We must take account of *potential* equalities, like the one above:
      beta => ...blah...
   If we still don't know what beta is, we conservatively treat it as potentially
   becoming an equality. Hence including 'irreds' in the calculation or has_given_eqs.

 * When flattening givens, we generate Given equalities like
     <F [a]> : F [a] ~ f,
   with Refl evidence, and we *don't* want those to count as an equality
   in the givens!  After all, the entire flattening business is just an
   internal matter, and the evidence does not mention any of the 'givens'
   of this implication.  So we do not treat inert_funeqs as a 'given equality'.

 * See Note [Let-bound skolems] for another wrinkle

 * We do *not* need to worry about representational equalities, because
   these do not affect the ability to float constraints.

Note [Let-bound skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
If   * the inert set contains a canonical Given CTyEqCan (a ~ ty)
and  * 'a' is a skolem bound in this very implication,

then:
a) The Given is pretty much a let-binding, like
      f :: (a ~ b->c) => a -> a
   Here the equality constraint is like saying
      let a = b->c in ...
   It is not adding any new, local equality  information,
   and hence can be ignored by has_given_eqs

b) 'a' will have been completely substituted out in the inert set,
   so we can safely discard it.  Notably, it doesn't need to be
   returned as part of 'fsks'

For an example, see #9211.

See also TcUnify Note [Deeper level on the left] for how we ensure
that the right variable is on the left of the equality when both are
tyvars.

You might wonder whether the skokem really needs to be bound "in the
very same implication" as the equuality constraint.
(c.f. #15009) Consider this:

  data S a where
    MkS :: (a ~ Int) => S a

  g :: forall a. S a -> a -> blah
  g x y = let h = \z. ( z :: Int
                      , case x of
                           MkS -> [y,z])
          in ...

From the type signature for `g`, we get `y::a` .  Then when when we
encounter the `\z`, we'll assign `z :: alpha[1]`, say.  Next, from the
body of the lambda we'll get

  [W] alpha[1] ~ Int                             -- From z::Int
  [W] forall[2]. (a ~ Int) => [W] alpha[1] ~ a   -- From [y,z]

Now, suppose we decide to float `alpha ~ a` out of the implication
and then unify `alpha := a`.  Now we are stuck!  But if treat
`alpha ~ Int` first, and unify `alpha := Int`, all is fine.
But we absolutely cannot float that equality or we will get stuck.
-}

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

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

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

    CFunEqCan { cc_fun :: Ct -> TyCon
cc_fun  = TyCon
tf,  cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType]
tys } ->
      InertCans
is { inert_funeqs :: FunEqMap Ct
inert_funeqs = FunEqMap Ct -> TyCon -> [PredType] -> FunEqMap Ct
forall a. FunEqMap a -> TyCon -> [PredType] -> FunEqMap a
delFunEq (InertCans -> FunEqMap Ct
inert_funeqs InertCans
is) TyCon
tf [PredType]
tys }

    CTyEqCan  { cc_tyvar :: Ct -> TcTyVar
cc_tyvar = TcTyVar
x,  cc_rhs :: Ct -> PredType
cc_rhs    = PredType
ty } ->
      InertCans
is { inert_eqs :: InertEqs
inert_eqs    = InertEqs -> TcTyVar -> PredType -> InertEqs
delTyEq (InertCans -> InertEqs
inert_eqs InertCans
is) TcTyVar
x PredType
ty }

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


lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour))
lookupFlatCache :: TyCon
-> [PredType] -> TcS (Maybe (TcCoercion, PredType, CtFlavour))
lookupFlatCache TyCon
fam_tc [PredType]
tys
  = do { IS { inert_flat_cache :: InertSet -> ExactFunEqMap (TcCoercion, PredType, CtFlavour)
inert_flat_cache = ExactFunEqMap (TcCoercion, PredType, CtFlavour)
flat_cache
            , inert_cans :: InertSet -> InertCans
inert_cans = IC { inert_funeqs :: InertCans -> FunEqMap Ct
inert_funeqs = FunEqMap Ct
inert_funeqs } } <- TcS InertSet
getTcSInerts
       ; Maybe (TcCoercion, PredType, CtFlavour)
-> TcS (Maybe (TcCoercion, PredType, CtFlavour))
forall (m :: * -> *) a. Monad m => a -> m a
return ([Maybe (TcCoercion, PredType, CtFlavour)]
-> Maybe (TcCoercion, PredType, CtFlavour)
forall a. [Maybe a] -> Maybe a
firstJusts [FunEqMap Ct -> Maybe (TcCoercion, PredType, CtFlavour)
lookup_inerts FunEqMap Ct
inert_funeqs,
                             ExactFunEqMap (TcCoercion, PredType, CtFlavour)
-> Maybe (TcCoercion, PredType, CtFlavour)
lookup_flats ExactFunEqMap (TcCoercion, PredType, CtFlavour)
flat_cache]) }
  where
    lookup_inerts :: FunEqMap Ct -> Maybe (TcCoercion, PredType, CtFlavour)
lookup_inerts FunEqMap Ct
inert_funeqs
      | Just (CFunEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ctev, cc_fsk :: Ct -> TcTyVar
cc_fsk = TcTyVar
fsk, cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType]
xis })
           <- FunEqMap Ct -> TyCon -> [PredType] -> Maybe Ct
forall a. FunEqMap a -> TyCon -> [PredType] -> Maybe a
findFunEq FunEqMap Ct
inert_funeqs TyCon
fam_tc [PredType]
tys
      , [PredType]
tys [PredType] -> [PredType] -> Bool
`eqTypes` [PredType]
xis   -- The lookup might find a near-match; see
                            -- Note [Use loose types in inert set]
      = (TcCoercion, PredType, CtFlavour)
-> Maybe (TcCoercion, PredType, CtFlavour)
forall a. a -> Maybe a
Just (HasDebugCallStack => CtEvidence -> TcCoercion
CtEvidence -> TcCoercion
ctEvCoercion CtEvidence
ctev, TcTyVar -> PredType
mkTyVarTy TcTyVar
fsk, CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ctev)
      | Bool
otherwise = Maybe (TcCoercion, PredType, CtFlavour)
forall a. Maybe a
Nothing

    lookup_flats :: ExactFunEqMap (TcCoercion, PredType, CtFlavour)
-> Maybe (TcCoercion, PredType, CtFlavour)
lookup_flats ExactFunEqMap (TcCoercion, PredType, CtFlavour)
flat_cache = ExactFunEqMap (TcCoercion, PredType, CtFlavour)
-> TyCon -> [PredType] -> Maybe (TcCoercion, PredType, CtFlavour)
forall a. ExactFunEqMap a -> TyCon -> [PredType] -> Maybe a
findExactFunEq ExactFunEqMap (TcCoercion, PredType, CtFlavour)
flat_cache TyCon
fam_tc [PredType]
tys


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

-- | Look up a dictionary inert. NB: the returned 'CtEvidence' might not
-- match the input exactly. Note [Use loose types in inert set].
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupInertDict :: InertCans -> CtLoc -> Class -> [PredType] -> Maybe CtEvidence
lookupInertDict (IC { inert_dicts :: InertCans -> FunEqMap Ct
inert_dicts = FunEqMap Ct
dicts }) CtLoc
loc Class
cls [PredType]
tys
  = case FunEqMap Ct -> CtLoc -> Class -> [PredType] -> Maybe Ct
forall a. DictMap a -> CtLoc -> Class -> [PredType] -> Maybe a
findDict FunEqMap Ct
dicts CtLoc
loc Class
cls [PredType]
tys of
      Just Ct
ct -> CtEvidence -> Maybe CtEvidence
forall a. a -> Maybe a
Just (Ct -> CtEvidence
ctEvidence Ct
ct)
      Maybe Ct
_       -> Maybe CtEvidence
forall a. Maybe a
Nothing

-- | Look up a solved inert. NB: the returned 'CtEvidence' might not
-- match the input exactly. See Note [Use loose types in inert set].
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
-- Returns just if exactly this predicate type exists in the solved.
lookupSolvedDict :: InertSet -> CtLoc -> Class -> [PredType] -> Maybe CtEvidence
lookupSolvedDict (IS { inert_solved_dicts :: InertSet -> DictMap CtEvidence
inert_solved_dicts = DictMap CtEvidence
solved }) CtLoc
loc Class
cls [PredType]
tys
  = case DictMap CtEvidence
-> CtLoc -> Class -> [PredType] -> Maybe CtEvidence
forall a. DictMap a -> CtLoc -> Class -> [PredType] -> Maybe a
findDict DictMap CtEvidence
solved CtLoc
loc Class
cls [PredType]
tys of
      Just CtEvidence
ev -> CtEvidence -> Maybe CtEvidence
forall a. a -> Maybe a
Just CtEvidence
ev
      Maybe CtEvidence
_       -> Maybe CtEvidence
forall a. Maybe a
Nothing

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

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


{- *********************************************************************
*                                                                      *
                   TcAppMap
*                                                                      *
************************************************************************

Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Say we know (Eq (a |> c1)) and we need (Eq (a |> c2)). One is clearly
solvable from the other. So, we do lookup in the inert set using
loose types, which omit the kind-check.

We must be careful when using the result of a lookup because it may
not match the requested info exactly!

-}

type TcAppMap a = UniqDFM (ListMap LooseTypeMap a)
    -- Indexed by tycon then the arg types, using "loose" matching, where
    -- we don't require kind equality. This allows, for example, (a |> co)
    -- to match (a).
    -- See Note [Use loose types in inert set]
    -- Used for types and classes; hence UniqDFM
    -- See Note [foldTM determinism] for why we use UniqDFM here

isEmptyTcAppMap :: TcAppMap a -> Bool
isEmptyTcAppMap :: TcAppMap a -> Bool
isEmptyTcAppMap TcAppMap a
m = TcAppMap a -> Bool
forall a. DVarEnv a -> Bool
isNullUDFM TcAppMap a
m

emptyTcAppMap :: TcAppMap a
emptyTcAppMap :: TcAppMap a
emptyTcAppMap = TcAppMap a
forall a. DVarEnv a
emptyUDFM

findTcApp :: TcAppMap a -> Unique -> [Type] -> Maybe a
findTcApp :: TcAppMap a -> Unique -> [PredType] -> Maybe a
findTcApp TcAppMap a
m Unique
u [PredType]
tys = do { ListMap LooseTypeMap a
tys_map <- TcAppMap a -> Unique -> Maybe (ListMap LooseTypeMap a)
forall key elt. Uniquable key => UniqDFM elt -> key -> Maybe elt
lookupUDFM TcAppMap a
m Unique
u
                       ; Key (ListMap LooseTypeMap) -> ListMap LooseTypeMap a -> Maybe a
forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM [PredType]
Key (ListMap LooseTypeMap)
tys ListMap LooseTypeMap a
tys_map }

delTcApp :: TcAppMap a -> Unique -> [Type] -> TcAppMap a
delTcApp :: TcAppMap a -> Unique -> [PredType] -> TcAppMap a
delTcApp TcAppMap a
m Unique
cls [PredType]
tys = (ListMap LooseTypeMap a -> ListMap LooseTypeMap a)
-> TcAppMap a -> Unique -> TcAppMap a
forall key elt.
Uniquable key =>
(elt -> elt) -> UniqDFM elt -> key -> UniqDFM elt
adjustUDFM (Key (ListMap LooseTypeMap)
-> ListMap LooseTypeMap a -> ListMap LooseTypeMap a
forall (m :: * -> *) a. TrieMap m => Key m -> m a -> m a
deleteTM [PredType]
Key (ListMap LooseTypeMap)
tys) TcAppMap a
m Unique
cls

insertTcApp :: TcAppMap a -> Unique -> [Type] -> a -> TcAppMap a
insertTcApp :: TcAppMap a -> Unique -> [PredType] -> a -> TcAppMap a
insertTcApp TcAppMap a
m Unique
cls [PredType]
tys a
ct = (Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a))
-> TcAppMap a -> Unique -> TcAppMap a
forall key elt.
Uniquable key =>
(Maybe elt -> Maybe elt) -> UniqDFM elt -> key -> UniqDFM elt
alterUDFM Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
alter_tm TcAppMap a
m Unique
cls
  where
    alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
alter_tm Maybe (ListMap LooseTypeMap a)
mb_tm = ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
forall a. a -> Maybe a
Just (Key (ListMap LooseTypeMap)
-> a -> ListMap LooseTypeMap a -> ListMap LooseTypeMap a
forall (m :: * -> *) a. TrieMap m => Key m -> a -> m a -> m a
insertTM [PredType]
Key (ListMap LooseTypeMap)
tys a
ct (Maybe (ListMap LooseTypeMap a)
mb_tm Maybe (ListMap LooseTypeMap a)
-> ListMap LooseTypeMap a -> ListMap LooseTypeMap a
forall a. Maybe a -> a -> a
`orElse` ListMap LooseTypeMap a
forall (m :: * -> *) a. TrieMap m => m a
emptyTM))

-- mapTcApp :: (a->b) -> TcAppMap a -> TcAppMap b
-- mapTcApp f = mapUDFM (mapTM f)

filterTcAppMap :: (Ct -> Bool) -> TcAppMap Ct -> TcAppMap Ct
filterTcAppMap :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
filterTcAppMap Ct -> Bool
f FunEqMap Ct
m
  = (ListMap LooseTypeMap Ct -> ListMap LooseTypeMap Ct)
-> FunEqMap Ct -> FunEqMap Ct
forall elt1 elt2. (elt1 -> elt2) -> UniqDFM elt1 -> UniqDFM elt2
mapUDFM ListMap LooseTypeMap Ct -> ListMap LooseTypeMap Ct
do_tm FunEqMap Ct
m
  where
    do_tm :: ListMap LooseTypeMap Ct -> ListMap LooseTypeMap Ct
do_tm ListMap LooseTypeMap Ct
tm = (Ct -> ListMap LooseTypeMap Ct -> ListMap LooseTypeMap Ct)
-> ListMap LooseTypeMap Ct
-> ListMap LooseTypeMap Ct
-> ListMap LooseTypeMap Ct
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM Ct -> ListMap LooseTypeMap Ct -> ListMap LooseTypeMap Ct
insert_mb ListMap LooseTypeMap Ct
tm ListMap LooseTypeMap Ct
forall (m :: * -> *) a. TrieMap m => m a
emptyTM
    insert_mb :: Ct -> ListMap LooseTypeMap Ct -> ListMap LooseTypeMap Ct
insert_mb Ct
ct ListMap LooseTypeMap Ct
tm
       | Ct -> Bool
f Ct
ct      = Key (ListMap LooseTypeMap)
-> Ct -> ListMap LooseTypeMap Ct -> ListMap LooseTypeMap Ct
forall (m :: * -> *) a. TrieMap m => Key m -> a -> m a -> m a
insertTM [PredType]
Key (ListMap LooseTypeMap)
tys Ct
ct ListMap LooseTypeMap Ct
tm
       | Bool
otherwise = ListMap LooseTypeMap Ct
tm
       where
         tys :: [PredType]
tys = case Ct
ct of
                CFunEqCan { cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType]
tys } -> [PredType]
tys
                CDictCan  { cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType]
tys } -> [PredType]
tys
                Ct
_ -> String -> SDoc -> [PredType]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"filterTcAppMap" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)

tcAppMapToBag :: TcAppMap a -> Bag a
tcAppMapToBag :: TcAppMap a -> Bag a
tcAppMapToBag TcAppMap a
m = (a -> Bag a -> Bag a) -> TcAppMap a -> Bag a -> Bag a
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldTcAppMap a -> Bag a -> Bag a
forall a. a -> Bag a -> Bag a
consBag TcAppMap a
m Bag a
forall a. Bag a
emptyBag

foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
foldTcAppMap a -> b -> b
k TcAppMap a
m b
z = (ListMap LooseTypeMap a -> b -> b) -> b -> TcAppMap a -> b
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldUDFM ((a -> b -> b) -> ListMap LooseTypeMap a -> b -> b
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> b -> b
k) b
z TcAppMap a
m


{- *********************************************************************
*                                                                      *
                   DictMap
*                                                                      *
********************************************************************* -}


{- Note [Tuples hiding implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
   f,g :: (?x::Int, C a) => a -> a
   f v = let ?x = 4 in g v

The call to 'g' gives rise to a Wanted constraint (?x::Int, C a).
We must /not/ solve this from the Given (?x::Int, C a), because of
the intervening binding for (?x::Int).  #14218.

We deal with this by arranging that we always fail when looking up a
tuple constraint that hides an implicit parameter. Not that this applies
  * both to the inert_dicts (lookupInertDict)
  * and to the solved_dicts (looukpSolvedDict)
An alternative would be not to extend these sets with such tuple
constraints, but it seemed more direct to deal with the lookup.

Note [Solving CallStack constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose f :: HasCallStack => blah.  Then

* Each call to 'f' gives rise to
    [W] s1 :: IP "callStack" CallStack    -- CtOrigin = OccurrenceOf f
  with a CtOrigin that says "OccurrenceOf f".
  Remember that HasCallStack is just shorthand for
    IP "callStack CallStack
  See Note [Overview of implicit CallStacks] in TcEvidence

* We cannonicalise such constraints, in TcCanonical.canClassNC, by
  pushing the call-site info on the stack, and changing the CtOrigin
  to record that has been done.
   Bind:  s1 = pushCallStack <site-info> s2
   [W] s2 :: IP "callStack" CallStack   -- CtOrigin = IPOccOrigin

* Then, and only then, we can solve the constraint from an enclosing
  Given.

So we must be careful /not/ to solve 's1' from the Givens.  Again,
we ensure this by arranging that findDict always misses when looking
up souch constraints.
-}

type DictMap a = TcAppMap a

emptyDictMap :: DictMap a
emptyDictMap :: DictMap a
emptyDictMap = DictMap a
forall a. DictMap a
emptyTcAppMap

findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict :: DictMap a -> CtLoc -> Class -> [PredType] -> Maybe a
findDict DictMap a
m CtLoc
loc Class
cls [PredType]
tys
  | Class -> Bool
isCTupleClass Class
cls
  , (PredType -> Bool) -> [PredType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any PredType -> Bool
hasIPPred [PredType]
tys   -- See Note [Tuples hiding implicit parameters]
  = Maybe a
forall a. Maybe a
Nothing

  | Just {} <- Class -> [PredType] -> Maybe FastString
isCallStackPred Class
cls [PredType]
tys
  , OccurrenceOf {} <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc
  = Maybe a
forall a. Maybe a
Nothing             -- See Note [Solving CallStack constraints]

  | Bool
otherwise
  = DictMap a -> Unique -> [PredType] -> Maybe a
forall a. TcAppMap a -> Unique -> [PredType] -> Maybe a
findTcApp DictMap a
m (Class -> Unique
forall a. Uniquable a => a -> Unique
getUnique Class
cls) [PredType]
tys

findDictsByClass :: DictMap a -> Class -> Bag a
findDictsByClass :: DictMap a -> Class -> Bag a
findDictsByClass DictMap a
m Class
cls
  | Just ListMap LooseTypeMap a
tm <- DictMap a -> Class -> Maybe (ListMap LooseTypeMap a)
forall key elt. Uniquable key => UniqDFM elt -> key -> Maybe elt
lookupUDFM DictMap a
m Class
cls = (a -> Bag a -> Bag a) -> ListMap LooseTypeMap a -> Bag a -> Bag a
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM a -> Bag a -> Bag a
forall a. a -> Bag a -> Bag a
consBag ListMap LooseTypeMap a
tm Bag a
forall a. Bag a
emptyBag
  | Bool
otherwise                  = Bag a
forall a. Bag a
emptyBag

delDict :: DictMap a -> Class -> [Type] -> DictMap a
delDict :: DictMap a -> Class -> [PredType] -> DictMap a
delDict DictMap a
m Class
cls [PredType]
tys = DictMap a -> Unique -> [PredType] -> DictMap a
forall a. TcAppMap a -> Unique -> [PredType] -> TcAppMap a
delTcApp DictMap a
m (Class -> Unique
forall a. Uniquable a => a -> Unique
getUnique Class
cls) [PredType]
tys

addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
addDict :: DictMap a -> Class -> [PredType] -> a -> DictMap a
addDict DictMap a
m Class
cls [PredType]
tys a
item = DictMap a -> Unique -> [PredType] -> a -> DictMap a
forall a. TcAppMap a -> Unique -> [PredType] -> a -> TcAppMap a
insertTcApp DictMap a
m (Class -> Unique
forall a. Uniquable a => a -> Unique
getUnique Class
cls) [PredType]
tys a
item

addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
addDictsByClass :: FunEqMap Ct -> Class -> Cts -> FunEqMap Ct
addDictsByClass FunEqMap Ct
m Class
cls Cts
items
  = FunEqMap Ct -> Class -> ListMap LooseTypeMap Ct -> FunEqMap Ct
forall key elt.
Uniquable key =>
UniqDFM elt -> key -> elt -> UniqDFM elt
addToUDFM FunEqMap Ct
m Class
cls ((Ct -> ListMap LooseTypeMap Ct -> ListMap LooseTypeMap Ct)
-> ListMap LooseTypeMap Ct -> Cts -> ListMap LooseTypeMap Ct
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> ListMap LooseTypeMap Ct -> ListMap LooseTypeMap Ct
forall (m :: * -> *).
(TrieMap m, Key m ~ [PredType]) =>
Ct -> m Ct -> m Ct
add ListMap LooseTypeMap Ct
forall (m :: * -> *) a. TrieMap m => m a
emptyTM Cts
items)
  where
    add :: Ct -> m Ct -> m Ct
add ct :: Ct
ct@(CDictCan { cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType]
tys }) m Ct
tm = Key m -> Ct -> m Ct -> m Ct
forall (m :: * -> *) a. TrieMap m => Key m -> a -> m a -> m a
insertTM [PredType]
Key m
tys Ct
ct m Ct
tm
    add Ct
ct m Ct
_ = String -> SDoc -> m Ct
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"addDictsByClass" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)

filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
filterDicts :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
filterDicts Ct -> Bool
f FunEqMap Ct
m = (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
filterTcAppMap Ct -> Bool
f FunEqMap Ct
m

partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
partitionDicts :: (Ct -> Bool) -> FunEqMap Ct -> (Cts, FunEqMap Ct)
partitionDicts Ct -> Bool
f FunEqMap Ct
m = (Ct -> (Cts, FunEqMap Ct) -> (Cts, FunEqMap Ct))
-> FunEqMap Ct -> (Cts, FunEqMap Ct) -> (Cts, FunEqMap Ct)
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldTcAppMap Ct -> (Cts, FunEqMap Ct) -> (Cts, FunEqMap Ct)
k FunEqMap Ct
m (Cts
forall a. Bag a
emptyBag, FunEqMap Ct
forall a. DictMap a
emptyDicts)
  where
    k :: Ct -> (Cts, FunEqMap Ct) -> (Cts, FunEqMap Ct)
k Ct
ct (Cts
yeses, FunEqMap Ct
noes) | Ct -> Bool
f Ct
ct      = (Ct
ct Ct -> Cts -> Cts
forall a. a -> Bag a -> Bag a
`consBag` Cts
yeses, FunEqMap Ct
noes)
                       | Bool
otherwise = (Cts
yeses,              Ct -> FunEqMap Ct -> FunEqMap Ct
add Ct
ct FunEqMap Ct
noes)
    add :: Ct -> FunEqMap Ct -> FunEqMap Ct
add ct :: Ct
ct@(CDictCan { cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType]
tys }) FunEqMap Ct
m
      = FunEqMap Ct -> Class -> [PredType] -> Ct -> FunEqMap Ct
forall a. DictMap a -> Class -> [PredType] -> a -> DictMap a
addDict FunEqMap Ct
m Class
cls [PredType]
tys Ct
ct
    add Ct
ct FunEqMap Ct
_ = String -> SDoc -> FunEqMap Ct
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"partitionDicts" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)

dictsToBag :: DictMap a -> Bag a
dictsToBag :: DictMap a -> Bag a
dictsToBag = DictMap a -> Bag a
forall a. DictMap a -> Bag a
tcAppMapToBag

foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
foldDicts = (a -> b -> b) -> DictMap a -> b -> b
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldTcAppMap

emptyDicts :: DictMap a
emptyDicts :: DictMap a
emptyDicts = DictMap a
forall a. DictMap a
emptyTcAppMap


{- *********************************************************************
*                                                                      *
                   FunEqMap
*                                                                      *
********************************************************************* -}

type FunEqMap a = TcAppMap a  -- A map whose key is a (TyCon, [Type]) pair

emptyFunEqs :: TcAppMap a
emptyFunEqs :: TcAppMap a
emptyFunEqs = TcAppMap a
forall a. DictMap a
emptyTcAppMap

findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq :: FunEqMap a -> TyCon -> [PredType] -> Maybe a
findFunEq FunEqMap a
m TyCon
tc [PredType]
tys = FunEqMap a -> Unique -> [PredType] -> Maybe a
forall a. TcAppMap a -> Unique -> [PredType] -> Maybe a
findTcApp FunEqMap a
m (TyCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique TyCon
tc) [PredType]
tys

funEqsToBag :: FunEqMap a -> Bag a
funEqsToBag :: FunEqMap a -> Bag a
funEqsToBag FunEqMap a
m = (a -> Bag a -> Bag a) -> FunEqMap a -> Bag a -> Bag a
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldTcAppMap a -> Bag a -> Bag a
forall a. a -> Bag a -> Bag a
consBag FunEqMap a
m Bag a
forall a. Bag a
emptyBag

findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
-- Get inert function equation constraints that have the given tycon
-- in their head.  Not that the constraints remain in the inert set.
-- We use this to check for derived interactions with built-in type-function
-- constructors.
findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
findFunEqsByTyCon FunEqMap a
m TyCon
tc
  | Just ListMap LooseTypeMap a
tm <- FunEqMap a -> TyCon -> Maybe (ListMap LooseTypeMap a)
forall key elt. Uniquable key => UniqDFM elt -> key -> Maybe elt
lookupUDFM FunEqMap a
m TyCon
tc = (a -> [a] -> [a]) -> ListMap LooseTypeMap a -> [a] -> [a]
forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM (:) ListMap LooseTypeMap a
tm []
  | Bool
otherwise                 = []

foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs = (a -> b -> b) -> FunEqMap a -> b -> b
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldTcAppMap

-- mapFunEqs :: (a -> b) -> FunEqMap a -> FunEqMap b
-- mapFunEqs = mapTcApp

-- filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
-- filterFunEqs = filterTcAppMap

insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
insertFunEq :: FunEqMap a -> TyCon -> [PredType] -> a -> FunEqMap a
insertFunEq FunEqMap a
m TyCon
tc [PredType]
tys a
val = FunEqMap a -> Unique -> [PredType] -> a -> FunEqMap a
forall a. TcAppMap a -> Unique -> [PredType] -> a -> TcAppMap a
insertTcApp FunEqMap a
m (TyCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique TyCon
tc) [PredType]
tys a
val

partitionFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> ([Ct], FunEqMap Ct)
-- Optimise for the case where the predicate is false
-- partitionFunEqs is called only from kick-out, and kick-out usually
-- kicks out very few equalities, so we want to optimise for that case
partitionFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> ([Ct], FunEqMap Ct)
partitionFunEqs Ct -> Bool
f FunEqMap Ct
m = ([Ct]
yeses, (Ct -> FunEqMap Ct -> FunEqMap Ct)
-> FunEqMap Ct -> [Ct] -> FunEqMap Ct
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> FunEqMap Ct -> FunEqMap Ct
forall a. Ct -> FunEqMap a -> FunEqMap a
del FunEqMap Ct
m [Ct]
yeses)
  where
    yeses :: [Ct]
yeses = (Ct -> [Ct] -> [Ct]) -> FunEqMap Ct -> [Ct] -> [Ct]
forall a b. (a -> b -> b) -> DictMap a -> b -> b
foldTcAppMap Ct -> [Ct] -> [Ct]
k FunEqMap Ct
m []
    k :: Ct -> [Ct] -> [Ct]
k Ct
ct [Ct]
yeses | Ct -> Bool
f Ct
ct      = Ct
ct Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: [Ct]
yeses
               | Bool
otherwise = [Ct]
yeses
    del :: Ct -> FunEqMap a -> FunEqMap a
del (CFunEqCan { cc_fun :: Ct -> TyCon
cc_fun = TyCon
tc, cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType]
tys }) FunEqMap a
m
        = FunEqMap a -> TyCon -> [PredType] -> FunEqMap a
forall a. FunEqMap a -> TyCon -> [PredType] -> FunEqMap a
delFunEq FunEqMap a
m TyCon
tc [PredType]
tys
    del Ct
ct FunEqMap a
_ = String -> SDoc -> FunEqMap a
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"partitionFunEqs" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)

delFunEq :: FunEqMap a -> TyCon -> [Type] -> FunEqMap a
delFunEq :: FunEqMap a -> TyCon -> [PredType] -> FunEqMap a
delFunEq FunEqMap a
m TyCon
tc [PredType]
tys = FunEqMap a -> Unique -> [PredType] -> FunEqMap a
forall a. TcAppMap a -> Unique -> [PredType] -> TcAppMap a
delTcApp FunEqMap a
m (TyCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique TyCon
tc) [PredType]
tys

------------------------------
type ExactFunEqMap a = UniqFM (ListMap TypeMap a)

emptyExactFunEqs :: ExactFunEqMap a
emptyExactFunEqs :: ExactFunEqMap a
emptyExactFunEqs = ExactFunEqMap a
forall elt. UniqFM elt
emptyUFM

findExactFunEq :: ExactFunEqMap a -> TyCon -> [Type] -> Maybe a
findExactFunEq :: ExactFunEqMap a -> TyCon -> [PredType] -> Maybe a
findExactFunEq ExactFunEqMap a
m TyCon
tc [PredType]
tys = do { ListMap TypeMap a
tys_map <- ExactFunEqMap a -> Unique -> Maybe (ListMap TypeMap a)
forall key elt. Uniquable key => UniqFM elt -> key -> Maybe elt
lookupUFM ExactFunEqMap a
m (TyCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique TyCon
tc)
                             ; Key (ListMap TypeMap) -> ListMap TypeMap a -> Maybe a
forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM [PredType]
Key (ListMap TypeMap)
tys ListMap TypeMap a
tys_map }

insertExactFunEq :: ExactFunEqMap a -> TyCon -> [Type] -> a -> ExactFunEqMap a
insertExactFunEq :: ExactFunEqMap a -> TyCon -> [PredType] -> a -> ExactFunEqMap a
insertExactFunEq ExactFunEqMap a
m TyCon
tc [PredType]
tys a
val = (Maybe (ListMap TypeMap a) -> Maybe (ListMap TypeMap a))
-> ExactFunEqMap a -> Unique -> ExactFunEqMap a
forall key elt.
Uniquable key =>
(Maybe elt -> Maybe elt) -> UniqFM elt -> key -> UniqFM elt
alterUFM Maybe (ListMap TypeMap a) -> Maybe (ListMap TypeMap a)
alter_tm ExactFunEqMap a
m (TyCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique TyCon
tc)
  where alter_tm :: Maybe (ListMap TypeMap a) -> Maybe (ListMap TypeMap a)
alter_tm Maybe (ListMap TypeMap a)
mb_tm = ListMap TypeMap a -> Maybe (ListMap TypeMap a)
forall a. a -> Maybe a
Just (Key (ListMap TypeMap)
-> a -> ListMap TypeMap a -> ListMap TypeMap a
forall (m :: * -> *) a. TrieMap m => Key m -> a -> m a -> m a
insertTM [PredType]
Key (ListMap TypeMap)
tys a
val (Maybe (ListMap TypeMap a)
mb_tm Maybe (ListMap TypeMap a) -> ListMap TypeMap a -> ListMap TypeMap a
forall a. Maybe a -> a -> a
`orElse` ListMap TypeMap a
forall (m :: * -> *) a. TrieMap m => m a
emptyTM))

{-
************************************************************************
*                                                                      *
*              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 Int
tcs_count     :: IORef Int, -- Global step count

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

      -- The main work-list and the flattening worklist
      -- See Note [Work list priorities] and
      TcSEnv -> IORef WorkList
tcs_worklist  :: IORef WorkList -- Current worklist
    }

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

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

instance Monad TcS where
#if !MIN_VERSION_base(4,13,0)
  fail = MonadFail.fail
#endif
  TcS a
m >>= :: TcS a -> (a -> TcS b) -> TcS b
>>= a -> TcS b
k   = (TcSEnv -> TcM b) -> TcS b
forall a. (TcSEnv -> TcM a) -> TcS a
TcS (\TcSEnv
ebs -> TcS a -> TcSEnv -> TcM a
forall a. TcS a -> TcSEnv -> TcM a
unTcS TcS a
m TcSEnv
ebs TcM a -> (a -> TcM b) -> TcM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
r -> TcS b -> TcSEnv -> TcM b
forall a. TcS a -> TcSEnv -> TcM a
unTcS (a -> TcS b
k a
r) TcSEnv
ebs)

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

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

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

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

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

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

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

failTcS, panicTcS  :: SDoc -> TcS a
warnTcS   :: WarningFlag -> SDoc -> TcS ()
addErrTcS :: SDoc -> TcS ()
failTcS :: SDoc -> TcS a
failTcS      = TcM a -> TcS a
forall a. TcM a -> TcS a
wrapTcS (TcM a -> TcS a) -> (SDoc -> TcM a) -> SDoc -> TcS a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> TcM a
forall a. SDoc -> TcRn a
TcM.failWith
warnTcS :: WarningFlag -> SDoc -> TcS ()
warnTcS WarningFlag
flag = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> (SDoc -> TcM ()) -> SDoc -> TcS ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WarnReason -> SDoc -> TcM ()
TcM.addWarn (WarningFlag -> WarnReason
Reason WarningFlag
flag)
addErrTcS :: SDoc -> TcS ()
addErrTcS    = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> (SDoc -> TcM ()) -> SDoc -> TcS ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SDoc -> TcM ()
TcM.addErr
panicTcS :: SDoc -> TcS a
panicTcS SDoc
doc = String -> SDoc -> TcS a
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"TcCanonical" SDoc
doc

traceTcS :: String -> SDoc -> TcS ()
traceTcS :: String -> SDoc -> TcS ()
traceTcS String
herald SDoc
doc = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (String -> SDoc -> TcM ()
TcM.traceTc String
herald SDoc
doc)

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

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

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

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

csTraceTcS :: SDoc -> TcS ()
csTraceTcS :: SDoc -> TcS ()
csTraceTcS SDoc
doc
  = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ TcM SDoc -> TcM ()
csTraceTcM (SDoc -> TcM SDoc
forall (m :: * -> *) a. Monad m => a -> m a
return SDoc
doc)

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
TcS ((TcSEnv -> TcM ()) -> TcS ()) -> (TcSEnv -> TcM ()) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \TcSEnv
env -> TcM SDoc -> TcM ()
csTraceTcM (TcM SDoc -> TcM ()) -> TcM SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
    do { Int
n <- IORef Int -> TcRnIf TcGblEnv TcLclEnv Int
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef (TcSEnv -> IORef Int
tcs_count TcSEnv
env)
       ; TcLevel
tclvl <- TcM TcLevel
TcM.getTcLevel
       ; SDoc -> TcM SDoc
forall (m :: * -> *) a. Monad m => a -> m a
return (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Step" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
n
                       SDoc -> SDoc -> SDoc
<> SDoc -> SDoc
brackets (String -> SDoc
text String
"l:" SDoc -> SDoc -> SDoc
<> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl SDoc -> SDoc -> SDoc
<> SDoc
comma SDoc -> SDoc -> SDoc
<>
                                    String -> SDoc
text String
"d:" SDoc -> SDoc -> SDoc
<> SubGoalDepth -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> SubGoalDepth
ctLocDepth (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev)))
                       SDoc -> SDoc -> SDoc
<+> SDoc
doc SDoc -> SDoc -> SDoc
<> SDoc
colon)
                     Int
4 (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev)) }

csTraceTcM :: TcM SDoc -> TcM ()
-- Constraint-solver tracing, -ddump-cs-trace
csTraceTcM :: TcM SDoc -> TcM ()
csTraceTcM TcM SDoc
mk_doc
  = do { DynFlags
dflags <- TcM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (  DumpFlag -> DynFlags -> Bool
dopt DumpFlag
Opt_D_dump_cs_trace DynFlags
dflags
                  Bool -> Bool -> Bool
|| DumpFlag -> DynFlags -> Bool
dopt DumpFlag
Opt_D_dump_tc_trace DynFlags
dflags )
              ( do { SDoc
msg <- TcM SDoc
mk_doc
                   ; DumpFlag -> SDoc -> TcM ()
TcM.traceTcRn DumpFlag
Opt_D_dump_cs_trace SDoc
msg }) }

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

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

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

runTcSWithEvBinds :: EvBindsVar
                  -> TcS a
                  -> TcM a
runTcSWithEvBinds :: EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds EvBindsVar
ev_binds_var TcS a
tcs
  = do { IORef Int
unified_var <- Int -> TcRnIf TcGblEnv TcLclEnv (IORef Int)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef Int
0
       ; IORef Int
step_count <- Int -> TcRnIf TcGblEnv TcLclEnv (IORef Int)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef Int
0
       ; IORef InertSet
inert_var <- InertSet -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef InertSet
emptyInert
       ; IORef WorkList
wl_var <- WorkList -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef WorkList
emptyWorkList
       ; let env :: TcSEnv
env = TcSEnv :: EvBindsVar
-> IORef Int
-> IORef Int
-> IORef InertSet
-> IORef WorkList
-> TcSEnv
TcSEnv { tcs_ev_binds :: EvBindsVar
tcs_ev_binds      = EvBindsVar
ev_binds_var
                          , tcs_unified :: IORef Int
tcs_unified       = IORef Int
unified_var
                          , tcs_count :: IORef Int
tcs_count         = IORef Int
step_count
                          , tcs_inerts :: IORef InertSet
tcs_inerts        = IORef InertSet
inert_var
                          , tcs_worklist :: IORef WorkList
tcs_worklist      = IORef WorkList
wl_var }

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

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

       ; IORef InertSet -> TcM ()
unflattenGivens IORef InertSet
inert_var

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

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

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

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

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

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

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

nestImplicTcS :: EvBindsVar
              -> TcLevel -> TcS a
              -> TcS a
nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a -> TcS a
nestImplicTcS EvBindsVar
ref TcLevel
inner_tclvl (TcS TcSEnv -> TcM a
thing_inside)
  = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \ TcSEnv { tcs_unified :: TcSEnv -> IORef Int
tcs_unified       = IORef Int
unified_var
                   , tcs_inerts :: TcSEnv -> IORef InertSet
tcs_inerts        = IORef InertSet
old_inert_var
                   , tcs_count :: TcSEnv -> IORef Int
tcs_count         = IORef Int
count
                   } ->
    do { InertSet
inerts <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
old_inert_var
       ; let nest_inert :: InertSet
nest_inert = InertSet
emptyInert
                            { inert_cans :: InertCans
inert_cans = InertSet -> InertCans
inert_cans InertSet
inerts
                            , inert_solved_dicts :: DictMap CtEvidence
inert_solved_dicts = InertSet -> DictMap CtEvidence
inert_solved_dicts InertSet
inerts }
                              -- See Note [Do not inherit the flat cache]
       ; IORef InertSet
new_inert_var <- InertSet -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef InertSet
nest_inert
       ; IORef WorkList
new_wl_var    <- WorkList -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef WorkList
emptyWorkList
       ; let nest_env :: TcSEnv
nest_env = TcSEnv :: EvBindsVar
-> IORef Int
-> IORef Int
-> IORef InertSet
-> IORef WorkList
-> TcSEnv
TcSEnv { tcs_ev_binds :: EvBindsVar
tcs_ev_binds      = EvBindsVar
ref
                               , tcs_unified :: IORef Int
tcs_unified       = IORef Int
unified_var
                               , tcs_count :: IORef Int
tcs_count         = IORef Int
count
                               , tcs_inerts :: IORef InertSet
tcs_inerts        = IORef InertSet
new_inert_var
                               , tcs_worklist :: IORef WorkList
tcs_worklist      = IORef WorkList
new_wl_var }
       ; a
res <- TcLevel -> TcM a -> TcM a
forall a. TcLevel -> TcM a -> TcM a
TcM.setTcLevel TcLevel
inner_tclvl (TcM a -> TcM a) -> TcM a -> TcM a
forall a b. (a -> b) -> a -> b
$
                TcSEnv -> TcM a
thing_inside TcSEnv
nest_env

       ; IORef InertSet -> TcM ()
unflattenGivens IORef InertSet
new_inert_var

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

{- Note [Do not inherit the flat cache]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We do not want to inherit the flat cache when processing nested
implications.  Consider
   a ~ F b, forall c. b~Int => blah
If we have F b ~ fsk in the flat-cache, and we push that into the
nested implication, we might miss that F b can be rewritten to F Int,
and hence perhpas solve it.  Moreover, the fsk from outside is
flattened out after solving the outer level, but and we don't
do that flattening recursively.
-}

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_flat_cache
-- (we want to inherit the latter from processing the Givens)
nestTcS :: TcS a -> TcS a
nestTcS (TcS TcSEnv -> TcM a
thing_inside)
  = (TcSEnv -> TcM a) -> TcS a
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM a) -> TcS a) -> (TcSEnv -> TcM a) -> TcS a
forall a b. (a -> b) -> a -> b
$ \ env :: TcSEnv
env@(TcSEnv { tcs_inerts :: TcSEnv -> IORef InertSet
tcs_inerts = IORef InertSet
inerts_var }) ->
    do { InertSet
inerts <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
inerts_var
       ; IORef InertSet
new_inert_var <- InertSet -> TcRnIf TcGblEnv TcLclEnv (IORef InertSet)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef InertSet
inerts
       ; IORef WorkList
new_wl_var    <- WorkList -> TcRnIf TcGblEnv TcLclEnv (IORef WorkList)
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef WorkList
emptyWorkList
       ; let nest_env :: TcSEnv
nest_env = TcSEnv
env { tcs_inerts :: IORef InertSet
tcs_inerts   = IORef InertSet
new_inert_var
                            , tcs_worklist :: IORef WorkList
tcs_worklist = IORef WorkList
new_wl_var }

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

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

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

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

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

checkTvConstraintsTcS :: SkolemInfo
                      -> [TcTyVar]        -- Skolems
                      -> TcS (result, Cts)
                      -> TcS result
-- Just like TcUnify.checkTvConstraints, but
--   - In the TcS monnad
--   - The thing-inside should not put things in the work-list
--     Instead, it returns the Wanted constraints it needs
--   - No 'givens', and no TcEvBinds; this is type-level constraints only
checkTvConstraintsTcS :: SkolemInfo -> [TcTyVar] -> TcS (result, Cts) -> TcS result
checkTvConstraintsTcS SkolemInfo
skol_info [TcTyVar]
skol_tvs (TcS TcSEnv -> TcM (result, Cts)
thing_inside)
  = (TcSEnv -> TcM result) -> TcS result
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM result) -> TcS result)
-> (TcSEnv -> TcM result) -> TcS result
forall a b. (a -> b) -> a -> b
$ \ TcSEnv
tcs_env ->
    do { let wl_panic :: IORef WorkList
wl_panic  = String -> SDoc -> IORef WorkList
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"TcSMonad.buildImplication" (SDoc -> IORef WorkList) -> SDoc -> IORef WorkList
forall a b. (a -> b) -> a -> b
$
                         SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfo
skol_info SDoc -> SDoc -> SDoc
$$ [TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
skol_tvs
                         -- This panic checks that the thing-inside
                         -- does not emit any work-list constraints
             new_tcs_env :: TcSEnv
new_tcs_env = TcSEnv
tcs_env { tcs_worklist :: IORef WorkList
tcs_worklist = IORef WorkList
wl_panic }

       ; (TcLevel
new_tclvl, (result
res, Cts
wanteds)) <- TcM (result, Cts) -> TcM (TcLevel, (result, Cts))
forall a. TcM a -> TcM (TcLevel, a)
TcM.pushTcLevelM (TcM (result, Cts) -> TcM (TcLevel, (result, Cts)))
-> TcM (result, Cts) -> TcM (TcLevel, (result, Cts))
forall a b. (a -> b) -> a -> b
$
                                        TcSEnv -> TcM (result, Cts)
thing_inside TcSEnv
new_tcs_env

       ; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Cts -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Cts
wanteds) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
         do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newNoTcEvBinds
            ; Implication
imp <- TcM Implication
TcM.newImplication
            ; let wc :: WantedConstraints
wc = WantedConstraints
emptyWC { wc_simple :: Cts
wc_simple = Cts
wanteds }
                  imp' :: Implication
imp' = Implication
imp { ic_tclvl :: TcLevel
ic_tclvl  = TcLevel
new_tclvl
                             , ic_skols :: [TcTyVar]
ic_skols  = [TcTyVar]
skol_tvs
                             , ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
wc
                             , ic_binds :: EvBindsVar
ic_binds  = EvBindsVar
ev_binds_var
                             , ic_info :: SkolemInfo
ic_info   = SkolemInfo
skol_info }

           -- Add the implication to the work-list
           ; IORef WorkList -> (WorkList -> WorkList) -> TcM ()
forall a gbl lcl. TcRef a -> (a -> a) -> TcRnIf gbl lcl ()
TcM.updTcRef (TcSEnv -> IORef WorkList
tcs_worklist TcSEnv
tcs_env)
                          (Bag Implication -> WorkList -> WorkList
extendWorkListImplic (Implication -> Bag Implication
forall a. a -> Bag a
unitBag Implication
imp')) }

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

checkConstraintsTcS :: SkolemInfo
                    -> [TcTyVar]        -- Skolems
                    -> [EvVar]          -- Givens
                    -> TcS (result, Cts)
                    -> TcS (result, TcEvBinds)
-- Just like checkConstraintsTcS, but
--   - In the TcS monnad
--   - The thing-inside should not put things in the work-list
--     Instead, it returns the Wanted constraints it needs
--   - I did not bother to put in the fast-path for
--     empty-skols/empty-givens, or for empty-wanteds, because
--     this function is used only for "quantified constraints" in
--     with both tests are pretty much guaranteed to fail
checkConstraintsTcS :: SkolemInfo
-> [TcTyVar]
-> [TcTyVar]
-> TcS (result, Cts)
-> TcS (result, TcEvBinds)
checkConstraintsTcS SkolemInfo
skol_info [TcTyVar]
skol_tvs [TcTyVar]
given (TcS TcSEnv -> TcM (result, Cts)
thing_inside)
  = (TcSEnv -> TcM (result, TcEvBinds)) -> TcS (result, TcEvBinds)
forall a. (TcSEnv -> TcM a) -> TcS a
TcS ((TcSEnv -> TcM (result, TcEvBinds)) -> TcS (result, TcEvBinds))
-> (TcSEnv -> TcM (result, TcEvBinds)) -> TcS (result, TcEvBinds)
forall a b. (a -> b) -> a -> b
$ \ TcSEnv
tcs_env ->
    do { let wl_panic :: IORef WorkList
wl_panic  = String -> SDoc -> IORef WorkList
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"TcSMonad.buildImplication" (SDoc -> IORef WorkList) -> SDoc -> IORef WorkList
forall a b. (a -> b) -> a -> b
$
                         SkolemInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr SkolemInfo
skol_info SDoc -> SDoc -> SDoc
$$ [TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
skol_tvs
                         -- This panic checks that the thing-inside
                         -- does not emit any work-list constraints
             new_tcs_env :: TcSEnv
new_tcs_env = TcSEnv
tcs_env { tcs_worklist :: IORef WorkList
tcs_worklist = IORef WorkList
wl_panic }

       ; (TcLevel
new_tclvl, (result
res, Cts
wanteds)) <- TcM (result, Cts) -> TcM (TcLevel, (result, Cts))
forall a. TcM a -> TcM (TcLevel, a)
TcM.pushTcLevelM (TcM (result, Cts) -> TcM (TcLevel, (result, Cts)))
-> TcM (result, Cts) -> TcM (TcLevel, (result, Cts))
forall a b. (a -> b) -> a -> b
$
                                        TcSEnv -> TcM (result, Cts)
thing_inside TcSEnv
new_tcs_env

       ; EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
       ; Implication
imp <- TcM Implication
TcM.newImplication
       ; let wc :: WantedConstraints
wc = WantedConstraints
emptyWC { wc_simple :: Cts
wc_simple = Cts
wanteds }
             imp' :: Implication
imp' = Implication
imp { ic_tclvl :: TcLevel
ic_tclvl  = TcLevel
new_tclvl
                        , ic_skols :: [TcTyVar]
ic_skols  = [TcTyVar]
skol_tvs
                        , ic_given :: [TcTyVar]
ic_given  = [TcTyVar]
given
                        , ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
wc
                        , ic_binds :: EvBindsVar
ic_binds  = EvBindsVar
ev_binds_var
                        , ic_info :: SkolemInfo
ic_info   = SkolemInfo
skol_info }

           -- Add the implication to the work-list
       ; IORef WorkList -> (WorkList -> WorkList) -> TcM ()
forall a gbl lcl. TcRef a -> (a -> a) -> TcRnIf gbl lcl ()
TcM.updTcRef (TcSEnv -> IORef WorkList
tcs_worklist TcSEnv
tcs_env)
                      (Bag Implication -> WorkList -> WorkList
extendWorkListImplic (Implication -> Bag Implication
forall a. a -> Bag a
unitBag Implication
imp'))

       ; (result, TcEvBinds) -> TcM (result, TcEvBinds)
forall (m :: * -> *) a. Monad m => a -> m a
return (result
res, EvBindsVar -> TcEvBinds
TcEvBinds EvBindsVar
ev_binds_var) }

{-
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 signficant performance difference
if you do so.
-}

-- Getters and setters of TcEnv fields
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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

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

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

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

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

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

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

emitWork :: [Ct] -> TcS ()
emitWork :: [Ct] -> TcS ()
emitWork [Ct]
cts
  = do { String -> SDoc -> TcS ()
traceTcS String
"Emitting fresh work" ([SDoc] -> SDoc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
cts))
       ; (WorkList -> WorkList) -> TcS ()
updWorkListTcS ([Ct] -> WorkList -> WorkList
extendWorkListCts [Ct]
cts) }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

{- *********************************************************************
*                                                                      *
*                Flatten skolems                                       *
*                                                                      *
********************************************************************* -}

newFlattenSkolem :: CtFlavour -> CtLoc
                 -> TyCon -> [TcType]                    -- F xis
                 -> TcS (CtEvidence, Coercion, TcTyVar)  -- [G/WD] x:: F xis ~ fsk
newFlattenSkolem :: CtFlavour
-> CtLoc
-> TyCon
-> [PredType]
-> TcS (CtEvidence, TcCoercion, TcTyVar)
newFlattenSkolem CtFlavour
flav CtLoc
loc TyCon
tc [PredType]
xis
  = do { stuff :: (CtEvidence, TcCoercion, TcTyVar)
stuff@(CtEvidence
ev, TcCoercion
co, TcTyVar
fsk) <- TcS (CtEvidence, TcCoercion, TcTyVar)
new_skolem
       ; let fsk_ty :: PredType
fsk_ty = TcTyVar -> PredType
mkTyVarTy TcTyVar
fsk
       ; TyCon -> [PredType] -> (TcCoercion, PredType, CtFlavour) -> TcS ()
extendFlatCache TyCon
tc [PredType]
xis (TcCoercion
co, PredType
fsk_ty, CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev)
       ; (CtEvidence, TcCoercion, TcTyVar)
-> TcS (CtEvidence, TcCoercion, TcTyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence, TcCoercion, TcTyVar)
stuff }
  where
    fam_ty :: PredType
fam_ty = TyCon -> [PredType] -> PredType
mkTyConApp TyCon
tc [PredType]
xis

    new_skolem :: TcS (CtEvidence, TcCoercion, TcTyVar)
new_skolem
      | CtFlavour
Given <- CtFlavour
flav
      = do { TcTyVar
fsk <- TcM TcTyVar -> TcS TcTyVar
forall a. TcM a -> TcS a
wrapTcS (PredType -> TcM TcTyVar
TcM.newFskTyVar PredType
fam_ty)

           -- Extend the inert_fsks list, for use by unflattenGivens
           ; (InertSet -> InertSet) -> TcS ()
updInertTcS ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \InertSet
is -> InertSet
is { inert_fsks :: [(TcTyVar, PredType)]
inert_fsks = (TcTyVar
fsk, PredType
fam_ty) (TcTyVar, PredType)
-> [(TcTyVar, PredType)] -> [(TcTyVar, PredType)]
forall a. a -> [a] -> [a]
: InertSet -> [(TcTyVar, PredType)]
inert_fsks InertSet
is }

           -- Construct the Refl evidence
           ; let pred :: PredType
pred = PredType -> PredType -> PredType
mkPrimEqPred PredType
fam_ty (TcTyVar -> PredType
mkTyVarTy TcTyVar
fsk)
                 co :: TcCoercion
co   = PredType -> TcCoercion
mkNomReflCo PredType
fam_ty
           ; CtEvidence
ev  <- CtLoc -> (PredType, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (PredType
pred, TcCoercion -> EvTerm
evCoercion TcCoercion
co)
           ; (CtEvidence, TcCoercion, TcTyVar)
-> TcS (CtEvidence, TcCoercion, TcTyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence
ev, TcCoercion
co, TcTyVar
fsk) }

      | Bool
otherwise  -- Generate a [WD] for both Wanted and Derived
                   -- See Note [No Derived CFunEqCans]
      = do { TcTyVar
fmv <- TcM TcTyVar -> TcS TcTyVar
forall a. TcM a -> TcS a
wrapTcS (PredType -> TcM TcTyVar
TcM.newFmvTyVar PredType
fam_ty)
           ; (CtEvidence
ev, TcCoercion
hole_co) <- CtLoc
-> Role -> PredType -> PredType -> TcS (CtEvidence, TcCoercion)
newWantedEq CtLoc
loc Role
Nominal PredType
fam_ty (TcTyVar -> PredType
mkTyVarTy TcTyVar
fmv)
           ; (CtEvidence, TcCoercion, TcTyVar)
-> TcS (CtEvidence, TcCoercion, TcTyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence
ev, TcCoercion
hole_co, TcTyVar
fmv) }

----------------------------
unflattenGivens :: IORef InertSet -> TcM ()
-- Unflatten all the fsks created by flattening types in Given
-- constraints. We must be sure to do this, else we end up with
-- flatten-skolems buried in any residual Wanteds
--
-- NB: this is the /only/ way that a fsk (MetaDetails = FlatSkolTv)
--     is filled in. Nothing else does so.
--
-- It's here (rather than in TcFlatten) because the Right Places
-- to call it are in runTcSWithEvBinds/nestImplicTcS, where it
-- is nicely paired with the creation an empty inert_fsks list.
unflattenGivens :: IORef InertSet -> TcM ()
unflattenGivens IORef InertSet
inert_var
 = do { InertSet
inerts <- IORef InertSet -> TcRnIf TcGblEnv TcLclEnv InertSet
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
inert_var
       ; String -> SDoc -> TcM ()
TcM.traceTc String
"unflattenGivens" ([(TcTyVar, PredType)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (InertSet -> [(TcTyVar, PredType)]
inert_fsks InertSet
inerts))
       ; ((TcTyVar, PredType) -> TcM ()) -> [(TcTyVar, PredType)] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TcTyVar, PredType) -> TcM ()
flatten_one (InertSet -> [(TcTyVar, PredType)]
inert_fsks InertSet
inerts) }
  where
    flatten_one :: (TcTyVar, PredType) -> TcM ()
flatten_one (TcTyVar
fsk, PredType
ty) = TcTyVar -> PredType -> TcM ()
TcM.writeMetaTyVar TcTyVar
fsk PredType
ty

----------------------------
extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
extendFlatCache :: TyCon -> [PredType] -> (TcCoercion, PredType, CtFlavour) -> TcS ()
extendFlatCache TyCon
tc [PredType]
xi_args stuff :: (TcCoercion, PredType, CtFlavour)
stuff@(TcCoercion
_, PredType
ty, CtFlavour
fl)
  | CtFlavour -> Bool
isGivenOrWDeriv CtFlavour
fl  -- Maintain the invariant that inert_flat_cache
                        -- only has [G] and [WD] CFunEqCans
  = do { DynFlags
dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_FlatCache DynFlags
dflags) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
    do { String -> SDoc -> TcS ()
traceTcS String
"extendFlatCache" ([SDoc] -> SDoc
vcat [ TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
<+> [PredType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [PredType]
xi_args
                                          , CtFlavour -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtFlavour
fl, PredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr PredType
ty ])
            -- 'co' can be bottom, in the case of derived items
       ; (InertSet -> InertSet) -> TcS ()
updInertTcS ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ is :: InertSet
is@(IS { inert_flat_cache :: InertSet -> ExactFunEqMap (TcCoercion, PredType, CtFlavour)
inert_flat_cache = ExactFunEqMap (TcCoercion, PredType, CtFlavour)
fc }) ->
            InertSet
is { inert_flat_cache :: ExactFunEqMap (TcCoercion, PredType, CtFlavour)
inert_flat_cache = ExactFunEqMap (TcCoercion, PredType, CtFlavour)
-> TyCon
-> [PredType]
-> (TcCoercion, PredType, CtFlavour)
-> ExactFunEqMap (TcCoercion, PredType, CtFlavour)
forall a.
ExactFunEqMap a -> TyCon -> [PredType] -> a -> ExactFunEqMap a
insertExactFunEq ExactFunEqMap (TcCoercion, PredType, CtFlavour)
fc TyCon
tc [PredType]
xi_args (TcCoercion, PredType, CtFlavour)
stuff } } }

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

----------------------------
unflattenFmv :: TcTyVar -> TcType -> TcS ()
-- Fill a flatten-meta-var, simply by unifying it.
-- This does NOT count as a unification in tcs_unified.
unflattenFmv :: TcTyVar -> PredType -> TcS ()
unflattenFmv TcTyVar
tv PredType
ty
  = ASSERT2( isMetaTyVar tv, ppr tv )
    (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
_ ->
    do { String -> SDoc -> TcM ()
TcM.traceTc String
"unflattenFmv" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
":=" SDoc -> SDoc -> SDoc
<+> PredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr PredType
ty)
       ; TcTyVar -> PredType -> TcM ()
TcM.writeMetaTyVar TcTyVar
tv PredType
ty }

----------------------------
demoteUnfilledFmv :: TcTyVar -> TcS ()
-- If a flatten-meta-var is still un-filled,
-- turn it into an ordinary meta-var
demoteUnfilledFmv :: TcTyVar -> TcS ()
demoteUnfilledFmv TcTyVar
fmv
  = TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ do { Bool
is_filled <- TcTyVar -> TcM Bool
TcM.isFilledMetaTyVar TcTyVar
fmv
                 ; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
is_filled (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
                   do { PredType
tv_ty <- PredType -> TcM PredType
TcM.newFlexiTyVarTy (TcTyVar -> PredType
tyVarKind TcTyVar
fmv)
                      ; TcTyVar -> PredType -> TcM ()
TcM.writeMetaTyVar TcTyVar
fmv PredType
tv_ty } }

-----------------------------
dischargeFunEq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
-- (dischargeFunEq tv co ty)
--     Preconditions
--       - ev :: F tys ~ tv   is a CFunEqCan
--       - tv is a FlatMetaTv of FlatSkolTv
--       - co :: F tys ~ xi
--       - fmv/fsk `notElem` xi
--       - fmv not filled (for Wanteds)
--       - xi is flattened (and obeys Note [Almost function-free] in TcRnTypes)
--
-- Then for [W] or [WD], we actually fill in the fmv:
--      set fmv := xi,
--      set ev  := co
--      kick out any inert things that are now rewritable
--
-- For [D], we instead emit an equality that must ultimately hold
--      [D] xi ~ fmv
--      Does not evaluate 'co' if 'ev' is Derived
--
-- For [G], emit this equality
--     [G] (sym ev; co) :: fsk ~ xi

-- See TcFlatten Note [The flattening story],
-- especially "Ownership of fsk/fmv"
dischargeFunEq :: CtEvidence -> TcTyVar -> TcCoercion -> PredType -> TcS ()
dischargeFunEq (CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
old_evar, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc }) TcTyVar
fsk TcCoercion
co PredType
xi
  = do { CtEvidence
new_ev <- CtLoc -> (PredType, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc ( PredType
new_pred, TcCoercion -> EvTerm
evCoercion TcCoercion
new_co  )
       ; [CtEvidence] -> TcS ()
emitWorkNC [CtEvidence
new_ev] }
  where
    new_pred :: PredType
new_pred = PredType -> PredType -> PredType
mkPrimEqPred (TcTyVar -> PredType
mkTyVarTy TcTyVar
fsk) PredType
xi
    new_co :: TcCoercion
new_co   = TcCoercion -> TcCoercion
mkTcSymCo (TcTyVar -> TcCoercion
mkTcCoVarCo TcTyVar
old_evar) TcCoercion -> TcCoercion -> TcCoercion
`mkTcTransCo` TcCoercion
co

dischargeFunEq ev :: CtEvidence
ev@(CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest }) TcTyVar
fmv TcCoercion
co PredType
xi
  = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
    do { TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest (TcCoercion -> EvTerm
evCoercion TcCoercion
co)
       ; TcTyVar -> PredType -> TcS ()
unflattenFmv TcTyVar
fmv PredType
xi
       ; Int
n_kicked <- TcTyVar -> TcS Int
kickOutAfterUnification TcTyVar
fmv
       ; String -> SDoc -> TcS ()
traceTcS String
"dischargeFmv" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
fmv SDoc -> SDoc -> SDoc
<+> SDoc
equals SDoc -> SDoc -> SDoc
<+> PredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr PredType
xi SDoc -> SDoc -> SDoc
$$ Int -> SDoc
pprKicked Int
n_kicked) }

dischargeFunEq (CtDerived { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc }) TcTyVar
fmv TcCoercion
_co PredType
xi
  = CtLoc -> Role -> PredType -> PredType -> TcS ()
emitNewDerivedEq CtLoc
loc Role
Nominal PredType
xi (TcTyVar -> PredType
mkTyVarTy TcTyVar
fmv)
              -- FunEqs are always at Nominal role

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

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

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

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

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

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

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

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

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

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

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

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

data MaybeNew = Fresh CtEvidence | Cached EvExpr

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

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

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

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

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

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

-- | Good for both equalities and non-equalities
setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm (HoleDest CoercionHole
hole) EvTerm
tm
  | Just TcCoercion
co <- EvTerm -> Maybe TcCoercion
evTermCoercion_maybe EvTerm
tm
  = do { VarSet -> TcS ()
useVars (TcCoercion -> VarSet
coVarsOfCo TcCoercion
co)
       ; TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ CoercionHole -> TcCoercion -> TcM ()
TcM.fillCoercionHole CoercionHole
hole TcCoercion
co }
  | Bool
otherwise
  = do { let co_var :: TcTyVar
co_var = CoercionHole -> TcTyVar
coHoleCoVar CoercionHole
hole
       ; EvBind -> TcS ()
setEvBind (TcTyVar -> EvTerm -> EvBind
mkWantedEvBind TcTyVar
co_var EvTerm
tm)
       ; TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ CoercionHole -> TcCoercion -> TcM ()
TcM.fillCoercionHole CoercionHole
hole (TcTyVar -> TcCoercion
mkTcCoVarCo TcTyVar
co_var) }

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

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

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

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

newEvVar :: TcPredType -> TcS EvVar
newEvVar :: PredType -> TcS TcTyVar
newEvVar PredType
pred = TcM TcTyVar -> TcS TcTyVar
forall a. TcM a -> TcS a
wrapTcS (PredType -> TcM TcTyVar
forall gbl lcl. PredType -> TcRnIf gbl lcl TcTyVar
TcM.newEvVar PredType
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 Constraint
newGivenEvVar :: CtLoc -> (PredType, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (PredType
pred, EvTerm
rhs)
  = do { TcTyVar
new_ev <- PredType -> EvTerm -> TcS TcTyVar
newBoundEvVarId PredType
pred EvTerm
rhs
       ; CtEvidence -> TcS CtEvidence
forall (m :: * -> *) a. Monad m => a -> m a
return (CtGiven :: PredType -> TcTyVar -> CtLoc -> CtEvidence
CtGiven { ctev_pred :: PredType
ctev_pred = PredType
pred, ctev_evar :: TcTyVar
ctev_evar = TcTyVar
new_ev, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc }) }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

matchFam :: TyCon -> [Type] -> TcS (Maybe (CoercionN, TcType))
-- Given (F tys) return (ty, co), where co :: F tys ~N ty
matchFam :: TyCon -> [PredType] -> TcS (Maybe (TcCoercion, PredType))
matchFam TyCon
tycon [PredType]
args = TcM (Maybe (TcCoercion, PredType))
-> TcS (Maybe (TcCoercion, PredType))
forall a. TcM a -> TcS a
wrapTcS (TcM (Maybe (TcCoercion, PredType))
 -> TcS (Maybe (TcCoercion, PredType)))
-> TcM (Maybe (TcCoercion, PredType))
-> TcS (Maybe (TcCoercion, PredType))
forall a b. (a -> b) -> a -> b
$ TyCon -> [PredType] -> TcM (Maybe (TcCoercion, PredType))
matchFamTcM TyCon
tycon [PredType]
args

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

{-
Note [Residual implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The wl_implics in the WorkList are the residual implication
constraints that are generated while solving or canonicalising the
current worklist.  Specifically, when canonicalising
   (forall a. t1 ~ forall a. t2)
from which we get the implication
   (forall a. t1 ~ t2)
See TcSMonad.deferTcSForAllEq
-}