GHC Handbook

Chapter 4

The constraint solver

What happens to the pile of facts the typechecker wrote down: a rewriting engine built around a carefully maintained set of "inert" constraints, and the compromises that make it both complete enough and quiet enough to use.

Where this lives in the tree

The previous chapter ended with a WantedConstraints tree and no attempt to solve any of it. This chapter is that attempt.

The solver is the part of GHC that most resembles a theorem prover, and it is worth saying up front that it is not a complete one. Haskell’s type system with its extensions is undecidable; the solver is a carefully-tuned incomplete procedure that accepts the programs people write, terminates on the ones they don’t, and produces errors a human can act on. Several of its most important design decisions are explicitly compromises between those three goals.

The inert set

The central data structure holds constraints that have been processed and cannot currently react with each other (hence inert):

data InertCans
  = IC { inert_eqs :: InertEqs
              -- All EqCt with a TyVarLHS; index is the LHS tyvar
              -- Domain = skolems and untouchables; a touchable would be unified

       , inert_funeqs :: InertFunEqs
              -- All EqCt with a TyFamLHS; index is the whole family head type.
              -- LHS is fully rewritten wrt inert_eqs

       , inert_dicts :: DictMap DictCt
              -- Dictionaries only
              -- All fully rewritten wrt inert_eqs

       , inert_qcis :: [QCInst]
       , ... }

The comments carry the invariant that makes the whole thing work: everything in the set is fully rewritten with respect to inert_eqs. If the set knows a ~ Int, then nothing anywhere else in the set still mentions a.

Maintaining that is the solver’s main job, and it is why adding a constraint is not a simple insertion. The basic loop is:

  1. Take a constraint off the work list.
  2. Rewrite it using everything in the inert set.
  3. Canonicalise it into a normal form (CEqCan, CDictCan, …).
  4. Try to solve it outright: from a Given, from an instance, from a top-level axiom.
  5. If it survives, add it to the inert set, and kick out any existing inert constraint that the newcomer can now rewrite, putting it back on the work list.

Kick-out is the step that surprises people. Adding one equality can eject a dozen constraints back into the queue, and that is not a failure mode: it is how the invariant is restored.

Which constraints may rewrite which

Givens may rewrite anything: they are facts. Wanteds rewriting Wanteds is the genuinely hard question, and GHC’s answer is the most-referenced Note in the whole solver:

Note [Wanteds rewrite Wanteds] GHC/Tc/Types/Constraint.hs:2496 
Should one Wanted constraint be allowed to rewrite another?

This example (along with #8450) suggests not:
   f :: a -> Bool
   f x = ( [x,'c'], [x,True] ) `seq` True
Here we get
  [W] a ~ Char
  [W] a ~ Bool
but we do not want to complain about Bool ~ Char!

This example suggests yes (indexed-types/should_fail/T4093a):
  type family Foo a
  f :: (Foo e ~ Maybe e) => Foo e
In the ambiguity check, we get
  [G] g1 :: Foo e ~ Maybe e
  [W] w1 :: Foo alpha ~ Foo e
  [W] w2 :: Foo alpha ~ Maybe alpha
w1 gets rewritten by the Given to become
  [W] w3 :: Foo alpha ~ Maybe e
Now, the only way to make progress is to allow Wanteds to rewrite Wanteds.
Rewriting w3 with w2 gives us
  [W] w4 :: Maybe alpha ~ Maybe e
which will soon get us to alpha := e and thence to victory.

TL;DR we want equality saturation.

We thus want Wanteds to rewrite Wanteds in order to accept more programs,
but we don't want Wanteds to rewrite Wanteds because doing so can create
inscrutable error messages. To solve this dilemma:

* We allow Wanteds to rewrite Wanteds, but each Wanted tracks the set of Wanteds
  it has been rewritten by, in its RewriterSet, stored in the ctev_rewriters
  field of the CtWanted constructor of CtEvidence.  (Only Wanteds have
  RewriterSets.)
Show the rest of this Note (57 more lines) 
* A RewriterSet is just a set of unfilled CoercionHoles. This is sufficient
  because only equalities (evidenced by coercion holes) are used for rewriting;
  other (dictionary) constraints cannot ever rewrite.

* The rewriter (in e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks and returns a RewriterSet,
  consisting of the evidence (a CoercionHole) for any Wanted equalities used in
  rewriting.

* Then GHC.Tc.Solver.Solve.rewriteEvidence and GHC.Tc.Solver.Equality.rewriteEqEvidence
  add this RewriterSet to the rewritten constraint's rewriter set.

* We prevent the unifier from unifying any equality with a non-empty rewriter set;
  unification effectively turns a Wanted into a Given, and we lose all tracking.
  See (REWRITERS) in Note [Unification preconditions] in GHC.Tc.Utils.Unify and
  Note [Unify only if the rewriter set is empty] in GHC.Solver.Equality.

* In error reporting, we simply suppress any errors that have been rewritten
  by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem,
  which uses `GHC.Tc.Zonk.Type.zonkRewriterSet` to look through any filled
  coercion holes. The idea is that we wish to report the "root cause" -- the
  error that rewrote all the others.

* In `selectNextWorkItem`, priorities equalities with no rewiters.  See
  Note [Prioritise Wanteds with empty RewriterSet] in GHC.Tc.Types.Constraint
  wrinkle (PER1).

* In error reporting, we prioritise Wanteds that have an empty RewriterSet:
  see Note [Prioritise Wanteds with empty RewriterSet].

Let's continue our first example above:

  inert: [W] w1 :: a ~ Char
  work:  [W] w2 :: a ~ Bool

Because Wanteds can rewrite Wanteds, w1 will rewrite w2, yielding

  inert: [W] w1 :: a ~ Char
         [W] w2 {w1}:: Char ~ Bool

The {w1} in the second line of output is the RewriterSet of w1.

Wrinkles:

(WRW1) When we find a constraint identical to one already in the inert set,
   we solve one from the other. Other things being equal, keep the one
   that has fewer (better still no) rewriters.
   See (CE4) in Note [Combining equalities] in GHC.Tc.Solver.Equality.

   To this accurately we should use `zonkRewriterSet` during canonicalisation,
   to eliminate rewriters that have now been solved.  Currently we only do so
   during error reporting; but perhaps we should change that.

(WRW2) When zonking a constraint (with `zonkCt` and `zonkCtEvidence`) we take
   the opportunity to zonk its `RewriterSet`, which eliminates solved ones.
   This doesn't guarantee that rewriter sets are always up to date -- see
   (WRW1) -- but it helps, and it de-clutters debug output.

The structure of that Note is worth admiring, because it is how a good design decision gets recorded. Two examples, pulling in opposite directions: one where letting Wanteds rewrite Wanteds produces an absurd error (Bool ~ Char, from a program that mentions neither together), one where refusing means a perfectly good program is rejected. “TL;DR we want equality saturation.” Then the resolution: allow it, but have every Wanted carry a RewriterSet recording which other Wanteds touched it, so that error reporting can suppress the ones whose “error” is really just a consequence of another failure.

That ctev_rewriters field in the previous chapter’s WantedCtEvidence exists solely for this. Its only purpose is error quality.

Equalities are the hard part

GHC/Tc/Solver/Equality.hs is 3,300 lines, and it is where the subtlety lives. Dictionary constraints are comparatively easy: look for a matching instance, produce evidence. Equalities have to contend with type families (which do not decompose), newtypes (which decompose only sometimes), representational vs nominal equality, and kinds that may themselves not yet be equal.

Two Notes give the flavour. First, the one that comes up whenever you write a recursive type family and get a “cannot construct infinite type” you did not expect:

Note [Type equality cycles] GHC/Tc/Solver/Equality.hs:2292 
Consider this situation (from indexed-types/should_compile/GivenLoop):

  instance C (Maybe b)
  *[G] a ~ Maybe (F a)
  [W] C a

or (typecheck/should_compile/T19682b):

  instance C (a -> b)
  *[W] alpha ~ (Arg alpha -> Res alpha)
  [W] C alpha

or (typecheck/should_compile/T21515):

  type family Code a
  *[G] Code a ~ '[ '[ Head (Head (Code a)) ] ]
  [W] Code a ~ '[ '[ alpha ] ]

In order to solve the final Wanted, we must use the starred constraint
for rewriting. But note that all starred constraints have occurs-check failures,
and so we can't straightforwardly add these to the inert set and
use them for rewriting. (NB: A rigid type constructor is at the
top of all RHSs, preventing reorienting in canEqTyVarFunEq in the tyvar
cases.)

The key idea is to replace the outermost type family applications in the RHS of
Show the rest of this Note (308 more lines) 
the starred constraints with a fresh variable, which we'll call a cycle-breaker
variable, or cbv. Then, relate the cbv back with the original type family
application via new equality constraints. Our situations thus become:

  instance C (Maybe b)
  [G] a ~ Maybe cbv
  [G] F a ~ cbv
  [W] C a

or

  instance C (a -> b)
  [W] alpha ~ (cbv1 -> cbv2)
  [W] Arg alpha ~ cbv1
  [W] Res alpha ~ cbv2
  [W] C alpha

or

  [G] Code a ~ '[ '[ cbv ] ]
  [G] Head (Head (Code a)) ~ cbv
  [W] Code a ~ '[ '[ alpha ] ]

This transformation (creating the new types and emitting new equality
constraints) is done by the `FamAppBreaker` field of `TEFA_Break`, which
in turn lives in the `tef_fam_app` field of `TyEqFlags`.  And that in
turn controls the behaviour of the workhorse: GHC.Tc.Utils.Unify.checkTyEqRhs.

The details depend on whether we're working with a Given or a Wanted.

Given

We emit a new Given, [G] F a ~ cbv, equating the type family application
to our new cbv. This is actually done by `break_given` in
`GHC.Tc.Solver.Monad.checkTypeEq`.

Note its orientation: The type family ends up on the left; see
Note [Orienting TyFamLHS/TyFamLHS]. No special treatment for
CycleBreakerTvs is necessary. This scenario is now easily soluble, by using
the first Given to rewrite the Wanted, which can now be solved.

(The first Given actually also rewrites the second one, giving
[G] F (Maybe cbv) ~ cbv, but this causes no trouble.)

Of course, we don't want our fresh variables leaking into e.g. error
messages.  So we fill in the metavariables with their original type family
applications after we're done running the solver (in nestImplicTcS and
runTcSWithEvBinds).  This is done by `restoreTyVarCycles`, which uses the
`inert_cycle_breakers` field in InertSet, which contains the pairings
invented in `break_given`.

That is, we transform
  [G] g : lhs ~ ...(F lhs)...
to
  [G] (Refl lhs) : F lhs ~ cbv      -- CEqCan
  [G] g          : lhs ~ ...cbv...  -- CEqCan

Note that
* `cbv` is a fresh cycle breaker variable.
* `cbv` is a meta-tyvar, but it is completely untouchable.
* We track the cycle-breaker variables in inert_cycle_breakers in InertSet
* We eventually fill in the cycle-breakers, with `cbv := F lhs`.
  No one else fills in CycleBreakerTvs!
* The evidence for the new `F lhs ~ cbv` constraint is Refl, because we know
  this fill-in is ultimately going to happen.
* In `inert_cycle_breakers`, we remember the (cbv, F lhs) pair; that is, we
  remember the /original/ type.  The [G] F lhs ~ cbv constraint may be rewritten
  by other givens (eg if we have another [G] lhs ~ (b,c)), but at the end we
  still fill in with cbv := F lhs
* This fill-in is done when solving is complete, by restoreTyVarCycles
  in nestImplicTcS and runTcSWithEvBinds.

Wanted

First, we do not cycle-break unless the LHS is a unifiable type variable
See Note [Don't cycle-break Wanteds when not unifying] in GHC.Tc.Solver.Monad.

OK, so suppose the LHS is a unifiable type variable.  The fresh cycle-breaker
variables here must actually be normal, touchable metavariables. That is, they
are TauTvs. Nothing at all unusual. Repeating the example from above, we have

  *[W] alpha ~ (Arg alpha -> Res alpha)

and we turn this into

  *[W] alpha ~ (cbv1 -> cbv2)
  [W] Arg alpha ~ cbv1
  [W] Res alpha ~ cbv2

where cbv1 and cbv2 are fresh TauTvs.  This is actually done within checkTyEqRhs,
called within canEqCanLHSFinish_try_unification, which will use the BreakWanted
FamAppBreaker.

Why TauTvs? See [Why TauTvs] below.

Critically, we emit the two new constraints (the last two above)
directly instead of calling wrapUnifierTcS. (Otherwise, we'd end up
unifying cbv1 and cbv2 immediately, achieving nothing.)  Next, we
unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This
unification happens immediately following a successful call to
checkTyEqRhs, in canEqCanLHSFinish_try_unification.

Now, we're here (including further context from our original example,
from the top of the Note):

  instance C (a -> b)
  [W] Arg (cbv1 -> cbv2) ~ cbv1
  [W] Res (cbv1 -> cbv2) ~ cbv2
  [W] C (cbv1 -> cbv2)

The first two W constraints reduce to reflexivity and are discarded,
and the last is easily soluble.

[Why TauTvs]:
Let's look at another example (typecheck/should_compile/T19682) where we need
to unify the cbvs:

  class    (AllEqF xs ys, SameShapeAs xs ys) => AllEq xs ys
  instance (AllEqF xs ys, SameShapeAs xs ys) => AllEq xs ys

  type family SameShapeAs xs ys :: Constraint where
    SameShapeAs '[] ys      = (ys ~ '[])
    SameShapeAs (x : xs) ys = (ys ~ (Head ys : Tail ys))

  type family AllEqF xs ys :: Constraint where
    AllEqF '[]      '[]      = ()
    AllEqF (x : xs) (y : ys) = (x ~ y, AllEq xs ys)

  [W] alpha ~ (Head alpha : Tail alpha)
  [W] AllEqF '[Bool] alpha

Without the logic detailed in this Note, we're stuck here, as AllEqF cannot
reduce and alpha cannot unify. Let's instead apply our cycle-breaker approach,
just as described above. We thus invent cbv1 and cbv2 and unify
alpha := cbv1 -> cbv2, yielding (after zonking)

  [W] Head (cbv1 : cbv2) ~ cbv1
  [W] Tail (cbv1 : cbv2) ~ cbv2
  [W] AllEqF '[Bool] (cbv1 : cbv2)

The first two W constraints simplify to reflexivity and are discarded.
But the last reduces:

  [W] Bool ~ cbv1
  [W] AllEq '[] cbv2

The first of these is solved by unification: cbv1 := Bool. The second
is solved by the instance for AllEq to become

  [W] AllEqF '[] cbv2
  [W] SameShapeAs '[] cbv2

While the first of these is stuck, the second makes progress, to lead to

  [W] AllEqF '[] cbv2
  [W] cbv2 ~ '[]

This second constraint is solved by unification: cbv2 := '[]. We now
have

  [W] AllEqF '[] '[]

which reduces to

  [W] ()

which is trivially satisfiable. Hooray!

Note that we need to unify the cbvs here; if we did not, there would be
no way to solve those constraints. That's why the cycle-breakers are
ordinary TauTvs.

How all this is implemented

We implement all this via the `TEFA_Break` constructor of `TyEqFamApp`,
itself stored in the `tef_fam_app` field of `TyEqFlags`, which controls
the behaviour of `GHC.Tc.Utils.Unify.checkTyEqRhs`.  The `TEFA_Break`
stuff happens when `checkTyEqRhs` encounters a family application.

We try the cycle-breaking trick:
* For Wanteds, when there is a touchable unification variable on the left
* For Givens, regardless of the LHS

EXCEPT that, in both cases, as `GHC.Tc.Solver.Monad.mkTEFA_Break` shows, we
don't use this trick:

* When the constraint we are looking at was itself created by cycle-breaking;
  see Detail (7) below.

* For representational equalities, as there is no concrete use case where it is
  helpful (unlike for nominal equalities).

  Furthermore, because function applications can be CanEqLHSs, but newtype
  applications cannot, the disparities between the cases are enough that it
  would be effortful to expand the idea to representational equalities. A quick
  attempt, with
      data family N a b
      f :: (Coercible a (N a b), Coercible (N a b) b) => a -> b
      f = coerce
  failed with "Could not match 'b' with 'b'." Further work is held off
  until when we have a concrete incentive to explore this dark corner.

More details:

 (1) We don't look under foralls, at all, in `checkTyEqRhs`.  There might be
     a cyclic occurrence underneath, in a case like
          [G] lhs ~ forall b. ... lhs ....
     but it doesn't matter because we will classify the constraint as Irred,
     so it will not be used for rewriting.

     Earlier versions required an extra, post-breaking, check.  Skipping this
     check causes typecheck/should_fail/GivenForallLoop and polykinds/T18451 to
     loop.  But now it is all simpler, with no need for a second check.

 (2) Historical Note: our goal here is to avoid loops in rewriting. We can thus
     skip looking in coercions, as we don't rewrite in coercions in the
     algorithm in GHC.Solver.Rewrite.  This doesn't seem relevant any more.
     We cycle break to make the constraint canonical.

 (3) As we cycle-break as described in this Note, we can build ill-kinded
     types. For example, if we have Proxy (F a) b, where (b :: F a), then
     replacing this with Proxy cbv b is ill-kinded. However, we will later
     set cbv := F a, and so the zonked type will be well-kinded again.
     The temporary ill-kinded type hurts no one, and avoiding this would
     be quite painfully difficult.

     Specifically, this detail does not contravene the Purely Kinded Type Invariant
     (Note [The Purely Kinded Type Invariant (PKTI)] in GHC.Tc.Gen.HsType).
     The PKTI says that we can call typeKind on any type, without failure.
     It would be violated if we, say, replaced a kind (a -> b) with a kind c,
     because an arrow kind might be consulted in piResultTys. Here, we are
     replacing one opaque type like (F a b c) with another, cbv (opaque in
     that we never assume anything about its structure, like that it has a
     result type or a RuntimeRep argument).

 (4) The evidence for the produced Givens is all just reflexive, because we
     will eventually set the cycle-breaker variable to be the type family, and
     then, after the zonk, all will be well. See also the notes at the end of
     the Given section of this Note.

 (5) The implementation in `checkTyEqRhs` is efficient because it only replaces
     a type family application with a type variable, if that particular
     appplication is implicated in the occurs check.  For example:
         [W] alpha ~ Maybe (F alpha, G beta)
     We'll end up calling GHC.Tc.Utils.Unify.checkFamApp
       * On `F alpha`, which fail and calls the cycle-breaker in TEFA_Break
       * On `G beta`, which succeeds no problem.

     However, we make no attempt to detect cases like a ~ (F a, F a) and use the
     same tyvar to replace F a. The constraint solver will common them up later!
     (Cf. Note [Apartness and type families] in GHC.Core.Unify, which goes to
     this extra effort.) However, this is really a very small corner case.  The
     investment to craft a clever, performant solution seems unworthwhile.

 (6) We often get the predicate associated with a constraint from its evidence
     with ctPred. We thus must not only make sure the generated CEqCan's fields
     have the updated RHS type (that is, the one produced by replacing type
     family applications with fresh variables), but we must also update the
     evidence itself. This is done by the call to rewriteEqEvidence in
     canEqCanLHSFinish.

 (7) We don't wish to apply this magic on the equalities created
     by this very same process. Consider this, from
     typecheck/should_compile/ContextStack2:

       type instance TF (a, b) = (TF a, TF b)
       t :: (a ~ TF (a, Int)) => ...

       [G] a ~ TF (a, Int)

     The RHS reduces, so we get

       [G] a ~ (TF a, TF Int)

     We then break cycles, to get

       [G] g1 :: a ~ (cbv1, cbv2)
       [G] g2 :: TF a ~ cbv1
       [G] g3 :: TF Int ~ cbv2

     g1 gets added to the inert set, as written. But then g2 becomes
     the work item. g1 rewrites g2 to become

       [G] TF (cbv1, cbv2) ~ cbv1

     which then uses the type instance to become

       [G] (TF cbv1, TF cbv2) ~ cbv1

     which looks remarkably like the Given we started with. If left unchecked,
     this will end up breaking cycles again, looping ad infinitum (and
     resulting in a context-stack reduction error, not an outright loop). The
     solution is easy: don't break cycles on an equality generated by breaking
     cycles. Instead, we mark this final Given as a CIrredCan with a
     NonCanonicalReason with the soluble occurs-check bit set (only).

     We track these equalities by giving them a special CtOrigin,
     CycleBreakerOrigin. This works for both Givens and Wanteds, as we need the
     logic in the W case for e.g. typecheck/should_fail/T17139.  Because this
     logic needs to work for Wanteds, too, we cannot simply look for a
     CycleBreakerTv on the left: Wanteds don't use them.


**********************************************************************
*                                                                    *
                   Rewriting evidence
*                                                                    *
**********************************************************************

And second, the case where a locally-available Given and a global instance both apply, where picking the instance would be unsound because the caller may have had a different one in mind:

Note [Instance and Given overlap] GHC/Tc/Solver/Dict.hs:1036 
Example, from the OutsideIn(X) paper:
       instance P x => Q [x]
       instance (x ~ y) => R y [x]

       wob :: forall a b. (Q [b], R b a) => a -> Int

       g :: forall a. Q [a] => [a] -> Int
       g x = wob x

From 'g' we get the implication constraint:
            forall a. Q [a] => (Q [beta], R beta [a])
If we react (Q [beta]) with its top-level axiom, we end up with a
(P beta), which we have no way of discharging. On the other hand,
if we react R beta [a] with the top-level we get  (beta ~ a), which
is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
now solvable by the given Q [a].

The partial solution is that:
  In matchClassInst (and thus in topReact), we return a matching
  instance only when there is no Given in the inerts which is
  unifiable to this particular dictionary.

  We treat any meta-tyvar as "unifiable" for this purpose,
  *including* untouchable ones.  But not skolems like 'a' in
  the implication constraint above.
Show the rest of this Note (50 more lines) 
The end effect is that, much as we do for overlapping instances, we
delay choosing a class instance if there is a possibility of another
instance OR a given to match our constraint later on. This fixes
tickets #4981 and #5002.

Other notes:

* The check is done *first*, so that it also covers classes
  with built-in instance solving, such as
     - constraint tuples
     - natural numbers
     - Typeable

* See also Note [What might equal later?] in GHC.Tc.Utils.Unify

* The given-overlap problem is arguably not easy to appear in practice
  due to our aggressive prioritization of equality solving over other
  constraints, but it is possible. I've added a test case in
  typecheck/should-compile/GivenOverlapping.hs

* Another "live" example is #10195; another is #10177.

* We ignore the overlap problem if -XIncoherentInstances is in force:
  see #6002 for a worked-out example where this makes a
  difference.

* Moreover notice that our goals here are different than the goals of
  the top-level overlapping checks. There we are interested in
  validating the following principle:

      If we inline a function f at a site where the same global
      instance environment is available as the instance environment at
      the definition site of f then we should get the same behaviour.

  But for the Given Overlap check our goal is just related to completeness of
  constraint solving.

* The solution is only a partial one.  Consider the above example with
       g :: forall a. Q [a] => [a] -> Int
       g x = let v = wob x
             in v
  and suppose we have -XNoMonoLocalBinds, so that we attempt to find the most
  general type for 'v'.  When generalising v's type we'll simplify its
  Q [alpha] constraint, but we don't have Q [a] in the 'givens', so we
  will use the instance declaration after all. #11948 was a case
  in point.

All of this is disgustingly delicate, so to discourage people from writing
simplifiable class givens, we warn about signatures that contain them;
see GHC.Tc.Validity Note [Simplifiable given constraints].

Termination is bought, not given

Nothing about the loop above terminates on its own. A type family can expand forever; superclass expansion can cycle; instances can chain indefinitely. GHC buys termination with explicit budgets: the solver counts, and gives up when the count runs out. ExpansionFuel is exactly what it sounds like:

Note [Expanding Recursive Superclasses and ExpansionFuel] GHC/Tc/Solver/Solve.hs:197 
Consider the class declaration (T21909)

    class C [a] => C a where
       foo :: a -> Int

and suppose during type inference we obtain an implication constraint:

    forall a. C a => C [[a]]

To solve this implication constraint, we first expand one layer of the superclass
of Given constraints, but not for Wanted constraints.
(See Note [Eagerly expand given superclasses] and Note [Why adding superclasses can help]
in GHC.Tc.Solver.Dict.) We thus get:

    [G] g1 :: C a
    [G] g2 :: C [a]    -- new superclass layer from g1
    [W] w1 :: C [[a]]

Now, we cannot solve `w1` directly from `g1` or `g2` as we may not have
any instances for C. So we expand a layer of superclasses of each Wanteds and Givens
that we haven't expanded yet.
This is done in `maybe_simplify_again`. And we get:

    [G] g1 :: C a
Show the rest of this Note (38 more lines) 
    [G] g2 :: C [a]
    [G] g3 :: C [[a]]    -- new superclass layer from g2, can solve w1
    [W] w1 :: C [[a]]
    [W] w2 :: C [[[a]]]  -- new superclass layer from w1, not solvable

Now, although we can solve `w1` using `g3` (obtained from expanding `g2`),
we have a new wanted constraint `w2` (obtained from expanding `w1`) that cannot be solved.
We thus make another go at solving in `maybe_simplify_again` by expanding more
layers of superclasses. This looping is futile as Givens will never be able to catch up with Wanteds.

Side Note: In principle we don't actually need to /solve/ `w2`, as it is a superclass of `w1`
but we only expand it to expose any functional dependencies (see Note [The superclass story])
But `w2` is a wanted constraint, so we will try to solve it like any other,
even though ultimately we will discard its evidence.

Solution: Simply bound the maximum number of layers of expansion for
Givens and Wanteds, with ExpansionFuel.  Give the Givens more fuel
(say 3 layers) than the Wanteds (say 1 layer). Now the Givens will
win.  The Wanteds don't need much fuel: we are only expanding at all
to expose functional dependencies, and wantedFuel=1 means we will
expand a full recursive layer.  If the superclass hierarchy is
non-recursive (the normal case) one layer is therefore full expansion.

The default value for wantedFuel = Constants.max_WANTEDS_FUEL = 1.
The default value for givenFuel  = Constants.max_GIVENS_FUEL = 3.
Both are configurable via the `-fgivens-fuel` and `-fwanteds-fuel`
compiler flags.

There are two preconditions for the default fuel values:
   (1) default givenFuel >= default wantedsFuel
   (2) default givenFuel < solverIterations

Precondition (1) ensures that we expand givens at least as many times as we expand wanted constraints
preferably givenFuel > wantedsFuel to avoid issues like T21909 while
the precondition (2) ensures that we do not reach the solver iteration limit and fail with a
more meaningful error message (see T19627)

This also applies for quantified constraints; see `-fqcs-fuel` compiler flag and `QCI.qci_pend_sc` field.

This is why -freduction-depth exists, and why raising it sometimes makes a program compile. The limit is not a soundness boundary; it is a stopping condition standing in for a decision procedure nobody has.

When it finishes

The solver returns a residual WantedConstraints. If it is empty, the module type-checks and every evidence hole has been filled. If not, the leftovers go to GHC/Tc/Errors.hs, whose job is to turn unsolved constraints into the message you actually see, and which uses the RewriterSet from above to decide which of several related failures is the real one.

Successfully solved constraints leave behind evidence: dictionaries and coercions, bound in the elaborated program. They are why the desugarer has something concrete to translate.

Seeing the evidence

The solver has no dump of its own. -ddump-tc-trace shows its working, but that is a debugging firehose rather than something to read. Unless, that is, the module is tiny by design: the trace explorer runs it on three-line modules and folds the output into a navigable tree. Watch it solve a dictionary, or an implication with a Given. What you can see here is its output, which is the evidence.

What you wrote.

{-# LANGUAGE GADTs #-}

-- | Why the typechecker separates constraint generation from constraint solving.
--
-- Each branch of `eval` type-checks under a *different* assumption: matching on
-- `IntLit` tells GHC that `a ~ Int`, matching on `BoolLit` that `a ~ Bool`. A
-- checker that unified eagerly would have nowhere to put a fact that holds only
-- inside one alternative, so GHC records it as an implication constraint with a
-- Given, and solves later.
--
-- In the desugared Core the same facts appear as coercions: the evidence that
-- `a` and `Int` really are the same type, made into a term.
module Gadt where

data Expr a where
  IntLit  :: Int -> Expr Int
  BoolLit :: Bool -> Expr Bool
  Add     :: Expr Int -> Expr Int -> Expr Int
  If      :: Expr Bool -> Expr a -> Expr a -> Expr a
  Eq      :: Expr Int -> Expr Int -> Expr Bool

eval :: Expr a -> a
eval (IntLit n) = n
eval (BoolLit b) = b
eval (Add x y) = eval x + eval y
eval (If c t e) = if eval c then eval t else eval e
eval (Eq x y) = eval x == eval y

-- A plain polymorphic function for contrast: no refinement anywhere, so no
-- implications are generated and the constraint set stays flat.
describe :: Show a => a -> String
describe x = "value: " ++ show x
Every coercion in the desugared Core is a solved equality constraint. The `coercions:` count in the RHS size header is a direct measure of how much work the solver did.

Switch to Full detail and read the RHS size line above eval: {terms: 32, types: 51, coercions: 18, ...}. Those eighteen coercions are solved constraints. Each Sym, Sub and composition in the body is the solver’s proof, written down in a form the rest of the compiler can check with Core Lint.

The concrete answer to “what does the solver produce?” is not a yes/no, but evidence terms.

Reading the source yourself

This is the hardest code in GHC to read cold. A workable order:

  1. GHC/Tc/Solver/InertSet.hs, and specifically its Notes rather than its functions. Note [inert_eqs: the inert equalities] and the kick-out Notes explain the invariant that everything else preserves.
  2. GHC/Tc/Solver/Solve.hs: solveOne and solveCt show the pipeline stages plainly.
  3. GHC/Tc/Solver/Rewrite.hs next, since rewriting is step two of every constraint’s life.
  4. GHC/Tc/Solver/Equality.hs last, and only with a specific question.

-ddump-tc-trace prints the solver’s every step. It is enormously verbose and the fastest way to understand why a particular program was rejected: start from a three-line failing module, never a real one. The trace pages are exactly that, pre-run: the full trace of modules with no mysteries in them, so the markers are familiar before you need them on a program with one.