Refactor of Coercion

This patch aims at generalizing the reflexive coercion to

  | GRefl Role Type MCoercion

As its name suggests, and as its typing rule makes precise, GRefl is generalised version of Refl:

     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 any coercion (MCo co). To know more about MCoercion see #14975.

This new coercion form will replace both Refl and the current CoherenceCo:

  | Refl Role Type

  -- Coherence applies a coercion to the left-hand type of another coercion
  -- See Note [Coherence]
  | CoherenceCo Coercion KindCoercion
     -- :: e -> N -> e

When the MCoercion is MRefl, GRefl is just the same as Refl.

It is easy to express CoherenceCo using GRefl. If g1 :: s ~r t, then

CoherenceCo g1 g2        :: (s |> g2) ~r t
Sym (GRefl r s g2) ; g1  :: (s |> g1) ~r t