diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver/Dict.hs')
| -rw-r--r-- | compiler/GHC/Tc/Solver/Dict.hs | 117 |
1 files changed, 79 insertions, 38 deletions
diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs index 8beff8279c..ae4835c683 100644 --- a/compiler/GHC/Tc/Solver/Dict.hs +++ b/compiler/GHC/Tc/Solver/Dict.hs @@ -69,7 +69,7 @@ solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage () -- NC: this comes from CNonCanonical or CIrredCan -- Precondition: already rewritten by inert set solveDictNC ev cls tys - = do { dict_ct <- simpleStage (canDictCt ev cls tys) + = do { dict_ct <- canDictCt ev cls tys ; solveDict dict_ct } solveDict :: DictCt -> SolverStage () @@ -100,18 +100,29 @@ updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev }) -- Add the new constraint to the inert set ; updInertCans (updDicts (addDict dict_ct)) } -canDictCt :: CtEvidence -> Class -> [Type] -> TcS DictCt +canDictCt :: CtEvidence -> Class -> [Type] -> SolverStage DictCt -- Once-only processing of Dict constraints: -- * expand superclasses -- * deal with CallStack canDictCt ev cls tys | isGiven ev -- See Note [Eagerly expand given superclasses] - = do { dflags <- getDynFlags + = Stage $ + do { dflags <- getDynFlags ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys - -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] - ; emitWork (listToBag sc_cts) - ; return (DictCt { di_ev = ev, di_cls = cls - , di_tys = tys, di_pend_sc = doNotExpand }) } + -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] + + -- For equality classes, /replace/ the current constraint with its + -- superclasses, rather than /adding/ them. + -- See (NC1) in Note [Naturally coherent classes] + ; if isEqualityClass cls + then case sc_cts of + [ct] -> startAgainWith ct + _ -> pprPanic "canDictCt" (ppr cls) + else + + do { emitWork (listToBag sc_cts) + ; continueWith (DictCt { di_ev = ev, di_cls = cls + , di_tys = tys, di_pend_sc = doNotExpand }) } } -- doNotExpand: We have already expanded superclasses for /this/ dict -- so set the fuel to doNotExpand to avoid repeating expansion @@ -123,7 +134,8 @@ canDictCt ev cls tys -- of solving it directly from a given. -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence -- and Note [Solving CallStack constraints] in GHC.Tc.Solver.Types - = do { -- First we emit a new constraint that will capture the + = Stage $ + do { -- First we emit a new constraint that will capture the -- given CallStack. let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name)) -- We change the origin to IPOccOrigin so @@ -139,18 +151,19 @@ canDictCt ev cls tys (ctLocSpan loc) (ctEvExpr new_ev) ; solveCallStack ev ev_cs - ; return (DictCt { di_ev = new_ev, di_cls = cls - , di_tys = tys, di_pend_sc = doNotExpand }) } + ; continueWith (DictCt { di_ev = new_ev, di_cls = cls + , di_tys = tys, di_pend_sc = doNotExpand }) } -- doNotExpand: No superclasses for class CallStack -- See invariants in CDictCan.cc_pend_sc | otherwise - = do { dflags <- getDynFlags + = Stage $ + do { dflags <- getDynFlags ; let fuel | classHasSCs cls = wantedsFuel dflags | otherwise = doNotExpand -- See Invariants in `CCDictCan.cc_pend_sc` - ; return (DictCt { di_ev = ev, di_cls = cls - , di_tys = tys, di_pend_sc = fuel }) } + ; continueWith (DictCt { di_ev = ev, di_cls = cls + , di_tys = tys, di_pend_sc = fuel }) } where loc = ctEvLoc ev orig = ctLocOrigin loc @@ -790,7 +803,7 @@ matchClassInst dflags inerts clas tys loc -- whether top level, or local quantified constraints. -- See Note [Instance and Given overlap] | not (xopt LangExt.IncoherentInstances dflags) - , not (naturallyCoherentClass clas) + , not (naturallyCoherentClass clas) -- See (NC3) in Note [Naturally coherent classes] , not (noMatchableGivenDicts inerts loc clas tys) = do { traceTcS "Delaying instance application" $ vcat [ text "Work item=" <+> pprClassPred clas tys ] @@ -822,8 +835,13 @@ matchClassInst dflags inerts clas tys loc -- See also Note [The equality types story] in GHC.Builtin.Types.Prim. naturallyCoherentClass :: Class -> Bool naturallyCoherentClass cls - = isCTupleClass cls - || cls `hasKey` heqTyConKey + = isCTupleClass cls || isEqualityClass cls + +isEqualityClass :: Class -> Bool +-- True of (~), (~~), and Coercible +-- These all have a single primitive-equality superclass, either (~N# or ~R#) +isEqualityClass cls + = cls `hasKey` heqTyConKey || cls `hasKey` eqTyConKey || cls `hasKey` coercibleTyConKey @@ -917,14 +935,50 @@ this: instance a ~# b => a ~~ b (See Note [The equality types story] in GHC.Builtin.Types.Prim.) -Faced with [W] t1 ~~ t2, it's always OK to reduce it to [W] t1 ~# t2, -without worrying about Note [Instance and Given overlap]. Why? Because -if we had [G] s1 ~~ s2, then we'd get the superclass [G] s1 ~# s2, and -so the reduction of the [W] constraint does not risk losing any solutions. +PS: the term "naturally coherent" doesn't really seem helpful. +Perhaps "invertible" or something? I left it for now though. -On the other hand, it can be fatal to /fail/ to reduce such -equalities, on the grounds of Note [Instance and Given overlap], -because many good things flow from [W] t1 ~# t2. +For naturally coherent classes: + +(NC1) For Givens, when expanding superclasses, we /replace/ the constraint + with its superclasses (which, remember, are equally powerful) rather than + /adding/ them. This can make a huge difference. Consider T17836, which + has a constraint like + forall b,c. a ~ (b,c) => + forall d,e. c ~ (d,e) => + ...etc... + If we just /add/ the superclasses of [G] g1:a ~ (b,c), we'll put + [G] g1:(a~(b,c)) in the inert set and emit [G] g2:a ~# (b,c). That will + kick out g1, and it'll be re-inserted as [G] g1':(b,c)~(b,c) which does + no good to anyone. When the implication is deeply nested, this has + quadratic cost, and no benefit. Just replace! + + Originally I tried this for all naturally-coherent classes, including + tuples. But discarding the tuple Given (which "replacing" does) means that + we may have to reconstruct it for a recursive call, and the optimiser isn't + quite clever enought to figure that out: see #10359 and its test case. + This is less pressing for equality classes because they have to be unpacked + strictly, so CSE-ing away the reconstuction works fine. Hence the use + of isEqualityClass rather than naturallyCoherentClass in canDictCt. + A bit ad-hoc. + +(NC2) Because of this replacement, we don't need do the fancy footwork + of Note [Solving superclass constraints], so the computation of `sc_loc` + in `mk_strict_superclasses` can be simpler. + + For tuple predicates, this matters, because their size can be large, + and we don't want to add a big class to the size of the dictionaries + in the chain. When we get down to a base predicate, we'll include + its size. See #10335 + +(NC3) Faced with [W] t1 ~ t2, it's always OK to reduce it to [W] t1 ~# t2, + without worrying about Note [Instance and Given overlap]. Why? Because + if we had [G] s1 ~ s2, then we'd get the superclass [G] s1 ~# s2, and + so the reduction of the [W] constraint does not risk losing any solutions. + + On the other hand, it can be fatal to /fail/ to reduce such equalities + on the grounds of Note [Instance and Given overlap], fbecause many good + things flow from [W] t1 ~# t2. The same reasoning applies to @@ -947,9 +1001,6 @@ And less obviously to: Examples: T5853, T10432, T5315, T9222, T2627b, T3028b -PS: the term "naturally coherent" doesn't really seem helpful. -Perhaps "invertible" or something? I left it for now though. - Note [Local instances and incoherence] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider @@ -1934,18 +1985,8 @@ mk_strict_superclasses fuel rec_clss ev@(CtGiven { ctev_evar = evar, ctev_loc = `App` (evId evar `mkVarApps` (tvs ++ dict_ids)) `mkVarApps` sc_tvs - sc_loc | isCTupleClass cls - = loc -- For tuple predicates, just take them apart, without - -- adding their (large) size into the chain. When we - -- get down to a base predicate, we'll include its size. - -- #10335 - - | isEqPredClass cls || cls `hasKey` coercibleTyConKey - = loc -- The only superclasses of ~, ~~, and Coercible are primitive - -- equalities, and they don't use the GivenSCOrigin mechanism - -- detailed in Note [Solving superclass constraints] in - -- GHC.Tc.TyCl.Instance. Skip for a tiny performance win. - + sc_loc | naturallyCoherentClass cls + = loc -- See (NC2) in Note [Naturally coherent classes] | otherwise = loc { ctl_origin = mk_sc_origin (ctLocOrigin loc) } |