Summary:
The patch is an attempt on #15192.

It defines a new coercion rule

```
 | GRefl Role Type MCoercion
```

which correspondes to the typing rule

```
     t1 : k1
  ------------------------------------
  GRefl r t1 MRefl: t1 ~r t1

     t1 : k1       co :: k1 ~ k2
  ------------------------------------
  GRefl r t1 (MCo co) : t1 ~r t1 |> co
```

MCoercion wraps a coercion, which might be reflexive (MRefl)
or not (MCo co). To know more about MCoercion see #14975.

We keep Refl ty as a special case for nominal reflexive coercions,
naemly, Refl ty :: ty ~n ty.

This commit is meant to be a general performance improvement,
but there are a few regressions. See #15192, comment:13 for
more information.

Test Plan: ./validate

Reviewers: bgamari, goldfire, simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15192

Differential Revision: https://phabricator.haskell.org/D4747