Refactor coercion rule

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


Refactor coercion rule

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: