From 3d1571896c477bf06d709bd6d8a958529c22875b Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 29 Nov 2022 17:14:52 -0800
Subject: [PATCH] fix: support escaped field names in dot-notation

---
 src/Lean/Elab/App.lean                  | 6 +++---
 tests/lean/run/fieldNamesWithMinus.lean | 7 +++++++
 2 files changed, 10 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/fieldNamesWithMinus.lean

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index edc7fb78ba..f4f2306e97 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -1291,8 +1291,8 @@ where
 
   toLVals : List Syntax → (first : Bool) → List LVal
     | [],            _     => []
-    | field::fields, true  => .fieldName field field.getId.toString (toName (field::fields)) fIdent :: toLVals fields false
-    | field::fields, false => .fieldName field field.getId.toString none fIdent :: toLVals fields false
+    | field::fields, true  => .fieldName field field.getId.getString! (toName (field::fields)) fIdent :: toLVals fields false
+    | field::fields, false => .fieldName field field.getId.getString! none fIdent :: toLVals fields false
 
 /-- Resolve `(.$id:ident)` using the expected type to infer namespace. -/
 private partial def resolveDotName (id : Syntax) (expectedType? : Option Expr) : TermElabM Name := do
@@ -1333,7 +1333,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     let elabFieldName (e field : Syntax) := do
       let newLVals := field.identComponents.map fun comp =>
         -- We use `none` in `suffix?` since `field` can't be part of a composite name
-        LVal.fieldName comp (toString comp.getId) none e
+        LVal.fieldName comp comp.getId.getString! none e
       elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
     let elabFieldIdx (e idxStx : Syntax) := do
       let some idx := idxStx.isFieldIdx? | throwError "invalid field index"
diff --git a/tests/lean/run/fieldNamesWithMinus.lean b/tests/lean/run/fieldNamesWithMinus.lean
new file mode 100644
index 0000000000..391cecdeac
--- /dev/null
+++ b/tests/lean/run/fieldNamesWithMinus.lean
@@ -0,0 +1,7 @@
+structure Minus where
+  «i-love-lisp» : Bool
+
+#check Minus.«i-love-lisp»
+#check { «i-love-lisp» := true : Minus }
+#check fun (x : Minus) => x.«i-love-lisp»
+#check fun (x : Minus) => (x).«i-love-lisp»