Gabor/arity

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

test/fail/ok/inference.tc.ok

@@ -73,34 +73,34 @@ to argument of type
   <V>V -> V
 to produce result of type
   ()
-because no instantiation of T__102 makes
-  <V>V -> V  <:  <U>T__102 -> U
+because no instantiation of T__105 makes
+  <V>V -> V  <:  <U>T__105 -> U
 inference.mo:118.1-118.31: type error [M0098], cannot implicitly instantiate function of type
   <T>(<U>U -> T) -> ()
 to argument of type
   <V>V -> V
 to produce result of type
   ()
-because no instantiation of T__103 makes
-  <V>V -> V  <:  <U>U -> T__103
+because no instantiation of T__106 makes
+  <V>V -> V  <:  <U>U -> T__106
 inference.mo:127.8-127.20: type error [M0098], cannot implicitly instantiate function of type
   <T>[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
   <T>[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
   <T>[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

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`)

test/run/param-arity.mo

@@ -0,0 +1,27 @@
+
+
+((func <T>(v : T) : () = ()) : <T>T -> (())) ((3,4));
+((func <T>(v : T) : (()) = ()) : <T>T -> (())) ((3,4));
+((func <T>(v : T) : (()) = ()) : <T>T -> (())) ((3,4));
+((func <T>(v : T) : (()) = ()) : <T>T -> ()) ((3,4));
+((func <T>(v : T) : (()) = ()) : <T>T -> ()) (3,4);
+// TODO: test all combinations
+
+
+// TODO: debug_show the argument to demonstrate it is intactly passed
+
+
+
+func foo<T, K <: T -> ()>(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));