From 6fb2f89f3c25b9d6a3df5bbc52a275caf57571d8 Mon Sep 17 00:00:00 2001
From: Claudio Russo <claudio@dfinity.org>
Date: Sun, 28 Sep 2025 22:07:01 +0100
Subject: [PATCH] used nested named type to disambiguate, wild card for
 positional (anonymous) matches

---
 doc/md/examples/grammar.txt |  5 ++++-
 src/mo_frontend/parser.mly  |  4 ++++
 src/mo_frontend/typing.ml   | 22 +++++++++++++++-------
 test/fail/implicit.mo       | 14 ++++++++++++++
 4 files changed, 37 insertions(+), 8 deletions(-)

diff --git a/doc/md/examples/grammar.txt b/doc/md/examples/grammar.txt
index b5959ca27ca..69d3bb6c930 100644
--- a/doc/md/examples/grammar.txt
+++ b/doc/md/examples/grammar.txt
@@ -10,6 +10,9 @@
 <implicit> ::= 
     'implicit'
 
+<id_wild> ::= 
+    '_'
+
 <typ_obj_sort> ::= 
     'object'
     'actor'
@@ -70,8 +73,8 @@
     <typ> 'or' <typ>
 
 <typ_item> ::= 
-    <implicit> <typ>
     <id> ':' <typ>
+    <id_wild> ':' <typ>
     <typ>
 
 <typ_args> ::= 
diff --git a/src/mo_frontend/parser.mly b/src/mo_frontend/parser.mly
index ceeb2e8dfb1..8a96a63643a 100644
--- a/src/mo_frontend/parser.mly
+++ b/src/mo_frontend/parser.mly
@@ -368,6 +368,9 @@ seplist1(X, SEP) :
 %inline implicit :
   | IMPLICIT { "implicit" @@ at $sloc }
 
+%inline id_wild :
+  | UNDERSCORE { "_" @@ at $sloc }
+
 %inline typ_id :
   | id=ID { id @= at $sloc }
 
@@ -486,6 +489,7 @@ typ :
 
 typ_item :
   | i=id COLON t=typ { Some i, t }
+  | i=id_wild COLON t=typ { Some i, t }
   | t=typ { None, t }
 
 typ_args :
diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml
index 4c75b1f190c..0d80e9da707 100644
--- a/src/mo_frontend/typing.ml
+++ b/src/mo_frontend/typing.ml
@@ -2454,16 +2454,24 @@ and infer_callee env exp =
      infer_exp_promote env exp, None
 
 and insert_holes at ts es =
+  let mk_hole pos hole_id =
+    let hole_sort = if hole_id = "" then Anon pos else Named hole_id in
+    {it = HoleE (hole_sort, ref {it = PrimE "hole"; at; note=empty_typ_note });
+      at;
+      note = empty_typ_note }
+  in
   let rec go n ts es =
     match (ts, es) with
+    | (T.Named ("implicit", T.Named (arg_name, t))) :: ts1, es ->
+      (mk_hole n arg_name) :: go (n + 1) ts1 es
     | (T.Named ("implicit", t)) :: ts1, es ->
-       {it = HoleE (Anon n, ref {it = PrimE "hole"; at; note=empty_typ_note });
-        at;
-        note = empty_typ_note } :: go (n+1) ts1 es
-    | (T.Named (arg_name, (T.Named ("implicit", t)))) :: ts1, es ->
-       {it = HoleE (Named arg_name, ref {it = PrimE "hole"; at; note=empty_typ_note });
-        at;
-        note = empty_typ_note } :: go (n+1) ts1 es
+      (mk_hole n "_") :: go (n + 1) ts1 es
+    | (T.Named (_inf_arg_name, (T.Named ("implicit", T.Named (arg_name, t))))) :: ts1, es ->
+      (* override inferred arg_name *)
+      (mk_hole n arg_name) :: go (n + 1) ts1 es
+    | (T.Named (inf_arg_name, (T.Named ("implicit", t)))) :: ts1, es ->
+      (* non-overriden, use inferred arg_name *)
+      (mk_hole n inf_arg_name) :: go (n + 1) ts1 es
     | (t :: ts1, e::es1) -> e :: go (n+1) ts1 es1
     | _, [] ->  []
     | [], es -> es
diff --git a/test/fail/implicit.mo b/test/fail/implicit.mo
index a38b3ed4d21..388c70f9505 100644
--- a/test/fail/implicit.mo
+++ b/test/fail/implicit.mo
@@ -86,3 +86,17 @@ func mkZero<T>(zero : implicit T) : T {
 };
 
 ignore mkZero<{ x : Nat }>();
+
+// tricky case: if we have two implicit arguments of the same name we currently need to add a second type annotation
+func c <T, U>(p1 : (T, U), p2 : (T, U),
+   cT : implicit (c : (T, T) -> Order),
+   cU : implicit (c : (U, U) -> Order))
+   : Order {
+   switch (cT(p1.0, p2.0)) {
+     case (#equal) { cU(p1.1, p2.1) };
+     case ord { ord };
+   };
+};
+
+ignore c((1,"a"),(0,"b")); // accepted
+