fix: add basic support for accessing the field of a section variable in the notation prechecker

see #435

src/Lean/Elab/Quotation/Precheck.lean

@@ -77,16 +77,32 @@ def runPrecheck (stx : Syntax) : TermElabM Unit := do
   if quotPrecheck.get opts && hygiene.get opts then
     precheck stx |>.run { quotLCtx := {} }
 
-@[builtinQuotPrecheck ident] def precheckIdent : Precheck
+private def isSectionVariable (e : Expr) : TermElabM Bool := do
+  return (← read).sectionFVars.any fun _ v => e == v
+
+@[builtinQuotPrecheck ident] def precheckIdent : Precheck := fun stx =>
+  match stx with
   | Syntax.ident info rawVal val preresolved => do
     if !preresolved.isEmpty then
       return
+    /- The precheck currently ignores field notation.
+       For example: the following notation is accepted although `foo` is not a valid field name for a `Nat` value.
+       ```
+       def x := 0
+       notation "x++" => x.foo
+       ```
+    -/
     if let _::_ ← resolveGlobalName val then
       return
     if (← read).quotLCtx.contains val then
       return
-    if quotPrecheck.allowSectionVars.get (← getOptions) && (← readThe Term.Context).sectionVars.contains val then
-      return
+    let rs ← try resolveName stx val [] [] catch _ => pure []
+    for (e, _) in rs do
+      match e with
+      | Expr.fvar fvarId .. =>
+        if quotPrecheck.allowSectionVars.get (← getOptions) && (← isSectionVariable e) then
+          return
+      | _ => pure ()
     throwError "unknown identifier '{val}' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check."
   | _ => throwUnsupportedSyntax
 

tests/lean/435b.lean

@@ -0,0 +1,10 @@
+structure Op (α : Type _) where op : α → α → α
+variable {α}
+variable (s : Op α)
+local infixr:60 " ∙ " => s.op
+local infixr:60 " ∙1 " => s.op1 -- TODO: generate error
+
+def x := 0
+
+notation "x++" => x.succ
+notation "x++" => x.foo  -- TODO: generate error