From b347f4868bb7c68e3021d8014027512aec8ba646 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 3 May 2015 21:05:32 -0700 Subject: [PATCH] test(tests/lean/eq_class_error): save "workaround" for cryptic error message --- tests/lean/eq_class_error.lean | 15 +++++++++++++++ tests/lean/eq_class_error.lean.expected.out | 7 +++++++ 2 files changed, 22 insertions(+) create mode 100644 tests/lean/eq_class_error.lean create mode 100644 tests/lean/eq_class_error.lean.expected.out diff --git a/tests/lean/eq_class_error.lean b/tests/lean/eq_class_error.lean new file mode 100644 index 000000000..2c0cc5fd2 --- /dev/null +++ b/tests/lean/eq_class_error.lean @@ -0,0 +1,15 @@ +inductive foo := +| a | b + +open foo + +-- This test demonstrates we need to disable local instances. +set_option elaborator.local_instances false + +definition decidable_eq_foo [instance] : ∀ f₁ f₂ : foo, decidable (f₁ = f₂) +| a a := by left; reflexivity +| a b := by right; contradiction +| b a := by right; contradiction +-- If we don't disable the local_instances, then type class resolution synthesizes the term (decidable_eq_foo b b) which is not a +-- valid "recursive application", and the recursive equation compiler fails with a cryptic message saying we should try to use well-founded recursion. +| b b := _ diff --git a/tests/lean/eq_class_error.lean.expected.out b/tests/lean/eq_class_error.lean.expected.out new file mode 100644 index 000000000..28e650db7 --- /dev/null +++ b/tests/lean/eq_class_error.lean.expected.out @@ -0,0 +1,7 @@ +eq_class_error.lean:15:10: error: don't know how to synthesize placeholder +decidable_eq_foo : Π (f₁ f₂ : foo), decidable (f₁ = f₂) +⊢ decidable (b = b) +eq_class_error.lean:9:11: error: failed to synthesize placeholder + +⊢ Π (f₁ f₂ : foo), + decidable (f₁ = f₂)