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
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
* *
**********************************************************************