From 69005777238ee8440cebc19c397e1d3d36136d31 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Feb 2020 10:41:12 -0800 Subject: [PATCH] doc: document issue AFAICT, it has been solved in the new frontend. See new test. cc @dselsam --- .../anonymous_constructor_error_msg.lean | 9 +++++++++ tests/lean/run/anonymous_ctor_error_msg.lean | 15 +++++++++++++++ 2 files changed, 24 insertions(+) create mode 100644 tests/lean/run/anonymous_ctor_error_msg.lean diff --git a/tests/elabissues/anonymous_constructor_error_msg.lean b/tests/elabissues/anonymous_constructor_error_msg.lean index ede12c5d08..55034f8449 100644 --- a/tests/elabissues/anonymous_constructor_error_msg.lean +++ b/tests/elabissues/anonymous_constructor_error_msg.lean @@ -2,6 +2,15 @@ This is an annoyingly unhelpful error message that I see all the time. An exact line number would help a lot, but even so it would be great to replace the `⟨...⟩` with the actual term in question. + +[Leo]: The bad position is due the transition to the new elaborator. +The new frontend produces the correct position. +Note that, the new frontend reports an error at `⟨4⟩`. This is the correct +position, and it is not possible to infer anything about the expected type since +`x4` is not used anywhere. So, the error message is the best we can get. +There is no actual term to replace. If we comment the line `let x4 := ...`, +the new elaborator succeeds. + -/ structure Foo := (n : Nat) diff --git a/tests/lean/run/anonymous_ctor_error_msg.lean b/tests/lean/run/anonymous_ctor_error_msg.lean new file mode 100644 index 0000000000..8c1791e269 --- /dev/null +++ b/tests/lean/run/anonymous_ctor_error_msg.lean @@ -0,0 +1,15 @@ +structure Foo := (n : Nat) + +def Foo.sum (xs : List Foo) : Foo := +xs.foldl (λ s x => ⟨s.n + x.n⟩) ⟨0⟩ + +new_frontend + +#check +let x1 := ⟨1⟩; +let x2 := ⟨2⟩; +let x3 := ⟨3⟩; +-- let x4 := ⟨4⟩; -- If this line is uncommented we get the error at `⟨` +let x5 := ⟨5⟩; +let x6 := ⟨6⟩; +Foo.sum [x1, x2, x3, x5, x6]