Note [Family applications in canonical constraints]
A constraint with a type family application in the RHS needs special care.
This is dealt with by `checkFamApp`.
(CFA1) First, occurs checks. If we have
[G] a ~ Maybe (F (Maybe a))
[W] alpha ~ Maybe (F (Maybe alpha))
it looks as if we have an occurs check. But go read
Note [Type equality cycles] in GHC.Tc.Solver.Equality
The same considerations apply when the LHS is a type family:
[G] G a ~ Maybe (F (Maybe (G a)))
[W] G alpha ~ Maybe (F (Maybe (G alpha)))
(CFA2) Second, promotion. If we have (#22194)
[W] alpha[2] ~ Maybe (F beta[4])
it is wrong to promote beta. Instead we want to split to
[W] alpha[2] ~ Maybe gamma[2]
[W] gamma[2] ~ F beta[4]
See Note [Promotion and level-checking] above.
(CFA3) Third, concrete type variables. If we have
[W] alpha[conc] ~ Maybe (F tys)
we want to add an extra variable thus:
[W] alpha[conc] ~ Maybe gamma[conc]
[W] gamma[conc] ~ F tys
Now we can unify alpha, and that might unlock something else.
In all these cases we want to create a fresh type variable, and
emit a new equality connecting it to the type family application.
Once these three cases are dealt with, the `tef_fam_app` field of `TypeEqFlags`
says what to do:
(CFA4) `TEFA_Recurse` is straightforward: just recurse into the arguments,
BUT use `recurseIntoFamTyConApp` to record that we are now "under" a
type-family application; see `famAppArgFlags`.
(CFA5) `TEFA_Break` is the clever one. It does a two-step process:
(1) Recurse into the arguments with `recurseIntoFamTyConApp`.
(2) If any of the arguments fail (level-check error, occurs check,
concreteness failure), use the `FamAppBreaker` to create a cycle breaker.
Remarks:
* It would be possible to use Step (2) above always, skipping Step (1).
But this would create many unnecessary cycle-breaker variables.
This was the cause of #25933.
* This always cycle-breaks the /outermost/ family application.
If we have [W] alpha ~ Maybe (F (G alpha)):
- We'll use checkFamApp on `(F (G alpha))`
- In Step (1), `recurseIntoFamTyConApp` sets `tef_fam_app := TEFA_Recurse`,
before looking at the argument `(G alpha)`. So we will not cycle-break
the latter
- The occurs check will fire when we hit `alpha`
- `checkFamApp` on `(F (G alpha))` will see the failure and invoke
the `FamAppBreaker`.
* Step (1) may fail because of a level-check problem, which activates step (2).
This is what implements (CFA2). References 2
- Type equality cycles GHC.Tc.Solver.Equality
- Promotion and level-checking GHC.Tc.Utils.Unify
Referenced by 5
- GHC.Tc.Utils.Unify call site ×5