Note [EqCt occurs check]

A CEqCan relates a CanEqLHS (a type variable or type family applications) on
its left to an arbitrary type on its right. It is used for rewriting.
Because it is used for rewriting, it would be disastrous if the RHS
were to mention the LHS: this would cause a loop in rewriting.

We thus perform an occurs-check. There is, of course, some subtlety:

* For type variables, the occurs-check looks deeply including kinds of
  type variables. This is because a CEqCan over a meta-variable is
  also used to inform unification, via `checkTyEqRhs`, called in
  `canEqCanLHSFinish_try_unification`.
  If the LHS appears anywhere in the RHS, at all, unification will create
  an infinite structure, which is bad.

* For type family applications, the occurs-check is shallow; it looks
  only in places where we might rewrite. (Specifically, it does not
  look in kinds or coercions.) An occurrence of the LHS in, say, an
  RHS coercion is OK, as we do not rewrite in coercions. No loop to
  be found.

  You might also worry about the possibility that a type family
  application LHS doesn't exactly appear in the RHS, but something
  that reduces to the LHS does. Yet that can't happen: the RHS is
  already inert, with all type family redexes reduced. So a simple
  syntactic check is just fine.

The occurs check is performed in GHC.Tc.Utils.Unify.checkTyEqRhs
and forms condition T3 in Note [Extending the inert equalities]
in GHC.Tc.Solver.InertSet.