Note [Shortcut solving]

GHC/Tc/Solver/Dict.hs:501 compiler 4 tickets

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

Referenced by 6