Refactor coercion rule

Authored by ningning on Mon, Jul 9, 7:02 PM.

Description

Refactor coercion rule

Summary:
The patch is an attempt on Trac #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 Trac #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 Trac #15192, comment:13 for
more information.

Test Plan: ./validate

Reviewers: bgamari, goldfire, simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: Trac #15192

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