Incorrect macro expansion(?) in doElem macro

Stream: metaprogramming / tactics

[Jannis Limperg]

A student of mine is trying to write a macro that transforms a match in a monadic context (i.e., the match is a doElem) into a different match. However, something seems to be going wrong when the macro is run: the new match gets a different right-hand side than the old match, even though we're not modifying the matchAlts at all. MWE:

import Lean

open Lean Lean.Parser Lean.Parser.Term

attribute [run_parser_attribute_hooks] matchAltExpr

macro "match_expri " t:term " with " alts:matchAltExpr* : doElem => do
  `(doElem| match $t:term with $alts:matchAlt*)

run_meta
  show MetaM Expr from do
  match_expri (Expr.const `True []) with
  | e => return e
/-
application type mismatch
  pure PUnit.unit
argument
  PUnit.unit
has type
  PUnit : Sort ?u.807
but is expected to have type
  Expr : Type
-/

Tracing shows that at some point during elaboration, the return e becomes return PUnit.unit. But I have no idea why this happens. @Sebastian Ullrich can you maybe help?

[Daniel Weber]

This causes a crash :thinking:

import Lean

open Lean Lean.Parser Lean.Parser.Term

attribute [run_parser_attribute_hooks] matchAltExpr

macro "match_expri " t:term " with " alts:matchAltExpr* : doElem => do
  `(doElem| match $t:term with $alts:matchAlt*)

set_option trace.Elab.match_syntax true

axiom test : False

run_meta
  show MetaM Expr from do
  match_expri test with

[Jannis Limperg]

The match elaborator might (reasonably) rely on the fact that there's no closed term of type False. So this might be unrelated.

[Daniel Weber]

I thought using match there works, but now it doesn't seem to

[Thomas Murrills]

I think this has to do with the fact that matchAltExpr parses a term on the rhs of the match alt, when you want to parse a doSeq. matchAlt(s) takes a default argument (rhsParser := termParser), and matchAltExpr is a thin wrapper around that; likewise, doMatchAlts is a thin wrapper around matchAlts (rhsParser := doSeq).

(Lean doesn't like the direct macro version of this, though—I'm guessing because doMatchAlts haven't been prepped for use in quotations.) (lead precedence is cargo-culted from other matches.)

import Lean

open Lean Lean.Parser Lean.Parser.Term

syntax:lead (name := matchExpri) "match_expri " term " with " doMatchAlts : doElem

macro_rules
| `(doElem|match_expri $t:term with $alts) => `(doElem|match $t:term with $alts)

#eval -- Lean.Expr.const `True []
  show MetaM Expr from do
    match_expri (Expr.const `True []) with
    | e => return e