Note [Self-substitution when unifying or matching]

What happens when we are unifying or matching two identical type variables?
     a ~ a

* When /unifying/, just succeed, without binding [a :-> a] in the substitution,
  else we'd get an infinite substitution.  We need to make this check before
  we do the occurs check, of course.

* When /matching/, and `a` is a bindable variable from the template, we /do/
  want to extend the substitution.  Remember, a successful match should map all
  the template variables (except ones that disappear when expanding synonyms),

  But when `a` is /not/ a bindable variable (perhaps it is a globally-in-scope
  skolem) we want to treat it like a constant `Int ~ Int` and succeed.

  Notice: no occurs check!  It's fine to match (a ~ Maybe a), because the
  template vars of the template come from a different name space to the free
  vars of the target.

  Note that this arrangement was provoked by a real failure, where the same
  unique ended up in the template as in the target. (It was a rule firing when
  compiling Data.List.NonEmpty.)

* What about matching a /non-bindable/ variable?  For example:
      template-vars   : {a}
      matching problem: (forall b. b -> a) ~ (forall c. c -> Int)
  We want to emerge with the substitution [a :-> Int]
  But on the way we will encounter (b ~ b), when we match the bits before the
  arrow under the forall, having renamed `c` to `b`.  This match should just
  succeed, just like (Int ~ Int), without extending the substitution.

  It's important to do this for /non-bindable/ variables, not just for
  forall-bound ones.  In an associated type
         instance C (Maybe a) where {  type F (Maybe a) = Int }
  `checkConsistentFamInst` matches (Maybe a) from the header against (Maybe a)
  from the type-family instance, with `a` marked as non-bindable.