Note [Solving a Wanted forall-constraint]

GHC/Tc/Solver/Solve.hs:1324 compiler 3 tickets

Solving a wanted forall (quantified) constraint
  [W] df :: forall a b. (Eq a, Ord b) => C x a b
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.

What we actually do is this:

* In `solveForAll` we see if we have an identical quantified constraint
  to solve it (using tryInertQCs).  In particular, solve a Wanted QCI
  from an identical Given.  This is more than a simple optimisation:
  see Note [Solving Wanted QCs from Given QCs]

  If not, just stash it in `inert_qcis :: [QCInst]`. (If it's a Given
  we can use it to solve other constraints; if a Wanted we will solve
  it later using `solveWantedQCIs`.)

* In the main `solveSimpleWanteds` (specifically `solve_one`):

  - We attempt to solve the `wc_simple` constraints with `solveSimples`
    Unsolved quantified constraints just accumulate in the `inert_qcis` field
    of the `InertSet`.

  - Then we use `solveWantedQCIs` to solve any quantified constraints. That
    often turns the `QCInst` into an `Implication`; but not invariably (WFA4)

Wrinkles:

(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 dictionary
  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 `solveWantedQCI`.  Now the mechanism described
  in Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance takes over.

(WFA3) Error messages. Suppose we are trying to solve the quantified constraint
            forall a. Eq a => Eq (c a)
  We don't just want to say "No instance for Eq (c a)".  It /really/ helps to
  say what quantified constraint we were trying to solve.

  So the `IsQC` origin carries that info, and `GHC.Tc.Errors.Ppr.pprQCOriginExtra`
  prints the extra info.

(WFA4) When `tcsmFullySolveQCIs` is on, we adopt an all-or-nothing strategy:
   either solve the forall-constraint /fully/ or do nothing at all.
   Why?  See (NFS1) in Note [Handling new-form SPECIALISE pragmas] in GHC.Tc.Gen.Sig

(WFA5) Why not /always/ us the all-or-nothing strategy, so we don't need a
  flag?  Several reasons:

  * Less efficient; `tcsmFullySolveQCIs` abandons the work done on the constraint,
    so we might do it again next time around.

  * More importantly, we would get worse results from `deriving`: #26315.
    In that code the `deriving` mechanism was trying to solve
           [W] df :: forall n. Eq (Const i n)
    If we turn it into an implication, we can simplfy that `Const` to get
    the residual implication
           forall n.  [W] d :: Eq i
    And then `approximateWC` can extract the (Eq i) as a plausible context for
    the instance.

  * Very much the same issue came up for the inferred type of a function that
    lacks a type signature #26376.  Again, if the forall-constraint is not
    turned into an implication `approximateWC` gives a less-good answer.

References 4

Referenced by 9