Note [Shortcut solving]
When we interact a [W] constraint with a [G] constraint that solves it, there is a possibility that we could produce better code if instead we solved from a top-level instance declaration (See #12791, #5835). For example: class M a b where m :: a -> b type C a b = (Num a, M a b) f :: C Int b => b -> Int -> Int f _ x = x + 1 The body of `f` requires a [W] `Num Int` instance. We could solve this constraint from the givens because we have `C Int b` and that provides us a solution for `Num Int`. This would let us produce core like the following (with -O2): f :: forall b. C Int b => b -> Int -> Int f = \ (@ b) ($d(%,%) :: C Int b) _ (eta1 :: Int) -> + @ Int (GHC.Classes.$p1(%,%) @ (Num Int) @ (M Int b) $d(%,%)) eta1 A.f1 This is bad! We could do /much/ better if we solved [W] `Num Int` directly from the instance that we have in scope: f :: forall b. C Int b => b -> Int -> Int f = \ (@ b) _ _ (x :: Int) -> 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. 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 plan is this: If we could solve a constraint from a local Given, try first to /completely/ solve the constraint using only top-level instances, /without/ using any local Givens. - If that succeeds, use it - If not, use the local Given An example that succeeds: class Eq a => C a b | b -> a where m :: b -> a f :: C [Int] b => b -> Bool f x = m x == [] We solve for `Eq [Int]`, which requires `Eq Int`, which we also have. This produces the following core: f :: forall b. C [Int] b => b -> Bool f = \ (@ b) ($dC :: C [Int] b) (x :: b) -> GHC.Classes.$fEq[]_$s$c== (m @ [Int] @ b $dC x) (GHC.Types.[] @ Int) An example that fails: class Eq a => C a b | b -> a where m :: b -> a f :: C [a] b => b -> Bool f x = m x == [] 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) -> == @ [a] (A.$p1C @ [a] @ b $dC) (m @ [a] @ b $dC eta) (GHC.Types.[] @ a) The moving parts are relatively simple: * To attempt to solve the constraint completely, we just recursively call the constraint solver. See the use of `tryShortCutTcS` in `tcShortCutSolver`. * When this attempted recursive solving, in `tryShortCutTcS`, we - start with an empty inert set: no Givens and no Wanteds - set a special mode `TcSShortCut`, which signals that we are trying to solve using only top-level instances. * When in TcSShortCut mode, since there are no Givens we can short-circuit; these are all just optimisations: - `tryInertDicts` - `GHC.Tc.Solver.Monad.lookupInertDict` - `noMatchableGivenDicts` - `matchLocalInst` - `GHC.Tc.Solver.Solve.runTcPluginsWanted` * In `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 #
References 1
- Shortcut solving: incoherence GHC.Tc.Solver.Dict
Referenced by 6
- GHC.Tc.Solver.Dict call site ×3
- GHC.Tc.Solver.Monad call site ×2
- TcSMode GHC.Tc.Solver.Monad