Note [Infinitary substitutions]

Do the types (x, x) and ([y], y) unify? The answer is seemingly "no" --
no substitution to finite types makes these match. This is the famous
"occurs check".

But, a substitution to *infinite* types can unify these two types:
  [x |-> [[...]]], y |-> [[[...]]] ].

Why do we care? Consider these two type family instances:

  type instance F x x   = Int
  type instance F [y] y = Bool

If we also have

  type instance Looper = [Looper]

then the instances potentially overlap -- they are not "apart". So we must
distinguish failure-to-unify from definitely-apart. The solution is to use
unification over infinite terms. This is possible (see [1] for lots of gory
details), but a full algorithm is a little more powerful than we need. Instead,
we make a conservative approximation and just omit the occurs check.

  [1]: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf

tcUnifyTys considers an occurs-check problem as the same as general unification
failure.

See also #8162.

It's worth noting that unification in the presence of infinite types is not
complete. This means that, sometimes, a closed type family does not reduce
when it should. See test case indexed-types/should_fail/Overlap15 for an
example.