* Closes#2426
A coercion from trait `T` to `T'` can be declared with the syntax
```
coercion instance
coeName {A} {{T A}} : T' A := ...
```
Coercions can be seen as instances with special resolution rules.
Coercion resolution rules
-------------------------
* If a non-coercion instance can be applied in a single instance
resolution step, no coercions are considered. No ambiguity results if
there exists some coercion which could be applied, but a non-coercion
instance exists - the non-coercion instances have priority.
* If no non-coercion instance can be applied in a single resolution
step, all minimal coercion paths which lead to an applicable
non-coercion instance are considered. If there is more than one,
ambiguity is reported.
Examples
----------
The following type-checks because:
1. There is no non-coercion instance found for `U String`.
2. There are two minimal coercion paths `U` <- `U1` and `U` <- `U2`, but
only one of them (`U` <- `U2`) ends in an applicable non-coercion
instance (`instU2` for `U2 String`).
```
trait
type U A := mkU {pp : A -> A};
trait
type U1 A := mkU1 {pp : A -> A};
trait
type U2 A := mkU2 {pp : A -> A};
coercion instance
fromU1toU {A} {{U1 A}} : U A :=
mkU@{
pp := U1.pp
};
coercion instance
fromU2toU {A} {{U2 A}} : U A :=
mkU@{
pp := U2.pp
};
instance
instU2 : U2 String := mkU2 id;
main : IO := printStringLn (U.pp "X")
```
The following results in an ambiguity error because:
1. There is no non-coercion instance found for `T Unit`.
2. There are two minimal coercion paths `T` <- `T1` and `T` <- `T2`,
both of which end in applicable non-coercion instances.
```
trait
type T A := mkT { pp : A → A };
trait
type T1 A := mkT1 { pp : A → A };
trait
type T2 A := mkT2 { pp : A → A };
instance
unitT1 : T1 Unit := mkT1 (pp := λ{_ := unit});
instance
unitT2 : T2 Unit := mkT2 (pp := λ{_ := unit});
coercion instance
fromT1toT {A} {{T1 A}} : T A := mkT@{
pp := T1.pp
};
coercion instance
fromT2toT {A} {{T2 A}} : T A := mkT@{
pp := T2.pp
};
main : Unit := T.pp unit;
```
The following type-checks, because there exists a non-coercion instance
for `T2 String`, so the coercion `fromT1toT2` is ignored during instance
resolution.
```
trait
type T1 A := mkT1 {pp : A -> A};
trait
type T2 A := mkT2 {pp : A -> A};
instance
instT1 {A} : T1 A :=
mkT1@{
pp := id
};
coercion instance
fromT1toT2 {A} {{M : T1 A}} : T2 A :=
mkT2@{
pp := T1.pp {{M}}
};
instance
instT2 : T2 String :=
mkT2@{
pp (s : String) : String := s ++str "!"
};
main : String := T2.pp "a";
```
