Note [Solving a Wanted forall-constraint]
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
- Handling new-form SPECIALISE pragmas GHC.Tc.Gen.Sig
- Solving Wanted QCs from Given QCs GHC.Tc.Solver.Solve
- Recursive superclasses GHC.Tc.TyCl.Instance
- Solving superclass constraints GHC.Tc.TyCl.Instance
Referenced by 9
- GHC.Tc.Solver.Solve call site ×7
- GHC.Tc.Errors.Ppr call site
- ApproximateWC GHC.Tc.Types.Constraint