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