diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 7678e24ecc2..0ec7f4344c5 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -637,6 +637,11 @@ and check_typ' env typ : T.typ = 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; @@ -823,8 +828,15 @@ 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 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" "type argument%a\ndoes not match parameter bound%a" display_typ_expand t @@ -1884,12 +1896,24 @@ and check_exp' env0 t exp : T.typ = t | _ -> let t' = infer_exp env0 exp in - if not (T.sub t' t) then + 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; - t' + u' and check_exp_field env (ef : exp_field) fts = let { mut; id; exp } = ef.it in 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 diff --git a/test/run/param-arity.mo b/test/run/param-arity.mo new file mode 100644 index 00000000000..d2cc7cb8bb6 --- /dev/null +++ b/test/run/param-arity.mo @@ -0,0 +1,27 @@ + + +((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; + + +//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));