{-# LANGUAGE CPP, DeriveFunctor, TypeFamilies, ScopedTypeVariables, TypeApplications,
             DerivingStrategies, GeneralizedNewtypeDeriving, ScopedTypeVariables, MultiWayIf, ViewPatterns #-}

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

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

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

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

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

    QCInst(..),

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

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

    newTcEvBinds, newNoTcEvBinds,
    newWantedEq, newWantedEq_SI, emitNewWantedEq,
    newWanted, newWanted_SI, newWantedEvVar,
    newWantedNC, newWantedEvVarNC,
    newDerivedNC,
    newBoundEvVarId,
    unifyTyVar, reportUnifications, touchabilityTest, TouchabilityTestResult(..),
    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(..), emptyInert,
    updInertTcS, updInertCans, updInertDicts, updInertIrreds,
    getHasGivenEqs, setInertCans,
    getInertEqs, getInertCans, getInertGivens,
    getInertInsols, getInnermostGivenEqLevel,
    getTcSInerts, setTcSInerts,
    matchableGivens, prohibitedSuperClassSolve, mightEqualLater,
    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 CEqCans
    EqualCtList(..), findTyEqs, foldTyEqs,
    findEq,

    -- Inert solved dictionaries
    addSolvedDict, lookupSolvedDict,

    -- Irreds
    foldIrreds,

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

    -- Inert function equalities
    findFunEq, findFunEqsByTyCon,

    instDFunType,                              -- Instantiation

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

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

    -- References
    newTcRef, readTcRef, writeTcRef, updTcRef,

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

    breakTyEqCycle_maybe, rewriterView
) where

#include "HsVersions.h"

import GHC.Prelude

import GHC.Driver.Env

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

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

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

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

import GHC.Types.Unique.Set
import GHC.Core.TyCon.Env
import GHC.Data.Maybe

import GHC.Core.Map.Type
import GHC.Data.TrieMap

import Control.Monad
import GHC.Utils.Monad
import Data.IORef
import GHC.Exts (oneShot)
import Data.List ( partition, mapAccumL )
import Data.List.NonEmpty ( NonEmpty(..), cons, toList, nonEmpty )
import qualified Data.List.NonEmpty as NE
import Control.Arrow ( first )

#if defined(DEBUG)
import GHC.Data.Graph.Directed
#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 flavours).
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]
* 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 GHC.Builtin.Types.Prim.

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]  -- CEqCan, 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_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_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_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest2
        , wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics2 })
   = WL { wl_eqs :: [Ct]
wl_eqs     = [Ct]
eqs1     forall a. [a] -> [a] -> [a]
++ [Ct]
eqs2
        , wl_rest :: [Ct]
wl_rest    = [Ct]
rest1    forall a. [a] -> [a] -> [a]
++ [Ct]
rest2
        , wl_implics :: Bag Implication
wl_implics = Bag Implication
implics1 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_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
  = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ct]
eqs forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ct]
rest

extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl = WorkList
wl { wl_eqs :: [Ct]
wl_eqs = Ct
ct forall a. a -> [a] -> [a]
: WorkList -> [Ct]
wl_eqs 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 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 (forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> Ct
mkNonCanonical [CtEvidence]
evs) WorkList
wl

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

extendWorkListCt :: Ct -> WorkList -> WorkList
-- Agnostic
extendWorkListCt :: Ct -> WorkList -> WorkList
extendWorkListCt Ct
ct WorkList
wl
 = case Type -> Pred
classifyPredType (Ct -> Type
ctPred Ct
ct) of
     EqPred {}
       -> Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl

     ClassPred Class
cls [Type]
_  -- 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 = 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_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics })
  = forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
rest Bool -> Bool -> Bool
&& forall a. Bag a -> Bool
isEmptyBag Bag Implication
implics

emptyWorkList :: WorkList
emptyWorkList :: WorkList
emptyWorkList = WL { wl_eqs :: [Ct]
wl_eqs  = [], wl_rest :: [Ct]
wl_rest = [], wl_implics :: Bag Implication
wl_implics = 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_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
  | Ct
ct:[Ct]
cts <- [Ct]
eqs  = forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_eqs :: [Ct]
wl_eqs    = [Ct]
cts })
  | Ct
ct:[Ct]
cts <- [Ct]
rest = forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_rest :: [Ct]
wl_rest   = [Ct]
cts })
  | Bool
otherwise      = forall a. Maybe a
Nothing

getWorkList :: TcS WorkList
getWorkList :: TcS WorkList
getWorkList = do { IORef WorkList
wl_var <- TcS (IORef WorkList)
getTcSWorkListRef
                 ; forall a. TcM a -> TcS a
wrapTcS (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 <- forall a. TcRef a -> TcS a
readTcRef IORef WorkList
wl_var
       ; case WorkList -> Maybe (Ct, WorkList)
selectWorkItem WorkList
wl of {
           Maybe (Ct, WorkList)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing ;
           Just (Ct
ct, WorkList
new_wl) ->
    do { -- checkReductionDepth (ctLoc ct) (ctPred ct)
         -- This is done by GHC.Tc.Solver.Interact.chooseInstance
       ; forall a. TcRef a -> a -> TcS ()
writeTcRef IORef WorkList
wl_var WorkList
new_wl
       ; forall (m :: * -> *) a. Monad m => a -> m a
return (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_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 forall a b. (a -> b) -> a -> b
$
     [SDoc] -> SDoc
vcat [ Bool -> SDoc -> SDoc
ppUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs) forall a b. (a -> b) -> a -> b
$
            String -> SDoc
text String
"Eqs =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
ppr [Ct]
eqs)
          , Bool -> SDoc -> SDoc
ppUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
rest) forall a b. (a -> b) -> a -> b
$
            String -> SDoc
text String
"Non-eqs =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
ppr [Ct]
rest)
          , Bool -> SDoc -> SDoc
ppUnless (forall a. Bag a -> Bool
isEmptyBag Bag Implication
implics) forall a b. (a -> b) -> a -> b
$
            SDoc -> SDoc -> SDoc
ifPprDebug (String -> SDoc
text String
"Implics =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
ppr (forall a. Bag a -> [a]
bagToList Bag Implication
implics)))
                       (String -> SDoc
text String
"(Implics omitted)")
          ])


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

type CycleBreakerVarStack = NonEmpty [(TcTyVar, TcType)]
   -- ^ a stack of (CycleBreakerTv, original family applications) lists
   -- first element in the stack corresponds to current implication;
   --   later elements correspond to outer implications
   -- used to undo the cycle-breaking needed to handle
   -- Note [Type equality cycles] in GHC.Tc.Solver.Canonical
   -- Why store the outer implications? For the use in mightEqualLater (only)

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

       , InertSet -> CycleBreakerVarStack
inert_cycle_breakers :: CycleBreakerVarStack

       , InertSet -> FunEqMap (Coercion, Type)
inert_famapp_cache :: FunEqMap (TcCoercion, TcType)
              -- Just a hash-cons cache for use when reducing family applications
              -- only
              --
              -- If    F tys :-> (co, rhs, flav),
              -- then  co :: rhs ~N F tys
              -- all evidence is from instances or Givens; no coercion holes here
              -- (We have no way of "kicking out" from the cache, so putting
              --  wanteds here means we can end up solving a Wanted with itself. Bad)

       , 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_solved_dicts :: InertSet -> DictMap CtEvidence
inert_solved_dicts = DictMap CtEvidence
solved_dicts })
      = [SDoc] -> SDoc
vcat [ forall a. Outputable a => a -> SDoc
ppr InertCans
ics
             , Bool -> SDoc -> SDoc
ppUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CtEvidence]
dicts) forall a b. (a -> b) -> a -> b
$
               String -> SDoc
text String
"Solved dicts =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
ppr [CtEvidence]
dicts) ]
         where
           dicts :: [CtEvidence]
dicts = forall a. Bag a -> [a]
bagToList (forall a. DictMap a -> Bag a
dictsToBag DictMap CtEvidence
solved_dicts)

emptyInertCans :: InertCans
emptyInertCans :: InertCans
emptyInertCans
  = IC { inert_eqs :: InertEqs
inert_eqs          = forall a. DVarEnv a
emptyDVarEnv
       , inert_given_eq_lvl :: TcLevel
inert_given_eq_lvl = TcLevel
topTcLevel
       , inert_given_eqs :: Bool
inert_given_eqs    = Bool
False
       , inert_dicts :: DictMap Ct
inert_dicts        = forall a. DictMap a
emptyDicts
       , inert_safehask :: DictMap Ct
inert_safehask     = forall a. DictMap a
emptyDicts
       , inert_funeqs :: FunEqMap EqualCtList
inert_funeqs       = forall a. DictMap a
emptyFunEqs
       , inert_insts :: [QCInst]
inert_insts        = []
       , inert_irreds :: Bag Ct
inert_irreds       = Bag Ct
emptyCts
       , inert_blocked :: Bag Ct
inert_blocked      = Bag Ct
emptyCts }

emptyInert :: InertSet
emptyInert :: InertSet
emptyInert
  = IS { inert_cans :: InertCans
inert_cans           = InertCans
emptyInertCans
       , inert_cycle_breakers :: CycleBreakerVarStack
inert_cycle_breakers = [] forall a. a -> [a] -> NonEmpty a
:| []
       , inert_famapp_cache :: FunEqMap (Coercion, Type)
inert_famapp_cache   = forall a. DictMap a
emptyFunEqs
       , inert_solved_dicts :: DictMap CtEvidence
inert_solved_dicts   = 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, degenerate 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 GHC.Tc.TyCl.Instance.

 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 instance 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
  - GHC.Tc.Solver.Monad.addSolvedDict adds a new solved dictionary,
    conditional on the kind of instance

  - It is only called when applying an instance decl,
    in GHC.Tc.Solver.Interact.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 CEqCans with a TyVarLHS; index is the LHS tyvar
              -- Domain = skolems and untouchables; a touchable would be unified

       , InertCans -> FunEqMap EqualCtList
inert_funeqs :: FunEqMap EqualCtList
              -- All CEqCans with a TyFamLHS; index is the whole family head type.
              -- LHS is fully rewritten (modulo eqCanRewrite constraints)
              --     wrt inert_eqs
              -- Can include all flavours, [G], [W], [WD], [D]

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

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

       , InertCans -> DictMap 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 "GHC.Tc.Solver"

       , InertCans -> Bag Ct
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 -> Bag Ct
inert_blocked :: Cts
              -- Equality predicates blocked on a coercion hole.
              -- Each Ct is a CIrredCan with cc_reason = HoleBlockerReason
              -- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
              -- wrinkle (2)
              -- These are stored separately from inert_irreds because
              -- they get kicked out for different reasons


       , InertCans -> TcLevel
inert_given_eq_lvl :: TcLevel
              -- The TcLevel of the innermost implication that has a Given
              -- equality of the sort that make a unification variable untouchable
              -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify).
              -- See Note [Tracking Given equalities] below

       , InertCans -> Bool
inert_given_eqs :: Bool
              -- True <=> The inert Givens *at this level* (tcl_tclvl)
              --          could includes at least one equality /other than/ a
              --          let-bound skolem equality.
              -- Reason: report these givens when reporting a failed equality
              -- See Note [Tracking Given equalities]
       }

type InertEqs    = DTyVarEnv EqualCtList

newtype EqualCtList = EqualCtList (NonEmpty Ct)
  deriving newtype EqualCtList -> SDoc
forall a. (a -> SDoc) -> Outputable a
ppr :: EqualCtList -> SDoc
$cppr :: EqualCtList -> SDoc
Outputable
  -- See Note [EqualCtList invariants]

unitEqualCtList :: Ct -> EqualCtList
unitEqualCtList :: Ct -> EqualCtList
unitEqualCtList Ct
ct = NonEmpty Ct -> EqualCtList
EqualCtList (Ct
ct forall a. a -> [a] -> NonEmpty a
:| [])

addToEqualCtList :: Ct -> EqualCtList -> EqualCtList
-- NB: This function maintains the "derived-before-wanted" invariant of EqualCtList,
-- but not the others. See Note [EqualCtList invariants]
addToEqualCtList :: Ct -> EqualCtList -> EqualCtList
addToEqualCtList Ct
ct (EqualCtList NonEmpty Ct
old_eqs)
  | Ct -> Bool
isWantedCt Ct
ct
  , Ct
eq1 :| [Ct]
eqs <- NonEmpty Ct
old_eqs
  = NonEmpty Ct -> EqualCtList
EqualCtList (Ct
eq1 forall a. a -> [a] -> NonEmpty a
:| Ct
ct forall a. a -> [a] -> [a]
: [Ct]
eqs)
  | Bool
otherwise
  = NonEmpty Ct -> EqualCtList
EqualCtList (Ct
ct forall a. a -> NonEmpty a -> NonEmpty a
`cons` NonEmpty Ct
old_eqs)

filterEqualCtList :: (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList
filterEqualCtList :: (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList
filterEqualCtList Ct -> Bool
pred (EqualCtList NonEmpty Ct
cts)
  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NonEmpty Ct -> EqualCtList
EqualCtList (forall a. [a] -> Maybe (NonEmpty a)
nonEmpty forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> NonEmpty a -> [a]
NE.filter Ct -> Bool
pred NonEmpty Ct
cts)

equalCtListToList :: EqualCtList -> [Ct]
equalCtListToList :: EqualCtList -> [Ct]
equalCtListToList (EqualCtList NonEmpty Ct
cts) = forall a. NonEmpty a -> [a]
toList NonEmpty Ct
cts

listToEqualCtList :: [Ct] -> Maybe EqualCtList
-- NB: This does not maintain invariants other than having the EqualCtList be
-- non-empty
listToEqualCtList :: [Ct] -> Maybe EqualCtList
listToEqualCtList [Ct]
cts = NonEmpty Ct -> EqualCtList
EqualCtList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [Ct]
cts

{- Note [Tracking Given equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For reasons described in (UNTOUCHABLE) in GHC.Tc.Utils.Unify
Note [Unification preconditions], we can't unify
   alpha[2] ~ Int
under a level-4 implication if there are any Given equalities
bound by the implications at level 3 of 4.  To that end, the
InertCans tracks

  inert_given_eq_lvl :: TcLevel
     -- The TcLevel of the innermost implication that has a Given
     -- equality of the sort that make a unification variable untouchable
     -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify).

We update inert_given_eq_lvl whenever we add a Given to the
inert set, in updateGivenEqs.

Then a unification variable alpha[n] is untouchable iff
    n < inert_given_eq_lvl
that is, if the unification variable was born outside an
enclosing Given equality.

Exactly which constraints should trigger (UNTOUCHABLE), and hence
should update inert_given_eq_lvl?

* We do /not/ need to worry about let-bound skolems, such ast
     forall[2] a. a ~ [b] => blah
  See Note [Let-bound skolems]

* Consider an implication
      forall[2]. beta[1] => alpha[1] ~ Int
  where beta is a unification variable that has already been unified
  to () in an outer scope.  Then alpha[1] is perfectly touchable and
  we can unify alpha := Int. So when deciding whether the givens contain
  an equality, we should canonicalise first, rather than just looking at
  the /original/ givens (#8644).

 * However, we must take account of *potential* equalities. Consider the
   same example again, but this time we have /not/ yet unified beta:
      forall[2] beta[1] => ...blah...

   Because beta might turn into an equality, updateGivenEqs conservatively
   treats it as a potential equality, and updates inert_give_eq_lvl

 * What about something like forall[2] a b. a ~ F b => [W] alpha[1] ~ X y z?

   That Given cannot affect the Wanted, because the Given is entirely
   *local*: it mentions only skolems bound in the very same
   implication. Such equalities need not make alpha untouchable. (Test
   case typecheck/should_compile/LocalGivenEqs has a real-life
   motivating example, with some detailed commentary.)
   Hence the 'mentionsOuterVar' test in updateGivenEqs.

   However, solely to support better error messages
   (see Note [HasGivenEqs] in GHC.Tc.Types.Constraint) we also track
   these "local" equalities in the boolean inert_given_eqs field.
   This field is used only to set the ic_given_eqs field to LocalGivenEqs;
   see the function getHasGivenEqs.

   Here is a simpler case that triggers this behaviour:

     data T where
       MkT :: F a ~ G b => a -> b -> T

     f (MkT _ _) = True

   Because of this behaviour around local equality givens, we can infer the
   type of f. This is typecheck/should_compile/LocalGivenEqs2.

 * We need not look at the equality relation involved (nominal vs
   representational), because representational equalities can still
   imply nominal ones. For example, if (G a ~R G b) and G's argument's
   role is nominal, then we can deduce a ~N b.

Note [Let-bound skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
If   * the inert set contains a canonical Given CEqCan (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.

For an example, see #9211.

See also GHC.Tc.Utils.Unify 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 skolem really needs to be bound "in the
very same implication" as the equuality constraint.
Consider this (c.f. #15009):

  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 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, unify alpha := a.  Now we are stuck with an unsolved alpha~Int!
So we must treat alpha as untouchable under the forall[2] implication.

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-CEqCan constraints are fully rewritten with respect
    to the CEqCan equalities (modulo eqCanRewrite of course;
    eg a wanted cannot rewrite a given)

  * CEqCan equalities: see Note [inert_eqs: the inert equalities]
    Also see documentation in Constraint.Ct for a list of invariants

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], followed by any number of [W]

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

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
  (See Note [Why R2?].)

Lemma (L0). 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 (lhs -f-> t), where
  lhs is a type variable or an exactly-saturated type family application
    (that is, lhs is a CanEqLHS)
  t is a type
  f is a flavour
such that
  (WF1) if (lhs1 -f1-> t1) in S
           (lhs2 -f2-> t2) in S
        then (f1 >= f2) implies that lhs1 does not appear within lhs2
  (WF2) if (lhs -f-> t) is in S, then t /= lhs

Definition [Applying a generalised substitution]
If S is a generalised substitution
   S(f,t0) = t,  if (t0 -fs-> t) in S, and fs >= f
           = apply S to components of t0, otherwise
See also Note [Flavours with roles].

Theorem: S(f,t0) is well defined as a function.
Proof: Suppose (lhs -f1-> t1) and (lhs -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: terminating generalised substitution
A generalised substitution S is *terminating* 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 CEqCans in inert_eqs should be a terminating generalised substitution
-----------------------------------------------------------------------------

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

Note [Why R2?]
~~~~~~~~~~~~~~
R2 states that, if we have f1 >= f and f2 >= f, then either f1 >= f2 or f2 >=
f1. If we do not have R2, we will easily fall into a loop.

To see why, imagine we have f1 >= f, f2 >= f, and that's it. Then, let our
inert set S = {a -f1-> b, b -f2-> a}. Computing S(f,a) does not terminate. And
yet, we have a hard time noticing an occurs-check problem when building S, as
the two equalities cannot rewrite one another.

R2 actually restricts our ability to accept user-written programs. See Note
[Deriveds do rewrite Deriveds] in GHC.Tc.Types.Constraint for an example.

Note [Rewritable]
~~~~~~~~~~~~~~~~~
This Note defines what it means for a type variable or type family application
(that is, a CanEqLHS) to be rewritable in a type. This definition is used
by the anyRewritableXXX family of functions and is meant to model the actual
behaviour in GHC.Tc.Solver.Rewrite.

Ignoring roles (for now): A CanEqLHS lhs is *rewritable* in a type t if the
lhs tree appears as a subtree within t without traversing any of the following
components of t:
  * coercions (whether they appear in casts CastTy or as arguments CoercionTy)
  * kinds of variable occurrences
The check for rewritability *does* look in kinds of the bound variable of a
ForAllTy.

Goal: If lhs is not rewritable in t, then t is a fixpoint of the generalised
substitution containing only {lhs -f*-> t'}, where f* is a flavour such that f* >= f
for all f.

The reason for this definition is that the rewriter does not rewrite in coercions
or variables' kinds. In turn, the rewriter does not need to rewrite there because
those places are never used for controlling the behaviour of the solver: these
places are not used in matching instances or in decomposing equalities.

There is one exception to the claim that non-rewritable parts of the tree do
not affect the solver: we sometimes do an occurs-check to decide e.g. how to
orient an equality. (See the comments on
GHC.Tc.Solver.Canonical.canEqTyVarFunEq.) Accordingly, the presence of a
variable in a kind or coercion just might influence the solver. Here is an
example:

  type family Const x y where
    Const x y = x

  AxConst :: forall x y. Const x y ~# x

  alpha :: Const Type Nat
  [W] alpha ~ Int |> (sym (AxConst Type alpha) ;;
                      AxConst Type alpha ;;
                      sym (AxConst Type Nat))

The cast is clearly ludicrous (it ties together a cast and its symmetric version),
but we can't quite rule it out. (See (EQ1) from
Note [Respecting definitional equality] in GHC.Core.TyCo.Rep to see why we need
the Const Type Nat bit.) And yet this cast will (quite rightly) prevent alpha
from unifying with the RHS. I (Richard E) don't have an example of where this
problem can arise from a Haskell program, but we don't have an air-tight argument
for why the definition of *rewritable* given here is correct.

Taking roles into account: we must consider a rewrite at a given role. That is,
a rewrite arises from some equality, and that equality has a role associated
with it. As we traverse a type, we track what role we are allowed to rewrite with.

For example, suppose we have an inert [G] b ~R# Int. Then b is rewritable in
Maybe b but not in F b, where F is a type function. This role-aware logic is
present in both the anyRewritableXXX functions and in the rewriter.
See also Note [anyRewritableTyVar must be role-aware] in GHC.Tc.Utils.TcType.

Note [Extending the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main Theorem [Stability under extension]
   Suppose we have a "work item"
       lhs -fw-> t
   and a terminating generalised substitution S,
   THEN the extended substitution T = S+(lhs -fw-> t)
        is a terminating generalised substitution
   PROVIDED
      (T1) S(fw,lhs) = lhs   -- 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) lhs not in t      -- No occurs check in the work item
          -- If lhs is a type family application, we require only that
          -- lhs is not *rewritable* in t. See Note [Rewritable] and
          -- Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.

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

              -- From here, we can assume fw >= fs
           OR (K4) lhs1 is a tyvar AND fs >= fw

           OR { (K1) lhs is not rewritable in lhs1. See Note [Rewritable].
                     Reason: if fw >= fs, WF1 says we can't have both
                             lhs0 -fw-> t  and  F lhs0 -fs-> s

                AND (K2): guarantees termination of the new substitution
                    {  (K2a) not (fs >= fs)
                    OR (K2b) lhs not in s }

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


Conditions (T1-T3) are established by the canonicaliser
Conditions (K1-K3) are established by GHC.Tc.Solver.Monad.kickOutRewritable

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

* T3 is guaranteed by an occurs-check on the work item.
  This is done during canonicalisation, in checkTypeEq; invariant
  (TyEq:OC) of CEqCan. See also Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.

* (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. See also (K2a) below.

* 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 (Lemma (L0)),
         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
              (lhs -fs-> t) in S, s.t.  (fs >= fw).
  Proof. Suppose the contrary (fs >= fw).  Then because of (T1),
  S(fw,lhs)=lhs.  But since fs>=fw, S(fw,lhs) = t, hence t=lhs.  But now we
  have (lhs -fs-> lhs) 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) and (K4) are about termination.  Intuitively, any infinite chain S^0(f,t),
  S^1(f,t), S^2(f,t).... must pass through the new work item infinitely
  often, since the substitution without the work item is terminating; 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)
    (this is Lemma (L0)), and hence this triple never plays a role in application S(f,t).
    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 lhs not in s, we have no further opportunity to apply the
    work item

  - (K4): See Note [K4]

* Lemma (L3). Suppose we have f* such that, for all f, f* >= f. Then
  if we are adding lhs -fw-> t (where T1, T2, and T3 hold), we will keep a -f*-> s.
  Proof. K4 holds; thus, we keep.

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 [K4]
~~~~~~~~~
K4 is a "keep" condition of Note [Extending the inert equalities].
Here is the scenario:

* We are considering adding (lhs -fw-> t) to the inert set S.
* S already has (lhs1 -fs-> s).
* We know S(fw, lhs) = lhs, S(fw, t) = t, and lhs is not rewritable in t.
  See Note [Rewritable]. These are (T1), (T2), and (T3).
* We further know fw >= fs. (If not, then we short-circuit via (K0).)

K4 says that we may keep lhs1 -fs-> s in S if:
  lhs1 is a tyvar AND fs >= fw

Why K4 guarantees termination:
  * If fs >= fw, we know a is not rewritable in t, because of (T2).
  * We further know lhs /= a, because of (T1).
  * Accordingly, a use of the new inert item lhs -fw-> t cannot create the conditions
    for a use of a -fs-> s (precisely because t does not mention a), and hence,
    the extended substitution (with lhs -fw-> t in it) is a terminating
    generalised substitution.

Recall that the termination generalised substitution includes only mappings that
pass an occurs check. This is (T3). At one point, we worried that the
argument here would fail if s mentioned a, but (T3) rules out this possibility.
Put another way: the terminating generalised substitution considers only the inert_eqs,
not other parts of the inert set (such as the irreds).

Can we liberalise K4? No.

Why we cannot drop the (fs >= fw) condition:
  * Suppose not (fs >= fw). It might be the case that t mentions a, and this
    can cause a loop. Example:

      Work:  [G] b ~ a
      Inert: [D] a ~ b

    (where G >= G, G >= D, and D >= D)
    If we don't kick out the inert, then we get a loop on e.g. [D] a ~ Int.

  * Note that the above example is different if the inert is a Given G, because
    (T1) won't hold.

Why we cannot drop the tyvar condition:
  * Presume fs >= fw. Thus, F tys is not rewritable in t, because of (T2).
  * Can the use of lhs -fw-> t create the conditions for a use of F tys -fs-> s?
    Yes! This can happen if t appears within tys.

    Here is an example:

      Work:  [G] a ~ Int
      Inert: [G] F Int ~ F a

    Now, if we have [W] F a ~ Bool, we will rewrite ad infinitum on the left-hand
    side. The key reason why K2b works in the tyvar case is that tyvars are atomic:
    if the right-hand side of an equality does not mention a variable a, then it
    cannot allow an equality with an LHS of a to fire. This is not the case for
    type family applications.

Bottom line: K4 can keep only inerts with tyvars on the left. Put differently,
K4 will never prevent an inert with a type family on the left from being kicked
out.

Consequence: We never kick out a Given/Nominal equality with a tyvar on the left.
This is Lemma (L3) of Note [Extending the inert equalities]. It is good because
it means we can effectively model the mutable filling of metavariables with
Given/Nominal equalities. That is: it should be the case that we could rewrite
our solver never to fill in a metavariable; instead, it would "solve" a wanted
like alpha ~ Int by turning it into a Given, allowing it to be used in rewriting.
We would want the solver to behave the same whether it uses metavariables or
Givens. And (L3) says that no Given/Nominals over tyvars are ever kicked out,
just like we never unfill a metavariable. Nice.

Getting this wrong (that is, allowing K4 to apply to situations with the type
family on the left) led to #19042. (At that point, K4 was known as K2b.)

Originally, this condition was part of K2, but #17672 suggests it should be
a top-level K condition.

Note [K3: completeness of solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(K3) is not necessary for the extended substitution
to be terminating.  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 terminating; 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
lhs of a work item is "exposed", where exposed means being at the
head of the top-level application chain (lhs t1 .. tn).  See
is_can_eq_lhs_head. 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 EqualCtList
inert_funeqs = FunEqMap EqualCtList
funeqs
          , inert_dicts :: InertCans -> DictMap Ct
inert_dicts = DictMap Ct
dicts
          , inert_safehask :: InertCans -> DictMap Ct
inert_safehask = DictMap Ct
safehask
          , inert_irreds :: InertCans -> Bag Ct
inert_irreds = Bag Ct
irreds
          , inert_blocked :: InertCans -> Bag Ct
inert_blocked = Bag Ct
blocked
          , inert_given_eq_lvl :: InertCans -> TcLevel
inert_given_eq_lvl = TcLevel
ge_lvl
          , inert_given_eqs :: InertCans -> Bool
inert_given_eqs = Bool
given_eqs
          , inert_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
insts })

    = SDoc -> SDoc
braces forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
      [ Bool -> SDoc -> SDoc
ppUnless (forall a. DVarEnv a -> Bool
isEmptyDVarEnv InertEqs
eqs) forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Equalities:"
          SDoc -> SDoc -> SDoc
<+> Bag Ct -> SDoc
pprCts (forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv EqualCtList -> Bag Ct -> Bag Ct
folder Bag Ct
emptyCts InertEqs
eqs)
      , Bool -> SDoc -> SDoc
ppUnless (forall a. TcAppMap a -> Bool
isEmptyTcAppMap FunEqMap EqualCtList
funeqs) forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Type-function equalities =" SDoc -> SDoc -> SDoc
<+> Bag Ct -> SDoc
pprCts (forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs EqualCtList -> Bag Ct -> Bag Ct
folder FunEqMap EqualCtList
funeqs Bag Ct
emptyCts)
      , Bool -> SDoc -> SDoc
ppUnless (forall a. TcAppMap a -> Bool
isEmptyTcAppMap DictMap Ct
dicts) forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Dictionaries =" SDoc -> SDoc -> SDoc
<+> Bag Ct -> SDoc
pprCts (forall a. DictMap a -> Bag a
dictsToBag DictMap Ct
dicts)
      , Bool -> SDoc -> SDoc
ppUnless (forall a. TcAppMap a -> Bool
isEmptyTcAppMap DictMap Ct
safehask) forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Safe Haskell unsafe overlap =" SDoc -> SDoc -> SDoc
<+> Bag Ct -> SDoc
pprCts (forall a. DictMap a -> Bag a
dictsToBag DictMap Ct
safehask)
      , Bool -> SDoc -> SDoc
ppUnless (Bag Ct -> Bool
isEmptyCts Bag Ct
irreds) forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Irreds =" SDoc -> SDoc -> SDoc
<+> Bag Ct -> SDoc
pprCts Bag Ct
irreds
      , Bool -> SDoc -> SDoc
ppUnless (Bag Ct -> Bool
isEmptyCts Bag Ct
blocked) forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Blocked =" SDoc -> SDoc -> SDoc
<+> Bag Ct -> SDoc
pprCts Bag Ct
blocked
      , Bool -> SDoc -> SDoc
ppUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QCInst]
insts) forall a b. (a -> b) -> a -> b
$
        String -> SDoc
text String
"Given instances =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
ppr [QCInst]
insts)
      , String -> SDoc
text String
"Innermost given equalities =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr TcLevel
ge_lvl
      , String -> SDoc
text String
"Given eqs at this level =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Bool
given_eqs
      ]
    where
      folder :: EqualCtList -> Bag Ct -> Bag Ct
folder (EqualCtList NonEmpty Ct
eqs) Bag Ct
rest = forall a. NonEmpty a -> Bag a
nonEmptyToBag NonEmpty Ct
eqs Bag Ct -> Bag Ct -> Bag Ct
`andCts` Bag Ct
rest

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

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

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

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

    The first Wanted gets rewritten to

           [W] Foo ee ~ Maybe e

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

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

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

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

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

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

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

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

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

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

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

Additional notes:

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

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

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

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

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

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

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

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

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

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

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

* Others: nothing is gained by splitting.

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

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

  work item: [WD] a ~ beta

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

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

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

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

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

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

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

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

We decompose the cast, yielding

  [D] a ~ beta

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

See #11379 for a case of this.

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

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

Reasons:

* It's less work: fewer pairs to compare

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

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

maybeEmitShadow :: InertCans -> Ct -> TcS Ct
-- See Note [The improvement story and derived shadows]
maybeEmitShadow :: InertCans -> Ct -> TcS Ct
maybeEmitShadow InertCans
ics Ct
ct
  | let ev :: CtEvidence
ev = Ct -> CtEvidence
ctEvidence Ct
ct
  , CtWanted { ctev_pred :: CtEvidence -> Type
ctev_pred = Type
pred, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc
             , ctev_nosh :: CtEvidence -> ShadowInfo
ctev_nosh = ShadowInfo
WDeriv } <- CtEvidence
ev
  , InertEqs -> FunEqMap EqualCtList -> Ct -> Bool
shouldSplitWD (InertCans -> InertEqs
inert_eqs InertCans
ics) (InertCans -> FunEqMap EqualCtList
inert_funeqs InertCans
ics) Ct
ct
  = do { String -> SDoc -> TcS ()
traceTcS String
"Emit derived shadow" (forall a. Outputable a => a -> SDoc
ppr Ct
ct)
       ; let derived_ev :: CtEvidence
derived_ev = CtDerived { ctev_pred :: Type
ctev_pred = Type
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
       ; forall (m :: * -> *) a. Monad m => a -> m a
return Ct
ct' }

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

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

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

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

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

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

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

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

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

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

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


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

addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
addTyEq InertEqs
old_eqs TcTyVar
tv Ct
ct
  = forall a. (a -> a -> a) -> DVarEnv a -> TcTyVar -> a -> DVarEnv a
extendDVarEnv_C EqualCtList -> EqualCtList -> EqualCtList
add_eq InertEqs
old_eqs TcTyVar
tv (Ct -> EqualCtList
unitEqualCtList Ct
ct)
  where
    add_eq :: EqualCtList -> EqualCtList -> EqualCtList
add_eq EqualCtList
old_eqs EqualCtList
_ = Ct -> EqualCtList -> EqualCtList
addToEqualCtList Ct
ct EqualCtList
old_eqs

addCanFunEq :: FunEqMap EqualCtList -> TyCon -> [TcType] -> Ct
            -> FunEqMap EqualCtList
addCanFunEq :: FunEqMap EqualCtList
-> TyCon -> [Type] -> Ct -> FunEqMap EqualCtList
addCanFunEq FunEqMap EqualCtList
old_eqs TyCon
fun_tc [Type]
fun_args Ct
ct
  = forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
alterTcApp FunEqMap EqualCtList
old_eqs TyCon
fun_tc [Type]
fun_args Maybe EqualCtList -> Maybe EqualCtList
upd
  where
    upd :: Maybe EqualCtList -> Maybe EqualCtList
upd (Just EqualCtList
old_equal_ct_list) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Ct -> EqualCtList -> EqualCtList
addToEqualCtList Ct
ct EqualCtList
old_equal_ct_list
    upd Maybe EqualCtList
Nothing                  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Ct -> EqualCtList
unitEqualCtList Ct
ct

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

findTyEqs :: InertCans -> TyVar -> [Ct]
findTyEqs :: InertCans -> TcTyVar -> [Ct]
findTyEqs InertCans
icans TcTyVar
tv = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] forall a. a -> a
id (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap @Maybe EqualCtList -> [Ct]
equalCtListToList forall a b. (a -> b) -> a -> b
$
                                  forall a. DVarEnv a -> TcTyVar -> Maybe a
lookupDVarEnv (InertCans -> InertEqs
inert_eqs InertCans
icans) TcTyVar
tv)

delEq :: InertCans -> CanEqLHS -> TcType -> InertCans
delEq :: InertCans -> CanEqLHS -> Type -> InertCans
delEq InertCans
ic CanEqLHS
lhs Type
rhs = case CanEqLHS
lhs of
    TyVarLHS TcTyVar
tv
      -> InertCans
ic { inert_eqs :: InertEqs
inert_eqs = forall a. (Maybe a -> Maybe a) -> DVarEnv a -> TcTyVar -> DVarEnv a
alterDVarEnv Maybe EqualCtList -> Maybe EqualCtList
upd (InertCans -> InertEqs
inert_eqs InertCans
ic) TcTyVar
tv }
    TyFamLHS TyCon
tf [Type]
args
      -> InertCans
ic { inert_funeqs :: FunEqMap EqualCtList
inert_funeqs = forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
alterTcApp (InertCans -> FunEqMap EqualCtList
inert_funeqs InertCans
ic) TyCon
tf [Type]
args Maybe EqualCtList -> Maybe EqualCtList
upd }
  where
    isThisOne :: Ct -> Bool
    isThisOne :: Ct -> Bool
isThisOne (CEqCan { cc_rhs :: Ct -> Type
cc_rhs = Type
t1 }) = Type -> Type -> Bool
tcEqTypeNoKindCheck Type
rhs Type
t1
    isThisOne Ct
other = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"delEq" (forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr InertCans
ic SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr Ct
other)

    upd :: Maybe EqualCtList -> Maybe EqualCtList
    upd :: Maybe EqualCtList -> Maybe EqualCtList
upd (Just EqualCtList
eq_ct_list) = (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList
filterEqualCtList (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> Bool
isThisOne) EqualCtList
eq_ct_list
    upd Maybe EqualCtList
Nothing           = forall a. Maybe a
Nothing

findEq :: InertCans -> CanEqLHS -> [Ct]
findEq :: InertCans -> CanEqLHS -> [Ct]
findEq InertCans
icans (TyVarLHS TcTyVar
tv) = InertCans -> TcTyVar -> [Ct]
findTyEqs InertCans
icans TcTyVar
tv
findEq InertCans
icans (TyFamLHS TyCon
fun_tc [Type]
fun_args)
  = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] forall a. a -> a
id (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap @Maybe EqualCtList -> [Ct]
equalCtListToList forall a b. (a -> b) -> a -> b
$
                 forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq (InertCans -> FunEqMap EqualCtList
inert_funeqs InertCans
icans) TyCon
fun_tc [Type]
fun_args)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

add_item :: TcLevel -> InertCans -> Ct -> InertCans
add_item :: TcLevel -> InertCans -> Ct -> InertCans
add_item TcLevel
tc_lvl
         ics :: InertCans
ics@(IC { inert_funeqs :: InertCans -> FunEqMap EqualCtList
inert_funeqs = FunEqMap EqualCtList
funeqs, inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs })
         item :: Ct
item@(CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs })
  = TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tc_lvl Ct
item forall a b. (a -> b) -> a -> b
$
    case CanEqLHS
lhs of
       TyFamLHS TyCon
tc [Type]
tys -> InertCans
ics { inert_funeqs :: FunEqMap EqualCtList
inert_funeqs = FunEqMap EqualCtList
-> TyCon -> [Type] -> Ct -> FunEqMap EqualCtList
addCanFunEq FunEqMap EqualCtList
funeqs TyCon
tc [Type]
tys Ct
item }
       TyVarLHS TcTyVar
tv     -> InertCans
ics { inert_eqs :: InertEqs
inert_eqs    = InertEqs -> TcTyVar -> Ct -> InertEqs
addTyEq InertEqs
eqs TcTyVar
tv Ct
item }

add_item TcLevel
tc_lvl ics :: InertCans
ics@(IC { inert_blocked :: InertCans -> Bag Ct
inert_blocked = Bag Ct
blocked })
         item :: Ct
item@(CIrredCan { cc_reason :: Ct -> CtIrredReason
cc_reason = HoleBlockerReason {}})
  = TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tc_lvl Ct
item forall a b. (a -> b) -> a -> b
$  -- this item is always an equality
    InertCans
ics { inert_blocked :: Bag Ct
inert_blocked = Bag Ct
blocked forall a. Bag a -> a -> Bag a
`snocBag` Ct
item }

add_item TcLevel
tc_lvl ics :: InertCans
ics@(IC { inert_irreds :: InertCans -> Bag Ct
inert_irreds = Bag Ct
irreds }) item :: Ct
item@(CIrredCan {})
  = TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tc_lvl Ct
item forall a b. (a -> b) -> a -> b
$   -- An Irred might turn out to be an
                                 -- equality, so we play safe
    InertCans
ics { inert_irreds :: Bag Ct
inert_irreds = Bag Ct
irreds forall a. Bag a -> a -> Bag a
`Bag.snocBag` Ct
item }

add_item TcLevel
_ InertCans
ics item :: Ct
item@(CDictCan { cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type]
tys })
  = InertCans
ics { inert_dicts :: DictMap Ct
inert_dicts = DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct
addDictCt (InertCans -> DictMap Ct
inert_dicts InertCans
ics) Class
cls [Type]
tys Ct
item }

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

updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
-- Set the inert_given_eq_level to the current level (tclvl)
-- if the constraint is a given equality that should prevent
-- filling in an outer unification variable.
-- See See Note [Tracking Given equalities]
updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tclvl Ct
ct inerts :: InertCans
inerts@(IC { inert_given_eq_lvl :: InertCans -> TcLevel
inert_given_eq_lvl = TcLevel
ge_lvl })
  | Bool -> Bool
not (Ct -> Bool
isGivenCt Ct
ct) = InertCans
inerts
  | Ct -> Bool
not_equality Ct
ct    = InertCans
inerts -- See Note [Let-bound skolems]
  | Bool
otherwise          = InertCans
inerts { inert_given_eq_lvl :: TcLevel
inert_given_eq_lvl = TcLevel
ge_lvl'
                                , inert_given_eqs :: Bool
inert_given_eqs    = Bool
True }
  where
    ge_lvl' :: TcLevel
ge_lvl' | TcLevel -> CtEvidence -> Bool
mentionsOuterVar TcLevel
tclvl (Ct -> CtEvidence
ctEvidence Ct
ct)
              -- Includes things like (c a), which *might* be an equality
            = TcLevel
tclvl
            | Bool
otherwise
            = TcLevel
ge_lvl

    not_equality :: Ct -> Bool
    -- True <=> definitely not an equality of any kind
    --          except for a let-bound skolem, which doesn't count
    --          See Note [Let-bound skolems]
    -- NB: no need to spot the boxed CDictCan (a ~ b) because its
    --     superclass (a ~# b) will be a CEqCan
    not_equality :: Ct -> Bool
not_equality (CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = TyVarLHS TcTyVar
tv }) = Bool -> Bool
not (TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl TcTyVar
tv)
    not_equality (CDictCan {})                     = Bool
True
    not_equality Ct
_                                 = Bool
False

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

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

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

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

       ; 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
                    -> CanEqLHS       -- The new equality is lhs ~ ty
                    -> InertCans
                    -> (WorkList, InertCans)
-- See Note [kickOutRewritable]
kick_out_rewritable :: CtFlavourRole -> CanEqLHS -> InertCans -> (WorkList, InertCans)
kick_out_rewritable CtFlavourRole
new_fr CanEqLHS
new_lhs
                    ics :: InertCans
ics@(IC { inert_eqs :: InertCans -> InertEqs
inert_eqs      = InertEqs
tv_eqs
                            , inert_dicts :: InertCans -> DictMap Ct
inert_dicts    = DictMap Ct
dictmap
                            , inert_funeqs :: InertCans -> FunEqMap EqualCtList
inert_funeqs   = FunEqMap EqualCtList
funeqmap
                            , inert_irreds :: InertCans -> Bag Ct
inert_irreds   = Bag Ct
irreds
                            , inert_insts :: InertCans -> [QCInst]
inert_insts    = [QCInst]
old_insts })
  | 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_safehask stays unchanged; is that right?
    inert_cans_in :: InertCans
inert_cans_in = InertCans
ics { inert_eqs :: InertEqs
inert_eqs      = InertEqs
tv_eqs_in
                        , inert_dicts :: DictMap Ct
inert_dicts    = DictMap Ct
dicts_in
                        , inert_funeqs :: FunEqMap EqualCtList
inert_funeqs   = FunEqMap EqualCtList
feqs_in
                        , inert_irreds :: Bag Ct
inert_irreds   = Bag Ct
irs_in
                        , inert_insts :: [QCInst]
inert_insts    = [QCInst]
insts_in }

    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_lhs
    -- is substituted; ditto the dictionaries, which may include (a~b)
    -- or (a~~b) constraints.
    kicked_out :: WorkList
kicked_out = 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 forall a. [a] -> [a] -> [a]
++ [Ct]
feqs_out })
                          ((Bag Ct
dicts_out Bag Ct -> Bag Ct -> Bag Ct
`andCts` Bag Ct
irs_out)
                            Bag Ct -> [Ct] -> Bag Ct
`extendCtsList` [Ct]
insts_out)

    ([Ct]
tv_eqs_out, InertEqs
tv_eqs_in) = forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv (forall container.
(container -> CanEqLHS -> EqualCtList -> container)
-> EqualCtList -> ([Ct], container) -> ([Ct], container)
kick_out_eqs InertEqs -> CanEqLHS -> EqualCtList -> InertEqs
extend_tv_eqs)
                                          ([], forall a. DVarEnv a
emptyDVarEnv) InertEqs
tv_eqs
    ([Ct]
feqs_out,   FunEqMap EqualCtList
feqs_in)   = forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs  (forall container.
(container -> CanEqLHS -> EqualCtList -> container)
-> EqualCtList -> ([Ct], container) -> ([Ct], container)
kick_out_eqs FunEqMap EqualCtList
-> CanEqLHS -> EqualCtList -> FunEqMap EqualCtList
extend_fun_eqs)
                                          FunEqMap EqualCtList
funeqmap ([], forall a. DictMap a
emptyFunEqs)
    (Bag Ct
dicts_out,  DictMap Ct
dicts_in)  = (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
partitionDicts   Ct -> Bool
kick_out_ct DictMap Ct
dictmap
    (Bag Ct
irs_out,    Bag Ct
irs_in)    = forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag     Ct -> Bool
kick_out_ct Bag Ct
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 GHC.Tc.Solver.Canonical
    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
       = 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 -> Type -> Bool
fr_can_rewrite_ty EqRel
NomEq (CtEvidence -> Type
ctEvPred (QCInst -> CtEvidence
qci_ev QCInst
qci))
      = forall a b. a -> Either a b
Left (CtEvidence -> Ct
mkNonCanonical CtEvidence
ev)
      | Bool
otherwise
      = forall a b. b -> Either a b
Right QCInst
qci

    (CtFlavour
_, EqRel
new_role) = CtFlavourRole
new_fr

    fr_tv_can_rewrite_ty :: TyVar -> EqRel -> Type -> Bool
    fr_tv_can_rewrite_ty :: TcTyVar -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty TcTyVar
new_tv EqRel
role Type
ty
      = Bool -> EqRel -> (EqRel -> TcTyVar -> Bool) -> Type -> Bool
anyRewritableTyVar Bool
True EqRel
role EqRel -> TcTyVar -> Bool
can_rewrite Type
ty
                  -- True: ignore casts and coercions
      where
        can_rewrite :: EqRel -> TyVar -> Bool
        can_rewrite :: EqRel -> TcTyVar -> Bool
can_rewrite EqRel
old_role TcTyVar
tv = EqRel
new_role EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
old_role Bool -> Bool -> Bool
&& TcTyVar
tv forall a. Eq a => a -> a -> Bool
== TcTyVar
new_tv

    fr_tf_can_rewrite_ty :: TyCon -> [TcType] -> EqRel -> Type -> Bool
    fr_tf_can_rewrite_ty :: TyCon -> [Type] -> EqRel -> Type -> Bool
fr_tf_can_rewrite_ty TyCon
new_tf [Type]
new_tf_args EqRel
role Type
ty
      = EqRel -> (EqRel -> TyCon -> [Type] -> Bool) -> Type -> Bool
anyRewritableTyFamApp EqRel
role EqRel -> TyCon -> [Type] -> Bool
can_rewrite Type
ty
      where
        can_rewrite :: EqRel -> TyCon -> [TcType] -> Bool
        can_rewrite :: EqRel -> TyCon -> [Type] -> Bool
can_rewrite EqRel
old_role TyCon
old_tf [Type]
old_tf_args
          = EqRel
new_role EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
old_role Bool -> Bool -> Bool
&&
            TyCon -> [Type] -> TyCon -> [Type] -> Bool
tcEqTyConApps TyCon
new_tf [Type]
new_tf_args TyCon
old_tf [Type]
old_tf_args
              -- it's possible for old_tf_args to have too many. This is fine;
              -- we'll only check what we need to.

    {-# INLINE fr_can_rewrite_ty #-}   -- perform the check here only once
    fr_can_rewrite_ty :: EqRel -> Type -> Bool
    fr_can_rewrite_ty :: EqRel -> Type -> Bool
fr_can_rewrite_ty = case CanEqLHS
new_lhs of
      TyVarLHS TcTyVar
new_tv             -> TcTyVar -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty TcTyVar
new_tv
      TyFamLHS TyCon
new_tf [Type]
new_tf_args -> TyCon -> [Type] -> EqRel -> Type -> Bool
fr_tf_can_rewrite_ty TyCon
new_tf [Type]
new_tf_args

    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?

    {-# INLINE kick_out_ct #-}   -- perform case on new_lhs here only once
    kick_out_ct :: Ct -> Bool
    -- Kick it out if the new CEqCan can rewrite the inert one
    -- See Note [kickOutRewritable]
    kick_out_ct :: Ct -> Bool
kick_out_ct = case CanEqLHS
new_lhs of
      TyVarLHS TcTyVar
new_tv -> \Ct
ct -> let fs :: CtFlavourRole
fs@(CtFlavour
_,EqRel
role) = Ct -> CtFlavourRole
ctFlavourRole Ct
ct in
                                CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs
                             Bool -> Bool -> Bool
&& TcTyVar -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty TcTyVar
new_tv EqRel
role (Ct -> Type
ctPred Ct
ct)
      TyFamLHS TyCon
new_tf [Type]
new_tf_args
        -> \Ct
ct -> let fs :: CtFlavourRole
fs@(CtFlavour
_, EqRel
role) = Ct -> CtFlavourRole
ctFlavourRole Ct
ct in
                  CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs
               Bool -> Bool -> Bool
&& TyCon -> [Type] -> EqRel -> Type -> Bool
fr_tf_can_rewrite_ty TyCon
new_tf [Type]
new_tf_args EqRel
role (Ct -> Type
ctPred Ct
ct)

    extend_tv_eqs :: InertEqs -> CanEqLHS -> EqualCtList -> InertEqs
    extend_tv_eqs :: InertEqs -> CanEqLHS -> EqualCtList -> InertEqs
extend_tv_eqs InertEqs
eqs (TyVarLHS TcTyVar
tv) EqualCtList
cts = forall a. DVarEnv a -> TcTyVar -> a -> DVarEnv a
extendDVarEnv InertEqs
eqs TcTyVar
tv EqualCtList
cts
    extend_tv_eqs InertEqs
eqs CanEqLHS
other EqualCtList
_cts = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extend_tv_eqs" (forall a. Outputable a => a -> SDoc
ppr InertEqs
eqs SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr CanEqLHS
other)

    extend_fun_eqs :: FunEqMap EqualCtList -> CanEqLHS -> EqualCtList
                   -> FunEqMap EqualCtList
    extend_fun_eqs :: FunEqMap EqualCtList
-> CanEqLHS -> EqualCtList -> FunEqMap EqualCtList
extend_fun_eqs FunEqMap EqualCtList
eqs (TyFamLHS TyCon
fam_tc [Type]
fam_args) EqualCtList
cts
      = forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp FunEqMap EqualCtList
eqs TyCon
fam_tc [Type]
fam_args EqualCtList
cts
    extend_fun_eqs FunEqMap EqualCtList
eqs CanEqLHS
other EqualCtList
_cts = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extend_fun_eqs" (forall a. Outputable a => a -> SDoc
ppr FunEqMap EqualCtList
eqs SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr CanEqLHS
other)

    kick_out_eqs :: (container -> CanEqLHS -> EqualCtList -> container)
                 -> EqualCtList -> ([Ct], container)
                 -> ([Ct], container)
    kick_out_eqs :: forall container.
(container -> CanEqLHS -> EqualCtList -> container)
-> EqualCtList -> ([Ct], container) -> ([Ct], container)
kick_out_eqs container -> CanEqLHS -> EqualCtList -> container
extend EqualCtList
eqs ([Ct]
acc_out, container
acc_in)
      = ([Ct]
eqs_out forall a. [a] -> [a] -> [a]
`chkAppend` [Ct]
acc_out, case [Ct] -> Maybe EqualCtList
listToEqualCtList [Ct]
eqs_in of
            Maybe EqualCtList
Nothing -> container
acc_in
            Just eqs_in_ecl :: EqualCtList
eqs_in_ecl@(EqualCtList (Ct
eq1 :| [Ct]
_))
                    -> container -> CanEqLHS -> EqualCtList -> container
extend container
acc_in (Ct -> CanEqLHS
cc_lhs Ct
eq1) EqualCtList
eqs_in_ecl)
      where
        ([Ct]
eqs_out, [Ct]
eqs_in) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Ct -> Bool
kick_out_eq (EqualCtList -> [Ct]
equalCtListToList EqualCtList
eqs)

    -- Implements criteria K1-K3 in Note [Extending the inert equalities]
    kick_out_eq :: Ct -> Bool
kick_out_eq (CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs, cc_rhs :: Ct -> Type
cc_rhs = Type
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  -- (K0) Keep it in the inert set if the new thing can't rewrite it

      -- Below here (fr_may_rewrite fs) is True

      | TyVarLHS TcTyVar
_ <- CanEqLHS
lhs
      , CtFlavourRole
fs CtFlavourRole -> CtFlavourRole -> Bool
`eqMayRewriteFR` CtFlavourRole
new_fr
      = Bool
False  -- (K4) Keep it in the inert set if the LHS is a tyvar and
               -- it can rewrite the work item. See Note [K4]

      | EqRel -> Type -> Bool
fr_can_rewrite_ty EqRel
eq_rel (CanEqLHS -> Type
canEqLHSType CanEqLHS
lhs)
      = Bool
True   -- (K1)
         -- The above check redundantly checks the role & flavour,
         -- but it's very convenient

      | Bool
kick_out_for_inertness    = Bool
True   -- (K2)
      | Bool
kick_out_for_completeness = Bool
True   -- (K3)
      | 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
&& EqRel -> Type -> Bool
fr_can_rewrite_ty EqRel
eq_rel Type
rhs_ty    -- (K2b)

        kick_out_for_completeness :: Bool
kick_out_for_completeness  -- (K3) and Note [K3: completeness of solving]
          = case EqRel
eq_rel of
              EqRel
NomEq  -> Type
rhs_ty Type -> Type -> Bool
`eqType` CanEqLHS -> Type
canEqLHSType CanEqLHS
new_lhs -- (K3a)
              EqRel
ReprEq -> CanEqLHS -> Type -> Bool
is_can_eq_lhs_head CanEqLHS
new_lhs Type
rhs_ty    -- (K3b)

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

    is_can_eq_lhs_head :: CanEqLHS -> Type -> Bool
is_can_eq_lhs_head (TyVarLHS TcTyVar
tv) = Type -> Bool
go
      where
        go :: Type -> Bool
go (Rep.TyVarTy TcTyVar
tv')   = TcTyVar
tv forall a. Eq a => a -> a -> Bool
== TcTyVar
tv'
        go (Rep.AppTy Type
fun Type
_)   = Type -> Bool
go Type
fun
        go (Rep.CastTy Type
ty Coercion
_)   = Type -> Bool
go Type
ty
        go (Rep.TyConApp {})   = Bool
False
        go (Rep.LitTy {})      = Bool
False
        go (Rep.ForAllTy {})   = Bool
False
        go (Rep.FunTy {})      = Bool
False
        go (Rep.CoercionTy {}) = Bool
False
    is_can_eq_lhs_head (TyFamLHS TyCon
fun_tc [Type]
fun_args) = Type -> Bool
go
      where
        go :: Type -> Bool
go (Rep.TyVarTy {})       = Bool
False
        go (Rep.AppTy {})         = Bool
False  -- no TyConApp to the left of an AppTy
        go (Rep.CastTy Type
ty Coercion
_)      = Type -> Bool
go Type
ty
        go (Rep.TyConApp TyCon
tc [Type]
args) = TyCon -> [Type] -> TyCon -> [Type] -> Bool
tcEqTyConApps TyCon
fun_tc [Type]
fun_args TyCon
tc [Type]
args
        go (Rep.LitTy {})         = Bool
False
        go (Rep.ForAllTy {})      = Bool
False
        go (Rep.FunTy {})         = Bool
False
        go (Rep.CoercionTy {})    = Bool
False

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

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

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

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

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

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

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

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

      | Bool
otherwise
      = forall a b. b -> Either a b
Right Ct
ct

    kick_ct Ct
other = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"kickOutAfterFillingCoercionHole" (forall a. Outputable a => a -> SDoc
ppr Ct
other)

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

When we add a new inert equality (lhs ~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) 'lhs' is free in the inert constraint (so that it *will*)
       rewrite it if we kick it out.

    For (b) we use anyRewritableCanLHS, which examines the types /and
    kinds/ 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 LHS!

  - 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

NB: we could in principle avoid kick-out:
  a) When unifying a meta-tyvar from an outer level, because
     then the entire implication will be iterated; see
     Note [The Unification Level Flag]

  b) For Givens, after a unification.  By (GivenInv) in GHC.Tc.Utils.TcType
     Note [TcLevel invariants], a Given can't include a meta-tyvar from
     its own level, so it falls under (a).  Of course, we must still
     kick out Givens when adding a new non-unification Given.

But kicking out more vigorously may lead to earlier unification and fewer
iterations, so we don't take advantage of these possibilities.

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.

Hence:
 * In the main simplifier loops in GHC.Tc.Solver (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 GHC.Tc.Solver.Monad.kick_out_rewritable)

 * We rewrite those insolubles in GHC.Tc.Solver.Canonical.
   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 -> [Type]
cc_tyargs = [Type]
tys })
  = InertCans
ics { inert_safehask :: DictMap Ct
inert_safehask = DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct
addDictCt (InertCans -> DictMap Ct
inert_dicts InertCans
ics) Class
cls [Type]
tys Ct
item }

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

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

getSafeOverlapFailures :: TcS Cts
-- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
getSafeOverlapFailures :: TcS (Bag Ct)
getSafeOverlapFailures
 = do { IC { inert_safehask :: InertCans -> DictMap Ct
inert_safehask = DictMap Ct
safehask } <- TcS InertCans
getInertCans
      ; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldDicts Ct -> Bag Ct -> Bag Ct
consCts DictMap Ct
safehask Bag Ct
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 -> [Type] -> TcS ()
addSolvedDict InstanceWhat
what CtEvidence
item Class
cls [Type]
tys
  | CtEvidence -> Bool
isWanted CtEvidence
item
  , InstanceWhat -> Bool
instanceReturnsDictCon InstanceWhat
what
  = do { String -> SDoc -> TcS ()
traceTcS String
"updSolvedSetTcs:" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr CtEvidence
item
       ; (InertSet -> InertSet) -> TcS ()
updInertTcS forall a b. (a -> b) -> a -> b
$ \ InertSet
ics ->
             InertSet
ics { inert_solved_dicts :: DictMap CtEvidence
inert_solved_dicts = forall a. DictMap a -> Class -> [Type] -> a -> DictMap a
addDict (InertSet -> DictMap CtEvidence
inert_solved_dicts InertSet
ics) Class
cls [Type]
tys CtEvidence
item } }
  | Bool
otherwise
  = forall (m :: * -> *) a. Monad m => a -> m a
return ()

getSolvedDicts :: TcS (DictMap CtEvidence)
getSolvedDicts :: TcS (DictMap CtEvidence)
getSolvedDicts = do { InertSet
ics <- TcS InertSet
getTcSInerts; 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 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
       ; forall a. TcM a -> TcS a
wrapTcS (do { InertSet
curr_inert <- forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
is_var
                     ; 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; 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 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 :: forall a. (InertCans -> (a, InertCans)) -> TcS a
updRetInertCans InertCans -> (a, InertCans)
upd_fn
  = do { IORef InertSet
is_var <- TcS (IORef InertSet)
getTcSInertsRef
       ; forall a. TcM a -> TcS a
wrapTcS (do { InertSet
inerts <- 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)
                     ; 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' })
                     ; 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 forall a b. (a -> b) -> a -> b
$ \ InertSet
inerts -> InertSet
inerts { inert_cans :: InertCans
inert_cans = InertCans -> InertCans
upd_fn (InertSet -> InertCans
inert_cans InertSet
inerts) }

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

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

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

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

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

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

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

get_sc_pending :: TcLevel -> InertCans -> ([Ct], InertCans)
get_sc_pending :: TcLevel -> InertCans -> ([Ct], InertCans)
get_sc_pending TcLevel
this_lvl ic :: InertCans
ic@(IC { inert_dicts :: InertCans -> DictMap Ct
inert_dicts = DictMap Ct
dicts, inert_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
insts })
  = 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 :: DictMap Ct
inert_dicts = DictMap Ct
dicts', inert_insts :: [QCInst]
inert_insts = [QCInst]
insts' })
  where
    sc_pending :: [Ct]
sc_pending = [Ct]
sc_pend_insts forall a. [a] -> [a] -> [a]
++ [Ct]
sc_pend_dicts

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

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

    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' forall a. a -> [a] -> [a]
: [Ct]
dicts
        | Bool
otherwise
        = [Ct]
dicts

    add :: Ct -> DictMap Ct -> DictMap Ct
    add :: Ct -> DictMap Ct -> DictMap Ct
add ct :: Ct
ct@(CDictCan { cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type]
tys }) DictMap Ct
dicts
        = DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct
addDictCt DictMap Ct
dicts Class
cls [Type]
tys Ct
ct
    add Ct
ct DictMap Ct
_ = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"getPendingScDicts" (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' 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) forall a. Eq a => a -> a -> Bool
== TcLevel
this_lvl
    -- We only want Givens from this level; see (3a) in
    -- Note [The superclass story] in GHC.Tc.Solver.Canonical

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

      ; let unsolved_tv_eqs :: Bag Ct
unsolved_tv_eqs  = forall b. (Ct -> b -> b) -> InertEqs -> b -> b
foldTyEqs Ct -> Bag Ct -> Bag Ct
add_if_unsolved InertEqs
tv_eqs Bag Ct
emptyCts
            unsolved_fun_eqs :: Bag Ct
unsolved_fun_eqs = forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs EqualCtList -> Bag Ct -> Bag Ct
add_if_unsolveds FunEqMap EqualCtList
fun_eqs Bag Ct
emptyCts
            unsolved_irreds :: Bag Ct
unsolved_irreds  = forall a. (a -> Bool) -> Bag a -> Bag a
Bag.filterBag Ct -> Bool
is_unsolved Bag Ct
irreds
            unsolved_blocked :: Bag Ct
unsolved_blocked = Bag Ct
blocked  -- all blocked equalities are W/D
            unsolved_dicts :: Bag Ct
unsolved_dicts   = forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldDicts Ct -> Bag Ct -> Bag Ct
add_if_unsolved DictMap Ct
idicts Bag Ct
emptyCts
            unsolved_others :: Bag Ct
unsolved_others  = forall a. [Bag a] -> Bag a
unionManyBags [ Bag Ct
unsolved_irreds
                                             , Bag Ct
unsolved_dicts
                                             , Bag Ct
unsolved_blocked ]

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

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

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

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

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

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

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

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

mentionsOuterVar :: TcLevel -> CtEvidence -> Bool
mentionsOuterVar :: TcLevel -> CtEvidence -> Bool
mentionsOuterVar TcLevel
tclvl CtEvidence
ev
  = (TcTyVar -> Bool) -> Type -> Bool
anyFreeVarsOfType (TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl) forall a b. (a -> b) -> a -> b
$
    CtEvidence -> Type
ctEvPred CtEvidence
ev

isOuterTyVar :: TcLevel -> TyCoVar -> Bool
-- True of a type variable that comes from a
-- shallower level than the ambient level (tclvl)
isOuterTyVar :: TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl TcTyVar
tv
  | TcTyVar -> Bool
isTyVar TcTyVar
tv = ASSERT2( not (isTouchableMetaTyVar tclvl tv), ppr tv <+> ppr tclvl  )
                 TcLevel
tclvl TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
tv
    -- ASSERT: we are dealing with Givens here, and invariant (GivenInv) from
    -- Note Note [TcLevel invariants] in GHC.Tc.Utils.TcType ensures that there can't
    -- be a touchable meta tyvar.   If this wasn't true, you might worry that,
    -- at level 3, a meta-tv alpha[3] gets unified with skolem b[2], and thereby
    -- becomes "outer" even though its level numbers says it isn't.
  | Bool
otherwise  = Bool
False  -- Coercion variables; doesn't much matter

-- | 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 "GHC.Tc.Solver.Interact"
matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
matchableGivens :: CtLoc -> Type -> InertSet -> Bag Ct
matchableGivens CtLoc
loc_w Type
pred_w inerts :: InertSet
inerts@(IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
inert_cans })
  = forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Ct -> Bool
matchable_given Bag Ct
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 :: Bag Ct
all_relevant_givens
      | Just (Class
clas, [Type]
_) <- Type -> Maybe (Class, [Type])
getClassPredTys_maybe Type
pred_w
      = forall a. DictMap a -> Class -> Bag a
findDictsByClass (InertCans -> DictMap Ct
inert_dicts InertCans
inert_cans) Class
clas
        forall a. Bag a -> Bag a -> Bag a
`unionBags` InertCans -> Bag Ct
inert_irreds InertCans
inert_cans
      | Bool
otherwise
      = InertCans -> Bag Ct
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 -> Type
ctev_pred = Type
pred_g } <- Ct -> CtEvidence
ctEvidence Ct
ct
      = InertSet -> Type -> CtLoc -> Type -> CtLoc -> Bool
mightEqualLater InertSet
inerts Type
pred_g CtLoc
loc_g Type
pred_w CtLoc
loc_w

      | Bool
otherwise
      = Bool
False

mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
-- See Note [What might equal later?]
-- Used to implement logic in Note [Instance and Given overlap] in GHC.Tc.Solver.Interact
mightEqualLater :: InertSet -> Type -> CtLoc -> Type -> CtLoc -> Bool
mightEqualLater InertSet
inert_set Type
given_pred CtLoc
given_loc Type
wanted_pred CtLoc
wanted_loc
  | CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
given_loc CtLoc
wanted_loc
  = Bool
False

  | Bool
otherwise
  = case BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG BindFun
bind_fun [Type
flattened_given] [Type
flattened_wanted] of
      UnifyResult
SurelyApart              -> Bool
False  -- types that are surely apart do not equal later
      MaybeApart MaybeApartReason
MARInfinite TCvSubst
_ -> Bool
False  -- see Example 7 in the Note.
      UnifyResult
_                        -> Bool
True

  where
    in_scope :: InScopeSet
in_scope  = VarSet -> InScopeSet
mkInScopeSet forall a b. (a -> b) -> a -> b
$ [Type] -> VarSet
tyCoVarsOfTypes [Type
given_pred, Type
wanted_pred]

    -- NB: flatten both at the same time, so that we can share mappings
    -- from type family applications to variables, and also to guarantee
    -- that the fresh variables are really fresh between the given and
    -- the wanted. Flattening both at the same time is needed to get
    -- Example 10 from the Note.
    ([Type
flattened_given, Type
flattened_wanted], TyVarEnv (TyCon, [Type])
var_mapping)
      = InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
flattenTysX InScopeSet
in_scope [Type
given_pred, Type
wanted_pred]

    bind_fun :: BindFun
    bind_fun :: BindFun
bind_fun TcTyVar
tv Type
rhs_ty
      | TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
      , TcTyVar -> MetaInfo -> Type -> Bool
can_unify TcTyVar
tv (TcTyVar -> MetaInfo
metaTyVarInfo TcTyVar
tv) Type
rhs_ty
         -- this checks for CycleBreakerTvs and TyVarTvs; forgetting
         -- the latter was #19106.
      = BindFlag
BindMe

         -- See Examples 4, 5, and 6 from the Note
      | Just (TyCon
_fam_tc, [Type]
fam_args) <- forall a. VarEnv a -> TcTyVar -> Maybe a
lookupVarEnv TyVarEnv (TyCon, [Type])
var_mapping TcTyVar
tv
      , (TcTyVar -> Bool) -> [Type] -> Bool
anyFreeVarsOfTypes TcTyVar -> Bool
mentions_meta_ty_var [Type]
fam_args
      = BindFlag
BindMe

      | Bool
otherwise
      = BindFlag
Apart

    -- True for TauTv and TyVarTv (and RuntimeUnkTv) meta-tyvars
    -- (as they can be unified)
    -- and also for CycleBreakerTvs that mentions meta-tyvars
    mentions_meta_ty_var :: TyVar -> Bool
    mentions_meta_ty_var :: TcTyVar -> Bool
mentions_meta_ty_var TcTyVar
tv
      | TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
      = case TcTyVar -> MetaInfo
metaTyVarInfo TcTyVar
tv of
          -- See Examples 8 and 9 in the Note
          MetaInfo
CycleBreakerTv
            -> (TcTyVar -> Bool) -> Type -> Bool
anyFreeVarsOfType TcTyVar -> Bool
mentions_meta_ty_var
                 (TcTyVar -> InertSet -> Type
lookupCycleBreakerVar TcTyVar
tv InertSet
inert_set)
          MetaInfo
_ -> Bool
True
      | Bool
otherwise
      = Bool
False

    -- like canSolveByUnification, but allows cbv variables to unify
    can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
    can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
can_unify TcTyVar
_lhs_tv MetaInfo
TyVarTv Type
rhs_ty  -- see Example 3 from the Note
      | Just TcTyVar
rhs_tv <- Type -> Maybe TcTyVar
tcGetTyVar_maybe Type
rhs_ty
      = case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
rhs_tv of
          MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
TyVarTv } -> Bool
True
          MetaTv {}                     -> Bool
False  -- could unify with anything
          SkolemTv {}                   -> Bool
True
          TcTyVarDetails
RuntimeUnk                    -> Bool
True
      | Bool
otherwise  -- not a var on the RHS
      = Bool
False
    can_unify TcTyVar
lhs_tv MetaInfo
_other Type
_rhs_ty = TcTyVar -> Bool
mentions_meta_ty_var TcTyVar
lhs_tv

prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
-- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
from_loc CtLoc
solve_loc
  | InstSCOrigin Int
_ TypeSize
given_size <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
from_loc
  , ScOrigin TypeSize
wanted_size <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
solve_loc
  = TypeSize
given_size forall a. Ord a => a -> a -> Bool
>= TypeSize
wanted_size
  | Bool
otherwise
  = Bool
False

{- *********************************************************************
*                                                                      *
    Cycle breakers
*                                                                      *
********************************************************************* -}

-- | Return the type family application a CycleBreakerTv maps to.
lookupCycleBreakerVar :: TcTyVar    -- ^ cbv, must be a CycleBreakerTv
                      -> InertSet
                      -> TcType     -- ^ type family application the cbv maps to
lookupCycleBreakerVar :: TcTyVar -> InertSet -> Type
lookupCycleBreakerVar TcTyVar
cbv (IS { inert_cycle_breakers :: InertSet -> CycleBreakerVarStack
inert_cycle_breakers = CycleBreakerVarStack
cbvs_stack })
-- This function looks at every environment in the stack. This is necessary
-- to avoid #20231. This function (and its one usage site) is the only reason
-- that we store a stack instead of just the top environment.
  | Just Type
tyfam_app <- ASSERT( (isCycleBreakerTyVar cbv) )
                      forall (f :: * -> *) a. Foldable f => f (Maybe a) -> Maybe a
firstJusts (forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TcTyVar
cbv) CycleBreakerVarStack
cbvs_stack)
  = Type
tyfam_app
  | Bool
otherwise
  = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"lookupCycleBreakerVar found an unbound cycle breaker" (forall a. Outputable a => a -> SDoc
ppr TcTyVar
cbv SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr CycleBreakerVarStack
cbvs_stack)

-- | Push a fresh environment onto the cycle-breaker var stack. Useful
-- when entering a nested implication.
pushCycleBreakerVarStack :: CycleBreakerVarStack -> CycleBreakerVarStack
pushCycleBreakerVarStack :: CycleBreakerVarStack -> CycleBreakerVarStack
pushCycleBreakerVarStack = ([] forall a. a -> NonEmpty a -> NonEmpty a
NE.<|)

-- | Add a new cycle-breaker binding to the top environment on the stack.
insertCycleBreakerBinding :: TcTyVar   -- ^ cbv, must be a CycleBreakerTv
                          -> TcType    -- ^ cbv's expansion
                          -> CycleBreakerVarStack -> CycleBreakerVarStack
insertCycleBreakerBinding :: TcTyVar -> Type -> CycleBreakerVarStack -> CycleBreakerVarStack
insertCycleBreakerBinding TcTyVar
cbv Type
expansion ([(TcTyVar, Type)]
top_env :| [[(TcTyVar, Type)]]
rest_envs)
  = ASSERT( (isCycleBreakerTyVar cbv) )
    ((TcTyVar
cbv, Type
expansion) forall a. a -> [a] -> [a]
: [(TcTyVar, Type)]
top_env) forall a. a -> [a] -> NonEmpty a
:| [[(TcTyVar, Type)]]
rest_envs

-- | Perform a monadic operation on all pairs in the top environment
-- in the stack.
forAllCycleBreakerBindings_ :: Monad m
                            => CycleBreakerVarStack
                            -> (TcTyVar -> TcType -> m ()) -> m ()
forAllCycleBreakerBindings_ :: forall (m :: * -> *).
Monad m =>
CycleBreakerVarStack -> (TcTyVar -> Type -> m ()) -> m ()
forAllCycleBreakerBindings_ ([(TcTyVar, Type)]
top_env :| [[(TcTyVar, Type)]]
_rest_envs) TcTyVar -> Type -> m ()
action
  = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(TcTyVar, Type)]
top_env (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TcTyVar -> Type -> m ()
action)
{-# INLINABLE forAllCycleBreakerBindings_ #-}  -- to allow SPECIALISE later


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

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

This is best understood by example.

1. C alpha  ~?  C Int

   That given certainly might match later.

2. C a  ~?  C Int

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

3. C alpha[tv]   ~?  C Int

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

4. C (F alpha)   ~?   C Int

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

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

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

6. C (F a)  ~?  C a

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

7. C (Maybe alpha)  ~?  C alpha

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

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

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

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

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

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

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

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

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

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

removeInertCts :: [Ct] -> InertCans -> InertCans
-- ^ Remove inert constraints from the 'InertCans', for use when a
-- typechecker plugin wishes to discard a given.
removeInertCts :: [Ct] -> InertCans -> InertCans
removeInertCts [Ct]
cts InertCans
icans = 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 -> [Type]
cc_tyargs = [Type]
tys } ->
      InertCans
is { inert_dicts :: DictMap Ct
inert_dicts = forall a. DictMap a -> Class -> [Type] -> DictMap a
delDict (InertCans -> DictMap Ct
inert_dicts InertCans
is) Class
cl [Type]
tys }

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

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

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

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

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

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

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

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

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

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

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


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

Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Whenever we are looking up an inert dictionary (CDictCan) or function
equality (CEqCan), we use a TcAppMap, which uses the Unique of the
class/type family tycon and then a trie which maps the arguments. This
trie does *not* need to match the kinds of the arguments; this Note
explains why.

Consider the types ty0 = (T ty1 ty2 ty3 ty4) and ty0' = (T ty1' ty2' ty3' ty4'),
where ty4 and ty4' have different kinds. Let's further assume that both types
ty0 and ty0' are well-typed. Because the kind of T is closed, it must be that
one of the ty1..ty3 does not match ty1'..ty3' (and that the kind of the fourth
argument to T is dependent on whichever one changed). Since we are matching
all arguments, during the inert-set lookup, we know that ty1..ty3 do indeed
match ty1'..ty3'. Therefore, the kind of ty4 and ty4' must match, too --
without ever looking at it.

Accordingly, we use LooseTypeMap, which skips the kind check when looking
up a type. I (Richard E) believe this is just an optimization, and that
looking at kinds would be harmless.

-}

type TcAppMap a = DTyConEnv (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] in GHC.Data.TrieMap for why we use DTyConEnv here

isEmptyTcAppMap :: TcAppMap a -> Bool
isEmptyTcAppMap :: forall a. TcAppMap a -> Bool
isEmptyTcAppMap TcAppMap a
m = forall a. DTyConEnv a -> Bool
isEmptyDTyConEnv TcAppMap a
m

emptyTcAppMap :: TcAppMap a
emptyTcAppMap :: forall a. DictMap a
emptyTcAppMap = forall a. DTyConEnv a
emptyDTyConEnv

findTcApp :: TcAppMap a -> TyCon -> [Type] -> Maybe a
findTcApp :: forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findTcApp TcAppMap a
m TyCon
tc [Type]
tys = do { ListMap LooseTypeMap a
tys_map <- forall a. DTyConEnv a -> TyCon -> Maybe a
lookupDTyConEnv TcAppMap a
m TyCon
tc
                        ; forall (m :: * -> *) b. TrieMap m => Key m -> m b -> Maybe b
lookupTM [Type]
tys ListMap LooseTypeMap a
tys_map }

delTcApp :: TcAppMap a -> TyCon -> [Type] -> TcAppMap a
delTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> TcAppMap a
delTcApp TcAppMap a
m TyCon
tc [Type]
tys = forall a. (a -> a) -> DTyConEnv a -> TyCon -> DTyConEnv a
adjustDTyConEnv (forall (m :: * -> *) a. TrieMap m => Key m -> m a -> m a
deleteTM [Type]
tys) TcAppMap a
m TyCon
tc

insertTcApp :: TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp TcAppMap a
m TyCon
tc [Type]
tys a
ct = forall a.
(Maybe a -> Maybe a) -> DTyConEnv a -> TyCon -> DTyConEnv a
alterDTyConEnv Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
alter_tm TcAppMap a
m TyCon
tc
  where
    alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
alter_tm Maybe (ListMap LooseTypeMap a)
mb_tm = forall a. a -> Maybe a
Just (forall (m :: * -> *) a. TrieMap m => Key m -> a -> m a -> m a
insertTM [Type]
tys a
ct (Maybe (ListMap LooseTypeMap a)
mb_tm forall a. Maybe a -> a -> a
`orElse` forall (m :: * -> *) a. TrieMap m => m a
emptyTM))

alterTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
alterTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
alterTcApp TcAppMap a
m TyCon
tc [Type]
tys XT a
upd = forall a.
(Maybe a -> Maybe a) -> DTyConEnv a -> TyCon -> DTyConEnv a
alterDTyConEnv Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
alter_tm TcAppMap a
m TyCon
tc
  where
    alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
    alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
alter_tm Maybe (ListMap LooseTypeMap a)
m_elt = forall a. a -> Maybe a
Just (forall (m :: * -> *) b. TrieMap m => Key m -> XT b -> m b -> m b
alterTM [Type]
tys XT a
upd (Maybe (ListMap LooseTypeMap a)
m_elt forall a. Maybe a -> a -> a
`orElse` forall (m :: * -> *) a. TrieMap m => m a
emptyTM))

filterTcAppMap :: forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
filterTcAppMap :: forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
filterTcAppMap a -> Bool
f TcAppMap a
m = forall a b. (a -> Maybe b) -> DTyConEnv a -> DTyConEnv b
mapMaybeDTyConEnv ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
one_tycon TcAppMap a
m
  where
    one_tycon :: ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
    one_tycon :: ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
one_tycon ListMap LooseTypeMap a
tm
      | forall (m :: * -> *) a. TrieMap m => m a -> Bool
isEmptyTM ListMap LooseTypeMap a
filtered_tm = forall a. Maybe a
Nothing
      | Bool
otherwise             = forall a. a -> Maybe a
Just ListMap LooseTypeMap a
filtered_tm
      where
        filtered_tm :: ListMap LooseTypeMap a
filtered_tm = forall (m :: * -> *) a. TrieMap m => (a -> Bool) -> m a -> m a
filterTM a -> Bool
f ListMap LooseTypeMap a
tm

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

foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
foldTcAppMap :: forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldTcAppMap a -> b -> b
k TcAppMap a
m b
z = forall elt a. (elt -> a -> a) -> a -> DTyConEnv elt -> a
foldDTyConEnv (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 GHC.Tc.Types.Evidence

* We cannonicalise such constraints, in GHC.Tc.Solver.Canonical.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 :: forall a. DictMap a
emptyDictMap = forall a. DictMap a
emptyTcAppMap

findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict :: forall a. DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict DictMap a
m CtLoc
loc Class
cls [Type]
tys
  | Class -> [Type] -> Bool
hasIPSuperClasses Class
cls [Type]
tys -- See Note [Tuples hiding implicit parameters]
  = forall a. Maybe a
Nothing

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

  | Bool
otherwise
  = forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findTcApp DictMap a
m (Class -> TyCon
classTyCon Class
cls) [Type]
tys

findDictsByClass :: DictMap a -> Class -> Bag a
findDictsByClass :: forall a. DictMap a -> Class -> Bag a
findDictsByClass DictMap a
m Class
cls
  | Just ListMap LooseTypeMap a
tm <- forall a. DTyConEnv a -> TyCon -> Maybe a
lookupDTyConEnv DictMap a
m (Class -> TyCon
classTyCon Class
cls) = forall (m :: * -> *) a b.
TrieMap m =>
(a -> b -> b) -> m a -> b -> b
foldTM forall a. a -> Bag a -> Bag a
consBag ListMap LooseTypeMap a
tm forall a. Bag a
emptyBag
  | Bool
otherwise                                     = forall a. Bag a
emptyBag

delDict :: DictMap a -> Class -> [Type] -> DictMap a
delDict :: forall a. DictMap a -> Class -> [Type] -> DictMap a
delDict DictMap a
m Class
cls [Type]
tys = forall a. TcAppMap a -> TyCon -> [Type] -> TcAppMap a
delTcApp DictMap a
m (Class -> TyCon
classTyCon Class
cls) [Type]
tys

addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
addDict :: forall a. DictMap a -> Class -> [Type] -> a -> DictMap a
addDict DictMap a
m Class
cls [Type]
tys a
item = forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp DictMap a
m (Class -> TyCon
classTyCon Class
cls) [Type]
tys a
item

addDictCt :: DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct
-- Like addDict, but combines [W] and [D] to [WD]
-- See Note [KeepBoth] in GHC.Tc.Solver.Interact
addDictCt :: DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct
addDictCt DictMap Ct
m Class
cls [Type]
tys Ct
new_ct = forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
alterTcApp DictMap Ct
m (Class -> TyCon
classTyCon Class
cls) [Type]
tys Maybe Ct -> Maybe Ct
xt_ct
  where
    new_ct_ev :: CtEvidence
new_ct_ev = Ct -> CtEvidence
ctEvidence Ct
new_ct

    xt_ct :: Maybe Ct -> Maybe Ct
    xt_ct :: Maybe Ct -> Maybe Ct
xt_ct (Just Ct
old_ct)
      | CtWanted { ctev_nosh :: CtEvidence -> ShadowInfo
ctev_nosh = ShadowInfo
WOnly } <- CtEvidence
old_ct_ev
      , CtDerived {} <- CtEvidence
new_ct_ev
      = forall a. a -> Maybe a
Just (Ct
old_ct { cc_ev :: CtEvidence
cc_ev = CtEvidence
old_ct_ev { ctev_nosh :: ShadowInfo
ctev_nosh = ShadowInfo
WDeriv }})
      | CtDerived {} <- CtEvidence
old_ct_ev
      , CtWanted { ctev_nosh :: CtEvidence -> ShadowInfo
ctev_nosh = ShadowInfo
WOnly } <- CtEvidence
new_ct_ev
      = forall a. a -> Maybe a
Just (Ct
new_ct { cc_ev :: CtEvidence
cc_ev = CtEvidence
new_ct_ev { ctev_nosh :: ShadowInfo
ctev_nosh = ShadowInfo
WDeriv }})
      where
        old_ct_ev :: CtEvidence
old_ct_ev = Ct -> CtEvidence
ctEvidence Ct
old_ct

    xt_ct Maybe Ct
_ = forall a. a -> Maybe a
Just Ct
new_ct

addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
addDictsByClass DictMap Ct
m Class
cls Bag Ct
items
  = forall a. DTyConEnv a -> TyCon -> a -> DTyConEnv a
extendDTyConEnv DictMap Ct
m (Class -> TyCon
classTyCon Class
cls) (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {m :: * -> *}.
(Key m ~ [Type], TrieMap m) =>
Ct -> m Ct -> m Ct
add forall (m :: * -> *) a. TrieMap m => m a
emptyTM Bag Ct
items)
  where
    add :: Ct -> m Ct -> m Ct
add ct :: Ct
ct@(CDictCan { cc_tyargs :: Ct -> [Type]
cc_tyargs = [Type]
tys }) m Ct
tm = forall (m :: * -> *) a. TrieMap m => Key m -> a -> m a -> m a
insertTM [Type]
tys Ct
ct m Ct
tm
    add Ct
ct m Ct
_ = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"addDictsByClass" (forall a. Outputable a => a -> SDoc
ppr Ct
ct)

filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
filterDicts Ct -> Bool
f DictMap Ct
m = forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
filterTcAppMap Ct -> Bool
f DictMap Ct
m

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

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

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

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


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

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

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

findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq :: forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq FunEqMap a
m TyCon
tc [Type]
tys = forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findTcApp FunEqMap a
m TyCon
tc [Type]
tys

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 :: forall a. FunEqMap a -> TyCon -> [a]
findFunEqsByTyCon FunEqMap a
m TyCon
tc
  | Just ListMap LooseTypeMap a
tm <- forall a. DTyConEnv a -> TyCon -> Maybe a
lookupDTyConEnv FunEqMap a
m TyCon
tc = 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 :: forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs = forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldTcAppMap

insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
insertFunEq :: forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertFunEq FunEqMap a
m TyCon
tc [Type]
tys a
val = forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp FunEqMap a
m TyCon
tc [Type]
tys a
val

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

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

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

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

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

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

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

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

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

      -- See Note [WorkList priorities] and
      TcSEnv -> IORef WorkList
tcs_worklist  :: IORef WorkList -- Current worklist
    }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

traceFireTcS :: CtEvidence -> SDoc -> TcS ()
-- Dump a rule-firing trace
traceFireTcS :: CtEvidence -> SDoc -> TcS ()
traceFireTcS CtEvidence
ev SDoc
doc
  = forall a. (TcSEnv -> TcM a) -> TcS a
mkTcS forall a b. (a -> b) -> a -> b
$ \TcSEnv
env -> TcM SDoc -> TcM ()
csTraceTcM forall a b. (a -> b) -> a -> b
$
    do { Int
n <- 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
       ; 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
<> 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
<> 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 (forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev)) }
{-# INLINE traceFireTcS #-}  -- see Note [INLINE conditional tracing utilities]

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

runTcS :: TcS a                -- What to run
       -> TcM (a, EvBindMap)
runTcS :: forall a. TcS a -> TcM (a, EvBindMap)
runTcS TcS a
tcs
  = do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
       ; a
res <- 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
       ; 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 :: forall a. TcS a -> TcM a
runTcSDeriveds TcS a
tcs
  = do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newTcEvBinds
       ; 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 :: forall a. TcS a -> TcM a
runTcSEqualities TcS a
thing_inside
  = do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
TcM.newNoTcEvBinds
       ; forall a. EvBindsVar -> TcS a -> TcM a
runTcSWithEvBinds EvBindsVar
ev_binds_var TcS a
thing_inside }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

nestTcS ::  TcS a -> TcS a
-- Use the current untouchables, augmenting the current
-- evidence bindings, and solved dictionaries
-- But have no effect on the InertCans, or on the inert_famapp_cache
-- (we want to inherit the latter from processing the Givens)
nestTcS :: forall a. TcS a -> TcS a
nestTcS (TcS TcSEnv -> TcM a
thing_inside)
  = forall a. (TcSEnv -> TcM a) -> TcS a
TcS 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 <- forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
inerts_var
       ; IORef InertSet
new_inert_var <- forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
TcM.newTcRef InertSet
inerts
       ; IORef WorkList
new_wl_var    <- 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 <- forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
TcM.readTcRef IORef InertSet
new_inert_var

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

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

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

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

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

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

       ; Implication -> TcS ()
emitImplication Implication
imp }


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

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

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

getTcSWorkListRef :: TcS (IORef WorkList)
getTcSWorkListRef :: TcS (IORef WorkList)
getTcSWorkListRef = forall a. (TcSEnv -> TcM a) -> TcS a
TcS (forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. TcRef a -> TcS a
readTcRef

setTcSInerts :: InertSet -> TcS ()
setTcSInerts :: InertSet -> TcS ()
setTcSInerts InertSet
ics = do { IORef InertSet
r <- TcS (IORef InertSet)
getTcSInertsRef; 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 <- forall a. TcRef a -> TcS a
readTcRef IORef WorkList
wl_var
       ; forall (m :: * -> *) a. Monad m => a -> m a
return (WorkList -> Bag Implication
wl_implics WorkList
wl_curr) }

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

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

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

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

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

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

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

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

updTcRef :: TcRef a -> (a->a) -> TcS ()
updTcRef :: forall a. TcRef a -> (a -> a) -> TcS ()
updTcRef TcRef a
ref a -> a
upd_fn = forall a. TcM a -> TcS a
wrapTcS (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 = forall a. (TcSEnv -> TcM a) -> TcS a
TcS (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcSEnv -> EvBindsVar
tcs_ev_binds)

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

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

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

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

data TouchabilityTestResult
  -- See Note [Solve by unification] in GHC.Tc.Solver.Interact
  -- which points out that having TouchableSameLevel is just an optimisation;
  -- we could manage with TouchableOuterLevel alone (suitably renamed)
  = TouchableSameLevel
  | TouchableOuterLevel [TcTyVar]   -- Promote these
                        TcLevel     -- ..to this level
  | Untouchable

instance Outputable TouchabilityTestResult where
  ppr :: TouchabilityTestResult -> SDoc
ppr TouchabilityTestResult
TouchableSameLevel            = String -> SDoc
text String
"TouchableSameLevel"
  ppr (TouchableOuterLevel [TcTyVar]
tvs TcLevel
lvl) = String -> SDoc
text String
"TouchableOuterLevel" SDoc -> SDoc -> SDoc
<> SDoc -> SDoc
parens (forall a. Outputable a => a -> SDoc
ppr TcLevel
lvl SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
tvs)
  ppr TouchabilityTestResult
Untouchable                   = String -> SDoc
text String
"Untouchable"

touchabilityTest :: CtFlavour -> TcTyVar -> TcType -> TcS TouchabilityTestResult
-- This is the key test for untouchability:
-- See Note [Unification preconditions] in GHC.Tc.Utils.Unify
-- and Note [Solve by unification] in GHC.Tc.Solver.Interact
touchabilityTest :: CtFlavour -> TcTyVar -> Type -> TcS TouchabilityTestResult
touchabilityTest CtFlavour
flav TcTyVar
tv1 Type
rhs
  | CtFlavour
flav forall a. Eq a => a -> a -> Bool
/= CtFlavour
Given  -- See Note [Do not unify Givens]
  , MetaTv { mtv_tclvl :: TcTyVarDetails -> TcLevel
mtv_tclvl = TcLevel
tv_lvl, mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info } <- TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
tv1
  , MetaInfo -> Type -> Bool
canSolveByUnification MetaInfo
info Type
rhs
  = do { TcLevel
ambient_lvl  <- TcS TcLevel
getTcLevel
       ; TcLevel
given_eq_lvl <- TcS TcLevel
getInnermostGivenEqLevel

       ; if | TcLevel
tv_lvl TcLevel -> TcLevel -> Bool
`sameDepthAs` TcLevel
ambient_lvl
            -> forall (m :: * -> *) a. Monad m => a -> m a
return TouchabilityTestResult
TouchableSameLevel

            | TcLevel
tv_lvl TcLevel -> TcLevel -> Bool
`deeperThanOrSame` TcLevel
given_eq_lvl   -- No intervening given equalities
            , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TcLevel -> TcTyVar -> Bool
does_not_escape TcLevel
tv_lvl) [TcTyVar]
free_skols  -- No skolem escapes
            -> forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar] -> TcLevel -> TouchabilityTestResult
TouchableOuterLevel [TcTyVar]
free_metas TcLevel
tv_lvl)

            | Bool
otherwise
            -> forall (m :: * -> *) a. Monad m => a -> m a
return TouchabilityTestResult
Untouchable }
  | Bool
otherwise
  = forall (m :: * -> *) a. Monad m => a -> m a
return TouchabilityTestResult
Untouchable
  where
     ([TcTyVar]
free_metas, [TcTyVar]
free_skols) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition TcTyVar -> Bool
isPromotableMetaTyVar forall a b. (a -> b) -> a -> b
$
                                forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet               forall a b. (a -> b) -> a -> b
$
                                Type -> VarSet
tyCoVarsOfType Type
rhs

     does_not_escape :: TcLevel -> TcTyVar -> Bool
does_not_escape TcLevel
tv_lvl TcTyVar
fv
       | TcTyVar -> Bool
isTyVar TcTyVar
fv = TcLevel
tv_lvl TcLevel -> TcLevel -> Bool
`deeperThanOrSame` TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
fv
       | Bool
otherwise  = Bool
True
       -- Coercion variables are not an escape risk
       -- If an implication binds a coercion variable, it'll have equalities,
       -- so the "intervening given equalities" test above will catch it
       -- Coercion holes get filled with coercions, so again no problem.

{- Note [Do not unify Givens]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this GADT match
   data T a where
      T1 :: T Int
      ...

   f x = case x of
           T1 -> True
           ...

So we get f :: T alpha[1] -> beta[1]
          x :: T alpha[1]
and from the T1 branch we get the implication
   forall[2] (alpha[1] ~ Int) => beta[1] ~ Bool

Now, clearly we don't want to unify alpha:=Int!  Yet at the moment we
process [G] alpha[1] ~ Int, we don't have any given-equalities in the
inert set, and hence there are no given equalities to make alpha untouchable.

NB: if it were alpha[2] ~ Int, this argument wouldn't hold.  But that
never happens: invariant (GivenInv) in Note [TcLevel invariants]
in GHC.Tc.Utils.TcType.

Simple solution: never unify in Givens!
-}

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

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

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

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

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

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

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

tcLookupClass :: Name -> TcS Class
tcLookupClass :: Name -> TcS Class
tcLookupClass Name
c = forall a. TcM a -> TcS a
wrapTcS 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 = forall a. TcM a -> TcS a
wrapTcS 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 = forall a. TcM a -> TcS a
wrapTcS  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 = forall a. TcM a -> TcS a
wrapTcS 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 = forall a. TcM a -> TcS a
wrapTcS 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 -> Type -> TcS ()
checkWellStagedDFun CtLoc
loc InstanceWhat
what Type
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 forall a. Ord a => a -> a -> Bool
> Int
impLevel
  = forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$ forall a. CtLoc -> TcM a -> TcM a
TcM.setCtLocM CtLoc
loc 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
  = 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 (forall a. Outputable a => a -> SDoc
ppr Type
pred)

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

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

isFilledMetaTyVar :: TcTyVar -> TcS Bool
isFilledMetaTyVar :: TcTyVar -> TcS Bool
isFilledMetaTyVar TcTyVar
tv = 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 = 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 = forall a. TcM a -> TcS a
wrapTcS ([TcTyVar] -> TcM [TcTyVar]
TcM.zonkTyCoVarsAndFVList [TcTyVar]
tvs)

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

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

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

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

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

zonkWC :: WantedConstraints -> TcS WantedConstraints
zonkWC :: WantedConstraints -> TcS WantedConstraints
zonkWC WantedConstraints
wc = 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 = forall a. TcM a -> TcS a
wrapTcS (TcTyVar -> TcM TcTyVar
TcM.zonkTyCoVarKind TcTyVar
tv)

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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


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

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

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

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

cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
cloneMetaTyVar TcTyVar
tv = 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
  = forall a. TcM a -> TcS a
wrapTcS (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 <- 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 :: Type
kind = TCvSubst -> Type -> Type
substTyUnchecked TCvSubst
subst (TcTyVar -> Type
tyVarKind TcTyVar
tv)
             ty' :: Type
ty'  = TcTyVar -> Type
mkTyVarTy (Name -> Type -> TcTyVarDetails -> TcTyVar
mkTcTyVar Name
name Type
kind TcTyVarDetails
details)
       ; String -> SDoc -> TcM ()
TcM.traceTc String
"instFlexi" (forall a. Outputable a => a -> SDoc
ppr Type
ty')
       ; forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst -> TcTyVar -> Type -> TCvSubst
extendTvSubst TCvSubst
subst TcTyVar
tv Type
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 -> [Type] -> TcS ClsInstResult
matchGlobalInst DynFlags
dflags Bool
short_cut Class
cls [Type]
tys
  = forall a. TcM a -> TcS a
wrapTcS (DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
TcM.matchGlobalInst DynFlags
dflags Bool
short_cut Class
cls [Type]
tys)

tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar])
tcInstSkolTyVarsX :: TCvSubst -> [TcTyVar] -> TcS (TCvSubst, [TcTyVar])
tcInstSkolTyVarsX TCvSubst
subst [TcTyVar]
tvs = forall a. TcM a -> TcS a
wrapTcS 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
       ; forall a. TcM a -> TcS a
wrapTcS 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
       ; forall a. TcM a -> TcS a
wrapTcS forall a b. (a -> b) -> a -> b
$
         do { VarSet
tcvs <- 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
            ; forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
TcM.writeTcRef IORef VarSet
ref VarSet
tcvs' } }

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

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

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

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

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

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

Yuk!
-}

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

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

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

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

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

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

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

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

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

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

-- no equalities here. Use newWantedEq instead
newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
newWantedEvVarNC :: CtLoc -> Type -> TcS CtEvidence
newWantedEvVarNC = ShadowInfo -> CtLoc -> Type -> 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 -> Type -> TcS CtEvidence
newWantedEvVarNC_SI ShadowInfo
si CtLoc
loc Type
pty
  = do { TcTyVar
new_ev <- Type -> TcS TcTyVar
newEvVar Type
pty
       ; String -> SDoc -> TcS ()
traceTcS String
"Emitting new wanted" (forall a. Outputable a => a -> SDoc
ppr TcTyVar
new_ev SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
pty SDoc -> SDoc -> SDoc
$$
                                         CtLoc -> SDoc
pprCtLoc CtLoc
loc)
       ; forall (m :: * -> *) a. Monad m => a -> m a
return (CtWanted { ctev_pred :: Type
ctev_pred = Type
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 -> Type -> TcS MaybeNew
newWantedEvVar = ShadowInfo -> CtLoc -> Type -> 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 -> Type -> TcS MaybeNew
newWantedEvVar_SI ShadowInfo
si CtLoc
loc Type
pty
  = do { Maybe CtEvidence
mb_ct <- CtLoc -> Type -> TcS (Maybe CtEvidence)
lookupInInerts CtLoc
loc Type
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" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr CtEvidence
ctev
                    ; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ EvExpr -> MaybeNew
Cached (CtEvidence -> EvExpr
ctEvExpr CtEvidence
ctev) }
            Maybe CtEvidence
_ -> do { CtEvidence
ctev <- ShadowInfo -> CtLoc -> Type -> TcS CtEvidence
newWantedEvVarNC_SI ShadowInfo
si CtLoc
loc Type
pty
                    ; 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 -> Type -> TcS MaybeNew
newWanted = ShadowInfo -> CtLoc -> Type -> TcS MaybeNew
newWanted_SI ShadowInfo
WDeriv

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

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

emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS ()
emitNewDeriveds :: CtLoc -> [Type] -> TcS ()
emitNewDeriveds CtLoc
loc [Type]
preds
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
preds
  = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = do { [CtEvidence]
evs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (CtLoc -> Type -> TcS CtEvidence
newDerivedNC CtLoc
loc) [Type]
preds
       ; String -> SDoc -> TcS ()
traceTcS String
"Emitting new deriveds" (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 -> Type -> Type -> TcS ()
emitNewDerivedEq CtLoc
loc Role
role Type
ty1 Type
ty2
  = do { CtEvidence
ev <- CtLoc -> Type -> TcS CtEvidence
newDerivedNC CtLoc
loc (Role -> Type -> Type -> Type
mkPrimEqPredRole Role
role Type
ty1 Type
ty2)
       ; String -> SDoc -> TcS ()
traceTcS String
"Emitting new derived equality" (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 -> Type -> TcS CtEvidence
newDerivedNC CtLoc
loc Type
pred
  = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CtDerived { ctev_pred :: Type
ctev_pred = Type
pred, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc }

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

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

matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (CoercionN, TcType))
-- Given (F tys) return (ty, co), where co :: F tys ~N ty
matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (Coercion, Type))
matchFamTcM TyCon
tycon [Type]
args
  = do { (FamInstEnv, FamInstEnv)
fam_envs <- TcM (FamInstEnv, FamInstEnv)
FamInst.tcGetFamInstEnvs
       ; let match_fam_result :: Maybe (Coercion, Type)
match_fam_result
              = (FamInstEnv, FamInstEnv)
-> Role -> TyCon -> [Type] -> Maybe (Coercion, Type)
reduceTyFamApp_maybe (FamInstEnv, FamInstEnv)
fam_envs Role
Nominal TyCon
tycon [Type]
args
       ; String -> SDoc -> TcM ()
TcM.traceTc String
"matchFamTcM" forall a b. (a -> b) -> a -> b
$
         [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Matching:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (TyCon -> [Type] -> Type
mkTyConApp TyCon
tycon [Type]
args)
              , forall {a} {a}.
(Outputable a, Outputable a) =>
Maybe (a, a) -> SDoc
ppr_res Maybe (Coercion, Type)
match_fam_result ]
       ; forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Coercion, Type)
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
<+> forall a. Outputable a => a -> SDoc
ppr a
ty
                                        , String -> SDoc
text String
"Coercion:" SDoc -> SDoc -> 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 GHC.Tc.Solver.Monad.deferTcSForAllEq
-}

{-
************************************************************************
*                                                                      *
              Breaking type equality cycles
*                                                                      *
************************************************************************
-}

-- | Conditionally replace all type family applications in the RHS with fresh
-- variables, emitting givens that relate the type family application to the
-- variable. See Note [Type equality cycles] in GHC.Tc.Solver.Canonical.
-- This only works under conditions as described in the Note; otherwise, returns
-- Nothing.
breakTyEqCycle_maybe :: CtEvidence
                      -> CheckTyEqResult   -- result of checkTypeEq
                      -> CanEqLHS
                      -> TcType     -- RHS
                      -> TcS (Maybe (CoercionN, TcType))
                         -- new RHS that doesn't have any type families
                         -- co :: new type ~N old type
                         -- TcTyVar is the LHS tv; convenient for the caller
breakTyEqCycle_maybe :: CtEvidence
-> CheckTyEqResult
-> CanEqLHS
-> Type
-> TcS (Maybe (Coercion, Type))
breakTyEqCycle_maybe (CtLoc -> CtOrigin
ctLocOrigin forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> CtLoc
ctEvLoc -> CycleBreakerOrigin CtOrigin
_) CheckTyEqResult
_ CanEqLHS
_ Type
_
  -- see Detail (7) of Note
  = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

breakTyEqCycle_maybe CtEvidence
ev CheckTyEqResult
cte_result CanEqLHS
lhs Type
rhs
  | EqRel
NomEq <- EqRel
eq_rel

  , CheckTyEqResult
cte_result CheckTyEqResult -> CheckTyEqProblem -> Bool
`cterHasOnlyProblem` CheckTyEqProblem
cteSolubleOccurs
     -- only do this if the only problem is a soluble occurs-check
     -- See Detail (8) of the Note.

  = do { Bool
should_break <- TcS Bool
final_check
       ; if Bool
should_break then do { (Coercion
co, Type
new_rhs) <- Type -> TcS (Coercion, Type)
go Type
rhs
                                 ; forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (Coercion
co, Type
new_rhs)) }
                         else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing }
  where
    flavour :: CtFlavour
flavour = CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev
    eq_rel :: EqRel
eq_rel  = CtEvidence -> EqRel
ctEvEqRel CtEvidence
ev

    final_check :: TcS Bool
final_check
      | CtFlavour
Given <- CtFlavour
flavour
      = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
      | CtFlavour -> Bool
ctFlavourContainsDerived CtFlavour
flavour
      , TyVarLHS TcTyVar
lhs_tv <- CanEqLHS
lhs
      = do { TouchabilityTestResult
result <- CtFlavour -> TcTyVar -> Type -> TcS TouchabilityTestResult
touchabilityTest CtFlavour
Derived TcTyVar
lhs_tv Type
rhs
           ; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case TouchabilityTestResult
result of
               TouchabilityTestResult
Untouchable -> Bool
False
               TouchabilityTestResult
_           -> Bool
True }
      | Bool
otherwise
      = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    -- This could be considerably more efficient. See Detail (5) of Note.
    go :: TcType -> TcS (CoercionN, TcType)
    go :: Type -> TcS (Coercion, Type)
go Type
ty | Just Type
ty' <- Type -> Maybe Type
rewriterView Type
ty = Type -> TcS (Coercion, Type)
go Type
ty'
    go (Rep.TyConApp TyCon
tc [Type]
tys)
      | TyCon -> Bool
isTypeFamilyTyCon TyCon
tc  -- worried about whether this type family is not actually
                              -- causing trouble? See Detail (5) of Note.
      = do { let ([Type]
fun_args, [Type]
extra_args) = forall a. Int -> [a] -> ([a], [a])
splitAt (TyCon -> Int
tyConArity TyCon
tc) [Type]
tys
                 fun_app :: Type
fun_app                = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
fun_args
                 fun_app_kind :: Type
fun_app_kind           = HasDebugCallStack => Type -> Type
tcTypeKind Type
fun_app
           ; (Coercion
co, Type
new_ty) <- Type -> Type -> TcS (Coercion, Type)
emit_work Type
fun_app_kind Type
fun_app
           ; ([Coercion]
extra_args_cos, [Type]
extra_args') <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM Type -> TcS (Coercion, Type)
go [Type]
extra_args
           ; forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
co [Coercion]
extra_args_cos, Type -> [Type] -> Type
mkAppTys Type
new_ty [Type]
extra_args') }
              -- Worried that this substitution will change kinds?
              -- See Detail (3) of Note

      | Bool
otherwise
      = do { ([Coercion]
cos, [Type]
tys) <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM Type -> TcS (Coercion, Type)
go [Type]
tys
           ; forall (m :: * -> *) a. Monad m => a -> m a
return (HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tc [Coercion]
cos, TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys) }

    go (Rep.AppTy Type
ty1 Type
ty2)
      = do { (Coercion
co1, Type
ty1') <- Type -> TcS (Coercion, Type)
go Type
ty1
           ; (Coercion
co2, Type
ty2') <- Type -> TcS (Coercion, Type)
go Type
ty2
           ; forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> Coercion -> Coercion
mkAppCo Coercion
co1 Coercion
co2, Type -> Type -> Type
mkAppTy Type
ty1' Type
ty2') }
    go (Rep.FunTy AnonArgFlag
vis Type
w Type
arg Type
res)
      = do { (Coercion
co_w, Type
w') <- Type -> TcS (Coercion, Type)
go Type
w
           ; (Coercion
co_arg, Type
arg') <- Type -> TcS (Coercion, Type)
go Type
arg
           ; (Coercion
co_res, Type
res') <- Type -> TcS (Coercion, Type)
go Type
res
           ; forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
Nominal Coercion
co_w Coercion
co_arg Coercion
co_res, AnonArgFlag -> Type -> Type -> Type -> Type
mkFunTy AnonArgFlag
vis Type
w' Type
arg' Type
res') }
    go (Rep.CastTy Type
ty Coercion
cast_co)
      = do { (Coercion
co, Type
ty') <- Type -> TcS (Coercion, Type)
go Type
ty
             -- co :: ty' ~N ty
             -- return_co :: (ty' |> cast_co) ~ (ty |> cast_co)
           ; forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> Role -> Type -> Type -> Coercion -> Coercion
castCoercionKind1 Coercion
co Role
Nominal Type
ty' Type
ty Coercion
cast_co, Type -> Coercion -> Type
mkCastTy Type
ty' Coercion
cast_co) }

    go ty :: Type
ty@(Rep.TyVarTy {})    = forall {m :: * -> *}. Monad m => Type -> m (Coercion, Type)
skip Type
ty
    go ty :: Type
ty@(Rep.LitTy {})      = forall {m :: * -> *}. Monad m => Type -> m (Coercion, Type)
skip Type
ty
    go ty :: Type
ty@(Rep.ForAllTy {})   = forall {m :: * -> *}. Monad m => Type -> m (Coercion, Type)
skip Type
ty  -- See Detail (1) of Note
    go ty :: Type
ty@(Rep.CoercionTy {}) = forall {m :: * -> *}. Monad m => Type -> m (Coercion, Type)
skip Type
ty  -- See Detail (2) of Note

    skip :: Type -> m (Coercion, Type)
skip Type
ty = forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion
mkNomReflCo Type
ty, Type
ty)

    emit_work :: TcKind                   -- of the function application
              -> TcType                   -- original function application
              -> TcS (CoercionN, TcType)  -- rewritten type (the fresh tyvar)
    emit_work :: Type -> Type -> TcS (Coercion, Type)
emit_work Type
fun_app_kind Type
fun_app = case CtFlavour
flavour of
      CtFlavour
Given ->
        do { TcTyVar
new_tv <- forall a. TcM a -> TcS a
wrapTcS (Type -> TcM TcTyVar
TcM.newCycleBreakerTyVar Type
fun_app_kind)
           ; let new_ty :: Type
new_ty     = TcTyVar -> Type
mkTyVarTy TcTyVar
new_tv
                 given_pred :: Type
given_pred = Type -> Type -> Type -> Type -> Type
mkHeteroPrimEqPred Type
fun_app_kind Type
fun_app_kind
                                                 Type
fun_app Type
new_ty
                 given_term :: EvTerm
given_term = Coercion -> EvTerm
evCoercion forall a b. (a -> b) -> a -> b
$ Type -> Coercion
mkNomReflCo Type
new_ty  -- See Detail (4) of Note
           ; CtEvidence
new_given <- CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
new_loc (Type
given_pred, EvTerm
given_term)
           ; String -> SDoc -> TcS ()
traceTcS String
"breakTyEqCycle replacing type family in Given" (forall a. Outputable a => a -> SDoc
ppr CtEvidence
new_given)
           ; [CtEvidence] -> TcS ()
emitWorkNC [CtEvidence
new_given]
           ; (InertSet -> InertSet) -> TcS ()
updInertTcS forall a b. (a -> b) -> a -> b
$ \InertSet
is ->
               InertSet
is { inert_cycle_breakers :: CycleBreakerVarStack
inert_cycle_breakers = TcTyVar -> Type -> CycleBreakerVarStack -> CycleBreakerVarStack
insertCycleBreakerBinding TcTyVar
new_tv Type
fun_app
                                             (InertSet -> CycleBreakerVarStack
inert_cycle_breakers InertSet
is) }
           ; forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion
mkNomReflCo Type
new_ty, Type
new_ty) }
                -- Why reflexive? See Detail (4) of the Note

      CtFlavour
_derived_or_wd ->
        do { TcTyVar
new_tv <- forall a. TcM a -> TcS a
wrapTcS (Type -> TcM TcTyVar
TcM.newFlexiTyVar Type
fun_app_kind)
           ; let new_ty :: Type
new_ty = TcTyVar -> Type
mkTyVarTy TcTyVar
new_tv
           ; Coercion
co <- CtLoc -> Role -> Type -> Type -> TcS Coercion
emitNewWantedEq CtLoc
new_loc Role
Nominal Type
new_ty Type
fun_app
           ; forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion
co, Type
new_ty) }

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

-- does not fit scenario from Note
breakTyEqCycle_maybe CtEvidence
_ CheckTyEqResult
_ CanEqLHS
_ Type
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

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

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