diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver/Monad.hs')
| -rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 1945 |
1 files changed, 41 insertions, 1904 deletions
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 3428e811ad..96228fcce5 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -3,23 +3,13 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# OPTIONS_GHC -Wno-incomplete-record-updates -Wno-incomplete-uni-patterns #-} +{-# OPTIONS_GHC -Wno-incomplete-record-updates #-} --- | Type definitions for the constraint solver +-- | Monadic 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, @@ -27,6 +17,11 @@ module GHC.Tc.Solver.Monad ( nestTcS, nestImplicTcS, setEvBindsTcS, emitImplicationTcS, emitTvImplicationTcS, + selectNextWorkItem, + getWorkList, + updWorkListTcS, + pushLevelNoWorkList, + runTcPluginTcS, addUsedGRE, addUsedGREs, keepAlive, matchGlobalInst, TcM.ClsInstResult(..), @@ -62,18 +57,17 @@ module GHC.Tc.Solver.Monad ( 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, + lookupInertDict, -- The Model kickOutAfterUnification, @@ -82,14 +76,6 @@ module GHC.Tc.Solver.Monad ( 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, @@ -100,9 +86,6 @@ module GHC.Tc.Solver.Monad ( lookupFamAppInert, lookupFamAppCache, extendFamAppCache, pprKicked, - -- Inert function equalities - findFunEq, findFunEqsByTyCon, - instDFunType, -- Instantiation -- MetaTyVars @@ -153,7 +136,9 @@ 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.Solver.Types +import GHC.Tc.Solver.InertSet import GHC.Tc.Types.Evidence import GHC.Core.Class @@ -173,1173 +158,25 @@ 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 Data.List ( mapAccumL ) +import Data.List.NonEmpty ( NonEmpty(..) ) 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 { 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] - - , wl_rest :: [Ct] - - , wl_implics :: Bag Implication -- See Note [Residual implications] - } - -appendWorkList :: WorkList -> WorkList -> WorkList -appendWorkList - (WL { wl_eqs = eqs1, wl_rest = rest1 - , wl_implics = implics1 }) - (WL { wl_eqs = eqs2, wl_rest = rest2 - , wl_implics = implics2 }) - = WL { wl_eqs = eqs1 ++ eqs2 - , wl_rest = rest1 ++ rest2 - , wl_implics = implics1 `unionBags` implics2 } - -workListSize :: WorkList -> Int -workListSize (WL { wl_eqs = eqs, wl_rest = rest }) - = length eqs + length rest - -extendWorkListEq :: Ct -> WorkList -> WorkList -extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl } - -extendWorkListNonEq :: Ct -> WorkList -> WorkList --- Extension by non equality -extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl } - -extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList -extendWorkListDeriveds evs wl - = extendWorkListCts (map mkNonCanonical evs) wl - -extendWorkListImplic :: Implication -> WorkList -> WorkList -extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl } - -extendWorkListCt :: Ct -> WorkList -> WorkList --- Agnostic -extendWorkListCt ct wl - = case classifyPredType (ctPred ct) of - EqPred {} - -> extendWorkListEq ct wl - - ClassPred cls _ -- See Note [Prioritise class equalities] - | isEqPredClass cls - -> extendWorkListEq ct wl - - _ -> extendWorkListNonEq ct wl - -extendWorkListCts :: [Ct] -> WorkList -> WorkList --- Agnostic -extendWorkListCts cts wl = foldr extendWorkListCt wl cts - -isEmptyWorkList :: WorkList -> Bool -isEmptyWorkList (WL { wl_eqs = eqs, wl_rest = rest, wl_implics = implics }) - = null eqs && null rest && isEmptyBag implics - -emptyWorkList :: WorkList -emptyWorkList = WL { wl_eqs = [], wl_rest = [], wl_implics = emptyBag } - -selectWorkItem :: WorkList -> Maybe (Ct, WorkList) --- See Note [Prioritise equalities] -selectWorkItem wl@(WL { wl_eqs = eqs, wl_rest = rest }) - | ct:cts <- eqs = Just (ct, wl { wl_eqs = cts }) - | ct:cts <- rest = Just (ct, wl { wl_rest = cts }) - | otherwise = Nothing - -getWorkList :: TcS WorkList -getWorkList = do { wl_var <- getTcSWorkListRef - ; wrapTcS (TcM.readTcRef wl_var) } - -selectNextWorkItem :: TcS (Maybe Ct) --- Pick which work item to do next --- See Note [Prioritise equalities] -selectNextWorkItem - = do { wl_var <- getTcSWorkListRef - ; wl <- readTcRef wl_var - ; case selectWorkItem wl of { - Nothing -> return Nothing ; - Just (ct, new_wl) -> - do { -- checkReductionDepth (ctLoc ct) (ctPred ct) - -- This is done by GHC.Tc.Solver.Interact.chooseInstance - ; writeTcRef wl_var new_wl - ; return (Just ct) } } } - --- Pretty printing -instance Outputable WorkList where - ppr (WL { wl_eqs = eqs, wl_rest = rest, wl_implics = implics }) - = text "WL" <+> (braces $ - vcat [ ppUnless (null eqs) $ - text "Eqs =" <+> vcat (map ppr eqs) - , ppUnless (null rest) $ - text "Non-eqs =" <+> vcat (map ppr rest) - , ppUnless (isEmptyBag implics) $ - ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics))) - (text "(Implics omitted)") - ]) - - -{- ********************************************************************* -* * - InertSet: the inert set -* * -* * -********************************************************************* -} - -data InertSet - = IS { inert_cans :: InertCans - -- Canonical Given, Wanted, Derived - -- Sometimes called "the inert set" - - , inert_cycle_breakers :: [(TcTyVar, TcType)] - -- a list of CycleBreakerTv / original family applications - -- used to undo the cycle-breaking needed to handle - -- Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical - - , 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) - - , 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 (IS { inert_cans = ics - , inert_solved_dicts = solved_dicts }) - = vcat [ ppr ics - , ppUnless (null dicts) $ - text "Solved dicts =" <+> vcat (map ppr dicts) ] - where - dicts = bagToList (dictsToBag solved_dicts) - -emptyInertCans :: InertCans -emptyInertCans - = IC { inert_eqs = emptyDVarEnv - , inert_given_eq_lvl = topTcLevel - , inert_given_eqs = False - , inert_dicts = emptyDicts - , inert_safehask = emptyDicts - , inert_funeqs = emptyFunEqs - , inert_insts = [] - , inert_irreds = emptyCts } - -emptyInert :: InertSet -emptyInert - = IS { inert_cans = emptyInertCans - , inert_cycle_breakers = [] - , inert_famapp_cache = emptyFunEqs - , inert_solved_dicts = 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 { 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 - - , 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] - - , inert_dicts :: DictMap Ct - -- Dictionaries only - -- All fully rewritten (modulo flavour constraints) - -- wrt inert_eqs - - , inert_insts :: [QCInst] - - , 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" - - , 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]) - - , 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 - - , 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 Outputable - -- See Note [EqualCtList invariants] - -unitEqualCtList :: Ct -> EqualCtList -unitEqualCtList ct = EqualCtList (ct :| []) - -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 old_eqs) - | isWantedCt ct - , eq1 :| eqs <- old_eqs - = EqualCtList (eq1 :| ct : eqs) - | otherwise - = EqualCtList (ct `cons` old_eqs) - -filterEqualCtList :: (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList -filterEqualCtList pred (EqualCtList cts) - = fmap EqualCtList (nonEmpty $ NE.filter pred cts) - -equalCtListToList :: EqualCtList -> [Ct] -equalCtListToList (EqualCtList cts) = toList cts - -listToEqualCtList :: [Ct] -> Maybe EqualCtList --- NB: This does not maintain invariants other than having the EqualCtList be --- non-empty -listToEqualCtList cts = EqualCtList <$> nonEmpty 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 canEqOK and 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 (IC { inert_eqs = eqs - , inert_funeqs = funeqs, inert_dicts = dicts - , inert_safehask = safehask, inert_irreds = irreds - , inert_given_eq_lvl = ge_lvl - , inert_given_eqs = given_eqs - , inert_insts = insts }) - - = braces $ vcat - [ ppUnless (isEmptyDVarEnv eqs) $ - text "Equalities:" - <+> pprCts (foldDVarEnv folder emptyCts eqs) - , ppUnless (isEmptyTcAppMap funeqs) $ - text "Type-function equalities =" <+> pprCts (foldFunEqs folder funeqs emptyCts) - , ppUnless (isEmptyTcAppMap dicts) $ - text "Dictionaries =" <+> pprCts (dictsToBag dicts) - , ppUnless (isEmptyTcAppMap safehask) $ - text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask) - , ppUnless (isEmptyCts irreds) $ - text "Irreds =" <+> pprCts irreds - , ppUnless (null insts) $ - text "Given instances =" <+> vcat (map ppr insts) - , text "Innermost given equalities =" <+> ppr ge_lvl - , text "Given eqs at this level =" <+> ppr given_eqs - ] - where - folder (EqualCtList eqs) rest = nonEmptyToBag eqs `andCts` rest - {- ********************************************************************* * * Shadow constraints and improvement @@ -1409,7 +246,8 @@ 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]. + the Givens and Wanteds; see Note [EqualCtList invariants] + in GHC.Tc.Solver.Types. * We make Derived shadows only for Wanteds, not Givens. So we have only [G], not [GD] and [G] plus splitting. See @@ -1693,55 +531,6 @@ isImprovable _ = True {- ********************************************************************* * * - Inert equalities -* * -********************************************************************* -} - -addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs -addTyEq old_eqs tv ct - = extendDVarEnv_C add_eq old_eqs tv (unitEqualCtList ct) - where - add_eq old_eqs _ = addToEqualCtList ct old_eqs - -addCanFunEq :: FunEqMap EqualCtList -> TyCon -> [TcType] -> Ct - -> FunEqMap EqualCtList -addCanFunEq old_eqs fun_tc fun_args ct - = alterTcApp old_eqs fun_tc fun_args upd - where - upd (Just old_equal_ct_list) = Just $ addToEqualCtList ct old_equal_ct_list - upd Nothing = Just $ unitEqualCtList ct - -foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b -foldTyEqs k eqs z - = foldDVarEnv (\(EqualCtList cts) z -> foldr k z cts) z eqs - -findTyEqs :: InertCans -> TyVar -> [Ct] -findTyEqs icans tv = maybe [] id (fmap @Maybe equalCtListToList $ - lookupDVarEnv (inert_eqs icans) tv) - -delEq :: InertCans -> CanEqLHS -> TcType -> InertCans -delEq ic lhs rhs = case lhs of - TyVarLHS tv - -> ic { inert_eqs = alterDVarEnv upd (inert_eqs ic) tv } - TyFamLHS tf args - -> ic { inert_funeqs = alterTcApp (inert_funeqs ic) tf args upd } - where - isThisOne :: Ct -> Bool - isThisOne (CEqCan { cc_rhs = t1 }) = tcEqTypeNoKindCheck rhs t1 - isThisOne other = pprPanic "delEq" (ppr lhs $$ ppr ic $$ ppr other) - - upd :: Maybe EqualCtList -> Maybe EqualCtList - upd (Just eq_ct_list) = filterEqualCtList (not . isThisOne) eq_ct_list - upd Nothing = Nothing - -findEq :: InertCans -> CanEqLHS -> [Ct] -findEq icans (TyVarLHS tv) = findTyEqs icans tv -findEq icans (TyFamLHS fun_tc fun_args) - = maybe [] id (fmap @Maybe equalCtListToList $ - findFunEq (inert_funeqs icans) fun_tc fun_args) - -{- ********************************************************************* -* * Inert instances: inert_insts * * ********************************************************************* -} @@ -1829,7 +618,7 @@ addInertCan ct ; ct <- maybeEmitShadow ics ct ; ics <- maybeKickOut ics ct ; tclvl <- getTcLevel - ; setInertCans (add_item tclvl ics ct) + ; setInertCans (addInertItem tclvl ics ct) ; traceTcS "addInertCan }" $ empty } @@ -1842,54 +631,6 @@ maybeKickOut ics ct | otherwise = return ics -add_item :: TcLevel -> InertCans -> Ct -> InertCans -add_item tc_lvl - ics@(IC { inert_funeqs = funeqs, inert_eqs = eqs }) - item@(CEqCan { cc_lhs = lhs }) - = updateGivenEqs tc_lvl item $ - case lhs of - TyFamLHS tc tys -> ics { inert_funeqs = addCanFunEq funeqs tc tys item } - TyVarLHS tv -> ics { inert_eqs = addTyEq eqs tv item } - -add_item tc_lvl ics@(IC { inert_irreds = irreds }) item@(CIrredCan {}) - = updateGivenEqs tc_lvl item $ -- An Irred might turn out to be an - -- equality, so we play safe - ics { inert_irreds = irreds `Bag.snocBag` item } - -add_item _ ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) - = ics { inert_dicts = addDictCt (inert_dicts ics) cls tys item } - -add_item _ _ item - = pprPanic "upd_inert set: can't happen! Inserting " $ - ppr 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 tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl }) - | not (isGivenCt ct) = inerts - | not_equality ct = inerts -- See Note [Let-bound skolems] - | otherwise = inerts { inert_given_eq_lvl = ge_lvl' - , inert_given_eqs = True } - where - ge_lvl' | mentionsOuterVar tclvl (ctEvidence ct) - -- Includes things like (c a), which *might* be an equality - = tclvl - | otherwise - = 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 (CEqCan { cc_lhs = TyVarLHS tv }) = not (isOuterTyVar tclvl tv) - not_equality (CDictCan {}) = True - not_equality _ = False - ----------------------------------------- kickOutRewritable :: CtFlavourRole -- Flavour/role of the equality that -- is being added to the inert set @@ -1897,7 +638,7 @@ kickOutRewritable :: CtFlavourRole -- Flavour/role of the equality that -> InertCans -> TcS (Int, InertCans) kickOutRewritable new_fr new_lhs ics - = do { let (kicked_out, ics') = kick_out_rewritable new_fr new_lhs ics + = do { let (kicked_out, ics') = kickOutRewritableLHS new_fr new_lhs ics n_kicked = workListSize kicked_out ; unless (n_kicked == 0) $ @@ -1924,194 +665,6 @@ kickOutRewritable new_fr new_lhs ics ; return (n_kicked, 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 new_fr new_lhs - ics@(IC { inert_eqs = tv_eqs - , inert_dicts = dictmap - , inert_funeqs = funeqmap - , inert_irreds = irreds - , inert_insts = old_insts }) - | not (new_fr `eqMayRewriteFR` new_fr) - = (emptyWorkList, 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] - - | otherwise - = (kicked_out, inert_cans_in) - where - -- inert_safehask stays unchanged; is that right? - inert_cans_in = ics { inert_eqs = tv_eqs_in - , inert_dicts = dicts_in - , inert_funeqs = feqs_in - , inert_irreds = irs_in - , inert_insts = 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 = foldr extendWorkListCt - (emptyWorkList { wl_eqs = tv_eqs_out ++ feqs_out }) - ((dicts_out `andCts` irs_out) - `extendCtsList` insts_out) - - (tv_eqs_out, tv_eqs_in) = foldDVarEnv (kick_out_eqs extend_tv_eqs) - ([], emptyDVarEnv) tv_eqs - (feqs_out, feqs_in) = foldFunEqs (kick_out_eqs extend_fun_eqs) - funeqmap ([], emptyFunEqs) - (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap - (irs_out, irs_in) = partitionBag kick_out_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] - (insts_out, insts_in) - | fr_may_rewrite (Given, NomEq) -- All the insts are Givens - = partitionWith kick_out_qci old_insts - | otherwise - = ([], old_insts) - kick_out_qci qci - | let ev = qci_ev qci - , fr_can_rewrite_ty NomEq (ctEvPred (qci_ev qci)) - = Left (mkNonCanonical ev) - | otherwise - = Right qci - - (_, new_role) = new_fr - - fr_tv_can_rewrite_ty :: TyVar -> EqRel -> Type -> Bool - fr_tv_can_rewrite_ty new_tv role ty - = anyRewritableTyVar True role can_rewrite ty - -- True: ignore casts and coercions - where - can_rewrite :: EqRel -> TyVar -> Bool - can_rewrite old_role tv = new_role `eqCanRewrite` old_role && tv == new_tv - - fr_tf_can_rewrite_ty :: TyCon -> [TcType] -> EqRel -> Type -> Bool - fr_tf_can_rewrite_ty new_tf new_tf_args role ty - = anyRewritableTyFamApp role can_rewrite ty - where - can_rewrite :: EqRel -> TyCon -> [TcType] -> Bool - can_rewrite old_role old_tf old_tf_args - = new_role `eqCanRewrite` old_role && - tcEqTyConApps new_tf new_tf_args old_tf 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 = case new_lhs of - TyVarLHS new_tv -> fr_tv_can_rewrite_ty new_tv - TyFamLHS new_tf new_tf_args -> fr_tf_can_rewrite_ty new_tf new_tf_args - - fr_may_rewrite :: CtFlavourRole -> Bool - fr_may_rewrite fs = new_fr `eqMayRewriteFR` 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 = case new_lhs of - TyVarLHS new_tv -> \ct -> let fs@(_,role) = ctFlavourRole ct in - fr_may_rewrite fs - && fr_tv_can_rewrite_ty new_tv role (ctPred ct) - TyFamLHS new_tf new_tf_args - -> \ct -> let fs@(_, role) = ctFlavourRole ct in - fr_may_rewrite fs - && fr_tf_can_rewrite_ty new_tf new_tf_args role (ctPred ct) - - extend_tv_eqs :: InertEqs -> CanEqLHS -> EqualCtList -> InertEqs - extend_tv_eqs eqs (TyVarLHS tv) cts = extendDVarEnv eqs tv cts - extend_tv_eqs eqs other _cts = pprPanic "extend_tv_eqs" (ppr eqs $$ ppr other) - - extend_fun_eqs :: FunEqMap EqualCtList -> CanEqLHS -> EqualCtList - -> FunEqMap EqualCtList - extend_fun_eqs eqs (TyFamLHS fam_tc fam_args) cts - = insertTcApp eqs fam_tc fam_args cts - extend_fun_eqs eqs other _cts = pprPanic "extend_fun_eqs" (ppr eqs $$ ppr other) - - kick_out_eqs :: (container -> CanEqLHS -> EqualCtList -> container) - -> EqualCtList -> ([Ct], container) - -> ([Ct], container) - kick_out_eqs extend eqs (acc_out, acc_in) - = (eqs_out `chkAppend` acc_out, case listToEqualCtList eqs_in of - Nothing -> acc_in - Just eqs_in_ecl@(EqualCtList (eq1 :| _)) - -> extend acc_in (cc_lhs eq1) eqs_in_ecl) - where - (eqs_out, eqs_in) = partition kick_out_eq (equalCtListToList eqs) - - -- Implements criteria K1-K3 in Note [Extending the inert equalities] - kick_out_eq (CEqCan { cc_lhs = lhs, cc_rhs = rhs_ty - , cc_ev = ev, cc_eq_rel = eq_rel }) - | not (fr_may_rewrite fs) - = 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 _ <- lhs - , fs `eqMayRewriteFR` new_fr - = False -- (K4) Keep it in the inert set if the LHS is a tyvar and - -- it can rewrite the work item. See Note [K4] - - | fr_can_rewrite_ty eq_rel (canEqLHSType lhs) - = True -- (K1) - -- The above check redundantly checks the role & flavour, - -- but it's very convenient - - | kick_out_for_inertness = True -- (K2) - | kick_out_for_completeness = True -- (K3) - | otherwise = False - - where - fs = (ctEvFlavour ev, eq_rel) - kick_out_for_inertness - = (fs `eqMayRewriteFR` fs) -- (K2a) - && fr_can_rewrite_ty eq_rel rhs_ty -- (K2b) - - kick_out_for_completeness -- (K3) and Note [K3: completeness of solving] - = case eq_rel of - NomEq -> rhs_ty `eqType` canEqLHSType new_lhs -- (K3a) - ReprEq -> is_can_eq_lhs_head new_lhs rhs_ty -- (K3b) - - kick_out_eq ct = pprPanic "keep_eq" (ppr ct) - - is_can_eq_lhs_head (TyVarLHS tv) = go - where - go (Rep.TyVarTy tv') = tv == tv' - go (Rep.AppTy fun _) = go fun - go (Rep.CastTy ty _) = go ty - go (Rep.TyConApp {}) = False - go (Rep.LitTy {}) = False - go (Rep.ForAllTy {}) = False - go (Rep.FunTy {}) = False - go (Rep.CoercionTy {}) = False - is_can_eq_lhs_head (TyFamLHS fun_tc fun_args) = go - where - go (Rep.TyVarTy {}) = False - go (Rep.AppTy {}) = False -- no TyConApp to the left of an AppTy - go (Rep.CastTy ty _) = go ty - go (Rep.TyConApp tc args) = tcEqTyConApps fun_tc fun_args tc args - go (Rep.LitTy {}) = False - go (Rep.ForAllTy {}) = False - go (Rep.FunTy {}) = False - go (Rep.CoercionTy {}) = False - kickOutAfterUnification :: TcTyVar -> TcS Int kickOutAfterUnification new_tv = do { ics <- getInertCans @@ -2165,69 +718,6 @@ kickOutAfterFillingCoercionHole hole filled_co else Right updated_ct kick_ct other = Right 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 ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) @@ -2251,7 +741,7 @@ getSafeOverlapFailures -------------- addSolvedDict :: InstanceWhat -> CtEvidence -> Class -> [Type] -> TcS () -- Conditionally add a new item in the solved set of the monad --- See Note [Solved dictionaries] +-- See Note [Solved dictionaries] in GHC.Tc.Solver.InertSet addSolvedDict what item cls tys | isWanted item , instanceReturnsDictCon what @@ -2434,7 +924,7 @@ getUnsolvedInerts getHasGivenEqs :: TcLevel -- TcLevel of this implication -> TcS ( HasGivenEqs -- are there Given equalities? , Cts ) -- Insoluble equalities arising from givens --- See Note [Tracking Given equalities] +-- See Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet getHasGivenEqs tclvl = do { inerts@(IC { inert_irreds = irreds , inert_given_eqs = given_eqs @@ -2446,7 +936,7 @@ getHasGivenEqs tclvl -- 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 + -- Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet has_ge | ge_lvl == tclvl = MaybeGivenEqs | given_eqs = LocalGivenEqs | otherwise = NoGivenEqs @@ -2459,132 +949,6 @@ getHasGivenEqs tclvl , text "Insols:" <+> ppr insols] ; return (has_ge, insols) } -mentionsOuterVar :: TcLevel -> CtEvidence -> Bool -mentionsOuterVar tclvl ev - = anyFreeVarsOfType (isOuterTyVar tclvl) $ - ctEvPred ev - -isOuterTyVar :: TcLevel -> TyCoVar -> Bool --- True of a type variable that comes from a --- shallower level than the ambient level (tclvl) -isOuterTyVar tclvl tv - | isTyVar tv = assertPpr (not (isTouchableMetaTyVar tclvl tv)) (ppr tv <+> ppr tclvl) $ - tclvl `strictlyDeeperThan` tcTyVarLevel 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. - | otherwise = 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 loc_w pred_w inerts@(IS { inert_cans = inert_cans }) - = filterBag matchable_given 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 - | Just (clas, _) <- getClassPredTys_maybe pred_w - = findDictsByClass (inert_dicts inert_cans) clas - `unionBags` inert_irreds inert_cans - | otherwise - = inert_irreds inert_cans - - matchable_given :: Ct -> Bool - matchable_given ct - | CtGiven { ctev_loc = loc_g, ctev_pred = pred_g } <- ctEvidence ct - = mightEqualLater inerts pred_g loc_g pred_w loc_w - - | otherwise - = 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 (IS { inert_cycle_breakers = cbvs }) - given_pred given_loc wanted_pred wanted_loc - | prohibitedSuperClassSolve given_loc wanted_loc - = False - - | otherwise - = case tcUnifyTysFG bind_fun [flattened_given] [flattened_wanted] of - SurelyApart -> False -- types that are surely apart do not equal later - MaybeApart MARInfinite _ -> False -- see Example 7 in the Note. - _ -> True - - where - in_scope = mkInScopeSet $ tyCoVarsOfTypes [given_pred, 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. - ([flattened_given, flattened_wanted], var_mapping) - = flattenTysX in_scope [given_pred, wanted_pred] - - bind_fun :: BindFun - bind_fun tv rhs_ty - | isMetaTyVar tv - , can_unify tv (metaTyVarInfo tv) rhs_ty - -- this checks for CycleBreakerTvs and TyVarTvs; forgetting - -- the latter was #19106. - = BindMe - - -- See Examples 4, 5, and 6 from the Note - | Just (_fam_tc, fam_args) <- lookupVarEnv var_mapping tv - , anyFreeVarsOfTypes mentions_meta_ty_var fam_args - = BindMe - - | otherwise - = 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 tv - | isMetaTyVar tv - = case metaTyVarInfo tv of - -- See Examples 8 and 9 in the Note - CycleBreakerTv - | Just tyfam_app <- lookup tv cbvs - -> anyFreeVarsOfType mentions_meta_ty_var tyfam_app - | otherwise - -> pprPanic "mightEqualLater finds an unbound cbv" (ppr tv $$ ppr cbvs) - _ -> True - | otherwise - = False - - -- like canSolveByUnification, but allows cbv variables to unify - can_unify :: TcTyVar -> MetaInfo -> Type -> Bool - can_unify _lhs_tv TyVarTv rhs_ty -- see Example 3 from the Note - | Just rhs_tv <- tcGetTyVar_maybe rhs_ty - = case tcTyVarDetails rhs_tv of - MetaTv { mtv_info = TyVarTv } -> True - MetaTv {} -> False -- could unify with anything - SkolemTv {} -> True - RuntimeUnk -> True - | otherwise -- not a var on the RHS - = False - can_unify lhs_tv _other _rhs_ty = mentions_meta_ty_var lhs_tv - -prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool --- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance -prohibitedSuperClassSolve from_loc solve_loc - | GivenOrigin (InstSC given_size) <- ctLocOrigin from_loc - , ScOrigin wanted_size <- ctLocOrigin solve_loc - = given_size >= wanted_size - | otherwise - = False - {- Note [Unsolved Derived equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In getUnsolvedInerts, we return a derived equality from the inert_eqs @@ -2777,240 +1141,6 @@ dropFromFamAppCache varset foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b foldIrreds k irreds z = foldr k z 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 m = isEmptyDTyConEnv m - -emptyTcAppMap :: TcAppMap a -emptyTcAppMap = emptyDTyConEnv - -findTcApp :: TcAppMap a -> TyCon -> [Type] -> Maybe a -findTcApp m tc tys = do { tys_map <- lookupDTyConEnv m tc - ; lookupTM tys tys_map } - -delTcApp :: TcAppMap a -> TyCon -> [Type] -> TcAppMap a -delTcApp m tc tys = adjustDTyConEnv (deleteTM tys) m tc - -insertTcApp :: TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a -insertTcApp m tc tys ct = alterDTyConEnv alter_tm m tc - where - alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM)) - -alterTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a -alterTcApp m tc tys upd = alterDTyConEnv alter_tm m tc - where - alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a) - alter_tm m_elt = Just (alterTM tys upd (m_elt `orElse` emptyTM)) - -filterTcAppMap :: forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a -filterTcAppMap f m = mapMaybeDTyConEnv one_tycon m - where - one_tycon :: ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a) - one_tycon tm - | isEmptyTM filtered_tm = Nothing - | otherwise = Just filtered_tm - where - filtered_tm = filterTM f tm - -tcAppMapToBag :: TcAppMap a -> Bag a -tcAppMapToBag m = foldTcAppMap consBag m emptyBag - -foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b -foldTcAppMap k m z = foldDTyConEnv (foldTM k) z 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 = emptyTcAppMap - -findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a -findDict m loc cls tys - | hasIPSuperClasses cls tys -- See Note [Tuples hiding implicit parameters] - = Nothing - - | Just {} <- isCallStackPred cls tys - , OccurrenceOf {} <- ctLocOrigin loc - = Nothing -- See Note [Solving CallStack constraints] - - | otherwise - = findTcApp m (classTyCon cls) tys - -findDictsByClass :: DictMap a -> Class -> Bag a -findDictsByClass m cls - | Just tm <- lookupDTyConEnv m (classTyCon cls) = foldTM consBag tm emptyBag - | otherwise = emptyBag - -delDict :: DictMap a -> Class -> [Type] -> DictMap a -delDict m cls tys = delTcApp m (classTyCon cls) tys - -addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a -addDict m cls tys item = insertTcApp m (classTyCon cls) tys 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 m cls tys new_ct = alterTcApp m (classTyCon cls) tys xt_ct - where - new_ct_ev = ctEvidence new_ct - - xt_ct :: Maybe Ct -> Maybe Ct - xt_ct (Just old_ct) - | CtWanted { ctev_nosh = WOnly } <- old_ct_ev - , CtDerived {} <- new_ct_ev - = Just (old_ct { cc_ev = old_ct_ev { ctev_nosh = WDeriv }}) - | CtDerived {} <- old_ct_ev - , CtWanted { ctev_nosh = WOnly } <- new_ct_ev - = Just (new_ct { cc_ev = new_ct_ev { ctev_nosh = WDeriv }}) - where - old_ct_ev = ctEvidence old_ct - - xt_ct _ = Just new_ct - -addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct -addDictsByClass m cls items - = extendDTyConEnv m (classTyCon cls) (foldr add emptyTM items) - where - add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm - add ct _ = pprPanic "addDictsByClass" (ppr ct) - -filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct -filterDicts f m = filterTcAppMap f m - -partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct) -partitionDicts f m = foldTcAppMap k m (emptyBag, emptyDicts) - where - k ct (yeses, noes) | f ct = (ct `consBag` yeses, noes) - | otherwise = (yeses, add ct noes) - add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) m - = addDict m cls tys ct - add ct _ = pprPanic "partitionDicts" (ppr ct) - -dictsToBag :: DictMap a -> Bag a -dictsToBag = tcAppMapToBag - -foldDicts :: (a -> b -> b) -> DictMap a -> b -> b -foldDicts = foldTcAppMap - -emptyDicts :: DictMap a -emptyDicts = emptyTcAppMap - - -{- ********************************************************************* -* * - FunEqMap -* * -********************************************************************* -} - -type FunEqMap a = TcAppMap a -- A map whose key is a (TyCon, [Type]) pair - -emptyFunEqs :: TcAppMap a -emptyFunEqs = emptyTcAppMap - -findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a -findFunEq m tc tys = findTcApp m tc 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 m tc - | Just tm <- lookupDTyConEnv m tc = foldTM (:) tm [] - | otherwise = [] - -foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b -foldFunEqs = foldTcAppMap - -insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a -insertFunEq m tc tys val = insertTcApp m tc tys val - {- ************************************************************************ * * @@ -3050,7 +1180,7 @@ data TcSEnv tcs_inerts :: IORef InertSet, -- Current inert set - -- See Note [WorkList priorities] and + -- See Note [WorkList priorities] in GHC.Tc.Solver.InertSet tcs_worklist :: IORef WorkList -- Current worklist } @@ -3497,6 +1627,24 @@ reportUnifications (TcS thing_inside) getDefaultInfo :: TcS ([Type], (Bool, Bool)) getDefaultInfo = wrapTcS TcM.tcGetDefaultTys +getWorkList :: TcS WorkList +getWorkList = do { wl_var <- getTcSWorkListRef + ; wrapTcS (TcM.readTcRef wl_var) } + +selectNextWorkItem :: TcS (Maybe Ct) +-- Pick which work item to do next +-- See Note [Prioritise equalities] +selectNextWorkItem + = do { wl_var <- getTcSWorkListRef + ; wl <- readTcRef wl_var + ; case selectWorkItem wl of { + Nothing -> return Nothing ; + Just (ct, new_wl) -> + do { -- checkReductionDepth (ctLoc ct) (ctPred ct) + -- This is done by GHC.Tc.Solver.Interact.chooseInstance + ; writeTcRef wl_var new_wl + ; return (Just ct) } } } + -- Just get some environments needed for instance looking up and matching -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -3936,7 +2084,8 @@ emitNewDerivedEq loc role ty1 ty2 ; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc) ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) } -- Very important: put in the wl_eqs - -- See Note [Prioritise equalities] (Avoiding fundep iteration) + -- See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet + -- (Avoiding fundep iteration) newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence newDerivedNC loc pred @@ -3974,18 +2123,6 @@ matchFamTcM tycon args , text "Coercion:" <+> ppr 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 variable cycles |