Łukasz Czajka cbd8253afd Instance coercions (#2444) ... * 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"; ```		2023-10-19 16:00:31 +02:00
..
Negative.hs	Instance coercions (#2444)	2023-10-19 16:00:31 +02:00
Positive.hs	Fix instance axiom bug (#2439)	2023-10-10 15:55:17 +02:00