Note [Non-trivial definitional equality]

Is ((IO |> co1) Int |> co2) equal to (IO Int)?
Assume
   co1 :: (Type->Type) ~ (Type->Wombat)
   co2 :: Wombat ~ Type
Well, yes.  The casts are just getting in the way.
See also Note [Respecting definitional equality].

So we do this:

(EQTYPE)
  The `eqType` function, which defines Core's type equality relation,
  - /ignores/ casts, and
  - /ignores/ coercion arguments
  - /provided/ two types have the same kind

This allows us to be a little sloppier in keeping track of coercions, which is a
good thing. It also means that eqType does not depend on eqCoercion, which is
also a good thing.

Why is this sensible? That is, why is something different than α-equivalence
appropriate for the implementation of eqType?

Anything smaller than ~ and homogeneous is an appropriate definition for
equality. The type safety of FC depends only on ~. Let's say η : τ ~ σ. Any
expression of type τ can be transmuted to one of type σ at any point by
casting. The same is true of expressions of type σ. So in some sense, τ and σ
are interchangeable.

But let's be more precise. If we examine the typing rules of FC (say, those in
https://richarde.dev/papers/2015/equalities/equalities.pdf)
there are several places where the same metavariable is used in two different
premises to a rule. (For example, see Ty_App.) There is an implicit equality
check here. What definition of equality should we use? By convention, we use
α-equivalence. Take any rule with one (or more) of these implicit equality
checks. Then there is an admissible rule that uses ~ instead of the implicit
check, adding in casts as appropriate.

The only problem here is that ~ is heterogeneous. To make the kinds work out
in the admissible rule that uses ~, it is necessary to homogenize the
coercions. That is, if we have η : (τ : κ1) ~ (σ : κ2), then we don't use η;
we use η |> kind η, which is homogeneous.

The effect of this all is that eqType, the implementation of the implicit
equality check, can use any homogeneous relation that is smaller than ~, as
those rules must also be admissible.

A more drawn out argument around all of this is presented in Section 7.2 of
Richard E's thesis (http://richarde.dev/papers/2016/thesis/eisenberg-thesis.pdf).

What would go wrong if we insisted on the casts matching? See the beginning of
Section 8 in the unpublished paper above. Theoretically, nothing at all goes
wrong. But in practical terms, getting the coercions right proved to be
nightmarish. And types would explode: during kind-checking, we often produce
reflexive kind coercions. When we try to cast by these, mkCastTy just discards
them. But if we used an eqType that distinguished between Int and Int |> <*>,
then we couldn't discard -- the output of kind-checking would be enormous,
and we would need enormous casts with lots of CoherenceCo's to straighten
them out.

Would anything go wrong if eqType looked through type families? No, not at
all. But that makes eqType rather hard to implement.

Thus, the guideline for eqType is that it should be the largest
easy-to-implement relation that is still smaller than ~ and homogeneous. The
precise choice of relation is somewhat incidental, as long as the smart
constructors and destructors in Type respect whatever relation is chosen.

Another helpful principle with eqType is this:

 (EQ) If (t1 `eqType` t2) then I can replace t1 by t2 anywhere.

This principle also tells us that eqType must relate only types with the
same kinds.

Interestingly, it must be the case that the free variables of t1 and t2
might be different, even if t1 `eqType` t2. A simple example of this is
if we have both cv1 :: k1 ~ k2 and cv2 :: k1 ~ k2 in the environment.
Then t1 = t |> cv1 and t2 = t |> cv2 are eqType; yet cv1 is in the free
vars of t1 and cv2 is in the free vars of t2. Unless we choose to implement
eqType to be just α-equivalence, this wrinkle around free variables
remains.

Yet not all is lost: we can say that any two equal types share the same
*relevant* free variables. Here, a relevant variable is a shallow
free variable (see Note [Shallow and deep free variables] in GHC.Core.TyCo.FVs)
that does not appear within a coercion. Note that type variables can
appear within coercions (in, say, a Refl node), but that coercion variables
cannot appear outside a coercion. We do not (yet) have a function to
extract relevant free variables, but it would not be hard to write if
the need arises.