Failure to elab a match statement in a command

Stream: lean4

[Michael Jam]

I am trying to compile and add a function definition to the environment, from a command. That definition contains a match statement.
However it silently fails to compile my definition and I don't know how to investigate the error.
Here is a mwe :

import Lean
open Lean Elab Command Term Meta

inductive I where
  | c1

def f1 : Nat :=
match I.c1 with
  | I.c1 => Nat.zero
#print f1

def gen_f2 : CommandElabM Unit := do
  let type <- termStxToExpr .none <| <- `(Nat)
  let val <- termStxToExpr (.some type) <| <- `(
    match I.c1 with
      | I.c1 => Nat.zero
    )
  let decl := Declaration.defnDecl <| mkDefinitionValEx `f2 [] type val .opaque .safe
  match (<- getEnv).addAndCompile {} decl with
  | .error e => throwError (e.toMessageData {})
  | .ok env => setEnv env
  where
    termStxToExpr (expectedType? : Option Expr) (stx : Syntax) :=
      elabTerm stx expectedType? |> TermElabM.run' |> MetaM.run' |> liftCoreM

elab "gen_f2" : command => gen_f2
-- set_option trace.Elab true
gen_f2
#print f2

The code doesn't fail to compile but #print f2 says:

def f2 : Nat :=
let _discr := I.c1;
sorryAx Nat

When I expect it to show the same as #print f1 which says:

def f1 : Nat :=
match I.c1 with
| I.c1 => Nat.zero

The issue here seems to happen when converting the match syntax to an Expr but I'm not sure.

What I'm really trying to do behind that mwe is to implement an attribute that automatically generates the .rec implementation of an inductive type. For some reason .rec has no implementation whereas match has one, to me it's really weird because as I see it, everything should be defined from .rec.

Thanks for suggestions

[Sebastian Ullrich]

I do get an error message at gen_f2

auxiliary declaration cannot be created when declaration name is not available

Use liftTermElabM

    termStxToExpr (expectedType? : Option Expr) (stx : Syntax) :=
      elabTerm stx expectedType? |> liftTermElabM `f2

[Sebastian Ullrich]

For some reason .rec has no implementation whereas match has one, to me it's really weird because as I see it, everything should be defined from .rec.

That may be true for the core language, but for code generation going through rec is awkward, especially for well-founded recursion