diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index d52b099bbf..e9359b7a64 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -101,15 +101,10 @@ def to_pexpr : syntax → elaborator_m expr
       pure (binder_info.implicit, bc)
     | bracketed_binder.view.strict_implicit {content := bc} :=
       pure (binder_info.strict_implicit, bc)
-    | bracketed_binder.view.inst_implicit {content := bc} :=
-      prod.mk binder_info.inst_implicit <$> (match bc.kind with
-        | some @inst_implicit_anonymous_binder :=
-          pure {ids := ["_inst_"], type := some {type := (view inst_implicit_anonymous_binder bc).type}}
-        | some @inst_implicit_named_binder :=
-          let v := view inst_implicit_named_binder bc in
-          pure {ids := [v.id], type := some {type := v.type}}
-        | _ := error stx "ill-formed lambda")
-    /-| bracketed_binder.view.anonymous_constructor {content := bc} :=-/
+    | bracketed_binder.view.inst_implicit {content := bc} := do
+      inst_implicit_binder_content.view.named bcn ← pure bc
+        | error stx "ill-formed lambda",
+      pure (binder_info.inst_implicit, {ids := [bcn.id], type := some {type := bcn.type}})
     | _ := error stx "ill-formed lambda",
     {ids := [binder_ident.view.id id], type := some type} ← pure bc | error stx "ill-formed lambda",
     expr.lam (mangle_ident id) bi <$> to_pexpr type.type <*> to_pexpr body
diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean
index 6d6bac4062..a2d885d2d5 100644
--- a/library/init/lean/expander.lean
+++ b/library/init/lean/expander.lean
@@ -53,7 +53,7 @@ review lambda {
     | binder_info.implicit := bracketed_binder.view.implicit {content := bc}
     | binder_info.strict_implicit := bracketed_binder.view.strict_implicit {content := bc}
     | binder_info.inst_implicit := bracketed_binder.view.inst_implicit
-      {content := review inst_implicit_named_binder {id := id, type := dom}}
+      {content := inst_implicit_binder_content.view.named {id := id, type := dom}}
     | binder_info.aux_decl := /- should not happen -/
       bracketed_binder.view.explicit {content := explicit_binder_content.view.other bc}
   ]},
@@ -90,13 +90,11 @@ def lambda.transform : transformer :=
         | bracketed_binder.view.implicit {content := bc} := (binder_info.implicit, bc)
         | bracketed_binder.view.strict_implicit {content := bc} := (binder_info.strict_implicit, bc)
         | bracketed_binder.view.inst_implicit {content := bc} :=
-          prod.mk binder_info.inst_implicit $ (match bc.kind with
-            | some @inst_implicit_anonymous_binder :=
-              {ids := ["_inst_"], type := some {type := (view inst_implicit_anonymous_binder bc).type}}
-            | some @inst_implicit_named_binder :=
-              let v := view inst_implicit_named_binder bc in
-              {ids := [v.id], type := some {type := v.type}}
-            | _ := {ids := []} /- unreachable -/)
+          prod.mk binder_info.inst_implicit $ (match bc with
+            | inst_implicit_binder_content.view.anonymous bca :=
+              {ids := ["_inst_"], type := some {type := bca.type}}
+            | inst_implicit_binder_content.view.named bcn :=
+              {ids := [bcn.id], type := some {type := bcn.type}})
         | bracketed_binder.view.anonymous_constructor _ := (binder_info.default, {ids := []}) /- unreachable -/),
         let type := (binder_content_type.view.type <$> bc.type).get_or_else $ review hole {},
         type ← match bc.default with
diff --git a/library/init/lean/parser/combinators.lean b/library/init/lean/parser/combinators.lean
index 291ff08764..2b1c66c9f5 100644
--- a/library/init/lean/parser/combinators.lean
+++ b/library/init/lean/parser/combinators.lean
@@ -165,9 +165,6 @@ instance longest_match.tokens (rs : list parser) [parser.has_tokens rs] : parser
 ⟨tokens rs⟩
 instance longest_match.view (rs : list parser) : parser.has_view syntax (longest_match rs) := default _
 
-/-- Parse a list `[p1, ..., pn]` of parsers as `p1 <|> ... <|> pn`.
-    The result will be wrapped in a node with the the index of the successful
-    parser as the name. -/
 def choice_aux : list parser → nat → parser
 | []      _ := error "choice: empty list"
 | (r::rs) i :=
@@ -175,15 +172,29 @@ def choice_aux : list parser → nat → parser
        pure $ syntax.mk_node ⟨name.mk_numeral name.anonymous i⟩ [stx] }
   <|> choice_aux rs (i+1)
 
+/-- Parse a list `[p1, ..., pn]` of parsers as `p1 <|> ... <|> pn`.
+    The result will be wrapped in a node with the index of the successful
+    parser as the name.
+
+    Remark: Does not have a `has_view` instance because we only use it in `node_choice!` macros
+    that define their own views. -/
 def choice (rs : list parser) : parser :=
 choice_aux rs 0
 
 instance choice.tokens (rs : list parser) [parser.has_tokens rs] : parser.has_tokens (choice rs) :=
 ⟨tokens rs⟩
 
-/- Remark: `choice` does not have `has_view` instance because we only use it at the pratt combinator
-   which doesn't need the view. -/
+/-- Like `choice`, but using `longest_match`. Does not create choice nodes, prefers the first successful parser. -/
+def longest_choice (rs : list parser) : parser :=
+do stx::stxs ← monad_parsec.longest_match $ rs.enum.map $ λ ⟨i, r⟩, do {
+     stx ← r,
+     pure $ syntax.mk_node ⟨name.mk_numeral name.anonymous i⟩ [stx]
+   } | error "unreachable",
+   pure stx
 
+instance longest_choice.tokens (rs : list parser) [parser.has_tokens rs] : parser.has_tokens (longest_choice rs) :=
+
+⟨tokens rs⟩
 instance try.tokens (r : parser) [parser.has_tokens r] : parser.has_tokens (try r) :=
 ⟨tokens r⟩
 instance try.view (r : parser) [i : parser.has_view α r] : parser.has_view α (try r) :=
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 23fc19f1ca..ac7668103d 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -110,10 +110,10 @@ node_choice! bracketed_binder {
   }, right: symbol ")"],
   implicit: node! implicit_binder ["{", content: binder_content.parser, "}"],
   strict_implicit: node! strict_implicit_binder ["⦃", content: binder_content.parser, "⦄"],
-  inst_implicit: node! inst_implicit_binder ["[", content: longest_match [
-    node! inst_implicit_named_binder [id: ident.parser, " : ", type: term.parser 0],
-    node! inst_implicit_anonymous_binder [type: term.parser 0]
-  ], "]"],
+  inst_implicit: node! inst_implicit_binder ["[", content: node_longest_choice! inst_implicit_binder_content {
+    named: node! inst_implicit_named_binder [id: ident.parser, " : ", type: term.parser 0],
+    anonymous: node! inst_implicit_anonymous_binder [type: term.parser 0]
+  }, "]"],
   anonymous_constructor: anonymous_constructor.parser,
 }
 
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index f0a3b6a2d4..261d985c1f 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -934,6 +934,8 @@ static expr parse_node(parser & p, unsigned, expr const *, pos_info const &) {
 }
 
 static expr parse_choice(parser & p, unsigned, expr const *, pos_info const &) {
+    name this_macro = p.get_token_info().value();
+    p.next();
     name macro = p.check_id_next("identifier expected");
     std::function<buffer<expr>()> go;
     buffer<expr> args;
@@ -962,7 +964,7 @@ static expr parse_choice(parser & p, unsigned, expr const *, pos_info const &) {
         p.next();
     }
     p.check_token_next("}", "`}` expected");
-    return mk_mdata(set_name(kvmap(), "node_choice!", macro), mk_lean_list(args));
+    return mk_mdata(set_name(kvmap(), this_macro, macro), mk_lean_list(args));
 }
 
 parse_table init_nud_table() {
@@ -999,7 +1001,8 @@ parse_table init_nud_table() {
     r = r.add({transition("match", mk_ext_action(parse_match))}, x0);
     r = r.add({transition("do", mk_ext_action(parse_do_expr))}, x0);
     r = r.add({transition("node!", mk_ext_action(parse_node))}, x0);
-    r = r.add({transition("node_choice!", mk_ext_action(parse_choice))}, x0);
+    r = r.add({transition("node_choice!", mk_ext_action_core(parse_choice))}, x0);
+    r = r.add({transition("node_longest_choice!", mk_ext_action_core(parse_choice))}, x0);
     return r;
 }
 
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 520e9e5de3..921c4941dc 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -3311,8 +3311,8 @@ expr elaborator::visit_node_macro(expr const & e, optional<expr> const & expecte
                  expected_type);
 }
 
-expr elaborator::visit_node_choice_macro(expr const & e, optional<expr> const & expected_type) {
-    name macro = *get_name(mdata_data(e), "node_choice!");
+expr elaborator::visit_node_choice_macro(expr const & e, bool longest_match, optional<expr> const & expected_type) {
+    name macro = *get_name(mdata_data(e), longest_match ? "node_longest_choice!" : "node_choice!");
     name esc_macro = macro.is_atomic() ? "«" + macro.to_string() + "»" : macro;
     expr args = mdata_expr(e);
     name full_macro = get_namespace(m_env) + macro;
@@ -3388,7 +3388,7 @@ expr elaborator::visit_node_choice_macro(expr const & e, optional<expr> const &
     return visit(mk_app(mk_const({"lean", "parser", "combinators", "node"}),
                         mk_const(full_macro),
                         mk_app(mk_const({"list", "cons"}),
-                               mk_app(mk_const({"lean", "parser", "combinators", "choice"}),
+                               mk_app(mk_const({"lean", "parser", "combinators", longest_match ? "longest_choice" : "choice"}),
                                       mk_lean_list(new_args)),
                                mk_const({"list", "nil"}))), expected_type);
 }
@@ -3438,7 +3438,9 @@ expr elaborator::visit_mdata(expr const & e, optional<expr> const & expected_typ
     } else if (get_name(mdata_data(e), "node!")) {
         return visit_node_macro(e, expected_type);
     } else if (get_name(mdata_data(e), "node_choice!")) {
-        return visit_node_choice_macro(e, expected_type);
+        return visit_node_choice_macro(e, false, expected_type);
+    } else if (get_name(mdata_data(e), "node_longest_choice!")) {
+        return visit_node_choice_macro(e, true, expected_type);
     } else {
         expr new_e = visit(mdata_expr(e), expected_type);
         return update_mdata(e, new_e);
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 35f31c0730..7cf18b00d4 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -238,7 +238,7 @@ private:
     expr visit_lambda(expr const & e, optional<expr> const & expected_type);
     expr visit_pi(expr const & e);
     expr visit_node_macro(expr const & e, optional<expr> const & expected_type);
-    expr visit_node_choice_macro(expr const & e, optional<expr> const & expected_type);
+    expr visit_node_choice_macro(expr const & e, bool longest_match, optional<expr> const & expected_type);
     expr visit_mdata(expr const & e, optional<expr> const & expected_type, bool is_app_fn);
     expr visit_app(expr const & e, optional<expr> const & expected_type);
     expr visit_let(expr const & e, optional<expr> const & expected_type);
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 08da284ec9..82f9f57872 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -97,7 +97,8 @@ void init_token_table(token_table & t) {
          {"@@", g_max_prec}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0},
          {"match", 0}, {"^.", g_max_prec+1}, {"::", 67},
-         {"renaming", 0}, {"extends", 0}, {"node!", g_max_prec}, {"node_choice!", g_max_prec}, {nullptr, 0}};
+         {"renaming", 0}, {"extends", 0}, {"node!", g_max_prec}, {"node_choice!", g_max_prec},
+         {"node_longest_choice!", g_max_prec}, {nullptr, 0}};
 
     char const * commands[] =
         {"theorem", "axiom", "axioms", "variable", "protected", "private", "hide",