Note [Family applications in canonical constraints]

GHC/Tc/Utils/Unify.hs:3973 compiler 2 tickets

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

Referenced by 5