From 63040e4380e15d09c8b93907bc76a28463699857 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Tue, 16 Jul 2024 20:17:44 +0200 Subject: [PATCH 1/8] WIP --- src/mo_frontend/typing.ml | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 7678e24ecc2..10b79bd12ae 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -631,12 +631,17 @@ and check_typ' env typ : T.typ = | TupT typs -> T.Tup (List.map (fun (_, t) -> check_typ env t) typs) | FuncT (sort, binds, typ1, typ2) -> - let cs, tbs, te, ce = check_typ_binds env binds in + let cs, tbs, te, ce = check_typ_binds env binds in let env' = infer_async_cap (adjoin_typs env te ce) sort.it cs tbs None typ.at in let typs1 = as_domT typ1 in let c, typs2 = as_codomT sort.it typ2 in let ts1 = List.map (check_typ env') typs1 in let ts2 = List.map (check_typ env') typs2 in + if (typ.at.left.file = "Xstdin") + then local_error env typ.at "M0000" + "typ1 type%a\ntyp1 type%a" + display_typ_expand (T.seq ts1) + display_typ_expand (T.seq ts2); check_shared_return env typ2.at sort.it c ts2; if not env.pre && Type.is_shared_sort sort.it then begin check_shared_binds env typ.at tbs; @@ -1884,6 +1889,12 @@ and check_exp' env0 t exp : T.typ = t | _ -> let t' = infer_exp env0 exp in + let t, t' = + if T.(is_func t && is_func t') + then + T.(let s, c, tbs, ts1, ts2 = as_func t in Func (s, c, tbs, [seq ts1], [seq ts2])), + T.(let s, c, tbs, ts1, ts2 = as_func t' in Func (s, c, tbs, [seq ts1], [seq ts2])) + else t, t' in if not (T.sub t' t) then local_error env0 exp.at "M0096" "expression of type%a\ncannot produce expected type%a" From d395d392235e3c46edffd630b86cdf334f3f67a5 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Tue, 16 Jul 2024 22:28:47 +0200 Subject: [PATCH 2/8] for functions, do the subtype check using the unary form but be sure to use the calling convention of the checker right now the supertype is returned, though! --- src/mo_frontend/typing.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 10b79bd12ae..08e32f97f3d 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -631,7 +631,7 @@ and check_typ' env typ : T.typ = | TupT typs -> T.Tup (List.map (fun (_, t) -> check_typ env t) typs) | FuncT (sort, binds, typ1, typ2) -> - let cs, tbs, te, ce = check_typ_binds env binds in + let cs, tbs, te, ce = check_typ_binds env binds in let env' = infer_async_cap (adjoin_typs env te ce) sort.it cs tbs None typ.at in let typs1 = as_domT typ1 in let c, typs2 = as_codomT sort.it typ2 in @@ -1889,18 +1889,19 @@ and check_exp' env0 t exp : T.typ = t | _ -> let t' = infer_exp env0 exp in - let t, t' = + let u, u', u'' = if T.(is_func t && is_func t') then T.(let s, c, tbs, ts1, ts2 = as_func t in Func (s, c, tbs, [seq ts1], [seq ts2])), - T.(let s, c, tbs, ts1, ts2 = as_func t' in Func (s, c, tbs, [seq ts1], [seq ts2])) - else t, t' in - if not (T.sub t' t) then + T.(let s, c, tbs, ts1, ts2 = as_func t' in Func (s, c, tbs, [seq ts1], [seq ts2])), + t + else t, t', t' in + if not (T.sub u' u) then local_error env0 exp.at "M0096" "expression of type%a\ncannot produce expected type%a" display_typ_expand t' display_typ_expand t; - t' + u'' and check_exp_field env (ef : exp_field) fts = let { mut; id; exp } = ef.it in From 88c19018bde188c053e4927dd92358b8c7cdf0e6 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Tue, 16 Jul 2024 23:04:29 +0200 Subject: [PATCH 3/8] WIP: attempt to transfer the supertype's arity onto the subtype --- src/mo_frontend/typing.ml | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 08e32f97f3d..943a913e965 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -1889,19 +1889,24 @@ and check_exp' env0 t exp : T.typ = t | _ -> let t' = infer_exp env0 exp in - let u, u', u'' = - if T.(is_func t && is_func t') - then - T.(let s, c, tbs, ts1, ts2 = as_func t in Func (s, c, tbs, [seq ts1], [seq ts2])), - T.(let s, c, tbs, ts1, ts2 = as_func t' in Func (s, c, tbs, [seq ts1], [seq ts2])), - t - else t, t', t' in + let u, u' = + let open T in + if is_func t && is_func t' then + let transfer_arity from toh = match from, List.map normalize toh with + | [_], _ -> [seq toh] + | _, [Tup ts] -> ts + | _, _ -> toh in + let s, c, tbs, ts1, ts2 = as_func t in + let dom, cod = transfer_arity ts1, transfer_arity ts2 in + Func (s, c, tbs, ts1, ts2), + let s, c, tbs, ts1, ts2 = as_func t' in Func (s, c, tbs, dom ts1, cod ts2) + else t, t' in if not (T.sub u' u) then local_error env0 exp.at "M0096" "expression of type%a\ncannot produce expected type%a" display_typ_expand t' display_typ_expand t; - u'' + u' and check_exp_field env (ef : exp_field) fts = let { mut; id; exp } = ef.it in From abe0cdc57ab2f0eded2513328edb718d718355e7 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Wed, 17 Jul 2024 12:05:07 +0200 Subject: [PATCH 4/8] when checking type bounds use the same calling convention transform --- src/mo_frontend/typing.ml | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 943a913e965..6a0960cac4c 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -828,8 +828,31 @@ and check_typ_bounds env (tbs : T.bind list) (ts : T.typ list) ats at = match tbs', ts', ats' with | tb::tbs', t::ts', at'::ats' -> if not env.pre then - let u = T.open_ ts tb.T.bound in - if not (T.sub t u) then + let open T in + let u = open_ ts tb.T.bound in + let t', u' = + + + + if is_func t && is_func u then + let transfer_arity from toh = match from, List.map normalize toh with + | [_], _ -> [seq toh] + | _, [Tup ts] -> ts + | _, _ -> toh in + let s, c, tbs, ts1, ts2 = as_func t in + let dom, cod = transfer_arity ts1, transfer_arity ts2 in + Func (s, c, tbs, ts1, ts2), + let s, c, tbs, ts1, ts2 = as_func u in Func (s, c, tbs, dom ts1, cod ts2) + else t, u in + + + + + + + + + if not (sub t' u') then local_error env at' "M0046" "type argument%a\ndoes not match parameter bound%a" display_typ_expand t From 7da5c6b7b4ea9e58675d77389230feacc5585c08 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Wed, 17 Jul 2024 12:10:08 +0200 Subject: [PATCH 5/8] cleanup and use the simpler way --- src/mo_frontend/typing.ml | 26 +++++--------------------- 1 file changed, 5 insertions(+), 21 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 6a0960cac4c..0ec7f4344c5 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -830,27 +830,11 @@ and check_typ_bounds env (tbs : T.bind list) (ts : T.typ list) ats at = if not env.pre then let open T in let u = open_ ts tb.T.bound in - let t', u' = - - - - if is_func t && is_func u then - let transfer_arity from toh = match from, List.map normalize toh with - | [_], _ -> [seq toh] - | _, [Tup ts] -> ts - | _, _ -> toh in - let s, c, tbs, ts1, ts2 = as_func t in - let dom, cod = transfer_arity ts1, transfer_arity ts2 in - Func (s, c, tbs, ts1, ts2), - let s, c, tbs, ts1, ts2 = as_func u in Func (s, c, tbs, dom ts1, cod ts2) - else t, u in - - - - - - - + let t', u' = if is_func t && is_func u + then + let s, c, tbs, ts1, ts2 = as_func t in Func (s, c, tbs, [seq ts1], [seq ts2]), + let s, c, tbs, ts1, ts2 = as_func u in Func (s, c, tbs, [seq ts1], [seq ts2]) + else t, u in if not (sub t' u') then local_error env at' "M0046" From 9c0fe790d693655ee82e7e1010539bf4fefb00b1 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Wed, 17 Jul 2024 12:24:05 +0200 Subject: [PATCH 6/8] testcase with stuff that works already --- test/run/param-arity.mo | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 test/run/param-arity.mo diff --git a/test/run/param-arity.mo b/test/run/param-arity.mo new file mode 100644 index 00000000000..26d666954c9 --- /dev/null +++ b/test/run/param-arity.mo @@ -0,0 +1,13 @@ +func foo ()>(k : K, v : T) = k v; + + +//foo<(Nat, Nat), (Nat, Nat)->()>(func(Int, Nat){}, (3,4)); +foo<(Nat, Nat), ((Nat, Nat))->()>(func(Int, Nat){}, (3,4)); +//foo<((Nat, Nat)), (Nat, Nat)->()>(func(Int, Nat){}, (3,4)); +foo<((Nat, Nat)), ((Nat, Nat))->()>(func(Int, Nat){}, (3,4)); + + +//foo<(Nat, Nat), (Nat, Nat)->()>(func((Int, Nat)){}, (3,4)); +foo<(Nat, Nat), ((Nat, Nat))->()>(func((Int, Nat)){}, (3,4)); +//foo<((Nat, Nat)), (Nat, Nat)->()>(func((Int, Nat)){}, (3,4)); +foo<((Nat, Nat)), ((Nat, Nat))->()>(func((Int, Nat)){}, (3,4)); From ad33b99ff480455f693c75d230a8ea2c99c3e9dc Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Wed, 17 Jul 2024 13:01:21 +0200 Subject: [PATCH 7/8] add TODOs --- test/run/param-arity.mo | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/test/run/param-arity.mo b/test/run/param-arity.mo index 26d666954c9..d2cc7cb8bb6 100644 --- a/test/run/param-arity.mo +++ b/test/run/param-arity.mo @@ -1,3 +1,17 @@ + + +((func (v : T) : () = ()) : T -> (())) ((3,4)); +((func (v : T) : (()) = ()) : T -> (())) ((3,4)); +((func (v : T) : (()) = ()) : T -> (())) ((3,4)); +((func (v : T) : (()) = ()) : T -> ()) ((3,4)); +((func (v : T) : (()) = ()) : T -> ()) (3,4); +// TODO: test all combinations + + +// TODO: debug_show the argument to demonstrate it is intactly passed + + + func foo ()>(k : K, v : T) = k v; From 3b853d234555e70f1d37383f2181f6304c2f39c7 Mon Sep 17 00:00:00 2001 From: Gabor Greif Date: Wed, 17 Jul 2024 13:10:23 +0200 Subject: [PATCH 8/8] reluctantly accepting these for now --- test/fail/ok/inference.tc.ok | 22 +++++++++--------- test/fail/ok/issue-3318.tc.ok | 37 +++++++++++-------------------- test/fail/ok/issue-3318.tc.ret.ok | 1 - 3 files changed, 24 insertions(+), 36 deletions(-) delete mode 100644 test/fail/ok/issue-3318.tc.ret.ok diff --git a/test/fail/ok/inference.tc.ok b/test/fail/ok/inference.tc.ok index 93545774329..17096522037 100644 --- a/test/fail/ok/inference.tc.ok +++ b/test/fail/ok/inference.tc.ok @@ -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__105 makes + V -> V <: T__105 -> 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__106 makes + V -> V <: U -> T__106 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__109 makes + [var Nat] <: [T__109] 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__110 makes + [Nat] <: [var T__110] and - T__107 <: () + T__110 <: () inference.mo:132.1-132.17: type error [M0098], cannot implicitly instantiate function of type [var T] -> T to argument of type @@ -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__120 makes + {type x = Nat} <: {x : T__120} 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-3318.tc.ok b/test/fail/ok/issue-3318.tc.ok index 3e7d42ba5e1..15bf33c0996 100644 --- a/test/fail/ok/issue-3318.tc.ok +++ b/test/fail/ok/issue-3318.tc.ok @@ -1,24 +1,13 @@ -issue-3318.mo:6.24-6.25: type error [M0096], expression of type - ((Nat, Nat)) -> (Int, Int) -cannot produce expected type - ((Nat, Nat)) -> ((Int, Int)) -issue-3318.mo:15.41-15.42: type error [M0096], expression of type - (Nat, Nat) -> (Nat, Nat) -cannot produce expected type - (Nat, Nat) -> ((Nat, Nat)) -issue-3318.mo:18.41-18.42: type error [M0096], expression of type - (Nat, Nat) -> (Nat, Nat) -cannot produce expected type - ((Nat, Nat)) -> (Nat, Nat) -issue-3318.mo:21.43-21.44: type error [M0096], expression of type - (Nat, Nat) -> (Nat, Nat) -cannot produce expected type - ((Nat, Nat)) -> ((Nat, Nat)) -issue-3318.mo:24.39-24.40: type error [M0096], expression of type - (Nat, Nat) -> ((Nat, Nat)) -cannot produce expected type - (Nat, Nat) -> (Nat, Nat) -issue-3318.mo:33.43-33.44: type error [M0096], expression of type - (Nat, Nat) -> ((Nat, Nat)) -cannot produce expected type - ((Nat, Nat)) -> ((Nat, Nat)) +issue-3318.mo:2.13-2.14: warning [M0194], unused identifier f (delete or rename to wildcard `_` or `_f`) +issue-3318.mo:11.6-11.8: warning [M0194], unused identifier t0 (delete or rename to wildcard `_` or `_t0`) +issue-3318.mo:14.6-14.8: warning [M0194], unused identifier t1 (delete or rename to wildcard `_` or `_t1`) +issue-3318.mo:17.6-17.8: warning [M0194], unused identifier t2 (delete or rename to wildcard `_` or `_t2`) +issue-3318.mo:20.6-20.8: warning [M0194], unused identifier t3 (delete or rename to wildcard `_` or `_t3`) +issue-3318.mo:23.6-23.8: warning [M0194], unused identifier t4 (delete or rename to wildcard `_` or `_t4`) +issue-3318.mo:26.6-26.8: warning [M0194], unused identifier t5 (delete or rename to wildcard `_` or `_t5`) +issue-3318.mo:29.6-29.8: warning [M0194], unused identifier t6 (delete or rename to wildcard `_` or `_t6`) +issue-3318.mo:32.6-32.8: warning [M0194], unused identifier t7 (delete or rename to wildcard `_` or `_t7`) +issue-3318.mo:35.6-35.8: warning [M0194], unused identifier t8 (delete or rename to wildcard `_` or `_t8`) +issue-3318.mo:40.6-40.8: warning [M0194], unused identifier u0 (delete or rename to wildcard `_` or `_u0`) +issue-3318.mo:42.6-42.8: warning [M0194], unused identifier u1 (delete or rename to wildcard `_` or `_u1`) +issue-3318.mo:44.6-44.8: warning [M0194], unused identifier u2 (delete or rename to wildcard `_` or `_u2`) diff --git a/test/fail/ok/issue-3318.tc.ret.ok b/test/fail/ok/issue-3318.tc.ret.ok deleted file mode 100644 index 69becfa16f9..00000000000 --- a/test/fail/ok/issue-3318.tc.ret.ok +++ /dev/null @@ -1 +0,0 @@ -Return code 1