{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module GHC.Tc.Solver.InertSet ( -- * The work list WorkList(..), isEmptyWorkList, emptyWorkList, extendWorkListNonEq, extendWorkListCt, extendWorkListCts, extendWorkListCtList, extendWorkListEq, extendWorkListEqs, appendWorkList, extendWorkListImplic, workListSize, selectWorkItem, -- * The inert set InertSet(..), InertCans(..), emptyInert, noMatchableGivenDicts, noGivenNewtypeReprEqs, updGivenEqs, mightEqualLater, prohibitedSuperClassSolve, -- * Inert equalities InertEqs, foldTyEqs, delEq, findEq, partitionInertEqs, partitionFunEqs, foldFunEqs, addEqToCans, -- * Inert Dicts updDicts, delDict, addDict, filterDicts, partitionDicts, addSolvedDict, -- * Inert Irreds InertIrreds, delIrred, addIrreds, addIrred, foldIrreds, findMatchingIrreds, updIrreds, addIrredToCans, -- * Kick-out KickOutSpec(..), kickOutRewritableLHS, -- * Cycle breaker vars CycleBreakerVarStack, pushCycleBreakerVarStack, addCycleBreakerBindings, forAllCycleBreakerBindings_, -- * Solving one from another InteractResult(..), solveOneFromTheOther ) where import GHC.Prelude import GHC.Tc.Types.Constraint import GHC.Tc.Types.Origin import GHC.Tc.Solver.Types import GHC.Tc.Utils.TcType import GHC.Types.Var import GHC.Types.Var.Env import GHC.Types.Var.Set import GHC.Types.Basic( SwapFlag(..) ) import GHC.Core.Reduction import GHC.Core.Predicate import GHC.Core.TyCo.FVs import qualified GHC.Core.TyCo.Rep as Rep import GHC.Core.Class( Class ) import GHC.Core.TyCon import GHC.Core.Class( classTyCon ) import GHC.Core.Unify import GHC.Utils.Misc ( partitionWith ) import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Data.Maybe import GHC.Data.Bag import Data.List.NonEmpty ( NonEmpty(..), (<|) ) import qualified Data.List.NonEmpty as NE import Data.Function ( on ) import Control.Monad ( forM_ ) {- ************************************************************************ * * * 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 over class constraints: * (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 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 equalities in the work-list), but generates yet more fundeps Solution: prioritise 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. Further refinements: * Among the equalities we prioritise ones with an empty rewriter set; see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint, wrinkle (W1). * Among equalities with an empty rewriter set, we prioritise nominal equalities. * They have more rewriting power, so doing them first is better. * Prioritising them ameliorates the incompleteness of newtype solving: see (Ex2) in Note [Decomposing newtype equalities] in GHC.Tc.Solver.Equality. 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. 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 -} -- See Note [WorkList priorities] data WorkList = WL { WorkList -> [Ct] wl_eqs_N :: [Ct] -- /Nominal/ equalities (s ~#N t), (s ~ t), (s ~~ t) -- with empty rewriter set , WorkList -> [Ct] wl_eqs_X :: [Ct] -- CEqCan, CDictCan, CIrredCan -- with empty rewriter set -- All other equalities: 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_rw_eqs :: [Ct] -- Like wl_eqs, but ones that have a non-empty -- rewriter set; or, more precisely, did when -- added to the WorkList -- We prioritise wl_eqs over wl_rw_eqs; -- see Note [Prioritise Wanteds with empty RewriterSet] -- in GHC.Tc.Types.Constraint for more details. , 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_N :: WorkList -> [Ct] wl_eqs_N = [Ct] eqs1_N, wl_eqs_X :: WorkList -> [Ct] wl_eqs_X = [Ct] eqs1_X, wl_rw_eqs :: WorkList -> [Ct] wl_rw_eqs = [Ct] rw_eqs1 , wl_rest :: WorkList -> [Ct] wl_rest = [Ct] rest1, wl_implics :: WorkList -> Bag Implication wl_implics = Bag Implication implics1 }) (WL { wl_eqs_N :: WorkList -> [Ct] wl_eqs_N = [Ct] eqs2_N, wl_eqs_X :: WorkList -> [Ct] wl_eqs_X = [Ct] eqs2_X, wl_rw_eqs :: WorkList -> [Ct] wl_rw_eqs = [Ct] rw_eqs2 , wl_rest :: WorkList -> [Ct] wl_rest = [Ct] rest2, wl_implics :: WorkList -> Bag Implication wl_implics = Bag Implication implics2 }) = WL { wl_eqs_N :: [Ct] wl_eqs_N = [Ct] eqs1_N [Ct] -> [Ct] -> [Ct] forall a. [a] -> [a] -> [a] ++ [Ct] eqs2_N , wl_eqs_X :: [Ct] wl_eqs_X = [Ct] eqs1_X [Ct] -> [Ct] -> [Ct] forall a. [a] -> [a] -> [a] ++ [Ct] eqs2_X , wl_rw_eqs :: [Ct] wl_rw_eqs = [Ct] rw_eqs1 [Ct] -> [Ct] -> [Ct] forall a. [a] -> [a] -> [a] ++ [Ct] rw_eqs2 , wl_rest :: [Ct] wl_rest = [Ct] rest1 [Ct] -> [Ct] -> [Ct] forall a. [a] -> [a] -> [a] ++ [Ct] rest2 , wl_implics :: Bag Implication wl_implics = Bag Implication implics1 Bag Implication -> Bag Implication -> Bag Implication forall a. Bag a -> Bag a -> Bag a `unionBags` Bag Implication implics2 } workListSize :: WorkList -> Int workListSize :: WorkList -> ScDepth workListSize (WL { wl_eqs_N :: WorkList -> [Ct] wl_eqs_N = [Ct] eqs_N, wl_eqs_X :: WorkList -> [Ct] wl_eqs_X = [Ct] eqs_X, wl_rw_eqs :: WorkList -> [Ct] wl_rw_eqs = [Ct] rw_eqs, wl_rest :: WorkList -> [Ct] wl_rest = [Ct] rest }) = [Ct] -> ScDepth forall a. [a] -> ScDepth forall (t :: * -> *) a. Foldable t => t a -> ScDepth length [Ct] eqs_N ScDepth -> ScDepth -> ScDepth forall a. Num a => a -> a -> a + [Ct] -> ScDepth forall a. [a] -> ScDepth forall (t :: * -> *) a. Foldable t => t a -> ScDepth length [Ct] eqs_X ScDepth -> ScDepth -> ScDepth forall a. Num a => a -> a -> a + [Ct] -> ScDepth forall a. [a] -> ScDepth forall (t :: * -> *) a. Foldable t => t a -> ScDepth length [Ct] rw_eqs ScDepth -> ScDepth -> ScDepth forall a. Num a => a -> a -> a + [Ct] -> ScDepth forall a. [a] -> ScDepth forall (t :: * -> *) a. Foldable t => t a -> ScDepth length [Ct] rest extendWorkListEq :: RewriterSet -> Ct -> WorkList -> WorkList extendWorkListEq :: RewriterSet -> Ct -> WorkList -> WorkList extendWorkListEq RewriterSet rewriters Ct ct wl :: WorkList wl@(WL { wl_eqs_N :: WorkList -> [Ct] wl_eqs_N = [Ct] eqs_N, wl_eqs_X :: WorkList -> [Ct] wl_eqs_X = [Ct] eqs_X, wl_rw_eqs :: WorkList -> [Ct] wl_rw_eqs = [Ct] rw_eqs }) | RewriterSet -> Bool isEmptyRewriterSet RewriterSet rewriters -- A wanted that has not been rewritten -- isEmptyRewriterSet: see Note [Prioritise Wanteds with empty RewriterSet] -- in GHC.Tc.Types.Constraint = if Type -> Bool isNomEqPred (Ct -> Type ctPred Ct ct) then WorkList wl { wl_eqs_N = ct : eqs_N } else WorkList wl { wl_eqs_X = ct : eqs_X } | Bool otherwise = WorkList wl { wl_rw_eqs = ct : rw_eqs } extendWorkListEqs :: RewriterSet -> Bag Ct -> WorkList -> WorkList -- Add [eq1,...,eqn] to the work-list -- They all have the same rewriter set -- The constraints will be solved in left-to-right order: -- see Note [Work-list ordering] in GHC.Tc.Solver.Equality -- -- Precondition: new_eqs is non-empty extendWorkListEqs :: RewriterSet -> Bag Ct -> WorkList -> WorkList extendWorkListEqs RewriterSet rewriters Bag Ct new_eqs wl :: WorkList wl@(WL { wl_eqs_N :: WorkList -> [Ct] wl_eqs_N = [Ct] eqs_N, wl_eqs_X :: WorkList -> [Ct] wl_eqs_X = [Ct] eqs_X, wl_rw_eqs :: WorkList -> [Ct] wl_rw_eqs = [Ct] rw_eqs }) | RewriterSet -> Bool isEmptyRewriterSet RewriterSet rewriters -- isEmptyRewriterSet: see Note [Prioritise Wanteds with empty RewriterSet] -- in GHC.Tc.Types.Constraint = case (Ct -> Bool) -> Bag Ct -> (Bag Ct, Bag Ct) forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a) partitionBag Ct -> Bool is_nominal Bag Ct new_eqs of (Bag Ct new_eqs_N, Bag Ct new_eqs_X) | Bag Ct -> Bool forall a. Bag a -> Bool isEmptyBag Bag Ct new_eqs_N -> WorkList wl { wl_eqs_X = new_eqs_X `push_on_front` eqs_X } | Bag Ct -> Bool forall a. Bag a -> Bool isEmptyBag Bag Ct new_eqs_X -> WorkList wl { wl_eqs_N = new_eqs_N `push_on_front` eqs_N } | Bool otherwise -> WorkList wl { wl_eqs_N = new_eqs_N `push_on_front` eqs_N , wl_eqs_X = new_eqs_X `push_on_front` eqs_X } -- These isEmptyBag tests are just trying -- to avoid creating unnecessary thunks | Bool otherwise = WorkList wl { wl_rw_eqs = new_eqs `push_on_front` rw_eqs } where push_on_front :: Bag Ct -> [Ct] -> [Ct] -- push_on_front puts the new equlities on the front of the queue push_on_front :: Bag Ct -> [Ct] -> [Ct] push_on_front Bag Ct new_eqs [Ct] eqs = (Ct -> [Ct] -> [Ct]) -> [Ct] -> Bag Ct -> [Ct] forall a b. (a -> b -> b) -> b -> Bag a -> b forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr (:) [Ct] eqs Bag Ct new_eqs is_nominal :: Ct -> Bool is_nominal Ct ct = Type -> Bool isNomEqPred (Ct -> Type ctPred Ct ct) extendWorkListNonEq :: Ct -> WorkList -> WorkList -- Extension by non equality extendWorkListNonEq :: Ct -> WorkList -> WorkList extendWorkListNonEq Ct ct WorkList wl = WorkList wl { wl_rest = ct : wl_rest wl } extendWorkListImplic :: Implication -> WorkList -> WorkList extendWorkListImplic :: Implication -> WorkList -> WorkList extendWorkListImplic Implication implic WorkList wl = WorkList wl { wl_implics = implic `consBag` wl_implics wl } extendWorkListCt :: Ct -> WorkList -> WorkList -- Agnostic about what kind of constraint extendWorkListCt :: Ct -> WorkList -> WorkList extendWorkListCt Ct ct WorkList wl = case Type -> Pred classifyPredType (CtEvidence -> Type ctEvPred CtEvidence ev) of EqPred {} -> RewriterSet -> Ct -> WorkList -> WorkList extendWorkListEq RewriterSet rewriters Ct ct WorkList wl ClassPred Class cls [Type] _ -- See Note [Prioritise class equalities] | Class -> Bool isEqualityClass Class cls -> RewriterSet -> Ct -> WorkList -> WorkList extendWorkListEq RewriterSet rewriters Ct ct WorkList wl Pred _ -> Ct -> WorkList -> WorkList extendWorkListNonEq Ct ct WorkList wl where ev :: CtEvidence ev = Ct -> CtEvidence ctEvidence Ct ct rewriters :: RewriterSet rewriters = CtEvidence -> RewriterSet ctEvRewriters CtEvidence ev extendWorkListCtList :: [Ct] -> WorkList -> WorkList extendWorkListCtList :: [Ct] -> WorkList -> WorkList extendWorkListCtList [Ct] cts WorkList wl = (Ct -> WorkList -> WorkList) -> WorkList -> [Ct] -> WorkList forall a b. (a -> b -> b) -> b -> [a] -> b forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr Ct -> WorkList -> WorkList extendWorkListCt WorkList wl [Ct] cts extendWorkListCts :: Cts -> WorkList -> WorkList extendWorkListCts :: Bag Ct -> WorkList -> WorkList extendWorkListCts Bag Ct cts WorkList wl = (Ct -> WorkList -> WorkList) -> WorkList -> Bag Ct -> WorkList forall a b. (a -> b -> b) -> b -> Bag a -> b forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr Ct -> WorkList -> WorkList extendWorkListCt WorkList wl Bag Ct cts isEmptyWorkList :: WorkList -> Bool isEmptyWorkList :: WorkList -> Bool isEmptyWorkList (WL { wl_eqs_N :: WorkList -> [Ct] wl_eqs_N = [Ct] eqs_N, wl_eqs_X :: WorkList -> [Ct] wl_eqs_X = [Ct] eqs_X , wl_rest :: WorkList -> [Ct] wl_rest = [Ct] rest, wl_implics :: WorkList -> Bag Implication wl_implics = Bag Implication implics }) = [Ct] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [Ct] eqs_N Bool -> Bool -> Bool && [Ct] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [Ct] eqs_X Bool -> Bool -> Bool && [Ct] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [Ct] rest Bool -> Bool -> Bool && Bag Implication -> Bool forall a. Bag a -> Bool isEmptyBag Bag Implication implics emptyWorkList :: WorkList emptyWorkList :: WorkList emptyWorkList = WL { wl_eqs_N :: [Ct] wl_eqs_N = [], wl_eqs_X :: [Ct] wl_eqs_X = [] , wl_rw_eqs :: [Ct] wl_rw_eqs = [], wl_rest :: [Ct] wl_rest = [], wl_implics :: Bag Implication wl_implics = Bag Implication forall a. Bag a emptyBag } selectWorkItem :: WorkList -> Maybe (Ct, WorkList) -- See Note [Prioritise equalities] selectWorkItem :: WorkList -> Maybe (Ct, WorkList) selectWorkItem wl :: WorkList wl@(WL { wl_eqs_N :: WorkList -> [Ct] wl_eqs_N = [Ct] eqs_N, wl_eqs_X :: WorkList -> [Ct] wl_eqs_X = [Ct] eqs_X , wl_rw_eqs :: WorkList -> [Ct] wl_rw_eqs = [Ct] rw_eqs, wl_rest :: WorkList -> [Ct] wl_rest = [Ct] rest }) | Ct ct:[Ct] cts <- [Ct] eqs_N = (Ct, WorkList) -> Maybe (Ct, WorkList) forall a. a -> Maybe a Just (Ct ct, WorkList wl { wl_eqs_N = cts }) | Ct ct:[Ct] cts <- [Ct] eqs_X = (Ct, WorkList) -> Maybe (Ct, WorkList) forall a. a -> Maybe a Just (Ct ct, WorkList wl { wl_eqs_X = cts }) | Ct ct:[Ct] cts <- [Ct] rw_eqs = (Ct, WorkList) -> Maybe (Ct, WorkList) forall a. a -> Maybe a Just (Ct ct, WorkList wl { wl_rw_eqs = cts }) | Ct ct:[Ct] cts <- [Ct] rest = (Ct, WorkList) -> Maybe (Ct, WorkList) forall a. a -> Maybe a Just (Ct ct, WorkList wl { wl_rest = cts }) | Bool otherwise = Maybe (Ct, WorkList) forall a. Maybe a Nothing -- Pretty printing instance Outputable WorkList where ppr :: WorkList -> SDoc ppr (WL { wl_eqs_N :: WorkList -> [Ct] wl_eqs_N = [Ct] eqs_N, wl_eqs_X :: WorkList -> [Ct] wl_eqs_X = [Ct] eqs_X, wl_rw_eqs :: WorkList -> [Ct] wl_rw_eqs = [Ct] rw_eqs , wl_rest :: WorkList -> [Ct] wl_rest = [Ct] rest, wl_implics :: WorkList -> Bag Implication wl_implics = Bag Implication implics }) = String -> SDoc forall doc. IsLine doc => String -> doc text String "WL" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> (SDoc -> SDoc forall doc. IsLine doc => doc -> doc braces (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat [ Bool -> SDoc -> SDoc forall doc. IsOutput doc => Bool -> doc -> doc ppUnless ([Ct] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [Ct] eqs_N) (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ String -> SDoc forall doc. IsLine doc => String -> doc text String "Eqs_N =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat ((Ct -> SDoc) -> [Ct] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map Ct -> SDoc forall a. Outputable a => a -> SDoc ppr [Ct] eqs_N) , Bool -> SDoc -> SDoc forall doc. IsOutput doc => Bool -> doc -> doc ppUnless ([Ct] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [Ct] eqs_X) (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ String -> SDoc forall doc. IsLine doc => String -> doc text String "Eqs_X =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat ((Ct -> SDoc) -> [Ct] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map Ct -> SDoc forall a. Outputable a => a -> SDoc ppr [Ct] eqs_X) , Bool -> SDoc -> SDoc forall doc. IsOutput doc => Bool -> doc -> doc ppUnless ([Ct] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [Ct] rw_eqs) (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ String -> SDoc forall doc. IsLine doc => String -> doc text String "RwEqs =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat ((Ct -> SDoc) -> [Ct] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map Ct -> SDoc forall a. Outputable a => a -> SDoc ppr [Ct] rw_eqs) , Bool -> SDoc -> SDoc forall doc. IsOutput doc => Bool -> doc -> doc ppUnless ([Ct] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [Ct] rest) (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ String -> SDoc forall doc. IsLine doc => String -> doc text String "Non-eqs =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat ((Ct -> SDoc) -> [Ct] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map Ct -> SDoc forall a. Outputable a => a -> SDoc ppr [Ct] rest) , Bool -> SDoc -> SDoc forall doc. IsOutput doc => Bool -> doc -> doc ppUnless (Bag Implication -> Bool forall a. Bag a -> Bool isEmptyBag Bag Implication implics) (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ SDoc -> SDoc -> SDoc forall doc. IsOutput doc => doc -> doc -> doc ifPprDebug (String -> SDoc forall doc. IsLine doc => String -> doc text String "Implics =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat ((Implication -> SDoc) -> [Implication] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map Implication -> SDoc forall a. Outputable a => a -> SDoc ppr (Bag Implication -> [Implication] forall a. Bag a -> [a] bagToList Bag Implication implics))) (String -> SDoc forall doc. IsLine doc => String -> doc text String "(Implics omitted)") ]) {- ********************************************************************* * * InertSet: the inert set * * * * ********************************************************************* -} type CycleBreakerVarStack = NonEmpty (Bag (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.Equality -- Why store the outer implications? For the use in mightEqualLater (only) -- -- Why NonEmpty? So there is always a top element to add to data InertSet = IS { InertSet -> InertCans inert_cans :: InertCans -- Canonical Given, Wanted -- Sometimes called "the inert set" , InertSet -> CycleBreakerVarStack inert_cycle_breakers :: CycleBreakerVarStack , InertSet -> FunEqMap Reduction inert_famapp_cache :: FunEqMap Reduction -- Just a hash-cons cache for use when reducing family applications -- only -- -- If F tys :-> (co, rhs, flav), -- then co :: F tys ~N rhs -- 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 DictCt inert_solved_dicts :: DictMap DictCt -- All Wanteds, of form (C t1 .. tn) -- Always a dictionary solved by an instance decl; never an implict parameter -- 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 DictCt inert_solved_dicts = DictMap DictCt solved_dicts }) = [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat [ InertCans -> SDoc forall a. Outputable a => a -> SDoc ppr InertCans ics , Bool -> SDoc -> SDoc forall doc. IsOutput doc => Bool -> doc -> doc ppUnless ([DictCt] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [DictCt] dicts) (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ String -> SDoc forall doc. IsLine doc => String -> doc text String "Solved dicts =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat ((DictCt -> SDoc) -> [DictCt] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map DictCt -> SDoc forall a. Outputable a => a -> SDoc ppr [DictCt] dicts) ] where dicts :: [DictCt] dicts = Bag DictCt -> [DictCt] forall a. Bag a -> [a] bagToList (DictMap DictCt -> Bag DictCt forall a. DictMap a -> Bag a dictsToBag DictMap DictCt solved_dicts) emptyInertCans :: InertCans emptyInertCans :: InertCans emptyInertCans = IC { inert_eqs :: InertEqs inert_eqs = InertEqs emptyTyEqs , inert_funeqs :: InertFunEqs inert_funeqs = InertFunEqs forall a. TcAppMap a emptyFunEqs , inert_given_eq_lvl :: TcLevel inert_given_eq_lvl = TcLevel topTcLevel , inert_given_eqs :: Bool inert_given_eqs = Bool False , inert_dicts :: DictMap DictCt inert_dicts = DictMap DictCt forall a. TcAppMap a emptyDictMap , inert_safehask :: DictMap DictCt inert_safehask = DictMap DictCt forall a. TcAppMap a emptyDictMap , inert_insts :: [QCInst] inert_insts = [] , inert_irreds :: InertIrreds inert_irreds = InertIrreds forall a. Bag a emptyBag } emptyInert :: InertSet emptyInert :: InertSet emptyInert = IS { inert_cans :: InertCans inert_cans = InertCans emptyInertCans , inert_cycle_breakers :: CycleBreakerVarStack inert_cycle_breakers = Bag (TcTyVar, Type) forall a. Bag a emptyBag Bag (TcTyVar, Type) -> [Bag (TcTyVar, Type)] -> CycleBreakerVarStack forall a. a -> [a] -> NonEmpty a :| [] , inert_famapp_cache :: FunEqMap Reduction inert_famapp_cache = FunEqMap Reduction forall a. TcAppMap a emptyFunEqs , inert_solved_dicts :: DictMap DictCt inert_solved_dicts = DictMap DictCt forall a. TcAppMap 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 applying 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.Dict.tryInstances - 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 * * * * ********************************************************************* -} {- 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 updGivenEqs. 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? (TGE1) We do /not/ need to worry about let-bound skolems, such as forall[2] a. a ~ [b] => blah See Note [Let-bound skolems] and the isOuterTyVar tests in `updGivenEqs` (TGE2) 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 subsequntly (see `getHasGivenEqs`), to set the ic_given_eqs field to LocalGivenEqs. (TGE3) 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). (TGE4) 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, updGivenEqs conservatively treats it as a potential equality, and updates inert_give_eq_lvl (TGE5) We should 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. Historical note: prior to #24938 we also ignored Given equalities that did not mention an "outer" type variable. But that is wrong, as #24938 showed. Another example is immortalised in test LocalGivenEqs2 data T where MkT :: F a ~ G b => a -> b -> T f (MkT _ _) = True We should not infer the type for `f`; let-bound-skolems does not apply. 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. The actual test is in `isLetBoundSkolemCt` Wrinkles: (LBS1) See GHC.Tc.Utils.Unify Note [Deeper level on the left] for how we ensure that the correct variable is on the left of the equality when both are tyvars. (LBS2) We also want this to work for forall a. [G] F b ~ a (CEqCt with TyFamLHS) Here the Given will have a TyFamLHS, with the skolem-bound tyvar on the RHS. See tests T24938a, and LocalGivenEqs. (LBS3) Happily (LBS2) also makes cycle-breakers work. Suppose we have forall a. [G] (F a) Int ~ a where F has arity 1, and `a` is the locally-bound skolem. Then, as Note [Type equality cycles] explains, we split into [G] F a ~ cbv, [G] cbv Int ~ a where `cbv` is the cycle breaker variable. But cbv has the same level as `a`, so `isOuterTyVar` (called in `isLetBoundSkolemCt`) will return False. This actually matters occasionally: see test LocalGivenEqs. You might wonder whether the skolem really needs to be bound "in the very same implication" as the equality 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. Possible future improvements. The current test just looks to see whether one side of an equality is a locally-bound skolem. But actually we could, in theory, do better: if one side (or both sides, actually) of an equality ineluctably mentions a local skolem, then the equality cannot possibly impact types outside of the implication (because doing to would cause those types to be ill-scoped). The problem is the "ineluctably": this means that no expansion, other solving, etc., could possibly get rid of the variable. This is hard, perhaps impossible, to know for sure, especially when we think about type family interactions. (And it's a user-visible property so we don't want it to be hard to predict.) So we keep the existing check, looking for one lone variable, because we're sure that variable isn't going anywhere. 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 [inert_eqs: the inert equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Our main invariant: the EqCts in inert_eqs should be a terminating generalised substitution -------------- 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 (WF3) No LHS in S is rewritable in an RHS in S, in the argument of a type family application (F ty1..tyn) where F heads a LHS in S --------- Definition [Applying a generalised substitution] ---------- If S is a generalised substitution S(f,lhs) = rhs, if (lhs -fs-> rhs) in S, and fs >= f S(f,T t1..tn) = T S(f1,t1)..S(fn,tn) S(f,t1 t2) = S(f,t1) S(f_N,t2) S(f,t) = t Here f1..fn are obtained from f and T using the roles of T, and f_N is the nominal version of f. See Note [Flavours with roles]. Notation: repeated application. S^0(f,t) = t S^(n+1)(f,t) = S(f, S^n(t)) S*(f,t) is the result of applying S until you reach a fixpoint --------- Definition [Terminating generalised substitution] --------- A generalised substitution S is *terminating* iff (IG1) for every f,t, there is an n such that 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. --------- End of definitions ------------------------------------ Rationale for (WF1)-(WF3) ------------------------- * (WF1) guarantees that S is well-defined /as a function/; see Theorem (S is a function) Theorem (S is a function): 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) Note: this argument isn't quite right. WF1 ensures that lhs1 does not appear inside lhs2, and that guarantees confluence. But I can't quite see how to make that argument precise. * (WF2) is a bit trivial. It means that if S is terminating, so that S^(n+1)(f,t) = S^n(f,t), then there is no LHS of S in S^n(f,t). We never get a silly infinite sequence a -> a -> a -> a .... which is technically a fixed point but would still go on for ever. * (WF3) is need for the termination proof. 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 [Avoiding rewriting cycles] in GHC.Tc.Types.Constraint for an example. Note [Rewritable] ~~~~~~~~~~~~~~~~~ Definition. 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. 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. This definition is used by the anyRewritableXXX family of functions and is meant to model the actual behaviour in GHC.Tc.Solver.Rewrite. 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. Wrinkles * 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. * 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.Equality.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. Note [Extending the inert equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Main Theorem [Stability under extension] GIVEN a "work item" [lhs_w -fw-> rhs_w] and a terminating generalised substitution S, SUCH THAT (T1) S(fw,lhs_w) = lhs_w -- LHS of work-item is a fixpoint of S(fw,_) (T2) S(fw,rhs_w) = rhs_w -- RHS of work-item is a fixpoint of S(fw,_) (T3) lhs_w not in rhs_w -- No occurs check in the work item -- If lhs is a type family application, we require only that -- lhs is not *rewritable* in rhs_w. See Note [Rewritable] and -- Note [EqCt occurs check] in GHC.Tc.Types.Constraint. (T4) no [lhs_s -fs-> rhs_s] in S meets [The KickOut Criteria] (i.e. we already kicked any such items out!) THEN the extended substitution T = S+(lhs_w -fw-> rhs_w) is a terminating generalised substitution How do we establish these conditions? * (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 [EqCt occurs check] in GHC.Tc.Types.Constraint. * (T4) is established by GHC.Tc.Solver.Monad.kickOutRewritable. If the inert set contains a triple that meets the KickOut Criteria, we kick it out and add it to the work list for later re-examination. See Note [The KickOut Criteria] Theorem: T (defined in "THEN" above) is a generalised substitution; that is, it satisfies (WF1)-(WF3) Proof: (WF1) Suppose we are adding [lhs_w -fw-> rhs_w], and [lhs_s -fs-> rhs_s] is in S. Then: - by (T1) if fs>=fw, lhs_s does not occur within lhs_w. - by (KK1) if fw>=fs, lhs_w is not rewritable in lhs_s, or we'd have kicked out the stable constraint. (WF2) is directly guaranteed by (T3) (WF3) No lhs_s in S is rewritable in rhs_w at all, because of (T2) And (KK2) guarantees that lhs_w is not rewritable under a type family in rhs_s Note [The KickOut Criteria] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ Kicking out is a Bad Thing: * It means we have to re-process a constraint. The less we kick out, the better. * In the limit, kicking can lead to non-termination: imagine that we /always/ kick out the entire inert set! * Because (mid 2024) we don't support sharing in constraints, excessive kicking out can lead to exponentially big constraints (#24984). So we seek to do as little kicking out as possible. For example, consider this, which happens a lot: Inert: g1: a ~ Maybe b Work: g2: b ~ Int We do /not/ kick out g1 when adding g2. The new substitution S' = {g1,g2} is still /terminating/ but it is not /idmempotent/. To apply S' to, say, (Tree a), we may need to apply it twice: Tree a --> Tree (Maybe b) --> Tree (Maybe Int) Here are the KickOut Criteria: When adding [lhs_w -fw-> rhs_w] to a well-formed terminating substitution S, element [lhs_s -fs-> rhs_s] in S meets the KickOut Criteria if: (KK0) fw >= fs AND any of (KK1), (KK2) or (KK3) hold * (KK1: satisfy WF1) `lhs_w` is rewritable in `lhs_s`. * (KK2: termination) `lhs_w` is rewritable in `rhs_s` in these positions: If not(fs>=fw) then (KK2a) anywhere else (KK2b) look only in the argument of type family applications, whose type family heads some LHS in `S` * (KK3: completeness) If not(fs >= fw) -- If fs can rewrite fw, kick-out is redundant/harmful * (KK3a) If the role of `fs` is Nominal: kick out if `rhs_s = lhs_w` * (KK3b) If the role of `fs` is Representational: kick out if `rhs_s` is of form `(lhs_w t1 .. tn)` Rationale * (KK0) kick out only if `fw` can rewrite `fs`. Reason: suppose we kick out (lhs1 -fs-> s), and add (lhs -fw-> t) to the ineart set. The latter can't rewrite the former, so the kick-out achieved nothing * (KK1) `lhs_w` is rewritable in `lhs_s`. Reason: needed to guarantee (WF1). See Theorem: T is well formed * (KK2) see Note [KK2: termination of the extended substitution] * (KK3) see Note [KK3: completeness of solving] The above story is a bit vague wrt roles, but the code is not. See Note [Flavours with roles] Note [KK2: termination of the extended substitution] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Proving termination of the extended substitution T is surprisingly tricky. * Reason for (KK2a). Consider Work: [G] b ~ a Inert: [W] a ~ b If we don't kick out the inert, then we get a loop on e.g. [W] a ~ Int. But if both were Wanted we really should not kick out (the substitution does not have to be idempotent). So we only look everywhere for the `lhs_w` if not (fs>=fw), that is the inert item cannot rewrite the work item. So in the above example we will kick out; but if both were Wanted we won't. * Reason for (KK2b). Consider the case where (fs >= fw) Work: [G] a ~ Int Inert: [G] F Int ~ F a If we just added the work item, the substitution would loop on type (F Int). So we must kick out the inert item, even though (fs>=fw). (KK2b) does this by looking for lhs_w under type family applications in rhs_s. (KK2b) makes kick-out less aggressive by looking only under type-family applications, in the case where (fs >= fw), and that made a /huge/ difference to #24944. Tricky examples in: #19042, #17672, #24984. The last (#24984) is particular subtle: Inert: [W] g1: F a0 ~ F a1 [W] g2: F a2 ~ F a1 [W] g3: F a3 ~ F a1 Now we add [W] g4: F a1 ~ F a7. Should we kick out g1,g2,g3? No! The substitution doesn't need to be idempotent, merely terminating. And in #24984 it turned out that we kept adding one new constraint and kicking out all the previous inert ones (and that rewriting led to exponentially big constraints due to lack of contraint sharing.) So we only want to look /under/ type family applications. The proof is hard. We start by ignoring flavours. Suppose that: * We are adding [lhs_w -fw-> rhs_w] to a well-formed, terminating substitution S. * None of the constraints in S meet the KickOut Criteria. * Define T = S+[lhs_w -fw-> rhs_w] * `f` is an arbitrary flavour Lemma 1: for any lhs_s in S, T*(f,lhs_s) terminates. Proof. * We know that r1 = S*(f,lhs_s) terminates. * Moreover, we know there are no occurrences of lhs_w under a type family (which is the head of a LHS) in r1 (KK2)+(WF3). We need (WF3) because you might wonder what if rhs_s is (F a), and [a --> lhs_w] was in S. But (WF3) prevents that. * Define r2 = r1{rhs_w/lhs_w}. We know that rhs_w has no occurrences of any lhs in S, nor of lhs_w. * Since any occurrence of lhs_w does not occur under a type family, the substitution won't make any F t1..tn ~ s in S match. * So r2 is a fixed point of T. Lemma 2: T*(f,lhs_w) teminates. Proof: no occurrences of any LHS in rhs_w. Theorem. For any type r, T*(r) terminates. Proof: 1. Consider any sub-term of r, which is a LHS of T. - Rewrite it with T*; this terminates (Lemma 1). - Do this simultaneously to all sub-terms that match a LHS of T, yielding r1. 2. Could this new r1 have a sub-term that is an LHS of T? Yes, but only if r has a sub-term F w, and w rewrote in Step 1 to w' and F w' matches a LHS in T. 3. Very well: apply step 1 again, but note that /doing so consumes one of the family applications in the original r/. 4. After Step 1 either we have reached a fixed point, or we repeat Step 1 consuming at least one family application of r. 5. There are only a finite number of family applications in r, so this process terminates. Example: Inert set: gs : F Int ~ b Work item: gw : b ~ Int F (F (F b)) --[gw]--> F (F (F Int)) --[gs]--> F (F b) --[gw]--> F (F Int) --[gs]--> F b --[gw]--> F Int --[gs]--> b --[gw]--> Int Notice that each iteration of Step 1 strips off one of the layers of F, all of which were in the original r. The argument is even more tricky when flavours are involved, and we have not fleshed it out in detail. Note [KK3: completeness of solving] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ (KK3) is not necessary for the extended substitution to be terminating. In fact (KK0) 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 (KK3) to the kick-out criteria: * (KK3: completeness) If not(fs >= fw) (KK3a) * (KK3b) If the role of `fs` is Nominal: kick out if `rhs_s = lhs_w` * (KK3c) If the role of `fs` is Representational: kick out if `rhs_s` is of form `(lhs_w t1 .. tn)` Wrinkles: * (KK3a) All this can only happen if the work-item can rewrite the inert one, /but not vice versa/; that is not(fs >= fw). It is useless to kick out if (fs >= fw) becuase then the work-item is already fully rewritten by the inert item. And too much kick-out is positively harmful. (Historical example #14363.) * (KK3b) addresses teh main example above for KK3. Another way to understand (KK3b) 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. * (KK3c) When considering roles, we also need the second clause (KK3b). 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 (KK3a), 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 head_is_new_lhs. This is encoded in (KK3c)). 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, 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 [inert_eqs: the inert equalities] may need to be revisited, but we don't think that the end conclusion is wrong. -} data InertCans -- See Note [Detailed InertCans Invariants] for more = IC { InertCans -> InertEqs inert_eqs :: InertEqs -- See Note [inert_eqs: the inert equalities] -- All EqCt with a TyVarLHS; index is the LHS tyvar -- Domain = skolems and untouchables; a touchable would be unified , InertCans -> InertFunEqs inert_funeqs :: InertFunEqs -- All EqCt with a TyFamLHS; index is the whole family head type. -- LHS is fully rewritten (modulo eqCanRewrite constraints) -- wrt inert_eqs -- Can include both [G] and [W] , InertCans -> DictMap DictCt inert_dicts :: DictMap DictCt -- Dictionaries only -- All fully rewritten (modulo flavour constraints) -- wrt inert_eqs , InertCans -> [QCInst] inert_insts :: [QCInst] , InertCans -> DictMap DictCt inert_safehask :: DictMap DictCt -- 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 -> InertIrreds inert_irreds :: InertIrreds -- 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 -> 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] , 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 type InertFunEqs = FunEqMap EqualCtList type InertIrreds = Bag IrredCt instance Outputable InertCans where ppr :: InertCans -> SDoc ppr (IC { inert_eqs :: InertCans -> InertEqs inert_eqs = InertEqs eqs , inert_funeqs :: InertCans -> InertFunEqs inert_funeqs = InertFunEqs funeqs , inert_dicts :: InertCans -> DictMap DictCt inert_dicts = DictMap DictCt dicts , inert_safehask :: InertCans -> DictMap DictCt inert_safehask = DictMap DictCt safehask , inert_irreds :: InertCans -> InertIrreds inert_irreds = InertIrreds irreds , 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 forall doc. IsLine doc => doc -> doc braces (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat [ Bool -> SDoc -> SDoc forall doc. IsOutput doc => Bool -> doc -> doc ppUnless (InertEqs -> Bool forall a. DVarEnv a -> Bool isEmptyDVarEnv InertEqs eqs) (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ String -> SDoc forall doc. IsLine doc => String -> doc text String "Equalities =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Bag EqCt -> SDoc forall a. Outputable a => Bag a -> SDoc pprBag ((EqCt -> Bag EqCt -> Bag EqCt) -> InertEqs -> Bag EqCt -> Bag EqCt forall b. (EqCt -> b -> b) -> InertEqs -> b -> b foldTyEqs EqCt -> Bag EqCt -> Bag EqCt forall a. a -> Bag a -> Bag a consBag InertEqs eqs Bag EqCt forall a. Bag a emptyBag) , Bool -> SDoc -> SDoc forall doc. IsOutput doc => Bool -> doc -> doc ppUnless (InertFunEqs -> Bool forall a. TcAppMap a -> Bool isEmptyTcAppMap InertFunEqs funeqs) (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ String -> SDoc forall doc. IsLine doc => String -> doc text String "Type-function equalities =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Bag EqCt -> SDoc forall a. Outputable a => Bag a -> SDoc pprBag ((EqCt -> Bag EqCt -> Bag EqCt) -> InertFunEqs -> Bag EqCt -> Bag EqCt forall b. (EqCt -> b -> b) -> InertFunEqs -> b -> b foldFunEqs EqCt -> Bag EqCt -> Bag EqCt forall a. a -> Bag a -> Bag a consBag InertFunEqs funeqs Bag EqCt forall a. Bag a emptyBag) , Bool -> SDoc -> SDoc forall doc. IsOutput doc => Bool -> doc -> doc ppUnless (DictMap DictCt -> Bool forall a. TcAppMap a -> Bool isEmptyTcAppMap DictMap DictCt dicts) (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ String -> SDoc forall doc. IsLine doc => String -> doc text String "Dictionaries =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Bag DictCt -> SDoc forall a. Outputable a => Bag a -> SDoc pprBag (DictMap DictCt -> Bag DictCt forall a. DictMap a -> Bag a dictsToBag DictMap DictCt dicts) , Bool -> SDoc -> SDoc forall doc. IsOutput doc => Bool -> doc -> doc ppUnless (DictMap DictCt -> Bool forall a. TcAppMap a -> Bool isEmptyTcAppMap DictMap DictCt safehask) (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ String -> SDoc forall doc. IsLine doc => String -> doc text String "Safe Haskell unsafe overlap =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Bag DictCt -> SDoc forall a. Outputable a => Bag a -> SDoc pprBag (DictMap DictCt -> Bag DictCt forall a. DictMap a -> Bag a dictsToBag DictMap DictCt safehask) , Bool -> SDoc -> SDoc forall doc. IsOutput doc => Bool -> doc -> doc ppUnless (InertIrreds -> Bool forall a. Bag a -> Bool isEmptyBag InertIrreds irreds) (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ String -> SDoc forall doc. IsLine doc => String -> doc text String "Irreds =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> InertIrreds -> SDoc forall a. Outputable a => Bag a -> SDoc pprBag InertIrreds irreds , Bool -> SDoc -> SDoc forall doc. IsOutput doc => Bool -> doc -> doc ppUnless ([QCInst] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [QCInst] insts) (SDoc -> SDoc) -> SDoc -> SDoc forall a b. (a -> b) -> a -> b $ String -> SDoc forall doc. IsLine doc => String -> doc text String "Given instances =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> [SDoc] -> SDoc forall doc. IsDoc doc => [doc] -> doc vcat ((QCInst -> SDoc) -> [QCInst] -> [SDoc] forall a b. (a -> b) -> [a] -> [b] map QCInst -> SDoc forall a. Outputable a => a -> SDoc ppr [QCInst] insts) , String -> SDoc forall doc. IsLine doc => String -> doc text String "Innermost given equalities =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> TcLevel -> SDoc forall a. Outputable a => a -> SDoc ppr TcLevel ge_lvl , String -> SDoc forall doc. IsLine doc => String -> doc text String "Given eqs at this level =" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> Bool -> SDoc forall a. Outputable a => a -> SDoc ppr Bool given_eqs ] {- ********************************************************************* * * Inert equalities * * ********************************************************************* -} emptyTyEqs :: InertEqs emptyTyEqs :: InertEqs emptyTyEqs = InertEqs forall a. DVarEnv a emptyDVarEnv addEqToCans :: TcLevel -> EqCt -> InertCans -> InertCans addEqToCans :: TcLevel -> EqCt -> InertCans -> InertCans addEqToCans TcLevel tc_lvl eq_ct :: EqCt eq_ct@(EqCt { eq_lhs :: EqCt -> CanEqLHS eq_lhs = CanEqLHS lhs }) ics :: InertCans ics@(IC { inert_funeqs :: InertCans -> InertFunEqs inert_funeqs = InertFunEqs funeqs, inert_eqs :: InertCans -> InertEqs inert_eqs = InertEqs eqs }) = TcLevel -> Ct -> InertCans -> InertCans updGivenEqs TcLevel tc_lvl (EqCt -> Ct CEqCan EqCt eq_ct) (InertCans -> InertCans) -> InertCans -> InertCans forall a b. (a -> b) -> a -> b $ case CanEqLHS lhs of TyFamLHS TyCon tc [Type] tys -> InertCans ics { inert_funeqs = addCanFunEq funeqs tc tys eq_ct } TyVarLHS TcTyVar tv -> InertCans ics { inert_eqs = addTyEq eqs tv eq_ct } addTyEq :: InertEqs -> TcTyVar -> EqCt -> InertEqs addTyEq :: InertEqs -> TcTyVar -> EqCt -> InertEqs addTyEq InertEqs old_eqs TcTyVar tv EqCt ct = (EqualCtList -> EqualCtList -> EqualCtList) -> InertEqs -> TcTyVar -> EqualCtList -> InertEqs forall a. (a -> a -> a) -> DVarEnv a -> TcTyVar -> a -> DVarEnv a extendDVarEnv_C EqualCtList -> EqualCtList -> EqualCtList add_eq InertEqs old_eqs TcTyVar tv [EqCt ct] where add_eq :: EqualCtList -> EqualCtList -> EqualCtList add_eq EqualCtList old_eqs EqualCtList _ = EqCt -> EqualCtList -> EqualCtList addToEqualCtList EqCt ct EqualCtList old_eqs foldTyEqs :: (EqCt -> b -> b) -> InertEqs -> b -> b foldTyEqs :: forall b. (EqCt -> b -> b) -> InertEqs -> b -> b foldTyEqs EqCt -> b -> b k InertEqs eqs b z = (EqualCtList -> b -> b) -> b -> InertEqs -> b forall a b. (a -> b -> b) -> b -> DVarEnv a -> b foldDVarEnv (\EqualCtList cts b z -> (EqCt -> b -> b) -> b -> EqualCtList -> b forall a b. (a -> b -> b) -> b -> [a] -> b forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr EqCt -> b -> b k b z EqualCtList cts) b z InertEqs eqs findTyEqs :: InertCans -> TyVar -> [EqCt] findTyEqs :: InertCans -> TcTyVar -> EqualCtList findTyEqs InertCans icans TcTyVar tv = forall (t :: * -> *) a. Foldable t => t [a] -> [a] concat @Maybe (InertEqs -> TcTyVar -> Maybe EqualCtList forall a. DVarEnv a -> TcTyVar -> Maybe a lookupDVarEnv (InertCans -> InertEqs inert_eqs InertCans icans) TcTyVar tv) delEq :: EqCt -> InertCans -> InertCans delEq :: EqCt -> InertCans -> InertCans delEq (EqCt { eq_lhs :: EqCt -> CanEqLHS eq_lhs = CanEqLHS lhs, eq_rhs :: EqCt -> Type eq_rhs = Type rhs }) InertCans ic = case CanEqLHS lhs of TyVarLHS TcTyVar tv -> InertCans ic { inert_eqs = alterDVarEnv upd (inert_eqs ic) tv } TyFamLHS TyCon tf [Type] args -> InertCans ic { inert_funeqs = alterTcApp (inert_funeqs ic) tf args upd } where isThisOne :: EqCt -> Bool isThisOne :: EqCt -> Bool isThisOne (EqCt { eq_rhs :: EqCt -> Type eq_rhs = Type t1 }) = Type -> Type -> Bool tcEqTypeNoKindCheck Type rhs Type t1 upd :: Maybe EqualCtList -> Maybe EqualCtList upd :: Maybe EqualCtList -> Maybe EqualCtList upd (Just EqualCtList eq_ct_list) = (EqCt -> Bool) -> EqualCtList -> Maybe EqualCtList filterEqualCtList (Bool -> Bool not (Bool -> Bool) -> (EqCt -> Bool) -> EqCt -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . EqCt -> Bool isThisOne) EqualCtList eq_ct_list upd Maybe EqualCtList Nothing = Maybe EqualCtList forall a. Maybe a Nothing findEq :: InertCans -> CanEqLHS -> [EqCt] findEq :: InertCans -> CanEqLHS -> EqualCtList findEq InertCans icans (TyVarLHS TcTyVar tv) = InertCans -> TcTyVar -> EqualCtList findTyEqs InertCans icans TcTyVar tv findEq InertCans icans (TyFamLHS TyCon fun_tc [Type] fun_args) = forall (t :: * -> *) a. Foldable t => t [a] -> [a] concat @Maybe (InertFunEqs -> TyCon -> [Type] -> Maybe EqualCtList forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a findFunEq (InertCans -> InertFunEqs inert_funeqs InertCans icans) TyCon fun_tc [Type] fun_args) {-# INLINE partition_eqs_container #-} partition_eqs_container :: forall container . container -- empty container -> (forall b. (EqCt -> b -> b) -> container -> b -> b) -- folder -> (EqCt -> container -> container) -- extender -> (EqCt -> Bool) -> container -> ([EqCt], container) partition_eqs_container :: forall container. container -> (forall b. (EqCt -> b -> b) -> container -> b -> b) -> (EqCt -> container -> container) -> (EqCt -> Bool) -> container -> (EqualCtList, container) partition_eqs_container container empty_container forall b. (EqCt -> b -> b) -> container -> b -> b fold_container EqCt -> container -> container extend_container EqCt -> Bool pred container orig_inerts = (EqCt -> (EqualCtList, container) -> (EqualCtList, container)) -> container -> (EqualCtList, container) -> (EqualCtList, container) forall b. (EqCt -> b -> b) -> container -> b -> b fold_container EqCt -> (EqualCtList, container) -> (EqualCtList, container) folder container orig_inerts ([], container empty_container) where folder :: EqCt -> ([EqCt], container) -> ([EqCt], container) folder :: EqCt -> (EqualCtList, container) -> (EqualCtList, container) folder EqCt eq_ct (EqualCtList acc_true, container acc_false) | EqCt -> Bool pred EqCt eq_ct = (EqCt eq_ct EqCt -> EqualCtList -> EqualCtList forall a. a -> [a] -> [a] : EqualCtList acc_true, container acc_false) | Bool otherwise = (EqualCtList acc_true, EqCt -> container -> container extend_container EqCt eq_ct container acc_false) partitionInertEqs :: (EqCt -> Bool) -- EqCt will always have a TyVarLHS -> InertEqs -> ([EqCt], InertEqs) partitionInertEqs :: (EqCt -> Bool) -> InertEqs -> (EqualCtList, InertEqs) partitionInertEqs = InertEqs -> (forall b. (EqCt -> b -> b) -> InertEqs -> b -> b) -> (EqCt -> InertEqs -> InertEqs) -> (EqCt -> Bool) -> InertEqs -> (EqualCtList, InertEqs) forall container. container -> (forall b. (EqCt -> b -> b) -> container -> b -> b) -> (EqCt -> container -> container) -> (EqCt -> Bool) -> container -> (EqualCtList, container) partition_eqs_container InertEqs emptyTyEqs (EqCt -> b -> b) -> InertEqs -> b -> b forall b. (EqCt -> b -> b) -> InertEqs -> b -> b foldTyEqs EqCt -> InertEqs -> InertEqs addInertEqs addInertEqs :: EqCt -> InertEqs -> InertEqs -- Precondition: CanEqLHS is a TyVarLHS addInertEqs :: EqCt -> InertEqs -> InertEqs addInertEqs eq_ct :: EqCt eq_ct@(EqCt { eq_lhs :: EqCt -> CanEqLHS eq_lhs = TyVarLHS TcTyVar tv }) InertEqs eqs = InertEqs -> TcTyVar -> EqCt -> InertEqs addTyEq InertEqs eqs TcTyVar tv EqCt eq_ct addInertEqs EqCt other InertEqs _ = String -> SDoc -> InertEqs forall a. HasCallStack => String -> SDoc -> a pprPanic String "extendInertEqs" (EqCt -> SDoc forall a. Outputable a => a -> SDoc ppr EqCt other) ------------------------ addCanFunEq :: InertFunEqs -> TyCon -> [TcType] -> EqCt -> InertFunEqs addCanFunEq :: InertFunEqs -> TyCon -> [Type] -> EqCt -> InertFunEqs addCanFunEq InertFunEqs old_eqs TyCon fun_tc [Type] fun_args EqCt ct = InertFunEqs -> TyCon -> [Type] -> (Maybe EqualCtList -> Maybe EqualCtList) -> InertFunEqs forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a alterTcApp InertFunEqs 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) = EqualCtList -> Maybe EqualCtList forall a. a -> Maybe a Just (EqualCtList -> Maybe EqualCtList) -> EqualCtList -> Maybe EqualCtList forall a b. (a -> b) -> a -> b $ EqCt -> EqualCtList -> EqualCtList addToEqualCtList EqCt ct EqualCtList old_equal_ct_list upd Maybe EqualCtList Nothing = EqualCtList -> Maybe EqualCtList forall a. a -> Maybe a Just [EqCt ct] foldFunEqs :: (EqCt -> b -> b) -> FunEqMap EqualCtList -> b -> b foldFunEqs :: forall b. (EqCt -> b -> b) -> InertFunEqs -> b -> b foldFunEqs EqCt -> b -> b k InertFunEqs fun_eqs b z = (EqualCtList -> b -> b) -> InertFunEqs -> b -> b forall a b. (a -> b -> b) -> TcAppMap a -> b -> b foldTcAppMap (\EqualCtList eqs b z -> (EqCt -> b -> b) -> b -> EqualCtList -> b forall a b. (a -> b -> b) -> b -> [a] -> b forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr EqCt -> b -> b k b z EqualCtList eqs) InertFunEqs fun_eqs b z partitionFunEqs :: (EqCt -> Bool) -- EqCt will have a TyFamLHS -> InertFunEqs -> ([EqCt], InertFunEqs) partitionFunEqs :: (EqCt -> Bool) -> InertFunEqs -> (EqualCtList, InertFunEqs) partitionFunEqs = InertFunEqs -> (forall b. (EqCt -> b -> b) -> InertFunEqs -> b -> b) -> (EqCt -> InertFunEqs -> InertFunEqs) -> (EqCt -> Bool) -> InertFunEqs -> (EqualCtList, InertFunEqs) forall container. container -> (forall b. (EqCt -> b -> b) -> container -> b -> b) -> (EqCt -> container -> container) -> (EqCt -> Bool) -> container -> (EqualCtList, container) partition_eqs_container InertFunEqs forall a. TcAppMap a emptyFunEqs (EqCt -> b -> b) -> InertFunEqs -> b -> b forall b. (EqCt -> b -> b) -> InertFunEqs -> b -> b foldFunEqs EqCt -> InertFunEqs -> InertFunEqs addFunEqs addFunEqs :: EqCt -> InertFunEqs -> InertFunEqs -- Precondition: EqCt is a TyFamLHS addFunEqs :: EqCt -> InertFunEqs -> InertFunEqs addFunEqs eq_ct :: EqCt eq_ct@(EqCt { eq_lhs :: EqCt -> CanEqLHS eq_lhs = TyFamLHS TyCon tc [Type] args }) InertFunEqs fun_eqs = InertFunEqs -> TyCon -> [Type] -> EqCt -> InertFunEqs addCanFunEq InertFunEqs fun_eqs TyCon tc [Type] args EqCt eq_ct addFunEqs EqCt other InertFunEqs _ = String -> SDoc -> InertFunEqs forall a. HasCallStack => String -> SDoc -> a pprPanic String "extendFunEqs" (EqCt -> SDoc forall a. Outputable a => a -> SDoc ppr EqCt other) {- ********************************************************************* * * Inert Dicts * * ********************************************************************* -} updDicts :: (DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans updDicts :: (DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans updDicts DictMap DictCt -> DictMap DictCt upd InertCans ics = InertCans ics { inert_dicts = upd (inert_dicts ics) } delDict :: DictCt -> DictMap a -> DictMap a delDict :: forall a. DictCt -> DictMap a -> DictMap a delDict (DictCt { di_cls :: DictCt -> Class di_cls = Class cls, di_tys :: DictCt -> [Type] di_tys = [Type] tys }) DictMap a m = DictMap a -> TyCon -> [Type] -> DictMap a forall a. TcAppMap a -> TyCon -> [Type] -> TcAppMap a delTcApp DictMap a m (Class -> TyCon classTyCon Class cls) [Type] tys addDict :: DictCt -> DictMap DictCt -> DictMap DictCt addDict :: DictCt -> DictMap DictCt -> DictMap DictCt addDict item :: DictCt item@(DictCt { di_cls :: DictCt -> Class di_cls = Class cls, di_tys :: DictCt -> [Type] di_tys = [Type] tys }) DictMap DictCt dm = DictMap DictCt -> TyCon -> [Type] -> DictCt -> DictMap DictCt forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a insertTcApp DictMap DictCt dm (Class -> TyCon classTyCon Class cls) [Type] tys DictCt item addSolvedDict :: DictCt -> DictMap DictCt -> DictMap DictCt addSolvedDict :: DictCt -> DictMap DictCt -> DictMap DictCt addSolvedDict item :: DictCt item@(DictCt { di_cls :: DictCt -> Class di_cls = Class cls, di_tys :: DictCt -> [Type] di_tys = [Type] tys }) DictMap DictCt dm = DictMap DictCt -> TyCon -> [Type] -> DictCt -> DictMap DictCt forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a insertTcApp DictMap DictCt dm (Class -> TyCon classTyCon Class cls) [Type] tys DictCt item filterDicts :: (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt filterDicts :: (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt filterDicts DictCt -> Bool f DictMap DictCt m = (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a filterTcAppMap DictCt -> Bool f DictMap DictCt m partitionDicts :: (DictCt -> Bool) -> DictMap DictCt -> (Bag DictCt, DictMap DictCt) partitionDicts :: (DictCt -> Bool) -> DictMap DictCt -> (Bag DictCt, DictMap DictCt) partitionDicts DictCt -> Bool f DictMap DictCt m = (DictCt -> (Bag DictCt, DictMap DictCt) -> (Bag DictCt, DictMap DictCt)) -> DictMap DictCt -> (Bag DictCt, DictMap DictCt) -> (Bag DictCt, DictMap DictCt) forall a b. (a -> b -> b) -> TcAppMap a -> b -> b foldTcAppMap DictCt -> (Bag DictCt, DictMap DictCt) -> (Bag DictCt, DictMap DictCt) k DictMap DictCt m (Bag DictCt forall a. Bag a emptyBag, DictMap DictCt forall a. TcAppMap a emptyDictMap) where k :: DictCt -> (Bag DictCt, DictMap DictCt) -> (Bag DictCt, DictMap DictCt) k DictCt ct (Bag DictCt yeses, DictMap DictCt noes) | DictCt -> Bool f DictCt ct = (DictCt ct DictCt -> Bag DictCt -> Bag DictCt forall a. a -> Bag a -> Bag a `consBag` Bag DictCt yeses, DictMap DictCt noes) | Bool otherwise = (Bag DictCt yeses, DictCt -> DictMap DictCt -> DictMap DictCt addDict DictCt ct DictMap DictCt noes) {- ********************************************************************* * * Inert Irreds * * ********************************************************************* -} addIrredToCans :: TcLevel -> IrredCt -> InertCans -> InertCans addIrredToCans :: TcLevel -> IrredCt -> InertCans -> InertCans addIrredToCans TcLevel tc_lvl IrredCt irred InertCans ics = TcLevel -> Ct -> InertCans -> InertCans updGivenEqs TcLevel tc_lvl (IrredCt -> Ct CIrredCan IrredCt irred) (InertCans -> InertCans) -> InertCans -> InertCans forall a b. (a -> b) -> a -> b $ (InertIrreds -> InertIrreds) -> InertCans -> InertCans updIrreds (IrredCt -> InertIrreds -> InertIrreds addIrred IrredCt irred) InertCans ics addIrreds :: [IrredCt] -> InertIrreds -> InertIrreds addIrreds :: [IrredCt] -> InertIrreds -> InertIrreds addIrreds [IrredCt] extras InertIrreds irreds | [IrredCt] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [IrredCt] extras = InertIrreds irreds | Bool otherwise = InertIrreds irreds InertIrreds -> InertIrreds -> InertIrreds forall a. Bag a -> Bag a -> Bag a `unionBags` [IrredCt] -> InertIrreds forall a. [a] -> Bag a listToBag [IrredCt] extras addIrred :: IrredCt -> InertIrreds -> InertIrreds addIrred :: IrredCt -> InertIrreds -> InertIrreds addIrred IrredCt extra InertIrreds irreds = InertIrreds irreds InertIrreds -> IrredCt -> InertIrreds forall a. Bag a -> a -> Bag a `snocBag` IrredCt extra updIrreds :: (InertIrreds -> InertIrreds) -> InertCans -> InertCans updIrreds :: (InertIrreds -> InertIrreds) -> InertCans -> InertCans updIrreds InertIrreds -> InertIrreds upd InertCans ics = InertCans ics { inert_irreds = upd (inert_irreds ics) } delIrred :: IrredCt -> InertCans -> InertCans -- Remove a particular (Given) Irred, on the instructions of a plugin -- For some reason this is done vis the evidence Id, not the type -- Compare delEq. I have not idea why delIrred :: IrredCt -> InertCans -> InertCans delIrred (IrredCt { ir_ev :: IrredCt -> CtEvidence ir_ev = CtEvidence ev }) InertCans ics = (InertIrreds -> InertIrreds) -> InertCans -> InertCans updIrreds ((IrredCt -> Bool) -> InertIrreds -> InertIrreds forall a. (a -> Bool) -> Bag a -> Bag a filterBag IrredCt -> Bool keep) InertCans ics where ev_id :: TcTyVar ev_id = CtEvidence -> TcTyVar ctEvEvId CtEvidence ev keep :: IrredCt -> Bool keep (IrredCt { ir_ev :: IrredCt -> CtEvidence ir_ev = CtEvidence ev' }) = TcTyVar ev_id TcTyVar -> TcTyVar -> Bool forall a. Eq a => a -> a -> Bool /= CtEvidence -> TcTyVar ctEvEvId CtEvidence ev' foldIrreds :: (IrredCt -> b -> b) -> InertIrreds -> b -> b foldIrreds :: forall b. (IrredCt -> b -> b) -> InertIrreds -> b -> b foldIrreds IrredCt -> b -> b k InertIrreds irreds b z = (IrredCt -> b -> b) -> b -> InertIrreds -> b forall a b. (a -> b -> b) -> b -> Bag a -> b forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr IrredCt -> b -> b k b z InertIrreds irreds findMatchingIrreds :: InertIrreds -> CtEvidence -> (Bag (IrredCt, SwapFlag), InertIrreds) findMatchingIrreds :: InertIrreds -> CtEvidence -> (Bag (IrredCt, SwapFlag), InertIrreds) findMatchingIrreds InertIrreds irreds CtEvidence ev | EqPred EqRel eq_rel1 Type lty1 Type rty1 <- Type -> Pred classifyPredType Type pred -- See Note [Solving irreducible equalities] = (IrredCt -> Either (IrredCt, SwapFlag) IrredCt) -> InertIrreds -> (Bag (IrredCt, SwapFlag), InertIrreds) forall a b c. (a -> Either b c) -> Bag a -> (Bag b, Bag c) partitionBagWith (EqRel -> Type -> Type -> IrredCt -> Either (IrredCt, SwapFlag) IrredCt match_eq EqRel eq_rel1 Type lty1 Type rty1) InertIrreds irreds | Bool otherwise = (IrredCt -> Either (IrredCt, SwapFlag) IrredCt) -> InertIrreds -> (Bag (IrredCt, SwapFlag), InertIrreds) forall a b c. (a -> Either b c) -> Bag a -> (Bag b, Bag c) partitionBagWith IrredCt -> Either (IrredCt, SwapFlag) IrredCt match_non_eq InertIrreds irreds where pred :: Type pred = CtEvidence -> Type ctEvPred CtEvidence ev match_non_eq :: IrredCt -> Either (IrredCt, SwapFlag) IrredCt match_non_eq IrredCt irred | IrredCt -> Type irredCtPred IrredCt irred Type -> Type -> Bool `tcEqTypeNoKindCheck` Type pred = (IrredCt, SwapFlag) -> Either (IrredCt, SwapFlag) IrredCt forall a b. a -> Either a b Left (IrredCt irred, SwapFlag NotSwapped) | Bool otherwise = IrredCt -> Either (IrredCt, SwapFlag) IrredCt forall a b. b -> Either a b Right IrredCt irred match_eq :: EqRel -> Type -> Type -> IrredCt -> Either (IrredCt, SwapFlag) IrredCt match_eq EqRel eq_rel1 Type lty1 Type rty1 IrredCt irred | EqPred EqRel eq_rel2 Type lty2 Type rty2 <- Type -> Pred classifyPredType (IrredCt -> Type irredCtPred IrredCt irred) , EqRel eq_rel1 EqRel -> EqRel -> Bool forall a. Eq a => a -> a -> Bool == EqRel eq_rel2 , Just SwapFlag swap <- Type -> Type -> Type -> Type -> Maybe SwapFlag match_eq_help Type lty1 Type rty1 Type lty2 Type rty2 = (IrredCt, SwapFlag) -> Either (IrredCt, SwapFlag) IrredCt forall a b. a -> Either a b Left (IrredCt irred, SwapFlag swap) | Bool otherwise = IrredCt -> Either (IrredCt, SwapFlag) IrredCt forall a b. b -> Either a b Right IrredCt irred match_eq_help :: Type -> Type -> Type -> Type -> Maybe SwapFlag match_eq_help Type lty1 Type rty1 Type lty2 Type rty2 | Type lty1 Type -> Type -> Bool `tcEqTypeNoKindCheck` Type lty2, Type rty1 Type -> Type -> Bool `tcEqTypeNoKindCheck` Type rty2 = SwapFlag -> Maybe SwapFlag forall a. a -> Maybe a Just SwapFlag NotSwapped | Type lty1 Type -> Type -> Bool `tcEqTypeNoKindCheck` Type rty2, Type rty1 Type -> Type -> Bool `tcEqTypeNoKindCheck` Type lty2 = SwapFlag -> Maybe SwapFlag forall a. a -> Maybe a Just SwapFlag IsSwapped | Bool otherwise = Maybe SwapFlag forall a. Maybe a Nothing {- Note [Solving irreducible equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider (#14333) [G] a b ~R# c d [W] c d ~R# a b Clearly we should be able to solve this! Even though the constraints are not decomposable. We solve this when looking up the work-item in the irreducible constraints to look for an identical one. When doing this lookup, findMatchingIrreds spots the equality case, and matches either way around. It has to return a swap-flag so we can generate evidence that is the right way round too. -} {- ********************************************************************* * * Adding to and removing from the inert set * * * * ********************************************************************* -} updGivenEqs :: 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 Note [Tracking Given equalities] -- -- Precondition: Ct is either CEqCan or CIrredCan updGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans updGivenEqs TcLevel tclvl Ct ct InertCans inerts | Bool -> Bool not (Ct -> Bool isGivenCt Ct ct) = InertCans inerts -- See Note [Let-bound skolems] | TcLevel -> Ct -> Bool isLetBoundSkolemCt TcLevel tclvl Ct ct = InertCans inerts { inert_given_eqs = True } -- At this point we are left with a constraint that either -- is an equality (F a ~ ty), or /might/ be, like (c a) | Bool otherwise = InertCans inerts { inert_given_eq_lvl = tclvl , inert_given_eqs = True } isLetBoundSkolemCt :: TcLevel -> Ct -> Bool -- See Note [Let-bound skolems] isLetBoundSkolemCt :: TcLevel -> Ct -> Bool isLetBoundSkolemCt TcLevel tclvl (CEqCan (EqCt { eq_lhs :: EqCt -> CanEqLHS eq_lhs = CanEqLHS lhs, eq_rhs :: EqCt -> Type eq_rhs = Type rhs })) = case CanEqLHS lhs of TyVarLHS TcTyVar tv -> Bool -> Bool not (TcLevel -> TcTyVar -> Bool isOuterTyVar TcLevel tclvl TcTyVar tv) TyFamLHS {} -> case Type -> Maybe TcTyVar getTyVar_maybe Type rhs of Just TcTyVar tv -> Bool -> Bool not (TcLevel -> TcTyVar -> Bool isOuterTyVar TcLevel tclvl TcTyVar tv) Maybe TcTyVar Nothing -> Bool False isLetBoundSkolemCt TcLevel _ Ct _ = Bool False data KickOutSpec -- See Note [KickOutSpec] = KOAfterUnify TcTyVarSet -- We have unified these tyvars | KOAfterAdding CanEqLHS -- We are adding to the inert set a canonical equality -- constraint with this LHS instance Outputable KickOutSpec where ppr :: KickOutSpec -> SDoc ppr (KOAfterUnify TcTyVarSet tvs) = String -> SDoc forall doc. IsLine doc => String -> doc text String "KOAfterUnify" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <> TcTyVarSet -> SDoc forall a. Outputable a => a -> SDoc ppr TcTyVarSet tvs ppr (KOAfterAdding CanEqLHS lhs) = String -> SDoc forall doc. IsLine doc => String -> doc text String "KOAfterAdding" SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <> SDoc -> SDoc forall doc. IsLine doc => doc -> doc parens (CanEqLHS -> SDoc forall a. Outputable a => a -> SDoc ppr CanEqLHS lhs) {- Note [KickOutSpec] ~~~~~~~~~~~~~~~~~~~~~~ KickOutSpec explains why we are kicking out. Important property: KOAfterAdding (TyVarLHS tv) should behave exactly like KOAfterUnifying (unitVarSet tv) The main reasons for treating the two separately are * More efficient in the single-tyvar case * The code is far more perspicuous -} data WhereToLook = LookEverywhere | LookOnlyUnderFamApps deriving( WhereToLook -> WhereToLook -> Bool (WhereToLook -> WhereToLook -> Bool) -> (WhereToLook -> WhereToLook -> Bool) -> Eq WhereToLook forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a $c== :: WhereToLook -> WhereToLook -> Bool == :: WhereToLook -> WhereToLook -> Bool $c/= :: WhereToLook -> WhereToLook -> Bool /= :: WhereToLook -> WhereToLook -> Bool Eq ) kickOutRewritableLHS :: KickOutSpec -> CtFlavourRole -> InertCans -> (Cts, InertCans) -- See Note [kickOutRewritable] kickOutRewritableLHS :: KickOutSpec -> CtFlavourRole -> InertCans -> (Bag Ct, InertCans) kickOutRewritableLHS KickOutSpec ko_spec new_fr :: CtFlavourRole new_fr@(CtFlavour _, EqRel new_role) ics :: InertCans ics@(IC { inert_eqs :: InertCans -> InertEqs inert_eqs = InertEqs tv_eqs , inert_dicts :: InertCans -> DictMap DictCt inert_dicts = DictMap DictCt dictmap , inert_funeqs :: InertCans -> InertFunEqs inert_funeqs = InertFunEqs funeqmap , inert_irreds :: InertCans -> InertIrreds inert_irreds = InertIrreds irreds , inert_insts :: InertCans -> [QCInst] inert_insts = [QCInst] old_insts }) = (Bag Ct 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 = tv_eqs_in , inert_dicts = dicts_in , inert_funeqs = feqs_in , inert_irreds = irs_in , inert_insts = insts_in } kicked_out :: Cts kicked_out :: Bag Ct kicked_out = ((DictCt -> Ct) -> Bag DictCt -> Bag Ct forall a b. (a -> b) -> Bag a -> Bag b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap DictCt -> Ct CDictCan Bag DictCt dicts_out Bag Ct -> Bag Ct -> Bag Ct `andCts` (IrredCt -> Ct) -> InertIrreds -> Bag Ct forall a b. (a -> b) -> Bag a -> Bag b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap IrredCt -> Ct CIrredCan InertIrreds irs_out) Bag Ct -> [Ct] -> Bag Ct `extendCtsList` [Ct] insts_out Bag Ct -> [Ct] -> Bag Ct `extendCtsList` (EqCt -> Ct) -> EqualCtList -> [Ct] forall a b. (a -> b) -> [a] -> [b] map EqCt -> Ct CEqCan EqualCtList tv_eqs_out Bag Ct -> [Ct] -> Bag Ct `extendCtsList` (EqCt -> Ct) -> EqualCtList -> [Ct] forall a b. (a -> b) -> [a] -> [b] map EqCt -> Ct CEqCan EqualCtList feqs_out (EqualCtList tv_eqs_out, InertEqs tv_eqs_in) = (EqCt -> Bool) -> InertEqs -> (EqualCtList, InertEqs) partitionInertEqs EqCt -> Bool kick_out_eq InertEqs tv_eqs (EqualCtList feqs_out, InertFunEqs feqs_in) = (EqCt -> Bool) -> InertFunEqs -> (EqualCtList, InertFunEqs) partitionFunEqs EqCt -> Bool kick_out_eq InertFunEqs funeqmap (Bag DictCt dicts_out, DictMap DictCt dicts_in) = (DictCt -> Bool) -> DictMap DictCt -> (Bag DictCt, DictMap DictCt) partitionDicts DictCt -> Bool kick_out_dict DictMap DictCt dictmap (InertIrreds irs_out, InertIrreds irs_in) = (IrredCt -> Bool) -> InertIrreds -> (InertIrreds, InertIrreds) forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a) partitionBag IrredCt -> Bool kick_out_irred InertIrreds 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.Solve insts_out :: [Ct] insts_in :: [QCInst] ([Ct] insts_out, [QCInst] insts_in) | CtFlavourRole -> Bool fr_may_rewrite (CtFlavour Given, EqRel NomEq) -- All the insts are Givens = (QCInst -> Either Ct QCInst) -> [QCInst] -> ([Ct], [QCInst]) forall a b c. (a -> Either b c) -> [a] -> ([b], [c]) partitionWith QCInst -> Either Ct QCInst kick_out_qci [QCInst] old_insts | Bool otherwise = ([], [QCInst] old_insts) kick_out_qci :: QCInst -> Either Ct QCInst kick_out_qci QCInst qci | let ev :: CtEvidence ev = QCInst -> CtEvidence qci_ev QCInst qci , WhereToLook -> EqRel -> Type -> Bool fr_can_rewrite_ty WhereToLook LookEverywhere EqRel NomEq (CtEvidence -> Type ctEvPred (QCInst -> CtEvidence qci_ev QCInst qci)) = Ct -> Either Ct QCInst forall a b. a -> Either a b Left (CtEvidence -> Ct mkNonCanonical CtEvidence ev) | Bool otherwise = QCInst -> Either Ct QCInst forall a b. b -> Either a b Right QCInst qci fr_tv_can_rewrite_ty :: WhereToLook -> (TyVar -> Bool) -> EqRel -> Type -> Bool fr_tv_can_rewrite_ty :: WhereToLook -> (TcTyVar -> Bool) -> EqRel -> Type -> Bool fr_tv_can_rewrite_ty WhereToLook where_to_look TcTyVar -> Bool check_tv EqRel role Type ty = EqRel -> (Bool -> EqRel -> TcTyVar -> Bool) -> Type -> Bool anyRewritableTyVar EqRel role Bool -> EqRel -> TcTyVar -> Bool can_rewrite Type ty where can_rewrite :: UnderFam -> EqRel -> TyVar -> Bool can_rewrite :: Bool -> EqRel -> TcTyVar -> Bool can_rewrite Bool is_under_famapp EqRel old_role TcTyVar tv = (WhereToLook where_to_look WhereToLook -> WhereToLook -> Bool forall a. Eq a => a -> a -> Bool == WhereToLook LookEverywhere Bool -> Bool -> Bool || Bool is_under_famapp) Bool -> Bool -> Bool && EqRel new_role EqRel -> EqRel -> Bool `eqCanRewrite` EqRel old_role Bool -> Bool -> Bool && TcTyVar -> Bool check_tv TcTyVar tv fr_tf_can_rewrite_ty :: WhereToLook -> TyCon -> [TcType] -> EqRel -> Type -> Bool fr_tf_can_rewrite_ty :: WhereToLook -> TyCon -> [Type] -> EqRel -> Type -> Bool fr_tf_can_rewrite_ty WhereToLook where_to_look TyCon new_tf [Type] new_tf_args EqRel role Type ty = EqRel -> (Bool -> EqRel -> TyCon -> [Type] -> Bool) -> Type -> Bool anyRewritableTyFamApp EqRel role Bool -> EqRel -> TyCon -> [Type] -> Bool can_rewrite Type ty where can_rewrite :: UnderFam -> EqRel -> TyCon -> [TcType] -> Bool can_rewrite :: Bool -> EqRel -> TyCon -> [Type] -> Bool can_rewrite Bool is_under_famapp EqRel old_role TyCon old_tf [Type] old_tf_args = (WhereToLook where_to_look WhereToLook -> WhereToLook -> Bool forall a. Eq a => a -> a -> Bool == WhereToLook LookEverywhere Bool -> Bool -> Bool || Bool is_under_famapp) Bool -> Bool -> Bool && 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. fr_can_rewrite_ty :: WhereToLook -> EqRel -> Type -> Bool -- UnderFam = True <=> look only under type-family applications fr_can_rewrite_ty :: WhereToLook -> EqRel -> Type -> Bool fr_can_rewrite_ty WhereToLook uf = case KickOutSpec ko_spec of -- See Note [KickOutSpec] KOAfterUnify TcTyVarSet tvs -> WhereToLook -> (TcTyVar -> Bool) -> EqRel -> Type -> Bool fr_tv_can_rewrite_ty WhereToLook uf (TcTyVar -> TcTyVarSet -> Bool `elemVarSet` TcTyVarSet tvs) KOAfterAdding (TyVarLHS TcTyVar tv) -> WhereToLook -> (TcTyVar -> Bool) -> EqRel -> Type -> Bool fr_tv_can_rewrite_ty WhereToLook uf (TcTyVar -> TcTyVar -> Bool forall a. Eq a => a -> a -> Bool == TcTyVar tv) KOAfterAdding (TyFamLHS TyCon tf [Type] tf_args) -> WhereToLook -> TyCon -> [Type] -> EqRel -> Type -> Bool fr_tf_can_rewrite_ty WhereToLook uf TyCon tf [Type] tf_args fr_may_rewrite :: CtFlavourRole -> Bool fr_may_rewrite :: CtFlavourRole -> Bool fr_may_rewrite CtFlavourRole fs = CtFlavourRole new_fr CtFlavourRole -> CtFlavourRole -> Bool `eqCanRewriteFR` CtFlavourRole fs -- Can the new item rewrite the inert item? kick_out_dict :: DictCt -> Bool -- Kick it out if the new CEqCan can rewrite the inert one -- See Note [kickOutRewritable] kick_out_dict :: DictCt -> Bool kick_out_dict (DictCt { di_tys :: DictCt -> [Type] di_tys = [Type] tys, di_ev :: DictCt -> CtEvidence di_ev = CtEvidence ev }) = CtFlavourRole -> Bool fr_may_rewrite (CtEvidence -> CtFlavour ctEvFlavour CtEvidence ev, EqRel NomEq) Bool -> Bool -> Bool && (Type -> Bool) -> [Type] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool any (WhereToLook -> EqRel -> Type -> Bool fr_can_rewrite_ty WhereToLook LookEverywhere EqRel NomEq) [Type] tys kick_out_irred :: IrredCt -> Bool kick_out_irred :: IrredCt -> Bool kick_out_irred (IrredCt { ir_ev :: IrredCt -> CtEvidence ir_ev = CtEvidence ev }) = CtFlavourRole -> Bool fr_may_rewrite (CtEvidence -> CtFlavour ctEvFlavour CtEvidence ev, EqRel eq_rel) Bool -> Bool -> Bool && WhereToLook -> EqRel -> Type -> Bool fr_can_rewrite_ty WhereToLook LookEverywhere EqRel eq_rel Type pred where pred :: Type pred = CtEvidence -> Type ctEvPred CtEvidence ev eq_rel :: EqRel eq_rel = Type -> EqRel predTypeEqRel Type pred -- Implements criteria K1-K3 in Note [Extending the inert equalities] kick_out_eq :: EqCt -> Bool kick_out_eq :: EqCt -> Bool kick_out_eq (EqCt { eq_lhs :: EqCt -> CanEqLHS eq_lhs = CanEqLHS lhs, eq_rhs :: EqCt -> Type eq_rhs = Type rhs_ty , eq_ev :: EqCt -> CtEvidence eq_ev = CtEvidence ev, eq_eq_rel :: EqCt -> EqRel eq_eq_rel = EqRel eq_rel }) -- (KK0) Keep it in the inert set if the new thing can't rewrite it | Bool -> Bool not (CtFlavourRole -> Bool fr_may_rewrite CtFlavourRole fs) = Bool False -- Below here (fr_may_rewrite fs) is True -- (KK1) | WhereToLook -> EqRel -> Type -> Bool fr_can_rewrite_ty WhereToLook LookEverywhere EqRel eq_rel (CanEqLHS -> Type canEqLHSType CanEqLHS lhs) = Bool True -- (KK1) -- The above check redundantly checks the role & flavour, -- but it's very convenient -- (KK2) | let where_to_look :: WhereToLook where_to_look | Bool fs_can_rewrite_fr = WhereToLook LookOnlyUnderFamApps | Bool otherwise = WhereToLook LookEverywhere , WhereToLook -> EqRel -> Type -> Bool fr_can_rewrite_ty WhereToLook where_to_look EqRel eq_rel Type rhs_ty = Bool True -- (KK3) | Bool -> Bool not Bool fs_can_rewrite_fr -- (KK3a) , case EqRel eq_rel of EqRel NomEq -> Type -> Bool is_new_lhs Type rhs_ty -- (KK3b) EqRel ReprEq -> Type -> Bool head_is_new_lhs Type rhs_ty -- (KK3c) = Bool True | Bool otherwise = Bool False where fs_can_rewrite_fr :: Bool fs_can_rewrite_fr = CtFlavourRole fs CtFlavourRole -> CtFlavourRole -> Bool `eqCanRewriteFR` CtFlavourRole new_fr fs :: CtFlavourRole fs = (CtEvidence -> CtFlavour ctEvFlavour CtEvidence ev, EqRel eq_rel) is_new_lhs :: Type -> Bool is_new_lhs :: Type -> Bool is_new_lhs = case KickOutSpec ko_spec of -- See Note [KickOutSpec] KOAfterUnify TcTyVarSet tvs -> TcTyVarSet -> Type -> Bool is_tyvar_ty_for TcTyVarSet tvs KOAfterAdding CanEqLHS lhs -> (HasCallStack => Type -> Type -> Bool Type -> Type -> Bool `eqType` CanEqLHS -> Type canEqLHSType CanEqLHS lhs) is_tyvar_ty_for :: TcTyVarSet -> Type -> Bool -- True if the type is equal to one of the tyvars is_tyvar_ty_for :: TcTyVarSet -> Type -> Bool is_tyvar_ty_for TcTyVarSet tvs Type ty = case Type -> Maybe TcTyVar getTyVar_maybe Type ty of Maybe TcTyVar Nothing -> Bool False Just TcTyVar tv -> TcTyVar tv TcTyVar -> TcTyVarSet -> Bool `elemVarSet` TcTyVarSet tvs head_is_new_lhs :: Type -> Bool head_is_new_lhs :: Type -> Bool head_is_new_lhs = case KickOutSpec ko_spec of -- See Note [KickOutSpec] KOAfterUnify TcTyVarSet tvs -> (TcTyVar -> Bool) -> Type -> Bool tv_at_head (TcTyVar -> TcTyVarSet -> Bool `elemVarSet` TcTyVarSet tvs) KOAfterAdding (TyVarLHS TcTyVar tv) -> (TcTyVar -> Bool) -> Type -> Bool tv_at_head (TcTyVar -> TcTyVar -> Bool forall a. Eq a => a -> a -> Bool == TcTyVar tv) KOAfterAdding (TyFamLHS TyCon tf [Type] tf_args) -> TyCon -> [Type] -> Type -> Bool fam_at_head TyCon tf [Type] tf_args tv_at_head :: (TyVar -> Bool) -> Type -> Bool tv_at_head :: (TcTyVar -> Bool) -> Type -> Bool tv_at_head TcTyVar -> Bool is_tv = Type -> Bool go where go :: Type -> Bool go (Rep.TyVarTy TcTyVar tv) = TcTyVar -> Bool is_tv TcTyVar tv go (Rep.AppTy Type fun Type _) = Type -> Bool go Type fun go (Rep.CastTy Type ty KindCoercion _) = 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 fam_at_head :: TyCon -> [Type] -> Type -> Bool fam_at_head :: TyCon -> [Type] -> Type -> Bool fam_at_head 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 KindCoercion _) = 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 {- 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! - 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] in GHC.Tc.Solver.Monad. 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.Equality See Note [Make sure that insolubles are fully rewritten] in GHC.Tc.Solver.Equality -} {- ********************************************************************* * * Queries * * * * ********************************************************************* -} 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 = Bool -> SDoc -> Bool -> Bool forall a. HasCallStack => Bool -> SDoc -> a -> a assertPpr (Bool -> Bool not (TcLevel -> TcTyVar -> Bool isTouchableMetaTyVar TcLevel tclvl TcTyVar tv)) (TcTyVar -> SDoc forall a. Outputable a => a -> SDoc ppr TcTyVar tv SDoc -> SDoc -> SDoc forall doc. IsLine doc => doc -> doc -> doc <+> TcLevel -> SDoc forall a. Outputable a => a -> SDoc ppr TcLevel tclvl) (Bool -> Bool) -> Bool -> Bool forall a b. (a -> b) -> a -> b $ 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 noGivenNewtypeReprEqs :: TyCon -> InertSet -> Bool -- True <=> there is no Irred looking like (N tys1 ~ N tys2) -- See Note [Decomposing newtype equalities] (EX2) in GHC.Tc.Solver.Equality -- This is the only call site. noGivenNewtypeReprEqs :: TyCon -> InertSet -> Bool noGivenNewtypeReprEqs TyCon tc InertSet inerts = Bool -> Bool not ((IrredCt -> Bool) -> InertIrreds -> Bool forall a. (a -> Bool) -> Bag a -> Bool anyBag IrredCt -> Bool might_help (InertCans -> InertIrreds inert_irreds (InertSet -> InertCans inert_cans InertSet inerts))) where might_help :: IrredCt -> Bool might_help IrredCt irred = case Type -> Pred classifyPredType (CtEvidence -> Type ctEvPred (IrredCt -> CtEvidence irredCtEvidence IrredCt irred)) of EqPred EqRel ReprEq Type t1 Type t2 | Just (TyCon tc1,[Type] _) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type]) Type -> Maybe (TyCon, [Type]) tcSplitTyConApp_maybe Type t1 , TyCon tc TyCon -> TyCon -> Bool forall a. Eq a => a -> a -> Bool == TyCon tc1 , Just (TyCon tc2,[Type] _) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type]) Type -> Maybe (TyCon, [Type]) tcSplitTyConApp_maybe Type t2 , TyCon tc TyCon -> TyCon -> Bool forall a. Eq a => a -> a -> Bool == TyCon tc2 -> Bool True Pred _ -> Bool False -- | Returns True iff there are no Given constraints that might, -- potentially, match the given class constraint. 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.Dict noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [TcType] -> Bool noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [Type] -> Bool noMatchableGivenDicts inerts :: InertSet inerts@(IS { inert_cans :: InertSet -> InertCans inert_cans = InertCans inert_cans }) CtLoc loc_w Class clas [Type] tys = Bool -> Bool not (Bool -> Bool) -> Bool -> Bool forall a b. (a -> b) -> a -> b $ (DictCt -> Bool) -> Bag DictCt -> Bool forall a. (a -> Bool) -> Bag a -> Bool anyBag DictCt -> Bool matchable_given (Bag DictCt -> Bool) -> Bag DictCt -> Bool forall a b. (a -> b) -> a -> b $ DictMap DictCt -> Class -> Bag DictCt forall a. DictMap a -> Class -> Bag a findDictsByClass (InertCans -> DictMap DictCt inert_dicts InertCans inert_cans) Class clas where pred_w :: Type pred_w = Class -> [Type] -> Type mkClassPred Class clas [Type] tys matchable_given :: DictCt -> Bool matchable_given :: DictCt -> Bool matchable_given (DictCt { di_ev :: DictCt -> CtEvidence di_ev = CtEvidence ev }) | CtGiven { ctev_loc :: CtEvidence -> CtLoc ctev_loc = CtLoc loc_g, ctev_pred :: CtEvidence -> Type ctev_pred = Type pred_g } <- CtEvidence ev = Maybe Subst -> Bool forall a. Maybe a -> Bool isJust (Maybe Subst -> Bool) -> Maybe Subst -> Bool forall a b. (a -> b) -> a -> b $ InertSet -> Type -> CtLoc -> Type -> CtLoc -> Maybe Subst 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 -> Maybe Subst -- See Note [What might equal later?] -- Used to implement logic in Note [Instance and Given overlap] in GHC.Tc.Solver.Dict mightEqualLater :: InertSet -> Type -> CtLoc -> Type -> CtLoc -> Maybe Subst 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 = Maybe Subst forall a. Maybe a Nothing | Bool otherwise = case BindFun -> [Type] -> [Type] -> UnifyResult tcUnifyTysFG BindFun bind_fun [Type flattened_given] [Type flattened_wanted] of Unifiable Subst subst -> Subst -> Maybe Subst forall a. a -> Maybe a Just Subst subst MaybeApart MaybeApartReason reason Subst subst | MaybeApartReason MARInfinite <- MaybeApartReason reason -- see Example 7 in the Note. -> Maybe Subst forall a. Maybe a Nothing | Bool otherwise -> Subst -> Maybe Subst forall a. a -> Maybe a Just Subst subst UnifyResult SurelyApart -> Maybe Subst forall a. Maybe a Nothing where in_scope :: InScopeSet in_scope = TcTyVarSet -> InScopeSet mkInScopeSet (TcTyVarSet -> InScopeSet) -> TcTyVarSet -> InScopeSet forall a b. (a -> b) -> a -> b $ [Type] -> TcTyVarSet 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) <- TyVarEnv (TyCon, [Type]) -> TcTyVar -> Maybe (TyCon, [Type]) 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 checkTopShape, 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 getTyVar_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 -- | Is it (potentially) loopy to use the first @ct1@ to solve @ct2@? -- -- Necessary (but not sufficient) conditions for this function to return @True@: -- -- - @ct1@ and @ct2@ both arise from superclass expansion, -- - @ct1@ is a Given and @ct2@ is a Wanted. -- -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance, (sc2). prohibitedSuperClassSolve :: CtLoc -- ^ is it loopy to use this one ... -> CtLoc -- ^ ... to solve this one? -> Bool -- ^ True ==> don't solve it prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool prohibitedSuperClassSolve CtLoc given_loc CtLoc wanted_loc | GivenSCOrigin SkolemInfoAnon _ ScDepth _ Bool blocked <- CtLoc -> CtOrigin ctLocOrigin CtLoc given_loc , Bool blocked , ScOrigin ClsInstOrQC _ NakedScFlag NakedSc <- CtLoc -> CtOrigin ctLocOrigin CtLoc wanted_loc = Bool True -- Prohibited if the Wanted is a superclass -- and the Given has come via a superclass selection from -- a predicate bigger than the head | Bool otherwise = Bool False {- 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. But see also Red Herring below. 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.Equality 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} Red Herring ~~~~~~~~~~~ In #21208, we have this scenario: instance forall b. C b [G] C a[sk] [W] C (F a[sk]) What should we do with that wanted? According to the logic above, the Given cannot match later (this is example 6), and so we use the global instance. But wait, you say: What if we learn later (say by a future type instance F a = a) that F a unifies with a? That looks like the Given might really match later! This mechanism described in this Note is *not* about this kind of situation, however. It is all asking whether a Given might match the Wanted *in this run of the solver*. It is *not* about whether a variable might be instantiated so that the Given matches, or whether a type instance introduced in a downstream module might make the Given match. The reason we care about what might match later is only about avoiding order-dependence. That is, we don't want to commit to a course of action that depends on seeing constraints in a certain order. But an instantiation of a variable and a later type instance don't introduce order dependency in this way, and so mightMatchLater is right to ignore these possibilities. Here is an example, with no type families, that is perhaps clearer: instance forall b. C (Maybe b) [G] C (Maybe Int) [W] C (Maybe a) What to do? We *might* say that the Given could match later and should thus block us from using the global instance. But we don't do this. Instead, we rely on class coherence to say that choosing the global instance is just fine, even if later we call a function with (a := Int). After all, in this run of the solver, [G] C (Maybe Int) will definitely never match [W] C (Maybe a). (Recall that we process Givens before Wanteds, so there is no [G] a ~ Int hanging about unseen.) Interestingly, in the first case (from #21208), the behavior changed between GHC 8.10.7 and GHC 9.2, with the latter behaving correctly and the former reporting overlapping instances. Test case: typecheck/should_compile/T21208. -} {- ********************************************************************* * * 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 <- Bool -> Maybe Type -> Maybe Type forall a. HasCallStack => Bool -> a -> a assert (TcTyVar -> Bool isCycleBreakerTyVar TcTyVar cbv) (Maybe Type -> Maybe Type) -> Maybe Type -> Maybe Type forall a b. (a -> b) -> a -> b $ NonEmpty (Maybe Type) -> Maybe Type forall (f :: * -> *) a. Foldable f => f (Maybe a) -> Maybe a firstJusts ((Bag (TcTyVar, Type) -> Maybe Type) -> CycleBreakerVarStack -> NonEmpty (Maybe Type) forall a b. (a -> b) -> NonEmpty a -> NonEmpty b NE.map (TcTyVar -> Bag (TcTyVar, Type) -> Maybe Type forall a b. Eq a => a -> Bag (a, b) -> Maybe b lookupBag TcTyVar cbv) CycleBreakerVarStack cbvs_stack) = Type tyfam_app | Bool otherwise = String -> SDoc -> Type forall a. HasCallStack => String -> SDoc -> a pprPanic String "lookupCycleBreakerVar found an unbound cycle breaker" (TcTyVar -> SDoc forall a. Outputable a => a -> SDoc ppr TcTyVar cbv SDoc -> SDoc -> SDoc forall doc. IsDoc doc => doc -> doc -> doc $$ CycleBreakerVarStack -> 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 = (Bag (TcTyVar, Type) forall a. Bag a emptyBag Bag (TcTyVar, Type) -> CycleBreakerVarStack -> CycleBreakerVarStack forall a. a -> NonEmpty a -> NonEmpty a <|) -- | Add a new cycle-breaker binding to the top environment on the stack. addCycleBreakerBindings :: Bag (TcTyVar, Type) -- ^ (cbv,expansion) pairs -> InertSet -> InertSet addCycleBreakerBindings :: Bag (TcTyVar, Type) -> InertSet -> InertSet addCycleBreakerBindings Bag (TcTyVar, Type) prs InertSet ics = Bool -> SDoc -> InertSet -> InertSet forall a. HasCallStack => Bool -> SDoc -> a -> a assertPpr (((TcTyVar, Type) -> Bool) -> Bag (TcTyVar, Type) -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool all (TcTyVar -> Bool isCycleBreakerTyVar (TcTyVar -> Bool) -> ((TcTyVar, Type) -> TcTyVar) -> (TcTyVar, Type) -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . (TcTyVar, Type) -> TcTyVar forall a b. (a, b) -> a fst) Bag (TcTyVar, Type) prs) (Bag (TcTyVar, Type) -> SDoc forall a. Outputable a => a -> SDoc ppr Bag (TcTyVar, Type) prs) (InertSet -> InertSet) -> InertSet -> InertSet forall a b. (a -> b) -> a -> b $ InertSet ics { inert_cycle_breakers = add_to (inert_cycle_breakers ics) } where add_to :: CycleBreakerVarStack -> CycleBreakerVarStack add_to (Bag (TcTyVar, Type) top_env :| [Bag (TcTyVar, Type)] rest_envs) = (Bag (TcTyVar, Type) prs Bag (TcTyVar, Type) -> Bag (TcTyVar, Type) -> Bag (TcTyVar, Type) forall a. Bag a -> Bag a -> Bag a `unionBags` Bag (TcTyVar, Type) top_env) Bag (TcTyVar, Type) -> [Bag (TcTyVar, Type)] -> CycleBreakerVarStack forall a. a -> [a] -> NonEmpty a :| [Bag (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_ (Bag (TcTyVar, Type) top_env :| [Bag (TcTyVar, Type)] _rest_envs) TcTyVar -> Type -> m () action = Bag (TcTyVar, Type) -> ((TcTyVar, Type) -> m ()) -> m () forall (t :: * -> *) (m :: * -> *) a b. (Foldable t, Monad m) => t a -> (a -> m b) -> m () forM_ Bag (TcTyVar, Type) top_env ((TcTyVar -> Type -> m ()) -> (TcTyVar, Type) -> m () forall a b c. (a -> b -> c) -> (a, b) -> c uncurry TcTyVar -> Type -> m () action) {-# INLINABLE forAllCycleBreakerBindings_ #-} -- to allow SPECIALISE later {- ********************************************************************* * * Solving one from another * * ********************************************************************* -} data InteractResult = KeepInert -- Keep the inert item, and solve the work item from it -- (if the latter is Wanted; just discard it if not) | KeepWork -- Keep the work item, and solve the inert item from it instance Outputable InteractResult where ppr :: InteractResult -> SDoc ppr InteractResult KeepInert = String -> SDoc forall doc. IsLine doc => String -> doc text String "keep inert" ppr InteractResult KeepWork = String -> SDoc forall doc. IsLine doc => String -> doc text String "keep work-item" solveOneFromTheOther :: Ct -- Inert (Dict or Irred) -> Ct -- WorkItem (same predicate as inert) -> InteractResult -- Precondition: -- * inert and work item represent evidence for the /same/ predicate -- * Both are CDictCan or CIrredCan -- -- We can always solve one from the other: even if both are wanted, -- although we don't rewrite wanteds with wanteds, we can combine -- two wanteds into one by solving one from the other solveOneFromTheOther :: Ct -> Ct -> InteractResult solveOneFromTheOther Ct ct_i Ct ct_w | CtWanted { ctev_loc :: CtEvidence -> CtLoc ctev_loc = CtLoc loc_w } <- CtEvidence ev_w , CtLoc -> CtLoc -> Bool prohibitedSuperClassSolve CtLoc loc_i CtLoc loc_w -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance = -- Inert must be Given InteractResult KeepWork | CtWanted {} <- CtEvidence ev_w = -- Inert is Given or Wanted case CtEvidence ev_i of CtGiven {} -> InteractResult KeepInert -- work is Wanted; inert is Given: easy choice. CtWanted {} -- Both are Wanted -- If only one has no pending superclasses, use it -- Otherwise we can get infinite superclass expansion (#22516) -- in silly cases like class C T b => C a b where ... | Bool -> Bool not Bool is_psc_i, Bool is_psc_w -> InteractResult KeepInert | Bool is_psc_i, Bool -> Bool not Bool is_psc_w -> InteractResult KeepWork -- If only one is a WantedSuperclassOrigin (arising from expanding -- a Wanted class constraint), keep the other: wanted superclasses -- may be unexpected by users | Bool -> Bool not Bool is_wsc_orig_i, Bool is_wsc_orig_w -> InteractResult KeepInert | Bool is_wsc_orig_i, Bool -> Bool not Bool is_wsc_orig_w -> InteractResult KeepWork -- otherwise, just choose the lower span -- reason: if we have something like (abs 1) (where the -- Num constraint cannot be satisfied), it's better to -- get an error about abs than about 1. -- This test might become more elaborate if we see an -- opportunity to improve the error messages | (RealSrcSpan -> RealSrcSpan -> Bool forall a. Ord a => a -> a -> Bool (<) (RealSrcSpan -> RealSrcSpan -> Bool) -> (CtLoc -> RealSrcSpan) -> CtLoc -> CtLoc -> Bool forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c `on` CtLoc -> RealSrcSpan ctLocSpan) CtLoc loc_i CtLoc loc_w -> InteractResult KeepInert | Bool otherwise -> InteractResult KeepWork -- From here on the work-item is Given | CtWanted { ctev_loc :: CtEvidence -> CtLoc ctev_loc = CtLoc loc_i } <- CtEvidence ev_i , CtLoc -> CtLoc -> Bool prohibitedSuperClassSolve CtLoc loc_w CtLoc loc_i = InteractResult KeepInert -- Just discard the un-usable Given -- This never actually happens because -- Givens get processed first | CtWanted {} <- CtEvidence ev_i = InteractResult KeepWork -- From here on both are Given -- See Note [Replacement vs keeping] | TcLevel lvl_i TcLevel -> TcLevel -> Bool `sameDepthAs` TcLevel lvl_w = InteractResult same_level_strategy | Bool otherwise -- Both are Given, levels differ = InteractResult different_level_strategy where ev_i :: CtEvidence ev_i = Ct -> CtEvidence ctEvidence Ct ct_i ev_w :: CtEvidence ev_w = Ct -> CtEvidence ctEvidence Ct ct_w pred :: Type pred = CtEvidence -> Type ctEvPred CtEvidence ev_i loc_i :: CtLoc loc_i = CtEvidence -> CtLoc ctEvLoc CtEvidence ev_i loc_w :: CtLoc loc_w = CtEvidence -> CtLoc ctEvLoc CtEvidence ev_w orig_i :: CtOrigin orig_i = CtLoc -> CtOrigin ctLocOrigin CtLoc loc_i orig_w :: CtOrigin orig_w = CtLoc -> CtOrigin ctLocOrigin CtLoc loc_w lvl_i :: TcLevel lvl_i = CtLoc -> TcLevel ctLocLevel CtLoc loc_i lvl_w :: TcLevel lvl_w = CtLoc -> TcLevel ctLocLevel CtLoc loc_w is_psc_w :: Bool is_psc_w = Ct -> Bool isPendingScDict Ct ct_w is_psc_i :: Bool is_psc_i = Ct -> Bool isPendingScDict Ct ct_i is_wsc_orig_i :: Bool is_wsc_orig_i = CtOrigin -> Bool isWantedSuperclassOrigin CtOrigin orig_i is_wsc_orig_w :: Bool is_wsc_orig_w = CtOrigin -> Bool isWantedSuperclassOrigin CtOrigin orig_w different_level_strategy :: InteractResult different_level_strategy -- Both Given | Type -> Bool isIPLikePred Type pred = if TcLevel lvl_w TcLevel -> TcLevel -> Bool `strictlyDeeperThan` TcLevel lvl_i then InteractResult KeepWork else InteractResult KeepInert | Bool otherwise = if TcLevel lvl_w TcLevel -> TcLevel -> Bool `strictlyDeeperThan` TcLevel lvl_i then InteractResult KeepInert else InteractResult KeepWork -- See Note [Replacement vs keeping] part (1) -- For the isIPLikePred case see Note [Shadowing of implicit parameters] -- in GHC.Tc.Solver.Dict same_level_strategy :: InteractResult same_level_strategy -- Both Given = case (CtOrigin orig_i, CtOrigin orig_w) of (GivenSCOrigin SkolemInfoAnon _ ScDepth depth_i Bool blocked_i, GivenSCOrigin SkolemInfoAnon _ ScDepth depth_w Bool blocked_w) | Bool blocked_i, Bool -> Bool not Bool blocked_w -> InteractResult KeepWork -- Case 2(a) from | Bool -> Bool not Bool blocked_i, Bool blocked_w -> InteractResult KeepInert -- Note [Replacement vs keeping] -- Both blocked or both not blocked | ScDepth depth_w ScDepth -> ScDepth -> Bool forall a. Ord a => a -> a -> Bool < ScDepth depth_i -> InteractResult KeepWork -- Case 2(c) from | Bool otherwise -> InteractResult KeepInert -- Note [Replacement vs keeping] (GivenSCOrigin {}, CtOrigin _) -> InteractResult KeepWork -- Case 2(b) from Note [Replacement vs keeping] (CtOrigin, CtOrigin) _ -> InteractResult KeepInert -- Case 2(d) from Note [Replacement vs keeping] {- Note [Replacement vs keeping] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When we have two Given constraints both of type (C tys), say, which should we keep? More subtle than you might think! This is all implemented in solveOneFromTheOther. 1) Constraints come from different levels (different_level_strategy) - For implicit parameters we want to keep the innermost (deepest) one, so that it overrides the outer one. See Note [Shadowing of implicit parameters] in GHC.Tc.Solver.Dict - For everything else, we want to keep the outermost one. Reason: that makes it more likely that the inner one will turn out to be unused, and can be reported as redundant. See Note [Tracking redundant constraints] in GHC.Tc.Solver. It transpires that using the outermost one is responsible for an 8% performance improvement in nofib cryptarithm2, compared to just rolling the dice. I didn't investigate why. 2) Constraints coming from the same level (i.e. same implication) (a) If both are GivenSCOrigin, choose the one that is unblocked if possible according to Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance. (b) Prefer constraints that are not superclass selections. Example: f :: (Eq a, Ord a) => a -> Bool f x = x == x Eager superclass expansion gives us two [G] Eq a constraints. We want to keep the one from the user-written Eq a, not the superclass selection. This means we report the Ord a as redundant with -Wredundant-constraints, not the Eq a. Getting this wrong was #20602. See also Note [Tracking redundant constraints] in GHC.Tc.Solver. (c) If both are GivenSCOrigin, chooose the one with the shallower superclass-selection depth, in the hope of identifying more correct redundant constraints. This is really a generalization of point (b), because the superclass depth of a non-superclass constraint is 0. (If the levels differ, we definitely won't have both with GivenSCOrigin.) (d) Finally, when there is still a choice, use KeepInert rather than KeepWork, for two reasons: - to avoid unnecessary munging of the inert set. - to cut off superclass loops; see Note [Superclass loops] in GHC.Tc.Solver.Dict Doing the level-check for implicit parameters, rather than making the work item always override, is important. Consider data T a where { T1 :: (?x::Int) => T Int; T2 :: T a } f :: (?x::a) => T a -> Int f T1 = ?x f T2 = 3 We have a [G] (?x::a) in the inert set, and at the pattern match on T1 we add two new givens in the work-list: [G] (?x::Int) [G] (a ~ Int) Now consider these steps - process a~Int, kicking out (?x::a) - process (?x::Int), the inner given, adding to inert set - process (?x::a), the outer given, overriding the inner given Wrong! The level-check ensures that the inner implicit parameter wins. (Actually I think that the order in which the work-list is processed means that this chain of events won't happen, but that's very fragile.) -}