refer to unnamed (hygienic) section variables in notations

Stream: lean4

[George Pîrlea]

I have a DSL where I define some section variables behind the user's back, so to speak, and I want to define notations to hide these away, but I can't figure out how to do it. Here's a MWE:

import Lean
open Lean Parser Elab Command

set_option quotPrecheck false

def toFnName (id : Ident) : Ident :=
  mkIdent (id.getId ++ `fn)

elab "function" nm:ident br:(bracketedBinder)* "=" dfn:term : command => do
  elabCommand $ ← runTermElabM fun _ => do
    `(command|def $(toFnName nm) $br* := $dfn)
  elabCommand $ ← runTermElabM fun vs => do
    let args ← vs.mapM (fun v => do
    let t ← PrettyPrinter.delab v ; dbg_trace "{t}" ; return t)
    let strName ← `(Lean.Parser.Command.notationItem|$(Lean.quote nm.getId.toString):str)
    `(local notation (priority := default) $strName => @$(toFnName nm) $args*)

variable (t : Type) [DecidableEq t]

set_option trace.Elab.command true
-- defines `local notation (priority := default) "foo" => @foo.fn t inst✝`
-- ... which throws an error when applied because `inst✝` is not a valid name
function foo (x : t) = (x = x)
#check foo.fn -- OK
#check foo    -- unknown identifier 'inst✝'

How can I refer to inst✝ (the DecidableEq instance) when I define the notation? Or maybe figure out when there is a hygienic name and try to synthesise the appropriate instance (but this might not always work)?

Perhaps there's a better solution to my problem than notations?

Any help is appreciated.

[George Pîrlea]

This is a work-around, but I can imagine this not always working:

let args ← vs.mapM (fun v => do
  let t ← PrettyPrinter.delab v
  let isHygienicName := (extractMacroScopes t.raw.getId).scopes.length > 0
  if isHygienicName then return ← `(term|_) else return t
)