From 757da9f6f36068fcf003ee4679d12f3e2f5f94c6 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 7 Aug 2022 18:36:43 +0200 Subject: [PATCH] fix: more accurate invalid shadowin error position --- src/Lean/Elab/Do.lean | 2 +- tests/lean/241.lean.expected.out | 22 +++++++++++----------- tests/lean/916.lean.expected.out | 2 +- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index a646ebc829..ac58c15224 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -1192,7 +1192,7 @@ def checkNotShadowingMutable (xs : Array Var) : M Unit := do let ctx ← read for x in xs do if ctx.mutableVars.contains x.getId then - throwInvalidShadowing x.getId + withRef x <| throwInvalidShadowing x.getId def withFor {α} (x : M α) : M α := withReader (fun ctx => { ctx with insideFor := true }) x diff --git a/tests/lean/241.lean.expected.out b/tests/lean/241.lean.expected.out index cb77a3487b..c6fb43ba65 100644 --- a/tests/lean/241.lean.expected.out +++ b/tests/lean/241.lean.expected.out @@ -1,13 +1,13 @@ -241.lean:3:2-3:14: error: mutable variable `xs` cannot be shadowed -241.lean:9:2-9:24: error: mutable variable `xs` cannot be shadowed -241.lean:16:4-16:12: error: mutable variable `xs` cannot be shadowed -241.lean:22:2-22:28: error: mutable variable `xs` cannot be shadowed -241.lean:28:2-28:18: error: mutable variable `xs` cannot be shadowed -241.lean:34:9-34:16: error: mutable variable `xs` cannot be shadowed -241.lean:41:9-41:16: error: mutable variable `xs` cannot be shadowed -241.lean:48:9-48:16: error: mutable variable `xs` cannot be shadowed -241.lean:58:6-58:27: error: mutable variable `xs` cannot be shadowed +241.lean:3:6-3:8: error: mutable variable `xs` cannot be shadowed +241.lean:9:7-9:9: error: mutable variable `xs` cannot be shadowed +241.lean:16:5-16:7: error: mutable variable `xs` cannot be shadowed +241.lean:22:7-22:9: error: mutable variable `xs` cannot be shadowed +241.lean:28:6-28:8: error: mutable variable `xs` cannot be shadowed +241.lean:34:14-34:16: error: mutable variable `xs` cannot be shadowed +241.lean:41:14-41:16: error: mutable variable `xs` cannot be shadowed +241.lean:48:14-48:16: error: mutable variable `xs` cannot be shadowed +241.lean:58:25-58:27: error: mutable variable `xs` cannot be shadowed 241.lean:67:8-67:10: error: mutable variable `xs` cannot be shadowed -241.lean:72:6-72:13: error: mutable variable `xs` cannot be shadowed +241.lean:72:7-72:9: error: mutable variable `xs` cannot be shadowed 241.lean:78:6-78:8: error: mutable variable `xs` cannot be shadowed -241.lean:84:2-86:17: error: mutable variable `xs` cannot be shadowed +241.lean:84:18-84:20: error: mutable variable `xs` cannot be shadowed diff --git a/tests/lean/916.lean.expected.out b/tests/lean/916.lean.expected.out index 0af62ee2f9..3ae055d157 100644 --- a/tests/lean/916.lean.expected.out +++ b/tests/lean/916.lean.expected.out @@ -1 +1 @@ -916.lean:3:2-3:19: error: mutable variable `x` cannot be shadowed +916.lean:3:7-3:8: error: mutable variable `x` cannot be shadowed