Simon Peyton Jones pushed to branch wip/T26115 at Glasgow Haskell Compiler / GHC Commits: 0d1363c0 by Simon Peyton Jones at 2025-06-28T23:00:40+01:00 Wibbles - - - - - 66114346 by Simon Peyton Jones at 2025-06-28T23:37:33+01:00 Wibble - - - - - 6 changed files: - compiler/GHC/Core/Opt/Specialise.hs - compiler/GHC/HsToCore/Binds.hs - compiler/GHC/Tc/Gen/Sig.hs - compiler/GHC/Tc/Solver/Dict.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs Changes: ===================================== compiler/GHC/Core/Opt/Specialise.hs ===================================== @@ -3375,7 +3375,7 @@ beats_or_same (CI { ci_key = args1 }) (CI { ci_key = args2 }) go_arg (SpecDict {}) (SpecDict {}) = True go_arg UnspecType UnspecType = True go_arg UnspecArg UnspecArg = True - go_arg _ _ = False + go_arg _ _ = False ---------------------- splitDictBinds :: FloatedDictBinds -> IdSet -> (FloatedDictBinds, OrdList DictBind, IdSet) @@ -3491,7 +3491,6 @@ newSpecIdSM old_name new_ty details info ; return (assert (not (isCoVarType new_ty)) $ mkLocalVar details new_name ManyTy new_ty info) } - {- Old (but interesting) stuff about unboxed bindings ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== compiler/GHC/HsToCore/Binds.hs ===================================== @@ -796,216 +796,6 @@ Note [Desugaring new-form SPECIALISE pragmas] which is desugared in this module by `dsSpec`. For the context see Note [Handling new-form SPECIALISE pragmas] in GHC.Tc.Gen.Sig -Suppose we have f :: forall p q. (Ord p, Eq q) => p -> q -> q, and a pragma - - {-# SPECIALISE forall x. f @[a] @[Int] x [3,4] #-} - -In `dsSpec` the `SpecPragE` will look something like this: - - SpecPragE { spe_fn_id = f - , spe_bndrs = @a (d:Ord a) (x:[a]) - , spe_call = let d2:Ord [a] = $dfOrdList d - d3:Eq [Int] = $dfEqList $dfEqInt - in f @[a] @[Int] d2 d3 x [3,4] } -We want to get - - RULE forall a (d2:Ord a) (d3:Eq [Int]) (x:[a]). - f @[a] @[Int] d2 d3 x [3,4] = $sf d2 x - - $sf :: forall a. Ord [a] => a -> Int - $sf = /\a. \d2 x. - let d3 = $dfEqList $dfEqInt - in <f-rhs> @[a] @[Int] d2 d3 x [3,4] - -Notice that - -(SP1) If the expression in the SPECIALISE pragma had a type signature, such as - SPECIALISE f :: Eq b => Int -> b -> b - then the desugared expression may have type abstractions and applications - "in the way", like this: - (/\b. (\d:Eq b). let d1 = $dfOrdInt in f @Int @b d1 d) @b (d2:Eq b) - The lambdas come from the type signature, which is then re-instantiated, - hence the applications of those lambdas. - - We use the simple optimiser to simplify this to - let { d = d2; d1 = $dfOrdInt } in f @Int @b d1 d - - Important: do no inlining in this "simple optimiser" phase: - use `simpleOptExprNoInline`. E.g. we don't want to turn it into - f @Int @b $dfOrdInt d2 - because the latter is harder to match. - - Similarly if we have - let { d1=d; d2=d } in f d1 d2 - we don't want to inline d1/d2 to get this - f d d - -(SP2) $sf does not simply quantify over (d:Ord a). Instead, to figure out what - it should quantify over, and to include the 'd3' binding in the body of $sf, - we use the function `prepareSpecLHS`. It takes the simplified LHS `core_call`, - and uses the dictionary bindings to figure out the RULE LHS and RHS. - - This is described in Note [prepareSpecLHS]. - -Note [prepareSpecLHS] -~~~~~~~~~~~~~~~~~~~~~ -To compute the appropriate RULE LHS and RHS for a new-form specialise pragma, -as described in Note [Desugaring new-form SPECIALISE pragmas], we use a function -called prepareSpecLHS. -It takes as input a list of (type and evidence) binders, and a Core expression. -For example, suppose its input is of the following form: - - spe_bndrs = @a (d:Ord a) - spe_call = - let - -- call these bindings the call_binds - d1 :: Num Int - d1 = $dfNumInt - d2 :: Ord [a] - d2 = $dfOrdList d - d3 :: Eq a - d3 = $p1Ord d3 - d4 :: Ord (F a) - d4 = d |> co1 - d5 :: Ord (G a) - d5 = d4 |> co2 - in - f @[a] @Int d1 d2 d3 d5 - -The goal of prepareSpecLHS is then to generate the following two things: - - - A specialisation, of the form: - - $sf = - let - in <f-rhs> @[a] @Int d1 d2 d3 d5 - - - A rule, of the form: - - RULE forall a d1 d2 d3 d5. f @[a] @Int d1 d2 d3 d5 = - let - in $sf - -That is, we must compute 'spec_args', 'rule_binds' and 'spec_binds'. A first -approach might be: - - - take spec_args = spe_bndrs, - - spec_binds = call_binds. - -If we did so, the RULE would look like: - - RULE forall a d1 d2 d3 d5. f @[a] @Int d1 d2 d3 d5 = - let d = <???> - in $sf @a d - -The problem is: how do we recover 'd' from 'd1', 'd2', 'd3', 'd5'? Essentially, -we need to run call_binds in reverse. In this example, we had: - - d1 :: Num Int - d1 = $dfNumInt - d2 :: Ord [a] - d2 = $dfOrdList d - d3 :: Eq a - d3 = $p1Ord d3 - d4 :: Ord (F a) - d4 = d |> co1 - d5 :: Ord (G a) - d5 = d4 |> co2 - -Let's try to recover (d: Ord a) from 'd1', 'd2', 'd4', 'd5': - - - d1 is a constant binding, so it doesn't help us. - - d2 uses a top-level instance, which we can't run in reverse; we can't - obtain Ord a from Ord [a]. - - d3 uses a superclass selector which prevents us from making progress. - - d5 is defined using d4, and both involve a cast. - In theory we could define d = d5 |> sym (co1 ; co2), but this gets - pretty complicated. - -This demonstrates the following: - - 1. The bindings can't necessarily be "run in reverse". - 2. Even if the bindings theoretically can be "run in reverse", it is not - straightforward to do so. - -Now, we could strive to make the let-bindings reversible. We already do this -to some extent for quantified constraints, as explained in -Note [Fully solving constraints for specialisation] in GHC.Tc.Gen.Sig, -using the TcSSpecPrag solver mode described in Note [TcSSpecPrag] in GHC.Tc.Solver.Monad. -However, given (2), we don't bother ensuring that e.g. we don't use top-level -class instances like in d2 above. Instead, we handle these bindings in -prepareSpecLHS as follows: - - (a) Go through the bindings in order. - - (1) Bindings like - d1 = $dfNumInt - depend only on constants and move to the specialised function body. - That is crucial -- it makes those specialised methods available in the - specialised body. These are the `spec_const_binds`. - - Note that these binds /can/ depend on locally-quantified /type/ variables. - For example, if we have - instance Monad (ST s) where ... - then the dictionary for (Monad (ST s)) is effectively a constant dictionary. - This is important to get specialisation for such types. Example in test T8331. - - (2) Other bindings, like - d2:Ord [a] = $dfOrdList d - d3 = d - depend on a locally-quantifed evidence variable `d`. - Surprisingly, /we want to drop these bindings entirely!/ - This is because, as explained above, it is too difficult to run these - in reverse. Instead, we drop them, and re-compute which dictionaries - we will quantify over. - - (3) Finally, inside those dictionary bindings we should find the call of the - function itself - f @[a] @[Int] d2 d3 x [3,4] - 'prepareSpecLHS' takes the call apart and returns its arguments. - - (b) Now, (a)(2) means that the RULE does not quantify over 'd' any more; it - quantifies over 'd1' 'd2' 'd3' 'd5'. So we recompute the `rule_bndrs` - from scratch. - - Moreover, the specialised function also no longer quantifies over 'd', - it quantifies over 'd2' 'd3' 'd5'. This set of binders is computed by - taking the RULE binders and subtracting off the binders from - the `spec_const_binds`. - -[Shortcoming] This whole approach does have one downside, compared to running -the let-bindings in reverse: it doesn't allow us to common-up dictionaries. -Consider for example: - - g :: forall a b. ( Eq a, Ord b ) => a -> b -> Bool - {-# SPECIALISE g :: forall c. Ord c => c -> c -> Bool #-} - -The input to prepareSpecLHS will be (more or less): - - spe_bndrs: @c (d:Ord c) - spe_call = - let - d1 :: Eq c - d1 = $p1Ord d - d2 :: Ord c - d2 = d - in - g @c @c d1 d2 - -The approach described in (2) will thus lead us to generate: - - RULE g @c @c d1 d2 = $sg @c d1 d2 - $sg @c d1 d2 = <g-rhs> @c @c d1 d2 - -when we would rather avoid passing both dictionaries, and instead generate: - - RULE g @c @c d1 d2 = let { d = d2 } in $sg @c d - $sg @c d = let { d1 = $p1Ord d; d2 = d } in <g-rhs> @c @c d1 d2 - -For now, we accept this infelicity. - -Note [Desugaring new-form SPECIALISE pragmas] -- Take 2 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have f :: forall a b c d. (Ord a, Ord b, Eq c, Ix d) => ... f = rhs @@ -1027,11 +817,11 @@ We /could/ generate RULE f d1 d2 d3 d4 e1..en = $sf d1 d2 d3 d4 $sf d1 d2 d3 d4 = <rhs> d1 d2 d3 d4 -But that would do no specialisation! What we want is this: +But that would do no specialisation at all! What we want is this: RULE f d1 _d2 _d3 d4 e1..en = $sf d1 d4 $sf d1 d4 = let d7 = d1 -- Renaming - dx1 = d7 -- Renaming - d6 = dx1 + dx1 = d1 -- Renaming + d6 = d1 -- Renaming d2 = $fOrdList d6 d3 = $fEqList $fEqInt in rhs d1 d2 d3 d4 @@ -1045,46 +835,61 @@ Notice that: to line things up The transformation goes in these steps + (S1) decomposeCall: decomopose `the_call` into - - `rev_binds`: the enclosing let-bindings (actually reversed) + - `binds`: the enclosing let-bindings - `rule_lhs_args`: the arguments of the call itself - We carefully arrange that the dictionary arguments of the actual - call, `rule_lhs_args` are all distinct dictionary variables, - not expressions. How? We use `simpleOptExprNoInline` to avoid - inlining the let-bindings. + + If the expression in the SPECIALISE pragma had a type signature, such as + SPECIALISE g :: Eq b => Int -> b -> b + then the desugared expression may have type abstractions and applications + "in the way", like this: + (/\b. (\d:Eq b). let d1 = $dfOrdInt in f @Int @b d1 d) @b (d2:Eq b) + The lambdas come from the type signature, which is then re-instantiated, + hence the applications of those lambdas. + + so `decomposeCall` uses the simple optimiser to simplify this to + let { d = d2; d1 = $dfOrdInt } in f @Int @b d1 d + + Wrinkle (S1a): do no inlining in this "simple optimiser" phase: + use `simpleOptExprNoInline`. E.g. we don't want to turn it into + f @Int @b $dfOrdInt d2 + because the latter is harder to match. Similarly if we have + let { d1=d; d2=d } in f d1 d2 + we don't want to inline d1/d2 to get this + f d d + + TL;DR: as a result the dictionary arguments of the actual call, + `rule_lhs_args` are all distinct dictionary variables, not + expressions. (S2) Compute `rule_bndrs`: the free vars of `rule_lhs_args`, which will be the forall'd template variables of the RULE. In the example, rule_bndrs = d1,d2,d3,d4 - -(S3) grabSpecBinds: transform `rev_binds` into `spec_binds`: the - bindings we will wrap around the call in the RHS of `$sf` - -(S4) Find `spec_bndrs`, the subset of `rule_bndrs` that we actually - need to pass to `$sf`, simply by filtering out those that are - bound by `spec_binds`. In the example - spec_bndrs = d1,d4 - - - Working inner -* Grab any bindings we can that will "shadow" the forall'd - rule-bndrs, giving specialised bindings for them. - * We keep a set of known_bndrs starting with {d1,..,dn} - * We keep a binding iff no free var is - (a) in orig_bndrs (i.e. not totally free) - (b) not in known_bndrs - * If we keep it, add its binder to known_bndrs; if not, don't - -To maximise what we can "grab", start by extracting /renamings/ of the -forall'd rule_bndrs, and bringing them to the top. A renaming is - rule_bndr = d -If we see this: - * Bring d=rule_bndr to the top - * Add d to the set of variables to look for on the right. - e.g. rule_bndrs = d1, d2 - Bindings { d7=d9; d1=d7 } - Bring to the top { d7=d1; d9=d7 } - + These variables will get values from a successful RULE match. + +(S3) `getRenamings`: starting from the rule_bndrs, make bindings for + all other variables that are equal to them. In the example, we + make renaming-bindings for d7, dx1, d6. + + NB1: we don't actually have to remove the original bindings; + it's harmless to leave them + NB2: We also reverse bindings like d1 = d2 |> co, to get + d2 = d1 |> sym co + It's easy and may help. + +(S4) `pickSpecBinds`: pick the bindings we want to keep in the + specialised function. We start from `known_vars`, the variables we + know, namely the `rule_bndrs` and the binders from (S3), which are + all equal to one of the `rule_bndrs`. + + Then we keep a binding if the free vars of its RHS are all known. + In our example, `d2` and `d3` are both picked, but `d4` is not. + The non-picked ones won't end up being specialised. + +(S5) Finally, work out which of the `rule_bndrs` we must pass on to + specialised function. We just filter out ones bound by a renaming + or a picked binding. -} ------------------------ @@ -1155,7 +960,9 @@ dsSpec_help :: Name -> Id -> CoreExpr -- Function to specialise -> InlinePragma -> [Var] -> CoreExpr -> DsM (Maybe (OrdList (Id,CoreExpr), CoreRule)) dsSpec_help poly_nm poly_id poly_rhs spec_inl orig_bndrs ds_call - = do { mb_call_info <- decomposeCall poly_id ds_call + = do { -- Decompose the call + -- Step (S1) of Note [Desugaring new-form SPECIALISE pragmas] + mb_call_info <- decomposeCall poly_id ds_call ; case mb_call_info of { Nothing -> return Nothing ; Just (binds, rule_lhs_args) -> @@ -1167,12 +974,17 @@ dsSpec_help poly_nm poly_id poly_rhs spec_inl orig_bndrs ds_call is_local :: Var -> Bool is_local v = v `elemVarSet` locals + -- Find `rule_bndrs`: (S2) of Note [Desugaring new-form SPECIALISE pragmas] rule_bndrs = scopedSort (exprsSomeFreeVarsList is_local rule_lhs_args) + -- getRenamings: (S3) of Note [Desugaring new-form SPECIALISE pragmas] rn_binds = getRenamings orig_bndrs binds rule_bndrs + + -- pickSpecBinds: (S4) of Note [Desugaring new-form SPECIALISE pragmas] known_vars = mkVarSet rule_bndrs `extendVarSetList` bindersOfBinds rn_binds picked_binds = pickSpecBinds is_local known_vars binds + -- Fins `spec_bndrs`: (S5) of Note [Desugaring new-form SPECIALISE pragmas] -- Make spec_bndrs, the variables to pass to the specialised -- function, by filtering out the rule_bndrs that aren't needed spec_binds_bndr_set = mkVarSet (bindersOfBinds picked_binds) @@ -1262,12 +1074,12 @@ dsSpec_help poly_nm poly_id poly_rhs spec_inl orig_bndrs ds_call decomposeCall :: Id -> CoreExpr -> DsM (Maybe ([CoreBind], [CoreExpr] )) -- Decompose the call into (let <binds> in f <args>) +-- See (S1) in Note [Desugaring new-form SPECIALISE pragmas] decomposeCall poly_id ds_call - = do { -- Simplify the (desugared) call; see wrinkle (SP1) - -- in Note [Desugaring new-form SPECIALISE pragmas] - ; dflags <- getDynFlags + = do { dflags <- getDynFlags ; let simpl_opts = initSimpleOpts dflags core_call = simpleOptExprNoInline simpl_opts ds_call + -- simpleOpeExprNoInlint: see Wrinkle (S1a)! ; case go [] core_call of { Nothing -> do { diagnosticDs (DsRuleLhsTooComplicated ds_call core_call) ===================================== compiler/GHC/Tc/Gen/Sig.hs ===================================== @@ -759,9 +759,7 @@ This is done in three parts. (1) Typecheck the expression, capturing its constraints - (2) Solve these constraints, but in special TcSSpecPrag mode which ensures - each original Wanted is either fully solved or left untouched. - See Note [Fully solving constraints for specialisation]. + (2) Solve these constraints (3) Compute the constraints to quantify over, using `getRuleQuantCts` on the unsolved constraints returned by (2). @@ -797,68 +795,6 @@ This is done in three parts. of the form: forall @a @b d1 d2 d3. f d1 d2 d3 = $sf d1 d2 d3 -Note [Fully solving constraints for specialisation] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -As far as specialisation is concerned, it is actively harmful to simplify -constraints without /fully/ solving them. - -Example: - - f :: ∀ a t. (Eq a, ∀x. Eq x => Eq (t x)). t a -> Char - {-# SPECIALISE f @Int #-} - - Typechecking 'f' will result in [W] Eq Int, [W] ∀x. Eq x => Eq (t x). - We absolutely MUST leave the quantified constraint alone, because we want to - quantify over it. If we were to try to simplify it, we would emit an - implication and would thereafter never be able to quantify over the original - quantified constraint. - - However, we still need to simplify quantified constraints that can be - /fully solved/ from instances, otherwise we would never be able to - specialise them away. Example: {-# SPECIALISE f @a @[] #-}. - -The conclusion is this: - - when solving the constraints that arise from a specialise pragma, following - the recipe described in Note [Handling new-form SPECIALISE pragmas], all - Wanted quantified constraints should either be: - - fully solved (no free evidence variables), or - - left untouched. - -To achieve this, we run the solver in a special "all-or-nothing" solving mode, -described in Note [TcSSpecPrag] in GHC.Tc.Solver.Monad. - -Note that a similar problem arises in other situations in which the solver takes -an irreversible step, such as using a top-level class instance. This is currently -less important, as the desugarer can handle these cases. To explain, consider: - - g :: ∀ a. Eq a => a -> Bool - {-# SPECIALISE g @[e] #-} - - Typechecking 'g' will result in [W] Eq [e]. Were we to simplify this to - [W] Eq e, we would have difficulty generating a RULE for the specialisation: - - $sg :: Eq e => [e] -> Bool - - RULE ∀ e (d :: Eq [e]). g @[e] d = $sg @e (??? :: Eq e) - -- Can't fill in ??? because we can't run instances in reverse. - - RULE ∀ e (d :: Eq e). g @[e] ($fEqList @e d) = $sg @e d - -- Bad RULE matching template: matches on the structure of a dictionary - - Moreover, there is no real benefit to any of this, because the specialiser - can't do anything useful from the knowledge that a dictionary for 'Eq [e]' is - constructed from a dictionary for 'Eq e' using the 'Eq' instance for lists. - -Here, it would make sense to also use the "solve completely" mechanism in the -typechecker to avoid producing evidence terms that we can't "run in reverse". -However, the current implementation tackles this issue in the desugarer, as is -explained in Note [prepareSpecLHS] in GHC.HsToCore.Binds. -So, for the time being at least, in TcSSpecPrag mode, we don't attempt to "fully solve" -constraints when we use a top-level instance. This might change in the future, -were we to decide to attempt to address [Shortcoming] in Note [prepareSpecLHS] -in GHC.HsToCore.Binds. - Note [Handling old-form SPECIALISE pragmas] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ NB: this code path is deprecated, and is scheduled to be removed in GHC 9.18, as per #25440. @@ -1039,7 +975,7 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl) <- tcRuleBndrs skol_info rule_bndrs $ tcInferRho spec_e - -- (2) Solve the resulting wanteds in TcSSpecPrag mode. + -- (2) Solve the resulting wanteds ; ev_binds_var <- newTcEvBinds ; spec_e_wanted <- setTcLevel rhs_tclvl $ runTcSWithEvBinds ev_binds_var $ ===================================== compiler/GHC/Tc/Solver/Dict.hs ===================================== @@ -462,30 +462,20 @@ from the instance that we have in scope: case x of { GHC.Types.I# x1 -> GHC.Types.I# (GHC.Prim.+# x1 1#) } ** NB: It is important to emphasize that all this is purely an optimization: -** exactly the same programs should typecheck with or without this -** procedure. - -Solving fully -~~~~~~~~~~~~~ -There is a reason why the solver does not simply try to solve such -constraints with top-level instances. If the solver finds a relevant -instance declaration in scope, that instance may require a context -that can't be solved for. A good example of this is: - - f :: Ord [a] => ... - f x = ..Need Eq [a]... - -If we have instance `Eq a => Eq [a]` in scope and we tried to use it, we would -be left with the obligation to solve the constraint Eq a, which we cannot. So we -must be conservative in our attempt to use an instance declaration to solve the -[W] constraint we're interested in. - -Our rule is that we try to solve all of the instance's subgoals -recursively all at once. Precisely: We only attempt to solve -constraints of the form `C1, ... Cm => C t1 ... t n`, where all the Ci -are themselves class constraints of the form `C1', ... Cm' => C' t1' -... tn'` and we only succeed if the entire tree of constraints is -solvable from instances. +** exactly the same programs should typecheck with or without this procedure. + +Consider + f :: Ord [a] => ... + f x = ..Need Eq [a]... +We could use the Eq [a] superclass of the Ord [a], or we could use the top-level +instance `Eq a => Eq [a]`. But if we did the latter we'd be stuck with an +insoluble constraint (Eq a). + +So the ShortCutSolving rule is this: + If we could solve a constraint from a local Given, + try first to /completely/ solve the constraint using only top-level instances. + - If that succeeds, use it + - If not, use the local Given An example that succeeds: @@ -511,7 +501,8 @@ An example that fails: f :: C [a] b => b -> Bool f x = m x == [] -Which, because solving `Eq [a]` demands `Eq a` which we cannot solve, produces: +Which, because solving `Eq [a]` demands `Eq a` which we cannot solve. so short-cut +solving fails and we use the superclass of C: f :: forall a b. C [a] b => b -> Bool f = \ (@ a) (@ b) ($dC :: C [a] b) (eta :: b) -> @@ -521,23 +512,49 @@ Which, because solving `Eq [a]` demands `Eq a` which we cannot solve, produces: (m @ [a] @ b $dC eta) (GHC.Types.[] @ a) -Note [Shortcut solving: type families] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have (#13943) - class Take (n :: Nat) where ... - instance {-# OVERLAPPING #-} Take 0 where .. - instance {-# OVERLAPPABLE #-} (Take (n - 1)) => Take n where .. - -And we have [W] Take 3. That only matches one instance so we get -[W] Take (3-1). Really we should now rewrite to reduce the (3-1) to 2, and -so on -- but that is reproducing yet more of the solver. Sigh. For now, -we just give up (remember all this is just an optimisation). - -But we must not just naively try to lookup (Take (3-1)) in the -InstEnv, or it'll (wrongly) appear not to match (Take 0) and get a -unique match on the (Take n) instance. That leads immediately to an -infinite loop. Hence the check that 'preds' have no type families -(isTyFamFree). +The moving parts are relatively simple: + +* To attempt to solve the constraint completely, we just recursively + call the constraint solver. See the use of `tryTcS` in + `tcShortCutSolver`. + +* When this attempted recursive solving, we set a special mode + `TcSShortCut`, which signals that we are trying to solve using only + top-level instances. We switch on `TcSShortCut` mode in + `tryShortCutSolver`. + +* When in TcSShortCut mode, we behave specially in a few places: + - `tryInertDicts`, where we would otherwise look for a Given to solve our Wantee + - `noMatchableGivenDicts`, which also consults the Givens + - `matchLocalInst`, which would otherwise consult Given quantified constraints + - `GHC.Tc.Solver.Instance.Class.matchInstEnv`: when short-cut solving, don't + pick overlappable top-level instances + + +Some wrinkles: + +(SCS1) Note [Shortcut solving: incoherence] + +(SCS2) The short-cut solver just uses the solver recursively, so we get its + full power: + + * We need to be able to handle recursive super classes. The + solved_dicts state ensures that we remember what we have already + tried to solve to avoid looping. + + * As #15164 showed, it can be important to exploit sharing between + goals. E.g. To solve G we may need G1 and G2. To solve G1 we may need H; + and to solve G2 we may need H. If we don't spot this sharing we may + solve H twice; and if this pattern repeats we may get exponentially bad + behaviour. + + * Suppose we have (#13943) + class Take (n :: Nat) where ... + instance {-# OVERLAPPING #-} Take 0 where .. + instance {-# OVERLAPPABLE #-} (Take (n - 1)) => Take n where .. + + And we have [W] Take 3. That only matches one instance so we get + [W] Take (3-1). Then we should reduce the (3-1) to 2, and continue. Note [Shortcut solving: incoherence] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -603,37 +620,6 @@ The output of `main` if we avoid the optimization under the effect of IncoherentInstances is `1`. If we were to do the optimization, the output of `main` would be `2`. -Note [Shortcut try_solve_from_instance] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The workhorse of the short-cut solver is - try_solve_from_instance :: (EvBindMap, DictMap CtEvidence) - -> CtEvidence -- Solve this - -> MaybeT TcS (EvBindMap, DictMap CtEvidence) -Note that: - -* The CtEvidence is the goal to be solved - -* The MaybeT manages early failure if we find a subgoal that - cannot be solved from instances. - -* The (EvBindMap, DictMap CtEvidence) is an accumulating purely-functional - state that allows try_solve_from_instance to augment the evidence - bindings and inert_solved_dicts as it goes. - - If it succeeds, we commit all these bindings and solved dicts to the - main TcS InertSet. If not, we abandon it all entirely. - -Passing along the solved_dicts important for two reasons: - -* We need to be able to handle recursive super classes. The - solved_dicts state ensures that we remember what we have already - tried to solve to avoid looping. - -* As #15164 showed, it can be important to exploit sharing between - goals. E.g. To solve G we may need G1 and G2. To solve G1 we may need H; - and to solve G2 we may need H. If we don't spot this sharing we may - solve H twice; and if this pattern repeats we may get exponentially bad - behaviour. Note [No Given/Given fundeps] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -942,20 +942,16 @@ The constraint solver can operate in different modes: * TcSVanilla: Normal constraint solving mode. This is the default. * TcSPMCheck: Used by the pattern match overlap checker. - Like TcSVanilla, but the idea is that the returned InertSet will - later be resumed, so we do not want to restore type-equality cycles - See also Note [Type equality cycles] in GHC.Tc.Solver.Equality + Like TcSVanilla, but the idea is that the returned InertSet will + later be resumed, so we do not want to restore type-equality cycles + See also Note [Type equality cycles] in GHC.Tc.Solver.Equality * TcSEarlyAbort: Abort (fail in the monad) as soon as we come across an insoluble constraint. This is used to fail-fast when checking for hole-fits. See Note [Speeding up valid hole-fits]. -* TcSSpecPrag: Solve constraints fully or not at all. This is described in - Note [TcSSpecPrag]. - - This mode is currently used in one place only: when solving constraints - arising from specialise pragmas. - See Note [Fully solving constraints for specialisation] in GHC.Tc.Gen.Sig. +* TcSShortCut: Solve constraints fully or not at all. This is described in + Note [Shortcut solving] in GHC.Tc.Solver.Dict -} data TcSEnv @@ -1126,54 +1122,6 @@ runTcSEarlyAbort tcs = do { ev_binds_var <- TcM.newTcEvBinds ; runTcSWithEvBinds' TcSEarlyAbort ev_binds_var tcs } --- | Run the 'TcS' monad in 'TcSSpecPrag' mode, which either fully solves --- individual Wanted quantified constraints or leaves them alone. --- - -{- Note [TcSSpecPrag] -~~~~~~~~~~~~~~~~~~~~~ -The TcSSpecPrag mode is a specialized constraint solving mode that guarantees -that Wanted quantified constraints are either: - - Fully solved with no free evidence variables, or - - Left completely untouched (no simplification at all) - -Examples: - - * [W] forall x. Eq x => Eq (f x). - - In TcSSpecPrag mode, we **do not** process this quantified constraint by - creating a new implication constraint; we leave it alone instead. - - * [W] Eq (Maybe Int). - - This constraint is solved fully, using two top-level Eq instances. - - * [W] forall x. Eq x => Eq [x]. - - This constraint is solved fully as well, using the Eq instance for lists. - -This functionality is crucially used by the specialiser, for which taking an -irreversible constraint solving steps is actively harmful, as described in -Note [Fully solving constraints for specialisation] in GHC.Tc.Gen.Sig. - -Note that currently we **do not** refrain from using top-level instances, -even though we also can't run them in reverse; this isn't a problem for the -specialiser (which is currently the sole consumer of this functionality). - -The implementation is as follows: in TcSSpecPrag mode, when we are about to -solve a Wanted quantified constraint by emitting an implication, we call the -special function `solveCompletelyIfRequired`. This function recursively calls -the solver but in TcSVanilla mode (i.e. full-blown solving, with no restrictions). -If this recursive call manages to solve all the remaining constraints fully, -then we proceed with that outcome (i.e. we continue with that inert set, etc). -Otherwise, we discard everything that happened in the recursive call, and -continue with the original quantified constraint unchanged. - -In the future, we could consider re-using this functionality for the short-cut -solver (see Note [Shortcut solving] in GHC.Tc.Solver.Dict), but we would have to -be wary of the performance implications. --} - -- | This can deal only with equality constraints. runTcSEqualities :: TcS a -> TcM a runTcSEqualities thing_inside @@ -1282,20 +1230,21 @@ setTcLevelTcS lvl (TcS thing_inside) nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a -> TcS a -nestImplicTcS ref inner_tclvl (TcS thing_inside) +nestImplicTcS ev_binds_var inner_tclvl (TcS thing_inside) = TcS $ \ env@(TcSEnv { tcs_inerts = old_inert_var }) -> do { inerts <- TcM.readTcRef old_inert_var -- Initialise the inert_cans from the inert_givens of the parent -- so that the child is not polluted with the parent's inert Wanteds + -- See Note [trySolveImplication] in GHC.Tc.Solver.Solve + -- All other InertSet fields are inherited ; let nest_inert = inerts { inert_cycle_breakers = pushCycleBreakerVarStack (inert_cycle_breakers inerts) , inert_cans = (inert_givens inerts) { inert_given_eqs = False } } - -- All other InertSet fields are inherited ; new_inert_var <- TcM.newTcRef nest_inert ; new_wl_var <- TcM.newTcRef emptyWorkList - ; let nest_env = env { tcs_ev_binds = ref + ; let nest_env = env { tcs_ev_binds = ev_binds_var , tcs_inerts = new_inert_var , tcs_worklist = new_wl_var } ; res <- TcM.setTcLevel inner_tclvl $ @@ -1306,7 +1255,7 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside) #if defined(DEBUG) -- Perform a check that the thing_inside did not cause cycles - ; ev_binds <- TcM.getTcEvBindsMap ref + ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var ; checkForCyclicBinds ev_binds #endif ; return res } ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -260,6 +260,11 @@ more meaningful error message (see T19627) This also applies for quantified constraints; see `-fqcs-fuel` compiler flag and `QCI.qci_pend_sc` field. -} +{- ******************************************************************************** +* * +* Solving implication constraints * +* * +******************************************************************************** -} solveNestedImplications :: Bag Implication -> TcS (Bag Implication) @@ -280,7 +285,22 @@ solveNestedImplications implics ; return unsolved_implics } +{- Note [trySolveImplication] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +`trySolveImplication` may be invoked while solving simple wanteds, notably from +`solveWantedForAll`. It returns a Bool to say if solving succeeded or failed. + +It used `nestImplicTcS` to build a nested scope. One subtle point is that +`nestImplicTcS` uses the `inert_givens` (not the `inert_cans`) of the current +inert set to initialse the `InertSet` of the nested scope. It super-important not +to pollute the sub-solving problem with the unsolved Wanteds of the current scope. + +Whenever we do `solveSimpleGivens`, we snapshot the `inert_cans` into `inert_givens`. +(At that moment there should be no Wanteds.) +-} + trySolveImplication :: Implication -> TcS Bool +-- See Note [trySolveImplication] trySolveImplication (Implic { ic_tclvl = tclvl , ic_binds = ev_binds_var , ic_given = given_ids @@ -977,6 +997,7 @@ solveSimpleGivens givens -- Capture the Givens in the inert_givens of the inert set -- for use by subsequent calls of nestImplicTcS + -- See Note [trySolveImplication] ; updInertSet (\is -> is { inert_givens = inert_cans is }) ; cans <- getInertCans @@ -1368,6 +1389,8 @@ solveWantedForAll qci tvs theta body_pred , unitBag (mkNonCanonical $ CtWanted wanted_ev)) } ; traceTcS "solveForAll {" (ppr skol_tvs $$ ppr given_ev_vars $$ ppr wanteds $$ ppr w_id) + + -- Try to solve the constraint completely ; ev_binds_var <- TcS.newTcEvBinds ; solved <- trySolveImplication $ (implicationPrototype loc_env) @@ -1381,9 +1404,13 @@ solveWantedForAll qci tvs theta body_pred ; traceTcS "solveForAll }" (ppr solved) ; evbs <- TcS.getTcEvBindsMap ev_binds_var ; if not solved - then do { addInertForAll qci + then do { -- Not completely solved; abandon that attempt and add the + -- original constraint to the inert set + addInertForAll qci ; stopWith (CtWanted wtd) "Wanted forall-constraint:unsolved" } - else do { setWantedEvTerm dest EvCanonical $ + + else do { -- Completely solved; build an evidence terms + setWantedEvTerm dest EvCanonical $ EvFun { et_tvs = skol_tvs, et_given = given_ev_vars , et_binds = evBindMapBinds evbs, et_body = w_id } ; stopWith (CtWanted wtd) "Wanted forall-constraint:solved" } } @@ -1404,36 +1431,68 @@ solveWantedForAll qci tvs theta body_pred ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Solving a wanted forall (quantified) constraint [W] df :: forall a b. (Eq a, Ord b) => C x a b -is delightfully easy. Just build an implication constraint +is delightfully easy in principle. Just build an implication constraint forall ab. (g1::Eq a, g2::Ord b) => [W] d :: C x a and discharge df thus: df = /\ab. \g1 g2. let <binds> in d where <binds> is filled in by solving the implication constraint. All the machinery is to hand; there is little to do. -We can take a more straightforward parth when there is a matching Given, e.g. - [W] dg :: forall c d. (Eq c, Ord d) => C x c d -In this case, it's better to directly solve the Wanted from the Given, instead -of building an implication. This is more than a simple optimisation; see -Note [Solving Wanted QCs from Given QCs]. +There are some tricky corners though: + +(WFA1) We can take a more straightforward parth when there is a matching Given, e.g. + [W] dg :: forall c d. (Eq c, Ord d) => C x c d + In this case, it's better to directly solve the Wanted from the Given, instead + of building an implication. This is more than a simple optimisation; see + Note [Solving Wanted QCs from Given QCs]. + +(WFA2) Termination: see #19690. We want to maintain the invariant (QC-INV): + + (QC-INV) Every quantified constraint returns a non-bottom dictionary + + just as every top-level instance declaration guarantees to return a non-bottom + dictionary. But as #19690 shows, it is possible to get a bottom dicionary + by superclass selection if we aren't careful. The situation is very similar + to that described in Note [Recursive superclasses] in GHC.Tc.TyCl.Instance; + and we use the same solution: + + * Give the Givens a CtOrigin of (GivenOrigin (InstSkol IsQC head_size)) + * Give the Wanted a CtOrigin of (ScOrigin IsQC NakedSc) + + Both of these things are done in solveForAll. Now the mechanism described + in Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance takes over. + +(WFA3) We do not actually emit an implication to solve later. Rather we + try to solve it completely immediately using `trySolveImplication` + - If successful, we can build evidence + - If unsuccessful, we abandon the attempt and add the unsolved + forall-constraint to the inert set. + Several reasons for this "solve immediately" approach -The tricky point is about termination: see #19690. We want to maintain -the invariant (QC-INV): + - It saves quite a bit of plumbing, tracking the emitted implications for + later solving; and the evidence would have to contain as-yet-incomplte + bindings which complicates tracking of unused Givens. - (QC-INV) Every quantified constraint returns a non-bottom dictionary + - We get better error messages, about failing to solve, say + (forall a. a->a) ~ (forall b. b->Int) -just as every top-level instance declaration guarantees to return a non-bottom -dictionary. But as #19690 shows, it is possible to get a bottom dicionary -by superclass selection if we aren't careful. The situation is very similar -to that described in Note [Recursive superclasses] in GHC.Tc.TyCl.Instance; -and we use the same solution: + - Consider + f :: forall f a. (Ix a, forall x. Eq x => Eq (f x)) => a -> f a + {-# SPECIALISE f :: forall f. (forall x. Eq x => Eq (f x)) => Int -> f Int #-} + This SPECIALISE is treated like an expression with a type signature, so + we instantiate the constraints, simplify them and re-generalise. From the + instantaiation we get [W] d :: (forall x. Eq a => Eq (f x)) + and we want to generalise over that. We do not want to attempt to solve it + and them get stuck, and emit an error message. If we can't solve it, better + to leave it alone -* Give the Givens a CtOrigin of (GivenOrigin (InstSkol IsQC head_size)) -* Give the Wanted a CtOrigin of (ScOrigin IsQC NakedSc) + We still need to simplify quantified constraints that can be + /fully solved/ from instances, otherwise we would never be able to + specialise them away. Example: {-# SPECIALISE f @[] @a #-}. -Both of these things are done in solveForAll. Now the mechanism described -in Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance takes over. + You might worry about the wasted work, but it is seldom repeated (because the + constraint solver seldom iterates much). Note [Solving a Given forall-constraint] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a729a7c6e96bd24724f3605adb96fb1... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a729a7c6e96bd24724f3605adb96fb1... You're receiving this email because of your account on gitlab.haskell.org.