diff --git a/Changelog.md b/Changelog.md
index d5de30d837b..196fd82609e 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -3,7 +3,10 @@
 ## Unreleased
 
 * motoko (`moc`)
-  * Experimental support for Mixins (#5459)
+
+  * Experimental support for `implicit` argument declarations (#5517).
+
+  * Experimental support for Mixins (#5459).
 
 ## 0.16.3 (2025-09-29)
 
diff --git a/doc/md/examples/grammar.txt b/doc/md/examples/grammar.txt
index 71c2a95703a..57cdd40b5fb 100644
--- a/doc/md/examples/grammar.txt
+++ b/doc/md/examples/grammar.txt
@@ -7,6 +7,9 @@
     X
     X SEP <list(X, SEP)>
 
+<id_wild> ::= 
+    '_'
+
 <typ_obj_sort> ::= 
     'object'
     'actor'
@@ -67,6 +70,7 @@
 
 <typ_item> ::= 
     <id> ':' <typ>
+    <id_wild> ':' <typ>
     <typ>
 
 <typ_args> ::= 
@@ -177,19 +181,26 @@
     <id>
     '_'
 
+<exp_arg> ::= 
+    <ob>
+    <lit>
+    '(' <list(<exp>, ',')> ')'
+    <id>
+    '_'
+
 <exp_post> ::= 
     <exp_nullary>
     '[' 'var'? <list(<exp_nonvar>, ',')> ']'
     <exp_post> '[' <exp> ']'
     <exp_post> '.'<nat>
     <exp_post> '.' <id>
-    <exp_post> <inst> <exp_nullary>
+    <exp_post> <inst> <exp_arg>
     <exp_post> '!'
     '(' 'system' <exp_post> '.' <id> ')'
 
 <exp_un> ::= 
     <exp_post>
-    <parenthetical> <exp_post> <inst> <exp_nullary>
+    <parenthetical> <exp_post> <inst> <exp_arg>
     '#' <id>
     '#' <id> <exp_nullary>
     '?' <exp_un>
diff --git a/src/lang_utils/error_codes.ml b/src/lang_utils/error_codes.ml
index 7598a9098b8..794a37e78ec 100644
--- a/src/lang_utils/error_codes.ml
+++ b/src/lang_utils/error_codes.ml
@@ -201,6 +201,9 @@ let error_codes : (string * string option) list =
     "M0227", None; (* Non-actor include *)
     "M0228", None; (* Only top-level mixins *)
     "M0229", None; (* Non-var pattern for mixin import *)
+    "M0230", None; (* Cannot determine implicit argument *)
+    "M0231", None; (* Ambiguous implicit argument *)
+    "M0232", None; (* Cannot infer type of implicit argument *)
   ]
 
 (** Message codes that can be both used as warnings and errors *)
diff --git a/src/lowering/desugar.ml b/src/lowering/desugar.ml
index 74e155a9a23..78087c26b26 100644
--- a/src/lowering/desugar.ml
+++ b/src/lowering/desugar.ml
@@ -44,6 +44,7 @@ let typed_phrase' f x =
   let n' = typ_note x.note in
   { x with it = f x.at n' x.it; note = n' }
 
+let is_empty_tup e = e.it = S.TupE []
 
 let rec exps es = List.map exp es
 
@@ -54,6 +55,7 @@ and exp e =
     | _ -> typed_phrase' exp' e
 
 and exp' at note = function
+  | S.HoleE (_, e) -> (exp !e).it
   | S.VarE i -> I.VarE ((match i.note with Var -> I.Var | Const -> I.Const), i.it)
   | S.ActorUrlE e ->
     I.(PrimE (ActorOfIdBlob note.Note.typ, [url e at]))
@@ -125,110 +127,118 @@ and exp' at note = function
     let tys = List.map (T.open_ vars) res_tys in
     I.FuncE (name, s, control, tbs', args, tys, wrap (exp e))
   (* Primitive functions in the prelude have particular shapes *)
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE p;_}, _);note;_}, _, e)
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE p;_}, _);note;_}, _, (_, e))
     when Lib.String.chop_prefix "num_conv" p <> None ->
     begin match String.split_on_char '_' p with
     | ["num"; "conv"; s1; s2] ->
       let p1 = Type.prim s1 in
       let p2 = Type.prim s2 in
-      I.PrimE (I.NumConvTrapPrim (p1, p2), [exp e])
+      I.PrimE (I.NumConvTrapPrim (p1, p2), [exp !e])
     | _ -> assert false
     end
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE p;_}, _);note;_}, _, e)
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE p;_}, _);note;_}, _, (_, e))
     when Lib.String.chop_prefix "num_wrap" p <> None ->
     begin match String.split_on_char '_' p with
     | ["num"; "wrap"; s1; s2] ->
       let p1 = Type.prim s1 in
       let p2 = Type.prim s2 in
-      I.PrimE (I.NumConvWrapPrim (p1, p2), [exp e])
+      I.PrimE (I.NumConvWrapPrim (p1, p2), [exp !e])
     | _ -> assert false
     end
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "decodeUtf8";_},_);_}, _, e) ->
-    I.PrimE (I.DecodeUtf8, [exp e])
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "encodeUtf8";_},_);_}, _, e) ->
-    I.PrimE (I.EncodeUtf8, [exp e])
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cast";_}, _);note;_}, _, e) ->
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "decodeUtf8";_},_);_}, _, (_, e)) ->
+    I.PrimE (I.DecodeUtf8, [exp !e])
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "encodeUtf8";_},_);_}, _, (_, e)) ->
+    I.PrimE (I.EncodeUtf8, [exp !e])
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cast";_}, _);note;_}, _, (_, e)) ->
     begin match note.S.note_typ with
     | T.Func (T.Local, T.Returns, [], ts1, ts2) ->
-      I.PrimE (I.CastPrim (T.seq ts1, T.seq ts2), [exp e])
+      I.PrimE (I.CastPrim (T.seq ts1, T.seq ts2), [exp !e])
     | _ -> assert false
     end
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "serialize";_}, _);note;_}, _, e) ->
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "serialize";_}, _);note;_}, _, (_, e)) ->
     begin match note.S.note_typ with
     | T.Func (T.Local, T.Returns, [], ts1, ts2) ->
-      I.PrimE (I.SerializePrim ts1, [exp e])
+      I.PrimE (I.SerializePrim ts1, [exp !e])
     | _ -> assert false
     end
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "deserialize";_}, _);note;_}, _, e) ->
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "deserialize";_}, _);note;_}, _, (_, e)) ->
     begin match note.S.note_typ with
     | T.Func (T.Local, T.Returns, [], ts1, ts2) ->
-      I.PrimE (I.DeserializePrim ts2, [exp e])
+      I.PrimE (I.DeserializePrim ts2, [exp (!e)])
     | _ -> assert false
     end
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "caller";_},_);_}, _, {it=S.TupE es;_}) ->
-    assert (es = []);
-    I.PrimE (I.ICCallerPrim, [])
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "deadline";_},_);_}, _, {it=S.TupE es;_}) ->
-    assert (es = []);
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "caller";_},_);_}, _, (_, e)) ->
+    (match !e with
+     | {it=S.TupE [];_} ->
+        I.PrimE (I.ICCallerPrim, [])
+     | _ -> assert false)
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "deadline";_},_);_}, _, (_, e)) ->
+    assert ((!e).it = S.TupE []);
     I.PrimE (I.ICReplyDeadlinePrim, [])
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "time";_},_);_}, _, {it=S.TupE es;_}) ->
-    assert (es = []);
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "time";_},_);_}, _, (_, e)) ->
+    assert ((!e).it = S.TupE []);
     I.PrimE (I.SystemTimePrim, [])
   (* Cycles *)
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesBalance";_},_);_}, _, {it=S.TupE es;_}) ->
-    assert (es = []);
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesBalance";_},_);_}, _, (_, e)) ->
+    assert (is_empty_tup !e);
     I.PrimE (I.SystemCyclesBalancePrim, [])
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesAvailable";_},_);_}, _, {it=S.TupE es;_}) ->
-    assert (es = []);
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesAvailable";_},_);_}, _, (_, e)) ->
+    assert (is_empty_tup !e);
     I.PrimE (I.SystemCyclesAvailablePrim, [])
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesRefunded";_},_);_}, _, {it=S.TupE es;_}) ->
-    assert (es = []);
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesRefunded";_},_);_}, _, (_, e)) ->
+    assert (is_empty_tup !e);
     I.PrimE (I.SystemCyclesRefundedPrim, [])
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesAccept";_},_);_}, _, e) ->
-    I.PrimE (I.SystemCyclesAcceptPrim, [exp e])
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesAdd";_},_);_}, _, e) ->
-    I.PrimE (I.SystemCyclesAddPrim, [exp e])
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesBurn";_},_);_}, _, e) ->
-    I.PrimE (I.SystemCyclesBurnPrim, [exp e])
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "timeoutSet";_},_);_}, _, e) ->
-    I.PrimE (I.SystemTimeoutSetPrim, [exp e])
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesAccept";_},_);_}, _, (_, e)) ->
+    I.PrimE (I.SystemCyclesAcceptPrim, [exp !e])
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesAdd";_},_);_}, _, (_, e)) ->
+    I.PrimE (I.SystemCyclesAddPrim, [exp !e])
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesBurn";_},_);_}, _, (_, e)) ->
+    I.PrimE (I.SystemCyclesBurnPrim, [exp !e])
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "timeoutSet";_},_);_}, _, (_, e)) ->
+    I.PrimE (I.SystemTimeoutSetPrim, [exp !e])
   (* Certified data *)
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "setCertifiedData";_},_);_}, _, e) ->
-    I.PrimE (I.SetCertifiedData, [exp e])
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "getCertificate";_},_);_}, _, {it=S.TupE es;_}) ->
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "setCertifiedData";_},_);_}, _, (_, e)) ->
+    I.PrimE (I.SetCertifiedData, [exp !e])
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "getCertificate";_},_);_}, _, (_, e)) ->
+    assert (is_empty_tup !e);
     I.PrimE (I.GetCertificate, [])
   (* Other *)
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE p;_},_);_}, _, {it=S.TupE es;_}) ->
-    I.PrimE (I.OtherPrim p, exps es)
-  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE p;_},_);_}, _, e) ->
-    I.PrimE (I.OtherPrim p, [exp e])
+  | S.CallE (None, {it=S.AnnotE ({it=S.PrimE p;_},_);_}, _, (_, e)) ->
+   (match (!e).it with
+    | S.TupE es ->
+      I.PrimE (I.OtherPrim p, exps es)
+    | _ ->
+      I.PrimE (I.OtherPrim p, [exp !e]))
   (* Optimizing array.size() *)
-  | S.CallE (None, {it=S.DotE (e1, proj, _); _}, _, {it=S.TupE [];_})
-      when T.is_array e1.note.S.note_typ && proj.it = "size" ->
+  | S.CallE (None, {it=S.DotE (e1, proj, _); _}, _, (_, e))
+     when is_empty_tup !e &&
+          T.is_array e1.note.S.note_typ && proj.it = "size" ->
     I.PrimE (I.OtherPrim "array_len", [exp e1])
-  | S.CallE (None, {it=S.DotE (e1, proj, _); _}, _, {it=S.TupE [];_})
-      when T.(is_prim Text) e1.note.S.note_typ && proj.it = "size" ->
+  | S.CallE (None, {it=S.DotE (e1, proj, _); _}, _, (_, e))
+      when is_empty_tup !e &&
+           T.(is_prim Text) e1.note.S.note_typ && proj.it = "size" ->
     I.PrimE (I.OtherPrim "text_len", [exp e1])
-  | S.CallE (None, {it=S.DotE (e1, proj, _); _}, _, {it=S.TupE [];_})
-      when T.(is_prim Blob) e1.note.S.note_typ && proj.it = "size" ->
+  | S.CallE (None, {it=S.DotE (e1, proj,_); _}, _, (_, e))
+      when is_empty_tup !e &&
+           T.(is_prim Blob) e1.note.S.note_typ && proj.it = "size" ->
     I.PrimE (I.OtherPrim "blob_size", [exp e1])
   (* Contextual dot call *)
-  | S.CallE (None, {it=S.DotE(e1, id, n);_}, inst, e2) when Option.is_some !n ->
+  | S.CallE (None, {it=S.DotE(e1, id, n);_}, inst, (_, e2)) when Option.is_some !n ->
      let func_exp = Option.get !n in
-     let args = S.contextual_dot_args e1 e2 func_exp in
+     let args = S.contextual_dot_args e1 !e2 func_exp in
      I.(PrimE (CallPrim inst.note, [exp func_exp; exp args]))
   (* Normal call *)
-  | S.CallE (None, e1, inst, e2) ->
-    I.(PrimE (CallPrim inst.note, [exp e1; exp e2]))
+  | S.CallE (None, e1, inst, (_, e2)) ->
+    I.(PrimE (CallPrim inst.note, [exp e1; exp !e2]))
   (* Call with parenthetical *)
-  | S.CallE (Some _ as par_opt, e1, inst, e2) ->
+  | S.CallE (Some _ as par_opt, e1, inst, (_, e2)) ->
     let send e1_typ = T.(is_func e1_typ &&
                            (let s, _, _, _, _ = as_func e1_typ in
                             is_shared_sort s || is_fut note.Note.typ)) in
     let ds, rs = parenthetical (send e1.note.S.note_typ) par_opt in
-    let v1, v2 = fresh_var "e1" e1.note.S.note_typ, fresh_var "e2" e2.note.S.note_typ in
+    let v1, v2 = fresh_var "e1" e1.note.S.note_typ, fresh_var "e2" (!e2).note.S.note_typ in
     (blockE
-       (ds @ letD v1 (exp e1) :: letD v2 (exp e2) :: rs)
+       (ds @ letD v1 (exp e1) :: letD v2 (exp !e2) :: rs)
        I.{ at; note; it = PrimE (CallPrim inst.note, [varE v1; varE v2]) }).it
   | S.BlockE [] -> (unitE ()).it
   | S.BlockE [{it = S.ExpD e; _}] -> (exp e).it
@@ -251,9 +261,9 @@ and exp' at note = function
   | S.WhileE (e1, e2) -> (whileE (exp e1) (exp e2)).it
   | S.LoopE (e1, None) -> I.LoopE (exp e1)
   | S.LoopE (e1, Some e2) -> (loopWhileE (exp e1) (exp e2)).it
-  | S.ForE (p, {it=S.CallE (None, {it=S.DotE (arr, proj, _); _}, _, e1); _}, e2)
+  | S.ForE (p, {it=S.CallE (None, {it=S.DotE (arr, proj, _); _}, _, (_, e1)); _}, e2)
       when T.is_array arr.note.S.note_typ && (proj.it = "vals" || proj.it = "values" || proj.it = "keys")
-    -> (transform_for_to_while p arr proj e1 e2).it
+    -> (transform_for_to_while p arr proj (!e1) e2).it
   | S.ForE (p, e1, e2) -> (forE (pat p) (exp e1) (exp e2)).it
   | S.DebugE e -> if !Mo_config.Flags.release_mode then (unitE ()).it else (exp e).it
   | S.LabelE (l, t, e) -> I.LabelE (l.it, t.Source.note, exp e)
diff --git a/src/mo_def/arrange.ml b/src/mo_def/arrange.ml
index 8399e7d8610..6a1c75bf92d 100644
--- a/src/mo_def/arrange.ml
+++ b/src/mo_def/arrange.ml
@@ -98,6 +98,7 @@ module Make (Cfg : Config) = struct
      currently. As a compromise, we annotate only the nodes that currently
      matter for the language server, i.e. the left expression of a [DotE] node. *)
   let rec exp ?(arrange_typ = false) e = source e.at (annot ~arrange_typ e.note (match e.it with
+    | HoleE (_, e) -> "HoleE" $$ [exp !e]
     | VarE x              -> "VarE"      $$ [id x]
     | LitE l              -> "LitE"      $$ [lit !l]
     | ActorUrlE e         -> "ActorUrlE" $$ [exp e]
@@ -135,7 +136,7 @@ module Make (Cfg : Config) = struct
         Atom (if sugar then "" else "=");
         exp e'
       ]
-    | CallE (par_opt, e1, ts, e2) -> "CallE" $$ parenthetical par_opt ([exp e1] @ inst ts @ [exp e2])
+    | CallE (par_opt, e1, ts, (_, e2)) -> "CallE" $$ parenthetical par_opt ([exp e1] @ inst ts @ [exp !e2])
     | BlockE ds           -> "BlockE"  $$ List.map dec ds
     | NotE e              -> "NotE"    $$ [exp e]
     | AndE (e1, e2)       -> "AndE"    $$ [exp e1; exp e2]
diff --git a/src/mo_def/syntax.ml b/src/mo_def/syntax.ml
index fc540a18bf1..1f22d8490ed 100644
--- a/src/mo_def/syntax.ml
+++ b/src/mo_def/syntax.ml
@@ -164,7 +164,9 @@ type sugar = bool (* Is the source of a function body a block `<block>`,
                      public functions as oneway, shared functions *)
 
 type exp = (exp', typ_note) Source.annotated_phrase
+and hole_sort = Named of string | Anon of int
 and exp' =
+  | HoleE of hole_sort * exp ref
   | PrimE of string                            (* primitive *)
   | VarE of id_ref                             (* variable *)
   | LitE of lit ref                            (* literal *)
@@ -188,7 +190,7 @@ and exp' =
   | ArrayE of mut * exp list                   (* array *)
   | IdxE of exp * exp                          (* array indexing *)
   | FuncE of string * sort_pat * typ_bind list * pat * typ option * sugar * exp  (* function *)
-  | CallE of exp option * exp * inst * exp     (* function call *)
+  | CallE of exp option * exp * inst * arg_exp     (* function call *)
   | BlockE of dec list                         (* block (with type after avoidance) *)
   | NotE of exp                                (* negation *)
   | AndE of exp * exp                          (* conjunction *)
@@ -214,7 +216,8 @@ and exp' =
   | IgnoreE of exp                             (* ignore *)
 (*
   | AtomE of string                            (* atom *)
-*)
+ *)
+and arg_exp = (bool * (exp ref))
 
 and assert_kind =
   | Runtime | Static | Invariant | Precondition | Postcondition | Concurrency of string | Loop_entry | Loop_continue | Loop_exit | Loop_invariant
diff --git a/src/mo_frontend/definedness.ml b/src/mo_frontend/definedness.ml
index e57f4d3e2a1..66c6eaf0282 100644
--- a/src/mo_frontend/definedness.ml
+++ b/src/mo_frontend/definedness.ml
@@ -80,9 +80,10 @@ let delayed_vars : f -> S.t =
 
 let rec exp msgs e : f = match e.it with
   (* Eager uses are either first-class uses of a variable: *)
+  | HoleE (s, e) -> exp msgs (!e)
   | VarE i              -> M.singleton i.it Eager
   (* Or anything that is occurring in a call (as this may call a closure): *)
-  | CallE (par_opt, e1, _ts, e2) -> eagerify (Option.to_list par_opt @ [e1; e2] |> exps msgs)
+  | CallE (par_opt, e1, _ts, (_, e2)) -> eagerify (Option.to_list par_opt @ [e1; !e2] |> exps msgs)
   (* And break, return, throw can be thought of as calling a continuation: *)
   | BreakE (_, e)
   | RetE e
diff --git a/src/mo_frontend/effect.ml b/src/mo_frontend/effect.ml
index 0eb0e9f0f54..f0aff39f8b6 100644
--- a/src/mo_frontend/effect.ml
+++ b/src/mo_frontend/effect.ml
@@ -49,10 +49,11 @@ let effect_exp (exp:Syntax.exp) : T.eff = eff exp
 (* infer the effect of an expression, assuming all sub-expressions are correctly effect-annotated es *)
 let rec infer_effect_exp (exp:Syntax.exp) : T.eff =
   match exp.it with
+  | HoleE _ -> T.Triv (* TBR *)
   | CallE (_, exp1, inst, exp2) when is_async_call exp1 inst exp2 ->
     T.Await
-  | CallE (Some par, exp1, _, exp2) ->
-    map_max_effs effect_exp [par; exp1; exp2]
+  | CallE (Some par, exp1, _, (_, exp2)) ->
+    map_max_effs effect_exp [par; exp1; !exp2]
   | PrimE _
   | VarE _
   | LitE _
@@ -83,7 +84,6 @@ let rec infer_effect_exp (exp:Syntax.exp) : T.eff =
   | IdxE (exp1, exp2)
   | RelE (_, exp1, _, exp2)
   | AssignE (exp1, exp2)
-  | CallE (None, exp1, _, exp2)
   | AndE (exp1, exp2)
   | OrE (exp1, exp2)
   | ImpliesE (exp1, exp2)
@@ -91,6 +91,8 @@ let rec infer_effect_exp (exp:Syntax.exp) : T.eff =
   | LoopE (exp1, Some exp2)
   | ForE (_, exp1, exp2) ->
     map_max_effs effect_exp [exp1; exp2]
+  | CallE (None, exp1, _, (_, exp2)) ->
+    map_max_effs effect_exp [exp1; !exp2]
   | DebugE exp1 ->
     effect_exp exp1
   | ToCandidE exps
diff --git a/src/mo_frontend/parser.mly b/src/mo_frontend/parser.mly
index 9e526691413..b100cb2a9c7 100644
--- a/src/mo_frontend/parser.mly
+++ b/src/mo_frontend/parser.mly
@@ -276,6 +276,7 @@ and objblock eo s id ty dec_fields =
 %left POWOP WRAPPOWOP
 
 %type<Mo_def.Syntax.exp> exp(ob) exp_nullary(ob) exp_plain exp_obj exp_nest
+%type<Mo_def.Syntax.exp * bool> exp_arg
 %type<Mo_def.Syntax.typ_item> typ_item
 %type<Mo_def.Syntax.typ> typ_un typ_nullary typ typ_pre typ_nobin
 %type<Mo_def.Syntax.vis> vis
@@ -365,6 +366,9 @@ seplist1(X, SEP) :
 %inline id :
   | id=ID { id @@ at $sloc }
 
+%inline id_wild :
+  | UNDERSCORE { "_" @@ at $sloc }
+
 %inline typ_id :
   | id=ID { id @= at $sloc }
 
@@ -482,6 +486,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 :
@@ -634,6 +639,20 @@ exp_nullary [@recover.expr mk_stub_expr loc] (B) :
   | UNDERSCORE
     { VarE ("_" @~ at $sloc) @? at $sloc }
 
+exp_arg:
+  | e=ob { e, false }
+  | l=lit
+    { LitE(ref l) @? at $sloc, false }
+  | LPAR es=seplist(exp(ob), COMMA) RPAR
+    { match es with [e] -> e, true | _ -> TupE(es) @? at $sloc, false }
+  | x=id
+    { VarE (x.it @~ x.at) @? at $sloc, false }
+  | PRIM s=TEXT
+    { PrimE(s) @? at $sloc, false }
+  | UNDERSCORE
+    { VarE ("_" @~ at $sloc) @? at $sloc, false }
+
+
 exp_post(B) :
   | e=exp_nullary(B)
     { e }
@@ -645,8 +664,11 @@ exp_post(B) :
     { ProjE (e, int_of_string s) @? at $sloc }
   | e=exp_post(B) DOT x=id
     { DotE(e, x, ref None) @? at $sloc }
-  | e1=exp_post(B) inst=inst e2=exp_nullary(ob)
-    { CallE(None, e1, inst, e2) @? at $sloc }
+  | e1=exp_post(B) inst=inst e2=exp_arg
+    {
+      let e2, sugar = e2 in
+      CallE(None, e1, inst, (sugar, ref e2)) @? at $sloc
+    }
   | e1=exp_post(B) BANG
     { BangE(e1) @? at $sloc }
   | LPAR SYSTEM e1=exp_post(B) DOT x=id RPAR
@@ -657,8 +679,9 @@ exp_post(B) :
 exp_un(B) :
   | e=exp_post(B)
     { e }
-  | par=parenthetical e1=exp_post(B) inst=inst e2=exp_nullary(ob)
-    { CallE(par, e1, inst, e2) @? at $sloc }
+  | par=parenthetical e1=exp_post(B) inst=inst e2=exp_arg
+     { let e2, sugar = e2 in
+       CallE(par, e1, inst, (sugar, ref e2)) @? at $sloc }
   | HASH x=id
     { TagE (x, TupE([]) @? at $sloc) @? at $sloc }
   | HASH x=id e=exp_nullary(ob)
diff --git a/src/mo_frontend/printers.ml b/src/mo_frontend/printers.ml
index b839da334f8..98a0286b611 100644
--- a/src/mo_frontend/printers.ml
+++ b/src/mo_frontend/printers.ml
@@ -193,6 +193,7 @@ let repr_of_symbol : xsymbol -> (string * string) =
   | X (N N_exp_nonvar_ob_) -> "<exp_nonvar(ob)>", eg_exp
   | X (N N_exp_nullary_bl_) -> "<exp_nullary(bl)>", eg_exp
   | X (N N_exp_nullary_ob_) -> "<exp_nullary(ob)>", eg_exp
+  | X (N N_exp_arg) -> "<exp_nullary(ob)>", eg_exp
   | X (N N_exp_plain) -> "<exp_plain>", "true"
   | X (N N_exp_post_bl_) -> "<exp_post(bl)>", eg_exp
   | X (N N_exp_post_ob_) -> "<exp_post(ob)>", eg_exp
diff --git a/src/mo_frontend/static.ml b/src/mo_frontend/static.ml
index be432280e21..35722ad0837 100644
--- a/src/mo_frontend/static.ml
+++ b/src/mo_frontend/static.ml
@@ -35,6 +35,7 @@ let pat_err m at =
 
 let rec exp m e = match e.it with
   (* Plain values *)
+  | HoleE (s, e) -> exp m !e
   | (PrimE _ | LitE _ | ActorUrlE _ | FuncE _) -> ()
   | (TagE (_, exp1) | OptE exp1) -> exp m exp1
   | TupE es -> List.iter (exp m) es
diff --git a/src/mo_frontend/traversals.ml b/src/mo_frontend/traversals.ml
index 51a1a28ebab..0ed43b0ca3e 100644
--- a/src/mo_frontend/traversals.ml
+++ b/src/mo_frontend/traversals.ml
@@ -3,6 +3,7 @@ open Syntax
 open Source
 
 let rec over_exp (f : exp -> exp) (exp : exp) : exp = match exp.it with
+  | HoleE (s, exp1) -> f { exp with it = HoleE (s, ref (over_exp f (!exp1))) }
   | ImportE _ | PrimE _ | VarE _ | LitE _ | ActorUrlE _ -> f exp
   | UnE (x, y, exp1) -> f { exp with it = UnE (x, y, over_exp f exp1) }
   | ShowE (x, exp1) -> f { exp with it = ShowE (x, over_exp f exp1) }
@@ -31,8 +32,8 @@ let rec over_exp (f : exp -> exp) (exp : exp) : exp = match exp.it with
      f { exp with it = RelE (x, over_exp f exp1, y, over_exp f exp2) }
   | AssignE (exp1, exp2) ->
      f { exp with it = AssignE (over_exp f exp1, over_exp f exp2) }
-  | CallE (par_opt, exp1, x, exp2) ->
-     f { exp with it = CallE (Option.map (over_exp f) par_opt, over_exp f exp1, x, over_exp f exp2) }
+  | CallE (par_opt, exp1, x, (s, exp2)) ->
+     f { exp with it = CallE (Option.map (over_exp f) par_opt, over_exp f exp1, x, (s, ref (over_exp f !exp2))) }
   | AndE (exp1, exp2) ->
      f { exp with it = AndE (over_exp f exp1, over_exp f exp2) }
   | OrE (exp1, exp2) ->
diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml
index 6ed44042295..352d9d509ac 100644
--- a/src/mo_frontend/typing.ml
+++ b/src/mo_frontend/typing.ml
@@ -1043,6 +1043,7 @@ and is_explicit_pat_field pf =
 
 let rec is_explicit_exp e =
   match e.it with
+  | HoleE _ -> false (* tbr *)
   | PrimE _ | ActorUrlE _
   | TagE _
   | BreakE _ | RetE _ | ThrowE _ ->
@@ -1303,6 +1304,145 @@ and combine_pat_srcs env t pat : unit =
   | AnnotP (pat1, _typ) -> combine_pat_srcs env t pat1
   | ParP pat1 -> combine_pat_srcs env t pat1
 
+
+type hole_candidate =
+  { path: exp;
+    desc: string;
+    typ : T.typ;
+  }
+
+(* All candidates are subtypes of the required type. The "greatest" of
+   these types is the "closest" to the required type. If we can
+   uniquely identify a single candidate that is the supertype of all
+   other candidates we pick it. *)
+let disambiguate_resolutions (candidates : hole_candidate list) =
+  let add_candidate (frontiers : hole_candidate list) (c : hole_candidate) =
+    let rec go (fs : hole_candidate list) = match fs with
+      | [] -> [c]
+      | f::fs' ->
+         if T.sub c.typ f.typ then
+           if T.eq c.typ f.typ then
+             (* c = f, so we keep both *)
+             f :: go fs'
+           else
+             (* c <: f, so f absorbs c *)
+             fs
+         else if T.sub f.typ c.typ then
+           (* f <: c, so c absorbs f *)
+           go fs'
+         else
+           (* no relation at all, so we keep both *)
+           f :: go fs'
+    in
+    go frontiers
+  in
+  match List.fold_left add_candidate [] candidates with
+  | [dom] -> Some dom
+  | _ -> None
+
+(** Searches for hole resolutions for [name] on a given [hole_sort] and [typ].
+    Returns [Ok(candidate)] when a single resolution is
+    found, [Error(file_paths)] when no resolution was found, but a
+    matching module could be imported, and reports an ambiguity error
+    when finding multiple resolutions.
+ *)
+let resolve_hole env at hole_sort typ =
+  let is_matching_lab lab =
+    match hole_sort with
+    | Named lab1 -> lab = lab1
+    | Anon _ -> true
+  in
+  let is_module (n, (t, _, _, _)) = match T.normalize t with
+    | T.Obj (T.Module, fs) -> Some (n, fs)
+    | _ -> None
+  in
+  let is_matching_typ typ1 = T.sub typ1 typ
+  in
+  let has_matching_field_typ = function
+    | T.{ lab; typ = Typ c; _ } -> None
+    | T.{ lab; typ = Mut t; _ } -> None
+    | T.{ lab = lab1; typ = typ1; _ } ->
+       if is_matching_lab lab1 &&
+          is_matching_typ typ1
+       then Some (lab1, typ1)
+       else None
+  in
+  let find_candidate (module_name, fs) =
+    List.find_map has_matching_field_typ fs |>
+      Option.map (fun (lab, typ)->
+          let path =
+            { it = DotE( { it = VarE {it = module_name; at = no_region; note = Const};
+                           at = Source.no_region;
+                           note = empty_typ_note
+                         },
+                         { it = lab; at = no_region; note = () },
+                         ref None);
+              at = Source.no_region;
+              note = empty_typ_note; }
+          in
+          ({ path; desc = module_name^"."^ lab; typ } : hole_candidate))
+  in
+  let find_candidate_val = function
+    (id, (t, _, _, _)) ->
+    if is_matching_lab id &&
+       is_matching_typ t
+    then
+      let path = { it =
+                   VarE {it = id; at = no_region; note = Const};
+                   at = Source.no_region;
+                   note = empty_typ_note }
+      in
+      Some { path; desc = id; typ = t }
+    else None
+  in
+  let eligible_env_vals =
+    let vals =
+      match hole_sort with
+      | Named id ->
+        (* narrow env to search *)
+        (match T.Env.find_opt id env.vals with
+         | Some info -> T.Env.singleton id info
+         | None -> T.Env.empty)
+      | Anon _ ->
+         env.vals (* search entire env *)
+    in
+    T.Env.to_seq vals |>
+      Seq.filter_map find_candidate_val |>
+      List.of_seq
+  in
+  let eligible_module_vals () =
+    T.Env.to_seq env.vals |>
+      Seq.filter_map is_module |>
+      Seq.filter_map find_candidate |>
+      List.of_seq
+  in
+  let eligible_vals =
+    match eligible_env_vals with
+    | [oc] -> [oc] (* first look in local env, otherwise consider module entries *)
+    | occs -> occs @ eligible_module_vals ()
+  in
+  match eligible_vals with
+  | [oc] -> Ok oc
+  | [] ->
+     let lib_candidates =
+       T.Env.to_seq env.libs |>
+         Seq.filter_map (fun (n, t) ->
+             match t with
+             | T.Obj (T.Module, fs) -> Some (n, fs)
+             | _ -> None) |>
+         Seq.filter_map find_candidate |>
+         List.of_seq in
+     Error (List.map (fun candidate -> candidate.desc) lib_candidates)
+  | ocs -> begin
+     match disambiguate_resolutions ocs with
+     | Some oc -> Ok oc
+     | None ->
+     let candidates = List.map (fun oc -> oc.desc) ocs in
+     error env at "M0231" "ambiguous implicit argument of type%a.\nThe available candidates are: %s"
+       display_typ typ
+       (String.concat ", " candidates)
+     end
+
 type ctx_dot_candidate =
   { module_name : T.lab;
     func_ty : T.typ;
@@ -1324,7 +1464,7 @@ let contextual_dot env name receiver_ty =
       true
     with _ ->
       false in
-  let is_module (n, (t, _, _, _)) = match t with
+  let is_module (n, (t, _, _, _)) = match T.normalize t with
     | T.Obj (T.Module, fs) -> Some (n, (t, fs))
     | _ -> None in
   let has_matching_self tf = match tf with
@@ -1399,6 +1539,9 @@ and infer_exp'' env exp : T.typ =
   let in_actor = env.in_actor in
   let env = {env with in_actor = false; in_prog = false; context = exp.it::env.context} in
   match exp.it with
+  | HoleE (_, e) ->
+    (* TODO: this should probably be an assert, not an error *)
+    error env exp.at "M0232" "cannot infer type of implicit argument"
   | PrimE _ ->
     error env exp.at "M0054" "cannot infer type of primitive"
   | VarE id ->
@@ -2026,6 +2169,27 @@ and check_exp env t exp =
 and check_exp' env0 t exp : T.typ =
   let env = {env0 with in_prog = false; in_actor = false; context = exp.it :: env0.context } in
   match exp.it, t with
+  | HoleE (s, e), t ->
+    let desc = function
+      | Named id -> "'"^id^"'"
+      | Anon idx -> "at position " ^ (Int.to_string idx)
+    in
+    begin match resolve_hole env exp.at s t with
+    | Ok {path; _} ->
+      e := path;
+      check_exp env t path;
+      t
+    | Error suggestions ->
+      let sug =
+         if suggestions = [] then
+         "\nHint: If you're trying to use an implicit argument you need to have a matching declaration in scope."
+         else Format.sprintf "\nHint: Did you mean to import %s?" (String.concat " or " suggestions)
+      in
+      error env exp.at "M0230" "Cannot determine implicit argument %s of type%a%s"
+        (desc s)
+        display_typ t
+        sug
+    end
   | PrimE s, T.Func _ ->
     t
   | LitE lit, _ ->
@@ -2321,8 +2485,35 @@ 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 ->
+      (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
+  in
+  if List.length es < List.length ts
+  then go 0 ts es
+  else es
 
-and infer_call env exp1 inst exp2 at t_expect_opt =
+and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt =
+  let exp2 = !ref_exp2 in
   let n = match inst.it with None -> 0 | Some (_, typs) -> List.length typs in
   let (t1, ctx_dot) = infer_callee env exp1 in
   let sort, tbs, t_arg, t_ret =
@@ -2345,6 +2536,21 @@ and infer_call env exp1 inst exp2 at t_expect_opt =
       | t' -> T.unit, [(t, t')]
     end
   in
+  let exp2 =
+    let es = match exp2.it with
+      | TupE es when not parenthesized -> es
+      | _ -> [exp2] in
+    (* Must not use T.as_seq here, as T.normalize will clear the
+       `implicit` Name in case of a single implicit argument *)
+    let ts = match t_arg with
+      | T.Tup ts -> ts
+      | t -> [t] in
+    let e' = match insert_holes exp2.at ts es with
+      | [e] -> e.it
+      | es -> TupE es in
+    { exp2 with it = e'}
+  in
+  if not env.pre then ref_exp2 := exp2; (* TODO: is this good enough *)
   let ts, t_arg', t_ret' =
     match tbs, inst.it with
     | [], (None | Some (_, []))  (* no inference required *)
@@ -2415,6 +2621,10 @@ and infer_call_instantiation env t1 tbs t_arg t_ret exp2 at t_expect_opt extra_s
           | T.Func (_, _, _, ts1, _) -> ts1 @ !must_solve
           | _ -> normalized_target :: !must_solve);
         target_type
+      | HoleE _, normalized_target ->
+        deferred := (exp, target_type) :: !deferred;
+        must_solve := normalized_target :: !must_solve;
+        target_type
       (* Future work: more cases to defer? *)
       | _ ->
         (* Infer and add a subtype problem for bi_match *)
@@ -2442,7 +2652,7 @@ and infer_call_instantiation env t1 tbs t_arg t_ret exp2 at t_expect_opt extra_s
   in
 
   (* Incorporate the return type into the subtyping constraints *)
-  let ret_typ_opt, subs = 
+  let ret_typ_opt, subs =
     match t_expect_opt with
     | None -> Some t_ret, subs
     | Some expected_ret -> None, (t_ret, expected_ret) :: subs
@@ -2488,7 +2698,13 @@ and infer_call_instantiation env t1 tbs t_arg t_ret exp2 at t_expect_opt extra_s
             (* We just have open [codom], we need to infer the body *)
             let actual_t = infer_exp env' body in
             subs := (actual_t, body_typ) :: !subs;
-          end
+        end
+      | HoleE _, typ ->
+         if not env.pre then begin
+           (* Check that all type variables in the type are fixed, fail otherwise *)
+           Bi_match.fail_when_types_are_not_closed remaining [typ];
+           check_exp env typ exp
+         end
       | _ ->
         (* Future work: Inferring will fail, we could report an explicit error instead *)
         subs := (infer_exp env exp, typ) :: !subs
@@ -2497,11 +2713,14 @@ and infer_call_instantiation env t1 tbs t_arg t_ret exp2 at t_expect_opt extra_s
 
     if not env.pre then begin
       (* Fix the manually decomposed terms as if they were inferred *)
-      let fix substitute = List.iter (fun (e, t) -> ignore (infer_exp_wrapper (fun _ _ -> substitute t) T.as_immut env e)) in
+     let fix substitute = List.iter (fun (e, t) ->
+         match e.it with
+         | HoleE _ -> ()
+         | _ -> ignore (infer_exp_wrapper (fun _ _ -> substitute t) T.as_immut env e)) in
       fix (T.open_ ts) to_fix;
       fix (T.open_ ts) deferred;
     end;
-(*   
+(*
     if not env.pre then
       info env at "inferred instantiation <%s>"
         (String.concat ", " (List.map T.string_of_typ ts));
diff --git a/src/mo_interpreter/interpret.ml b/src/mo_interpreter/interpret.ml
index 0415038c1e8..3bc69d0bbcc 100644
--- a/src/mo_interpreter/interpret.ml
+++ b/src/mo_interpreter/interpret.ml
@@ -443,6 +443,7 @@ and interpret_exp_mut env exp (k : V.value V.cont) =
   last_env := env;
   Profiler.bump_region exp.at ;
   match exp.it with
+  | HoleE (_, e) -> interpret_exp_mut env (!e) k
   | PrimE s ->
     k (V.Func (CC.call_conv_of_typ exp.note.note_typ,
        Prim.prim { Prim.trap = trap exp.at "%s" } s
@@ -605,7 +606,8 @@ and interpret_exp_mut env exp (k : V.value V.cont) =
       | T.Shared _ -> make_message env name exp.note.note_typ v
       | T.Local -> v
     in k v'
-  | CallE (par, exp1, typs, exp2) ->
+  | CallE (par, exp1, typs, (_, exp2)) ->
+    let exp2 = !exp2 in
     interpret_par env par
       (fun v ->
         ignore (V.as_obj v);
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
index 3dfb65f8aed..7ae95c4d7f6 100644
--- a/src/viper/trans.ml
+++ b/src/viper/trans.ml
@@ -805,10 +805,10 @@ and assign_stmts ctxt at (lval : lvalue) (e : M.exp) : seqn' =
   match e with
   | M.({it=TupE [];_}) -> [], []
   | M.({it=AnnotE (e, _);_}) -> assign_stmts ctxt at lval e
-  | M.({it=CallE (_, {it=M.DotE ({it=M.VarE(m);_}, {it="init";_}, _);_}, _inst, args);_})
+  | M.({it=CallE (_, {it=M.DotE ({it=M.VarE(m);_}, {it="init";_}, _);_}, _inst, (_, args));_})
       when Imports.find_opt (m.it) ctxt.imports = Some(IM_base_Array)
       ->
-    begin match args with
+    begin match !args with
     | M.({it=TupE([e1;e2]); _}) ->
       fld_via_tmp_var ctxt lval t (fun x ->
         let lhs = !!(LocalVar (x, tr_typ ctxt t)) in
@@ -817,7 +817,7 @@ and assign_stmts ctxt at (lval : lvalue) (e : M.exp) : seqn' =
             ; !!(InhaleS (array_size_inv at lhs (exp ctxt e1)))
             ; !!(InhaleS (array_init_const at ctxt lhs (array_elem_t t) (exp ctxt e2))) ]
       )
-    | _ -> unsupported args.at (Arrange.exp args)
+    | _ -> unsupported (!args).at (Arrange.exp (!args))
     end
   | M.({it = CallE(_, {it = VarE m; _}, inst, args); _}) ->
     fld_via_tmp_var ctxt lval t (fun x ->
@@ -858,8 +858,8 @@ and via_tmp_var ctxt (lval : lvalue) (t : T.typ) (f : id -> seqn') : seqn' =
     let stmt = !!(assign_stmt lval tmp_e) in
     d :: ds, stmts @ [stmt]
 
-and call_args ctxt e =
-  match e with
+and call_args ctxt (_, e) =
+  match !e with
   | {it = M.TupE args; _} -> List.map (fun arg -> exp ctxt arg) args
   | arg -> [exp ctxt arg]
 
@@ -880,8 +880,9 @@ and exp ctxt e =
     end
   | M.AnnotE(a, b) ->
     exp ctxt a
-  | M.CallE (_, {it=M.DotE (e1, {it="size";_}, _);_}, _inst, {it=M.TupE ([]);at;_})
-      -> sizeE at (exp ctxt e1)
+  | M.CallE (_, {it=M.DotE (e1, {it="size";_}, _);_}, _inst, (_, arg))
+    when !(arg).it = M.(TupE [])
+      -> sizeE (!arg).at (exp ctxt e1)
   | M.LitE r ->
     begin match !r with
     | M.BoolLit b ->
@@ -961,29 +962,36 @@ and exp ctxt e =
       let n = List.length es in
       ctxt.reqs.tuple_arities := IntSet.add n !(ctxt.reqs.tuple_arities);
       !!(CallE (tup_con_name n, List.map (exp ctxt) es))
-  | M.CallE (_, { it = M.DotE ({it=M.VarE(m);_}, {it=predicate_name;_}, _); _ }, _inst, { it = M.FuncE (_, _, _, pattern, _, _, e); note; _ })
-    when Imports.find_opt (m.it) ctxt.imports = Some(IM_Prim)
-      && (predicate_name = "forall" || predicate_name = "exists")
+  | M.CallE (_, { it = M.DotE ({it=M.VarE(m);_}, {it=predicate_name;_}, _); _ }, _inst, (_, arg))
+     when match !arg with
+          | { it = M.FuncE (_, _, _, pattern, _, _, e); note; _ } ->
+            Imports.find_opt (m.it) ctxt.imports = Some(IM_Prim)
+            && (predicate_name = "forall" || predicate_name = "exists")
+          | _ -> false
     ->
-    let binders = extract_binders pattern in
-    let typs =
-      match M.(note.note_typ) with
-      | T.Func (_, _, _, [ T.Tup args ], _) -> args
-      | T.Func (_, _, _, [ arg ], _) -> [ arg ]
-      | _ -> []
-    in
-    let typed_binders =
-      List.fold_left2
-        (fun acc b t -> (id b, t) :: acc)
-        [] binders typs
-    in
-    let ctxt = add_locals ctxt typed_binders in
-    let typed_binders = List.map (fun (b, t) -> (b, tr_typ ctxt t)) typed_binders in
-    let e = exp ctxt e in
-    (match predicate_name with
-    | "forall" -> !!(ForallE (typed_binders, e))
-    | "exists" -> !!(ExistsE (typed_binders, e))
-    | _ -> assert false)
+    begin match !arg with
+      | { it = M.FuncE (_, _, _, pattern, _, _, e); note; _ } ->
+      let binders = extract_binders pattern in
+      let typs =
+        match M.(note.note_typ) with
+        | T.Func (_, _, _, [ T.Tup args ], _) -> args
+        | T.Func (_, _, _, [ arg ], _) -> [ arg ]
+        | _ -> []
+      in
+      let typed_binders =
+        List.fold_left2
+          (fun acc b t -> (id b, t) :: acc)
+          [] binders typs
+      in
+      let ctxt = add_locals ctxt typed_binders in
+      let typed_binders = List.map (fun (b, t) -> (b, tr_typ ctxt t)) typed_binders in
+      let e = exp ctxt e in
+      (match predicate_name with
+      | "forall" -> !!(ForallE (typed_binders, e))
+      | "exists" -> !!(ExistsE (typed_binders, e))
+      | _ -> assert false)
+      | _ -> unsupported e.at (Arrange.exp e)
+    end
   | M.CallE (_, { it = M.DotE ({it=M.VarE(m);_}, {it="Ret";_}, _); _ }, _, _)
     when Imports.find_opt (m.it) ctxt.imports = Some(IM_Prim) -> !!(FldE "$Res")
   | _ ->
diff --git a/src/viper/traversals.ml b/src/viper/traversals.ml
index cec4bd8f7ab..3834f756f50 100644
--- a/src/viper/traversals.ml
+++ b/src/viper/traversals.ml
@@ -12,6 +12,7 @@ type visitor =
 
 let rec over_exp (v : visitor) (exp : exp) : exp =
   v.visit_exp (match exp.it with
+  | HoleE (s, e) -> { exp with it = HoleE (s, ref (over_exp v !e)) }
   | ImportE _ | PrimE _ | VarE _ | LitE _ | ActorUrlE _ -> exp
   | UnE (x, y, exp1) -> { exp with it = UnE (x, y, over_exp v exp1) }
   | ShowE (x, exp1) -> { exp with it = ShowE (x, over_exp v exp1) }
@@ -36,7 +37,7 @@ let rec over_exp (v : visitor) (exp : exp) : exp =
   | IdxE (exp1, exp2) -> { exp with it = IdxE (over_exp v exp1, over_exp v exp2) }
   | RelE (x, exp1, y, exp2) -> { exp with it = RelE (x, over_exp v exp1, y, over_exp v exp2) }
   | AssignE (exp1, exp2) -> { exp with it = AssignE (over_exp v exp1, over_exp v exp2) }
-  | CallE (exp_opt, exp1, inst, exp2) -> { exp with it = CallE (Option.map (over_exp v) exp_opt, over_exp v exp1, over_inst v inst, over_exp v exp2) }
+  | CallE (exp_opt, exp1, inst, (s, exp2)) -> { exp with it = CallE (Option.map (over_exp v) exp_opt, over_exp v exp1, over_inst v inst, (s, ref (over_exp v (!exp2)))) }
   | AndE (exp1, exp2) -> { exp with it = AndE (over_exp v exp1, over_exp v exp2) }
   | OrE (exp1, exp2) -> { exp with it = OrE (over_exp v exp1, over_exp v exp2) }
   | ImpliesE (exp1, exp2) -> { exp with it = ImpliesE (over_exp v exp1, over_exp v exp2) }
diff --git a/test/check-error-codes.py b/test/check-error-codes.py
index a8574cb277f..238532655cc 100755
--- a/test/check-error-codes.py
+++ b/test/check-error-codes.py
@@ -41,6 +41,7 @@
     "M0164", # unknown record or variant label in textual representation
     "M0165", # odd expected type
     "M0191", # compiler warning about wasm features (hard to trigger)
+    "M0232", # cannot infer type of implicit argument
     }
 
 def populate_error_codes():
diff --git a/test/fail/implicit-best-candidate.mo b/test/fail/implicit-best-candidate.mo
new file mode 100644
index 00000000000..b5a0d258263
--- /dev/null
+++ b/test/fail/implicit-best-candidate.mo
@@ -0,0 +1,60 @@
+type A = {};
+type B = { a : Int };
+type C = { a : Int; b : Text };
+
+let a : A = {};
+let b : B = { a = 0 };
+let c : C = { a = 0; b = "" };
+
+module Contravariant {
+  module MA {
+    public func cmp(_ : A, _ : A) : Nat = 1;
+  };
+
+  module MB1 {
+    public func cmp(_ : B, _ : B) : Nat = 21;
+  };
+
+  module MB2 {
+    public func cmp(_ : B, _ : B) : Nat = 22;
+  };
+
+  module MC {
+    public func cmp(_ : C, _ : C) : Nat = 3;
+  };
+
+  func cmp<T>(x : T, y : T, cmp : (implicit : (T, T) -> Nat)) : Nat {
+    cmp(x, y);
+  };
+
+  public func diamond() {
+    assert cmp(b, c) == 2;
+  };
+};
+
+module Covariant {
+  module MA {
+    public let default : A = {};
+  };
+
+  module MB1 {
+    public let default : B = { a = 0 };
+  };
+
+  module MB2 {
+    public let default : B = { a = 17 };
+  };
+
+  module MC {
+    public let default : C = { a = 0; b = "" };
+  };
+
+  func default<T>(default : (implicit : T)) : T = default;
+
+  public func diamond() {
+    ignore default<B>();
+  };
+};
+
+Contravariant.diamond();
+Covariant.diamond();
diff --git a/test/fail/implicit.mo b/test/fail/implicit.mo
new file mode 100644
index 00000000000..ecad49962ff
--- /dev/null
+++ b/test/fail/implicit.mo
@@ -0,0 +1,107 @@
+
+type Order = {#less;#greater;#equal};
+
+module M {
+  public func c(n : Nat, m: Nat) : Order {
+    if (n < m) #less
+    else if (n == m) #greater
+    else #equal;
+  };
+
+  public func ambiguous(n : Nat, m: Nat) : Order {
+    if (n < m) #less
+    else if (n == m) #greater
+    else #equal;
+  };
+
+};
+
+module N {
+  public func c(n : Text, m: Text) : Order {
+     #equal;
+  };
+
+  public func ambiguous(n : Nat, m: Nat) : Order {
+    if (n < m) #less
+    else if (n == m) #greater
+    else #equal;
+  };
+};
+
+func f1(n : Nat, m : Nat, c : (implicit : (Nat, Nat) -> Order)) {
+  ignore c(n, m);
+};
+
+func f2<T>(n : T, m : T, c : (implicit : (T, T) -> Order)) {
+  ignore c(n, m);
+};
+
+func f3(n : Nat, m : Nat, d : (implicit : Nat -> Order)) {
+};
+
+
+f1(0, 1, M.c); //accept
+f2(0, 1, M.c); //accept
+
+f1("0", "1", M.c); // reject
+f2("0", "1", N.c); // accept
+
+f1(0, 1); //accept
+f2(0, 1); //accept
+
+f2("0", "1"); // accept
+
+f2(true, true); // reject
+
+f3(1, 1); // reject
+
+func f4(n : Nat, m : Nat, bogus : (implicit : (Nat, Nat) -> Order)) {
+};
+
+f4(1, 1); // reject
+
+// retype f4 with as f4 with different implicit name
+let f5 : (Nat, Nat, (c : (implicit : (Nat, Nat) -> Order))) -> () = f4;
+
+f5(1, 1); // accept
+
+func f6(n : Nat, m : Nat, ambiguous : (implicit : (Nat, Nat) -> Order)) {
+};
+
+f6(1, 1); // reject
+
+
+module XY {
+  public type XY = { x : Nat; y : Nat };
+  public let zero : XY = { x = 0; y = 0 };
+};
+
+module XZ {
+  public type XZ = { x : Nat; z : Nat };
+  public let zero : XZ = { x = 0; z = 0 };
+};
+
+func mkZero<T>(zero : (implicit : T)) : T {
+  zero
+};
+
+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
+
+func tuple(pair : (Nat, Nat), c : (implicit : (Nat, Nat) -> Order)) : Order {
+  c(pair.0, pair.1)
+};
+
+assert tuple(3, 3);
diff --git a/test/fail/ok/implicit-best-candidate.tc.ok b/test/fail/ok/implicit-best-candidate.tc.ok
new file mode 100644
index 00000000000..c5d1239ff9d
--- /dev/null
+++ b/test/fail/ok/implicit-best-candidate.tc.ok
@@ -0,0 +1,6 @@
+implicit-best-candidate.mo:31.15-31.21: type error [M0231], ambiguous implicit argument of type
+  ({a : Int}, {a : Int}) -> Nat.
+The available candidates are: MA.cmp, MB1.cmp, MB2.cmp
+implicit-best-candidate.mo:55.22-55.24: type error [M0231], ambiguous implicit argument of type
+  {a : Int}.
+The available candidates are: MB1.default, MB2.default, MC.default
diff --git a/test/fail/ok/implicit-best-candidate.tc.ret.ok b/test/fail/ok/implicit-best-candidate.tc.ret.ok
new file mode 100644
index 00000000000..69becfa16f9
--- /dev/null
+++ b/test/fail/ok/implicit-best-candidate.tc.ret.ok
@@ -0,0 +1 @@
+Return code 1
diff --git a/test/fail/ok/implicit.tc.ok b/test/fail/ok/implicit.tc.ok
new file mode 100644
index 00000000000..e31cbed5122
--- /dev/null
+++ b/test/fail/ok/implicit.tc.ok
@@ -0,0 +1,23 @@
+implicit.mo:46.4-46.7: type error [M0050], literal of type
+  Text
+does not have expected type
+  Nat
+implicit.mo:54.3-54.15: type error [M0230], Cannot determine implicit argument 'c' of type
+  (Bool, Bool) -> Order
+Hint: If you're trying to use an implicit argument you need to have a matching declaration in scope.
+implicit.mo:56.3-56.9: type error [M0230], Cannot determine implicit argument 'd' of type
+  Nat -> Order
+Hint: If you're trying to use an implicit argument you need to have a matching declaration in scope.
+implicit.mo:61.3-61.9: type error [M0230], Cannot determine implicit argument 'bogus' of type
+  (Nat, Nat) -> Order
+Hint: If you're trying to use an implicit argument you need to have a matching declaration in scope.
+implicit.mo:71.3-71.9: type error [M0231], ambiguous implicit argument of type
+  (Nat, Nat) -> Order.
+The available candidates are: M.ambiguous, N.ambiguous
+implicit.mo:88.27-88.29: type error [M0231], ambiguous implicit argument of type
+  {x : Nat}.
+The available candidates are: XY.zero, XZ.zero
+implicit.mo:107.14-107.15: type error [M0050], literal of type
+  Nat
+does not have expected type
+  (Nat, Nat)
diff --git a/test/fail/ok/implicit.tc.ret.ok b/test/fail/ok/implicit.tc.ret.ok
new file mode 100644
index 00000000000..69becfa16f9
--- /dev/null
+++ b/test/fail/ok/implicit.tc.ret.ok
@@ -0,0 +1 @@
+Return code 1
diff --git a/test/run/implicit-best-candidate.mo b/test/run/implicit-best-candidate.mo
new file mode 100644
index 00000000000..390d0b148f5
--- /dev/null
+++ b/test/run/implicit-best-candidate.mo
@@ -0,0 +1,56 @@
+type A = {};
+type B = { a : Int };
+type C = { a : Int; b : Text };
+
+let a : A = {};
+let b : B = { a = 0 };
+let c : C = { a = 0; b = "" };
+
+module Contravariant {
+  module MA {
+    public func cmp(_ : A, _ : A) : Nat = 1;
+  };
+
+  module MB {
+    public func cmp(_ : B, _ : B) : Nat = 2;
+  };
+
+  module MC {
+    public func cmp(_ : C, _ : C) : Nat = 3;
+  };
+
+  func cmp<T>(x : T, y : T, cmp : (implicit : (T, T) -> Nat)) : Nat {
+    cmp(x, y);
+  };
+
+  public func test() {
+    assert cmp(a, b) == 1;
+    assert cmp(b, c) == 2;
+    assert cmp(c, c) == 3;
+  };
+};
+
+module Covariant {
+  module MA {
+    public let default : A = {};
+  };
+
+  module MB {
+    public let default : B = { a = 0 };
+  };
+
+  module MC {
+    public let default : C = { a = 0; b = "" };
+  };
+
+  func default<T>(default : (implicit : T)) : T = default;
+
+  public func test() {
+    assert default<A>() == a;
+    assert default<B>().a == 0;
+    assert default<C>().b == "";
+  };
+};
+
+Contravariant.test();
+Covariant.test();
diff --git a/test/run/implicit-map.mo b/test/run/implicit-map.mo
new file mode 100644
index 00000000000..b14c7087702
--- /dev/null
+++ b/test/run/implicit-map.mo
@@ -0,0 +1,31 @@
+module Map {
+  public class Map<T, U>(k_ : T, u_ : U) {
+    public let k = k_;
+    public let u = u_;
+  };
+
+  public type Self<T, U> = Map<T, U>;
+
+  public func get<T, U>(map : Self<T, U>, x : T, compare : (implicit : (T, T) -> Int)) : ?U {
+    if (compare(map.k, x) == 0) ?map.u else null;
+  };
+};
+
+func compare(n : Nat, m : Nat) : Int = n - m;
+
+let map : Map.Map<Nat, Text> = Map.Map(1, "abc");
+
+let t0 : Nat = 0;
+let t1 : Nat = 1;
+
+let n1 = map.get(t0);
+let n2 = map.get t0;
+let n3 = map.get(t0, compare);
+let n4 = map.get<Nat, Text>(t0);
+assert n1 == null and n2 == null and n3 == null and n4 == null;
+
+let o1 = map.get(t1);
+let o2 = map.get t1;
+let o3 = map.get(t1, compare);
+let o4 = map.get<Nat, Text>(t1);
+assert o1 == ?"abc" and o2 == ?"abc" and o3 == ?"abc" and o4 == ?"abc";
diff --git a/test/run/implicit.mo b/test/run/implicit.mo
new file mode 100644
index 00000000000..79f14a87db2
--- /dev/null
+++ b/test/run/implicit.mo
@@ -0,0 +1,96 @@
+import Prim "mo:prim";
+
+type Order = {#less;#greater;#equal};
+
+module M {
+
+  public func c(n : Nat, m: Nat) : Order {
+    Prim.debugPrint (debug_show (#c1(n,m)));
+    if (n < m) #less
+    else if (n == m) #greater
+    else #equal;
+  };
+};
+
+module N {
+  public func c(n : Text, m: Text) : Order {
+     Prim.debugPrint (debug_show (#c2(n,m)));
+     #equal;
+  };
+
+};
+
+func f1(n : Nat, m : Nat, c : (implicit : (Nat, Nat) -> Order)) {
+  ignore c(n, m);
+};
+
+func f2<T>(n : T, m : T, c : (implicit : (T, T) -> Order)) {
+  ignore c(n, m);
+};
+
+func f3(n : Nat, m : Nat, _ : (implicit : Nat -> Order)) {
+};
+
+
+
+f1(0, 1, M.c); //accept
+f2(0, 1, M.c); //accept
+
+//f1("0", "1", M.c); // reject
+f2("0", "1", N.c); // accept
+
+f1(0, 1); //accept
+f2(0, 1); //accept
+
+f2("0", "1"); // accept
+
+do {
+
+  func c(n : Text, m: Text) : Order {
+     Prim.debugPrint (debug_show (#c3(n,m)));
+     #equal;
+  };
+
+  f2("0", "1"); // accept (resolve to local c)
+};
+
+//f2(true, true); // reject
+
+//f3(1, 1); // reject
+
+func unary<T>(c : (implicit : (T, T) -> Order), t : T) {
+  ignore c(t, t)
+};
+
+unary(10);
+
+func nullary<T>(c : (implicit : (T, T) -> Order)) {
+  ignore c;
+};
+nullary<Nat>();
+
+module Nat {
+  public func eq(x : Nat, y : Nat) : Bool {
+    Prim.debugPrint("nat eq");
+    x == y
+  };
+};
+
+module Int {
+  public func eq(x : Int, y : Int) : Bool {
+    Prim.debugPrint("int eq");
+    x == y
+  };
+};
+
+func isEq<T>(x : T, y : T, eq : (implicit : (T, T) -> Bool)) : Bool {
+  eq(x, y)
+};
+
+assert isEq<Nat>(3, 3);
+
+func tuple(pair : (Nat, Nat), eq : (implicit : (Nat, Nat) -> Bool)) : Bool {
+  eq(pair.0, pair.1)
+};
+
+assert tuple((3, 3));
diff --git a/test/run/implicits-example.mo b/test/run/implicits-example.mo
new file mode 100644
index 00000000000..f0b5b733703
--- /dev/null
+++ b/test/run/implicits-example.mo
@@ -0,0 +1,56 @@
+import {debugPrint} "mo:prim";
+
+module Nat {
+  public func toText(n : Nat) : Text { debug_show n };
+};
+
+
+module Int {
+  public func toText(i : Int) : Text { debug_show i };
+};
+
+
+module Array {
+
+  public func toText<T>(as : [T], toText: (implicit : T -> Text)) : Text {
+     var t = "";
+     for (a in as.vals()) {
+       t := t # (toText(a));
+     };
+     t
+  }
+
+};
+
+
+module Pair {
+
+  public func toText<T,U>(
+    p : (T, U),
+    toTextT : (implicit : (toText : T -> Text)),
+    toTextU : (implicit : (toText : U -> Text)),
+    )
+    : Text {
+      "(" # toTextT(p.0) # "," # toTextU(p.1) # ")"
+    };
+
+};
+
+
+func test () {
+
+  Array.toText([1,2,3], Nat.toText) // explicit arguments
+  |> debugPrint _;
+
+  Array.toText([1,2,3]) // implicit arguments
+  |> debugPrint _;
+
+  Pair.toText((1,2), Nat.toText, Nat.toText) // explicit arguments
+  |> debugPrint _;
+
+  Pair.toText((1,2))
+  |> debugPrint _ ; // implicit arguments
+
+};
+
+test();
diff --git a/test/run/ok/implicit.run-ir.ok b/test/run/ok/implicit.run-ir.ok
new file mode 100644
index 00000000000..91b21d101d8
--- /dev/null
+++ b/test/run/ok/implicit.run-ir.ok
@@ -0,0 +1,10 @@
+#c1(0, 1)
+#c1(0, 1)
+#c2("0", "1")
+#c1(0, 1)
+#c1(0, 1)
+#c2("0", "1")
+#c3("0", "1")
+#c1(10, 10)
+nat eq
+nat eq
diff --git a/test/run/ok/implicit.run-low.ok b/test/run/ok/implicit.run-low.ok
new file mode 100644
index 00000000000..91b21d101d8
--- /dev/null
+++ b/test/run/ok/implicit.run-low.ok
@@ -0,0 +1,10 @@
+#c1(0, 1)
+#c1(0, 1)
+#c2("0", "1")
+#c1(0, 1)
+#c1(0, 1)
+#c2("0", "1")
+#c3("0", "1")
+#c1(10, 10)
+nat eq
+nat eq
diff --git a/test/run/ok/implicit.run.ok b/test/run/ok/implicit.run.ok
new file mode 100644
index 00000000000..91b21d101d8
--- /dev/null
+++ b/test/run/ok/implicit.run.ok
@@ -0,0 +1,10 @@
+#c1(0, 1)
+#c1(0, 1)
+#c2("0", "1")
+#c1(0, 1)
+#c1(0, 1)
+#c2("0", "1")
+#c3("0", "1")
+#c1(10, 10)
+nat eq
+nat eq
diff --git a/test/run/ok/implicit.tc.ok b/test/run/ok/implicit.tc.ok
new file mode 100644
index 00000000000..c22ad65f5fc
--- /dev/null
+++ b/test/run/ok/implicit.tc.ok
@@ -0,0 +1,3 @@
+implicit.mo:31.6-31.8: warning [M0194], unused identifier f3 (delete or rename to wildcard `_` or `_f3`)
+implicit.mo:31.9-31.10: warning [M0194], unused identifier n (delete or rename to wildcard `_` or `_n`)
+implicit.mo:31.18-31.19: warning [M0194], unused identifier m (delete or rename to wildcard `_` or `_m`)
diff --git a/test/run/ok/implicit.wasm-run.ok b/test/run/ok/implicit.wasm-run.ok
new file mode 100644
index 00000000000..91b21d101d8
--- /dev/null
+++ b/test/run/ok/implicit.wasm-run.ok
@@ -0,0 +1,10 @@
+#c1(0, 1)
+#c1(0, 1)
+#c2("0", "1")
+#c1(0, 1)
+#c1(0, 1)
+#c2("0", "1")
+#c3("0", "1")
+#c1(10, 10)
+nat eq
+nat eq
diff --git a/test/run/ok/implicits-example.run-ir.ok b/test/run/ok/implicits-example.run-ir.ok
new file mode 100644
index 00000000000..2b795f3fe41
--- /dev/null
+++ b/test/run/ok/implicits-example.run-ir.ok
@@ -0,0 +1,4 @@
+123
+123
+(1,2)
+(1,2)
diff --git a/test/run/ok/implicits-example.run-low.ok b/test/run/ok/implicits-example.run-low.ok
new file mode 100644
index 00000000000..2b795f3fe41
--- /dev/null
+++ b/test/run/ok/implicits-example.run-low.ok
@@ -0,0 +1,4 @@
+123
+123
+(1,2)
+(1,2)
diff --git a/test/run/ok/implicits-example.run.ok b/test/run/ok/implicits-example.run.ok
new file mode 100644
index 00000000000..2b795f3fe41
--- /dev/null
+++ b/test/run/ok/implicits-example.run.ok
@@ -0,0 +1,4 @@
+123
+123
+(1,2)
+(1,2)
diff --git a/test/run/ok/implicits-example.wasm-run.ok b/test/run/ok/implicits-example.wasm-run.ok
new file mode 100644
index 00000000000..2b795f3fe41
--- /dev/null
+++ b/test/run/ok/implicits-example.wasm-run.ok
@@ -0,0 +1,4 @@
+123
+123
+(1,2)
+(1,2)