Note [inert_eqs: the inert equalities]

Our main invariant:
   the EqCts in inert_eqs should be a
        terminating generalised substitution

Definition [Can-rewrite relation] --------------
A "can-rewrite" relation between flavours, written f1 >= f2, is a
binary relation with the following properties

  (R1) >= is transitive
  (R2) If f1 >= f, and f2 >= f,
       then either f1 >= f2 or f2 >= f1
  (See Note [Why R2?].)

Lemma (L0). If f1 >= f then f1 >= f1
Proof.      By property (R2), with f1=f2

Definition [Generalised substitution] ---------------
A "generalised substitution" S is a set of triples (lhs -f-> t), where
  - lhs is a type variable or an exactly-saturated type family application
                  (that is, lhs is a CanEqLHS)
  - t is a type
  - f is a flavour

such that

  (WF1) if (lhs1 -f1-> t1) in S
           (lhs2 -f2-> t2) in S
        then (f1 >= f2) implies that lhs1 does not appear within lhs2

  (WF2) if (lhs -f-> t) is in S, then t /= lhs

  (WF3) No LHS in S is rewritable in an RHS in S,
        in the argument of a type family application (F ty1..tyn)
        where F heads a LHS in S

Definition [Applying a generalised substitution] ----------
If S is a generalised substitution
   S(f,lhs)      = rhs,             if (lhs -fs-> rhs) in S, and fs >= f
   S(f,T t1..tn) = T S(f1,t1)..S(fn,tn)
   S(f,t1 t2)    = S(f,t1) S(f_N,t2)
   S(f,t)        = t
Here f1..fn are obtained from f and T using the roles of T, and f_N is
the nominal version of f.  See Note [Flavours with roles].

Notation: repeated application.
  S^0(f,t)     = t
  S^(n+1)(f,t) = S(f, S^n(t))
  S*(f,t) is the result of applying S until you reach a fixpoint

 Definition [Terminating generalised substitution] ---------
A generalised substitution S is *terminating* iff

  (IG1) for every f,t, there is an n such that
             S^n(f,t) = S^(n+1)(f,t)

By (IG1) we define S*(f,t) to be the result of exahaustively
applying S(f,_) to t.
End of definitions ------------------------------------


Rationale for (WF1)-(WF3)

* (WF1) guarantees that S is well-defined /as a function/;
  see Theorem (S is a function)

   Theorem (S is a function): S(f,t0) is well defined as a function.
   Proof: Suppose (lhs -f1-> t1) and (lhs -f2-> t2) are both in S,
               and  f1 >= f and f2 >= f
          Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
   Note: this argument isn't quite right.  WF1 ensures that lhs1 does
   not appear inside lhs2, and that guarantees confluence. But I can't quite
   see how to make that argument precise.

* (WF2) is a bit trivial.  It means that if S is terminating, so that
  S^(n+1)(f,t) = S^n(f,t), then there is no LHS of S in S^n(f,t).  We
  never get a silly infinite sequence a -> a -> a -> a  .... which is
  technically a fixed point but would still go on for ever.

* (WF3) is need for the termination proof.

Note that termination is not the same as idempotence.  To apply S to a
type, you may have to apply it recursively.  But termination does
guarantee that this recursive use will terminate.