From e7aa785822674cf872df82bf18e501cc424fee54 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 27 Feb 2026 02:17:27 +0100 Subject: [PATCH] chore: tighten a do match elaborator test case to prevent global defaulting (#12675) This PR enshrines that the do `match` elaborator does not globally default instances, in contrast to the term `match` elaborator. --- tests/elab/newdo.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tests/elab/newdo.lean b/tests/elab/newdo.lean index d5b160790a..6d5a4a8356 100644 --- a/tests/elab/newdo.lean +++ b/tests/elab/newdo.lean @@ -484,12 +484,13 @@ example (cache : Std.HashMap (Nat × Nat) Bool) : Bool := Id.run do let := cache.contains key return false --- Extracted from MathlibTest.random.lean. The problem here is that the `for` loop macro used to --- expand `for _ in [:0] do body` to `for x✝ in [:0] do match x✝ with | _ => body` and that caused --- defaulting of `count` to `Nat`. +-- Extracted from MathlibTest.random.lean. The problem here is that the `match` elaborator used to +-- destructure the `(x, y)` pattern into `x` and `y` caused defaulting of `count` to `Nat`. +-- Nowadays, the `match` elaborator does not trigger global defaulting (in constrast to the term +-- `match` elaborator), fixing this test case. example : IO Bool := do let mut count := 0 - for _ in [:0] do count := count + 1 + for (x, y) in ([] : List (Nat × Nat)) do count := count + 1 return Float.abs count > 0 end Repros