From acb56252104dace444fa86a514a15603b297ed1a Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Thu, 11 Jul 2024 21:52:12 +0200 Subject: [PATCH 1/8] tweaks --- src/ir_passes/await.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ir_passes/await.ml b/src/ir_passes/await.ml index 3cf213b2b2e..7ef19bdc480 100644 --- a/src/ir_passes/await.ml +++ b/src/ir_passes/await.ml @@ -594,7 +594,7 @@ and t_comp_unit context = function let e = fresh_var "e" T.catch in ProgU [ funcD throw e (assertE (falseE ())); - expD (c_block context' ds (tupE []) (meta (T.unit) (fun v1 -> tupE []))) + expD (c_block context' ds (tupE []) (meta T.unit (fun v1 -> tupE []))) ] end | ActorU (as_opt, ds, ids, { meta = m; preupgrade; postupgrade; heartbeat; timer; inspect}, t) -> @@ -619,7 +619,7 @@ and t_ignore_throw context exp = { (blockE [ funcD throw e (tupE[]); ] - (c_exp context' exp (meta (T.unit) (fun v1 -> tupE [])))) + (c_exp context' exp (meta T.unit (fun v1 -> tupE [])))) (* timer logic requires us to preserve any source location, or timer won't be initialized in compile.ml *) with at = exp.at From f1de79655bc32c4e8dee0fbb2cf1ca39e8a87d25 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Sun, 14 Jul 2024 15:52:40 +0200 Subject: [PATCH 2/8] tweak --- src/codegen/compile.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/codegen/compile.ml b/src/codegen/compile.ml index 4272fe6f10c..2106a1541fb 100644 --- a/src/codegen/compile.ml +++ b/src/codegen/compile.ml @@ -10590,8 +10590,7 @@ and compile_prim_invocation (env : E.t) ae p es at = let call_as_prim = match fun_sr, sort with | SR.Const (_, Const.Fun (mk_fi, Const.PrimWrapper prim)), _ -> begin match n_args, e2.it with - | 0, _ -> true - | 1, _ -> true + | (0 | 1), _ -> true | n, PrimE (TupPrim, es) when List.length es = n -> true | _, _ -> false end From 555223be9340900789f9a2b0d15a22a7a9aaa437 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Sun, 14 Jul 2024 19:09:24 +0200 Subject: [PATCH 3/8] generate less lambdas on the fly instead call into the new `@coerce_cont`. --- src/ir_passes/async.ml | 2 +- src/prelude/internals.mo | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ir_passes/async.ml b/src/ir_passes/async.ml index 5d4a000cabf..fc72051fe5d 100644 --- a/src/ir_passes/async.ml +++ b/src/ir_passes/async.ml @@ -84,7 +84,7 @@ let new_nary_async_reply ts = [k; r] -->* ( varE unary_async -*- (tupE [ - [v] -->* (varE k -*- varE v); + varE (var "@coerce_cont" (k --> ([v] -->* unitE()) |> typ)) -*- varE k; varE r ]) ) diff --git a/src/prelude/internals.mo b/src/prelude/internals.mo index 596a2fa2c2e..d4687de0c0d 100644 --- a/src/prelude/internals.mo +++ b/src/prelude/internals.mo @@ -307,6 +307,8 @@ func @getSystemRefund() : @Refund { return (prim "cyclesRefunded" : () -> Nat) (); }; +func @coerce_cont(k : () -> ()) : @Cont<()> = func() = k (); + func @new_async() : (@Async, @Cont, @Cont) { let w_null = func(r : @Refund, t : T) { }; let r_null = func(_ : Error) {}; From 8cc1342ff6eafdbce77a5fa452e69666bbfa62f6 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Sun, 14 Jul 2024 21:31:45 +0200 Subject: [PATCH 4/8] integrate also the invocation of the `unary_async` --- src/ir_passes/async.ml | 11 ++--------- src/prelude/internals.mo | 7 ++++++- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/src/ir_passes/async.ml b/src/ir_passes/async.ml index fc72051fe5d..8a24b133995 100644 --- a/src/ir_passes/async.ml +++ b/src/ir_passes/async.ml @@ -78,16 +78,9 @@ let new_nary_async_reply ts = (* construct the n-ary async value, coercing the continuation, if necessary *) let nary_async = let coerce u = - let v = fresh_var "v" u in let k = fresh_var "k" (contT u T.unit) in - let r = fresh_var "r" (err_contT T.unit) in - [k; r] -->* ( - varE unary_async -*- - (tupE [ - varE (var "@coerce_cont" (k --> ([v] -->* unitE()) |> typ)) -*- varE k; - varE r - ]) - ) + varE (var "@coerce_and_cont" (unary_async --> ([k; fail] -->* (varE unary_async -*- tupE [varE unary_fulfill; varE fail])) |> typ)) + -*- varE unary_async in match ts with | [t1] -> diff --git a/src/prelude/internals.mo b/src/prelude/internals.mo index d4687de0c0d..e6b9c300636 100644 --- a/src/prelude/internals.mo +++ b/src/prelude/internals.mo @@ -307,7 +307,12 @@ func @getSystemRefund() : @Refund { return (prim "cyclesRefunded" : () -> Nat) (); }; -func @coerce_cont(k : () -> ()) : @Cont<()> = func() = k (); +func @coerce_and_cont(a : @Async<()>) : + (k : () -> (), r : @Cont) -> { + #suspend; + #schedule : () -> () + } = + func(k, r) = a(func() = k(), r); func @new_async() : (@Async, @Cont, @Cont) { let w_null = func(r : @Refund, t : T) { }; From 662225c9cde8ba294bca88d99d0ddbe57269a053 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Mon, 15 Jul 2024 10:46:04 +0200 Subject: [PATCH 5/8] WIP: specialise only for {0, 2}-ary later I'll generate the rest --- src/ir_passes/async.ml | 44 +++++++++++++++++++++++++++------------- src/prelude/internals.mo | 15 +++++++++----- 2 files changed, 40 insertions(+), 19 deletions(-) diff --git a/src/ir_passes/async.ml b/src/ir_passes/async.ml index 8a24b133995..d30bf865560 100644 --- a/src/ir_passes/async.ml +++ b/src/ir_passes/async.ml @@ -71,30 +71,46 @@ let new_async t = let fail = fresh_var "fail" (typ (projE call_new_async 2)) in (async, fulfill, fail), call_new_async +let coerce_and_cont0T = + T.Func ( + T.Local, + T.Returns, + [], + [t_async_fut unary T.unit], + [t_async_fut nary T.unit]) + +let coerce_and_cont2T = + let t = T.(Tup [Var ("T", 0); Var ("U", 1)]) in + T.Func ( + T.Local, + T.Returns, + [ { var = "T"; sort = T.Type; bound = T.Any }; { var = "U"; sort = T.Type; bound = T.Any } ], + [t_async_fut unary t], + [t_async_fut nary t]) + let new_nary_async_reply ts = (* The async implementation isn't n-ary *) let t = T.seq ts in let (unary_async, unary_fulfill, fail), call_new_async = new_async t in (* construct the n-ary async value, coercing the continuation, if necessary *) let nary_async = - let coerce u = - let k = fresh_var "k" (contT u T.unit) in - varE (var "@coerce_and_cont" (unary_async --> ([k; fail] -->* (varE unary_async -*- tupE [varE unary_fulfill; varE fail])) |> typ)) - -*- varE unary_async - in match ts with | [t1] -> - begin - match T.normalize t1 with - | T.Tup _ -> - (* TODO(#3740): find a better fix than PR #3741 *) - (* HACK *) - coerce t1 - | _ -> + begin match T.normalize t1 with + | T.Tup [] -> + varE (var "@coerce_and_cont0" coerce_and_cont0T) -*- varE unary_async + | T.Tup [t; u] -> + callE (varE (var "@coerce_and_cont2" coerce_and_cont2T)) [t; u] (varE unary_async) + (* TODO(#3740): find a better fix than PR #3741 *) + (* HACK *) + | T.Tup _ -> failwith "GEN TUPLE" + | _ -> varE unary_async end - | ts1 -> - coerce t + | [] -> + varE (var "@coerce_and_cont0" coerce_and_cont0T) -*- varE unary_async + | [t; u] -> + callE (varE (var "@coerce_and_cont2" coerce_and_cont2T)) [t; u] (varE unary_async) in (* construct the n-ary reply callback that take a *sequence* of values to fulfill the async *) let nary_reply = diff --git a/src/prelude/internals.mo b/src/prelude/internals.mo index e6b9c300636..4c3231c3ea4 100644 --- a/src/prelude/internals.mo +++ b/src/prelude/internals.mo @@ -307,12 +307,17 @@ func @getSystemRefund() : @Refund { return (prim "cyclesRefunded" : () -> Nat) (); }; -func @coerce_and_cont(a : @Async<()>) : +func @coerce_and_cont2(a : @Async<(T, U)>) : + (k : (T, U) -> (), r : @Cont) -> { + #suspend; + #schedule : () -> () + } = func(k, r) = a(func tup = k tup, r); + +func @coerce_and_cont0(a : @Async<()>) : (k : () -> (), r : @Cont) -> { - #suspend; - #schedule : () -> () - } = - func(k, r) = a(func() = k(), r); + #suspend; + #schedule : () -> () + } = func(k, r) = a(func() = k(), r); func @new_async() : (@Async, @Cont, @Cont) { let w_null = func(r : @Refund, t : T) { }; From 7a61404ea2b6d449dfe43ff64c807a54d29661c6 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Mon, 15 Jul 2024 11:29:01 +0200 Subject: [PATCH 6/8] WIP: bring back `coerce` --- src/ir_passes/async.ml | 28 +++++++++++++++++++++------- test/run-drun/await.mo | 3 +++ test/run-drun/ok/await.drun-run.ok | 2 ++ test/run-drun/ok/await.run-ir.ok | 2 ++ test/run-drun/ok/await.run-low.ok | 2 ++ test/run-drun/ok/await.run.ok | 2 ++ test/run-drun/ok/await.tc.ok | 1 - 7 files changed, 32 insertions(+), 8 deletions(-) diff --git a/src/ir_passes/async.ml b/src/ir_passes/async.ml index d30bf865560..be82219b5f8 100644 --- a/src/ir_passes/async.ml +++ b/src/ir_passes/async.ml @@ -94,23 +94,37 @@ let new_nary_async_reply ts = let (unary_async, unary_fulfill, fail), call_new_async = new_async t in (* construct the n-ary async value, coercing the continuation, if necessary *) let nary_async = + let coerce u = + let v = fresh_var "v" u in + let k = fresh_var "k" (contT u T.unit) in + let r = fresh_var "r" (err_contT T.unit) in + [k; r] -->* ( + varE unary_async -*- + (tupE [ + [v] -->* (varE k -*- varE v); + varE r + ]) + ) + in match ts with | [t1] -> begin match T.normalize t1 with | T.Tup [] -> - varE (var "@coerce_and_cont0" coerce_and_cont0T) -*- varE unary_async - | T.Tup [t; u] -> - callE (varE (var "@coerce_and_cont2" coerce_and_cont2T)) [t; u] (varE unary_async) + varE (var "@coerce_and_cont00" coerce_and_cont0T) -*- varE unary_async + | T.Tup ([_; _] as tu) -> + callE (varE (var "@coerce_and_cont2" coerce_and_cont2T)) tu (varE unary_async) (* TODO(#3740): find a better fix than PR #3741 *) (* HACK *) - | T.Tup _ -> failwith "GEN TUPLE" - | _ -> + | T.Tup _ -> coerce t1 + | _ -> varE unary_async end | [] -> varE (var "@coerce_and_cont0" coerce_and_cont0T) -*- varE unary_async - | [t; u] -> - callE (varE (var "@coerce_and_cont2" coerce_and_cont2T)) [t; u] (varE unary_async) + | [_; _] -> + callE (varE (var "@coerce_and_cont2" coerce_and_cont2T)) ts (varE unary_async) + | _ -> + coerce t in (* construct the n-ary reply callback that take a *sequence* of values to fulfill the async *) let nary_reply = diff --git a/test/run-drun/await.mo b/test/run-drun/await.mo index b75980772d7..66a7da7a69a 100644 --- a/test/run-drun/await.mo +++ b/test/run-drun/await.mo @@ -66,6 +66,9 @@ actor a { Prim.debugPrint a; Prim.debugPrint b; }; + Prim.debugPrint (debug_show (await p())); + Prim.debugPrint (debug_show (await async (1, "two", '3'))); + await async (); ignore(await a); ignore(await b); diff --git a/test/run-drun/ok/await.drun-run.ok b/test/run-drun/ok/await.drun-run.ok index a2a53fe56d3..87f56f3528c 100644 --- a/test/run-drun/ok/await.drun-run.ok +++ b/test/run-drun/ok/await.drun-run.ok @@ -18,10 +18,12 @@ debug.print: cnt: 2 i: 2 debug.print: cnt: 3 i: 4 debug.print: cnt: 4 i: 5 debug.print: cnt: 5 i: 10 +debug.print: ("fst", "snd") debug.print: . debug.print: cnt: 6 i: 3 debug.print: cnt: 7 i: 6 debug.print: cnt: 8 i: 11 +debug.print: (1, "two", '3') debug.print: . debug.print: cnt: 9 i: 7 debug.print: cnt: 10 i: 12 diff --git a/test/run-drun/ok/await.run-ir.ok b/test/run-drun/ok/await.run-ir.ok index 6c5b990f341..70d3f2a6aa1 100644 --- a/test/run-drun/ok/await.run-ir.ok +++ b/test/run-drun/ok/await.run-ir.ok @@ -16,10 +16,12 @@ cnt: 2 i: 2 cnt: 3 i: 4 cnt: 4 i: 5 cnt: 5 i: 10 +("fst", "snd") . cnt: 6 i: 3 cnt: 7 i: 6 cnt: 8 i: 11 +(1, "two", '3') . cnt: 9 i: 7 cnt: 10 i: 12 diff --git a/test/run-drun/ok/await.run-low.ok b/test/run-drun/ok/await.run-low.ok index 6c5b990f341..70d3f2a6aa1 100644 --- a/test/run-drun/ok/await.run-low.ok +++ b/test/run-drun/ok/await.run-low.ok @@ -16,10 +16,12 @@ cnt: 2 i: 2 cnt: 3 i: 4 cnt: 4 i: 5 cnt: 5 i: 10 +("fst", "snd") . cnt: 6 i: 3 cnt: 7 i: 6 cnt: 8 i: 11 +(1, "two", '3') . cnt: 9 i: 7 cnt: 10 i: 12 diff --git a/test/run-drun/ok/await.run.ok b/test/run-drun/ok/await.run.ok index 6c5b990f341..70d3f2a6aa1 100644 --- a/test/run-drun/ok/await.run.ok +++ b/test/run-drun/ok/await.run.ok @@ -16,10 +16,12 @@ cnt: 2 i: 2 cnt: 3 i: 4 cnt: 4 i: 5 cnt: 5 i: 10 +("fst", "snd") . cnt: 6 i: 3 cnt: 7 i: 6 cnt: 8 i: 11 +(1, "two", '3') . cnt: 9 i: 7 cnt: 10 i: 12 diff --git a/test/run-drun/ok/await.tc.ok b/test/run-drun/ok/await.tc.ok index ae698746651..44cd32879da 100644 --- a/test/run-drun/ok/await.tc.ok +++ b/test/run-drun/ok/await.tc.ok @@ -1,3 +1,2 @@ await.mo:45.9-45.10: warning [M0194], unused identifier g (delete or rename to wildcard `_` or `_g`) -await.mo:63.10-63.11: warning [M0194], unused identifier p (delete or rename to wildcard `_` or `_p`) await.mo:64.9-64.10: warning [M0194], unused identifier h (delete or rename to wildcard `_` or `_h`) From 31359bb4850cc5ff3de9121d96355153629ba5be Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Mon, 15 Jul 2024 11:50:24 +0200 Subject: [PATCH 7/8] accept --- test/run-drun/ok/do-async-poly.tc.ok | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/test/run-drun/ok/do-async-poly.tc.ok b/test/run-drun/ok/do-async-poly.tc.ok index 6933d16c735..8c6052d687d 100644 --- a/test/run-drun/ok/do-async-poly.tc.ok +++ b/test/run-drun/ok/do-async-poly.tc.ok @@ -1,10 +1,10 @@ do-async-poly.mo:8.42-8.43: type error [M0033], async has non-shared content type - T__20 -do-async-poly.mo:13.42-13.43: type error [M0033], async has non-shared content type T__21 -do-async-poly.mo:18.44-18.45: type error [M0033], async has non-shared content type +do-async-poly.mo:13.42-13.43: type error [M0033], async has non-shared content type T__22 -do-async-poly.mo:22.42-22.43: type error [M0033], async has non-shared content type +do-async-poly.mo:18.44-18.45: type error [M0033], async has non-shared content type T__23 -do-async-poly.mo:26.43-26.44: type error [M0033], async has non-shared content type +do-async-poly.mo:22.42-22.43: type error [M0033], async has non-shared content type T__24 +do-async-poly.mo:26.43-26.44: type error [M0033], async has non-shared content type + T__25 From 2d6fe4a6bc05d56e51ec9637399d75bab8ce7b3f Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Mon, 15 Jul 2024 12:27:49 +0200 Subject: [PATCH 8/8] accept --- test/fail/ok/cyclic-bound5.tc.ok | 2 +- test/fail/ok/inference.tc.ok | 42 ++++++++++++++--------------- test/fail/ok/issue-2391.tc.ok | 4 +-- test/fail/ok/modexp2.tc.ok | 2 +- test/fail/ok/modexp5.tc.ok | 2 +- test/fail/ok/pretty-inference.tc.ok | 24 ++++++++--------- 6 files changed, 38 insertions(+), 38 deletions(-) diff --git a/test/fail/ok/cyclic-bound5.tc.ok b/test/fail/ok/cyclic-bound5.tc.ok index f762ed70591..c19db40be86 100644 --- a/test/fail/ok/cyclic-bound5.tc.ok +++ b/test/fail/ok/cyclic-bound5.tc.ok @@ -1 +1 @@ -cyclic-bound5.mo:7.8-7.17: type error [M0043], type parameter U__1 has cyclic bounds U__1 <: U__1 +cyclic-bound5.mo:7.8-7.17: type error [M0043], type parameter U__2 has cyclic bounds U__2 <: U__2 diff --git a/test/fail/ok/inference.tc.ok b/test/fail/ok/inference.tc.ok index 93545774329..d20304974f3 100644 --- a/test/fail/ok/inference.tc.ok +++ b/test/fail/ok/inference.tc.ok @@ -25,7 +25,7 @@ to argument of type to produce result of type Any because type parameter T has an open bound - U__12 + U__13 mentioning another type parameter, so that explicit type instantiation is required due to limitation of inference inference.mo:95.8-95.26: type error [M0098], cannot implicitly instantiate function of type (T, T) -> (U, U) @@ -34,7 +34,7 @@ to argument of type to produce result of type Any because type parameter T has an open bound - U__13 + U__14 mentioning another type parameter, so that explicit type instantiation is required due to limitation of inference inference.mo:96.8-96.23: type error [M0098], cannot implicitly instantiate function of type (T, T) -> (U, U) @@ -43,7 +43,7 @@ to argument of type to produce result of type Any because type parameter T has an open bound - U__14 + U__15 mentioning another type parameter, so that explicit type instantiation is required due to limitation of inference inference.mo:111.8-111.17: type error [M0098], cannot implicitly instantiate function of type T -> T @@ -73,34 +73,34 @@ to argument of type V -> V to produce result of type () -because no instantiation of T__102 makes - V -> V <: T__102 -> U +because no instantiation of T__103 makes + V -> V <: T__103 -> U inference.mo:118.1-118.31: type error [M0098], cannot implicitly instantiate function of type (U -> T) -> () to argument of type V -> V to produce result of type () -because no instantiation of T__103 makes - V -> V <: U -> T__103 +because no instantiation of T__104 makes + V -> V <: U -> T__104 inference.mo:127.8-127.20: type error [M0098], cannot implicitly instantiate function of type [T] -> T to argument of type [var Nat] to produce result of type Any -because no instantiation of T__106 makes - [var Nat] <: [T__106] +because no instantiation of T__107 makes + [var Nat] <: [T__107] inference.mo:130.1-130.13: type error [M0098], cannot implicitly instantiate function of type [var T] -> T to argument of type [Nat] to produce result of type () -because no instantiation of T__107 makes - [Nat] <: [var T__107] +because no instantiation of T__108 makes + [Nat] <: [var T__108] and - T__107 <: () + T__108 <: () inference.mo:132.1-132.17: type error [M0098], cannot implicitly instantiate function of type [var T] -> T to argument of type @@ -115,24 +115,24 @@ so that no valid instantiation exists inference.mo:137.4-137.8: type error [M0098], cannot implicitly instantiate function of type U -> () to argument of type - T__39 + T__40 to produce result of type () because implicit instantiation of type parameter U is over-constrained with - T__39 <: U <: {} + T__40 <: U <: {} where - T__39 U -> U + U -> U to argument of type - T__42 + T__43 to produce result of type None because implicit instantiation of type parameter U is over-constrained with - T__42 <: U <: None + T__43 <: U <: None where - T__42 (Bool, [var T], [var T]) -> [var T] @@ -151,7 +151,7 @@ to argument of type {type x = Nat} to produce result of type Any -because no instantiation of T__117 makes - {type x = Nat} <: {x : T__117} +because no instantiation of T__118 makes + {type x = Nat} <: {x : T__118} inference.mo:183.8-183.21: type error [M0045], wrong number of type arguments: expected 2 but got 0 inference.mo:186.8-186.15: type error [M0045], wrong number of type arguments: expected 1 but got 0 diff --git a/test/fail/ok/issue-2391.tc.ok b/test/fail/ok/issue-2391.tc.ok index 4c641fdaffd..44a87524224 100644 --- a/test/fail/ok/issue-2391.tc.ok +++ b/test/fail/ok/issue-2391.tc.ok @@ -1,3 +1,3 @@ -issue-2391.mo:3.3-3.35: type error [M0137], type C = {y : T__16} references type parameter T__16 from an outer scope -issue-2391.mo:10.3-10.47: type error [M0137], type C = {y : T__17} references type parameter T__17 from an outer scope +issue-2391.mo:3.3-3.35: type error [M0137], type C = {y : T__17} references type parameter T__17 from an outer scope +issue-2391.mo:10.3-10.47: type error [M0137], type C = {y : T__18} references type parameter T__18 from an outer scope issue-2391.mo:16.3-16.64: type error [M0137], type C = {y : (T1, T2)} references type parameters T2, T1 from an outer scope diff --git a/test/fail/ok/modexp2.tc.ok b/test/fail/ok/modexp2.tc.ok index ef377bf0e2d..1e50c4d781f 100644 --- a/test/fail/ok/modexp2.tc.ok +++ b/test/fail/ok/modexp2.tc.ok @@ -1,2 +1,2 @@ modexp2.mo:11.16-11.17: type error [M0030], type field U does not exist in type - module {type T = U; f : ???} + module {type T = U__1; f : ???} diff --git a/test/fail/ok/modexp5.tc.ok b/test/fail/ok/modexp5.tc.ok index d33dae930b1..40c9d3f8ac9 100644 --- a/test/fail/ok/modexp5.tc.ok +++ b/test/fail/ok/modexp5.tc.ok @@ -1 +1 @@ -modexp5.mo:6.20-6.30: type error [M0137], type U = T__18 references type parameter T__18 from an outer scope +modexp5.mo:6.20-6.30: type error [M0137], type U = T__19 references type parameter T__19 from an outer scope diff --git a/test/fail/ok/pretty-inference.tc.ok b/test/fail/ok/pretty-inference.tc.ok index e7dddc07fc2..e7f36b3fb9c 100644 --- a/test/fail/ok/pretty-inference.tc.ok +++ b/test/fail/ok/pretty-inference.tc.ok @@ -170,8 +170,8 @@ to argument of type (Nat, Nat) to produce result of type () -because no instantiation of T__42, U__12 makes - (Nat, Nat) <: (T__42, U__12) +because no instantiation of T__43, U__13 makes + (Nat, Nat) <: (T__43, U__13) and Nat <: () pretty-inference.mo:44.1-44.9: type error [M0098], cannot implicitly instantiate function of type @@ -180,8 +180,8 @@ to argument of type ((Nat, Bool), (Nat, Bool)) to produce result of type () -because no instantiation of T__43, U__13 makes - ((Nat, Bool), (Nat, Bool)) <: (T__43, U__13) +because no instantiation of T__44, U__14 makes + ((Nat, Bool), (Nat, Bool)) <: (T__44, U__14) and Nat <: () pretty-inference.mo:46.1-46.9: type error [M0098], cannot implicitly instantiate function of type @@ -190,9 +190,9 @@ to argument of type (((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool))) to produce result of type () -because no instantiation of T__44, U__14 makes +because no instantiation of T__45, U__15 makes (((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool))) <: - (T__44, U__14) + (T__45, U__15) and Nat <: () pretty-inference.mo:48.1-48.9: type error [M0098], cannot implicitly instantiate function of type @@ -202,10 +202,10 @@ to argument of type (((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool)))) to produce result of type () -because no instantiation of T__45, U__15 makes +because no instantiation of T__46, U__16 makes ((((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool))), (((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool)))) <: - (T__45, U__15) + (T__46, U__16) and Nat <: () pretty-inference.mo:50.1-50.9: type error [M0098], cannot implicitly instantiate function of type @@ -217,12 +217,12 @@ to argument of type (((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool))))) to produce result of type () -because no instantiation of T__46, U__16 makes +because no instantiation of T__47, U__17 makes (((((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool))), (((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool)))), ((((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool))), (((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool))))) <: - (T__46, U__16) + (T__47, U__17) and Nat <: () pretty-inference.mo:52.1-52.9: type error [M0098], cannot implicitly instantiate function of type @@ -238,7 +238,7 @@ to argument of type (((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool)))))) to produce result of type () -because no instantiation of T__47, U__17 makes +because no instantiation of T__48, U__18 makes ((((((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool))), (((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool)))), ((((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool))), @@ -247,6 +247,6 @@ because no instantiation of T__47, U__17 makes (((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool)))), ((((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool))), (((Nat, Bool), (Nat, Bool)), ((Nat, Bool), (Nat, Bool)))))) <: - (T__47, U__17) + (T__48, U__18) and Nat <: ()