A match expression as example return type triggers lean.unknownIdentifier error

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

This should be accepted:

example (x : Bool) :
    match x with
    | true  => String
    | false => Nat
  :=
  match x with
  | true => "hello"
  | false => (42: Nat)

It currently fails with

Unknown constant `_example.match_1`
Error code: lean.unknownIdentifier

Context

It is accepted if I turn example into def foo.

It is also accepted if I use a let to name the return type:

example (x : Bool) :
    let τ := match x with
      | true  => String
      | false => Nat
    τ
  :=
  match x with
  | true => "hello"
  | false => (42: Nat)

Steps to Reproduce

1. Write any example having as its return type a match expression.

Expected behavior: No errors.

Actual behavior: An error is triggered. Apparently the match is compiled as an internal identifier which is however not in scope where it should be.

Versions

Lean 4.30.0-nightly-2026-03-19
Target: x86_64-unknown-linux-gnu

Start by reproducing the minimal example in Lean nightly and compare it with the working def foo and let variants. Trace how the example's match return type is handled, then verify that the original example is accepted without a lean.unknownIdentifier error.