Errors in `do`-notation pattern variables swallowed by "unsupported syntax pattern"

[david-christiansen]

Description

Ambiguous name errors while pattern matching in do-notation are swallowed and replaced by an unrelated message about syntax pattern matching.

Context

This occurred while migrating Verso code to a Lean version that included parts of Verso upstreamed. This led to ambiguous name issues when the old code was incompletely deleted that were very difficult to diagnose.

Steps to Reproduce

1. Enter the following code:

   inductive A where | a
   inductive AA where | a
   
   open A in
   open AA in
   def f (x : Option Nat) : Id Nat := Id.run do
     if let some a := x then
       22
     else
       33
   
   

2. Observe the error:

   unsupported pattern in syntax match
     some a
   

   No syntax matching is occurring.
3. Remove the do-notation:

   inductive A where | a
   inductive AA where | a
   
   open A in
   open AA in
   def f (x : Option Nat) : Id Nat :=
     if let some a := x then
       22
     else
       33
   

4. Observe the error:

   ambiguous pattern, use fully qualified name, possible interpretations [AA.a, A.a]
   

Expected behavior: I would expect the error messages to be identical

Actual behavior: Using do-notation results in a much worse error message.

Versions

This is present in 4.24.0, 4.24.0-rc1, and nightly-2025-09-14

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[david-christiansen]

This is related to #2215, but it's triggered by a semantic error rather than a syntactic one. It may be the same as #8304, though it is triggered differently and the error occurs at the correct location.