Processing sepBy's

Stream: lean4

[Siddharth Bhat]

Suppose I have a syntax category called kvbare of string key-values, given by the syntax key===value. I now want to create a macro for a "dictionary", which is given by <[ key1 === value, key2 === value2, ..., keyn === valuen ]>. The macro should desugar into List (String × String). Here's what I have so far:

declare_syntax_cat kvbare
syntax str "===" str  : kvbare

syntax "kvbare% " kvbare : term
macro_rules
  | `(kvbare% $i:strLit ===  $j:strLit ) => `( ($i , $j) )

def foobare := (kvbare%  "foobare"  ===  "barbare" )

declare_syntax_cat dict
syntax "<[" sepBy(kvbare, ",") "]>" : dict

syntax "dict% " dict : term
macro_rules
  | `(dict% <[ $kvs,* ]> ) => do
     let initList <- `([])
     kvs.getElems.foldlM (init := initList) fun xs kv => `((kvbare% $kv) :: $xs )

def dict0 : List (String×String) := (dict% <[  ]> )
#print dict0

def dict1 : List (String×String) := (dict% <[ "foo" === "bar" ]> )
#print dict1


def dict2 : List (String×String) := (dict% <[ 1 === 2 ]> )
#print dict2

This works properly on dict0 and dict1, and correctly errors on dict2, since the key and value are int, not string. I have a few questions at this stage:

1. What are the special features of the MacroM monad? For one, one can use quoting inside the MacroM context. Are the functions I should be aware of / are commonly used, as a macro author?
2. The error for dict2 is:

crash.lean:37:46: error: expected ']>'
def dict2 : List (String × String) :=
[]

is it possible to add hints to produce a more precise error? I would have expected an error of the form expected kvbare pointing at 1 === 2. I understand if this is difficult/impossible due to the complexity of the LEAN parser.