weird type mismatch error location

Stream: lean4

[Edward van de Meent]

i was going along metaprogramming when suddenly i noticed something... in the following example, the "type mismatch" error occurs in (what i think is) the wrong spot:

import Lean
open Lean Elab Meta Command Tactic

syntax foo := (ppSpace "(" ident " foo " tactic ")" )*

structure Foo where

def elabFoo : Syntax → CommandElabM Unit
  | `(foo| $[($ids foo $tac)]*) => do -- error on `tac`
    let mut userArgs : NameMap Term := {}
    for (name, t) in (ids.map (·.getId)).zip tac do -- while i'd expect it here
      userArgs := userArgs.insert name t
  | _ => throwUnsupportedSyntax

[Edward van de Meent]

is this a bug?

[Edward van de Meent]

and if so, is this a bug with core, or with the vscode extension?

[Aaron Liu]

This seems to be a bug with core

[Kyle Miller]

Thanks, reported it: lean4#7837

Technically the bug is in your code :smile: But I do agree that core's matching code is missing something here. The syntax quotation matching works by expanding the code like a macro, creating some new syntax, and somewhere this syntax must be missing a type ascription to act as a "checkpoint" to prevent types from propagating backwards into the generated matching code.