Test case for primEraseEquality (#5784)

agda · Mar 6, 2022 · 441026c · 441026c
1 parent 711df66
commit 441026c
Showing 1 changed file with 21 additions and 0 deletions.
diff --git a/test/Succeed/Issue5784.agda b/test/Succeed/Issue5784.agda
@@ -0,0 +1,21 @@
+-- Andreas, 2022-03-02, issue #5784, reported by Trebor-Huang
+-- Test case by Ulf Norell
+
+-- primEraseEquality needs to normalized the sides of the equation,
+-- not just reduce them.
+
+open import Agda.Builtin.Nat
+open import Agda.Builtin.Equality
+open import Agda.Builtin.Equality.Erase
+
+data Wrap : Set where
+  wrap : Nat → Wrap
+
+test : wrap (1 + 1) ≡ wrap 2
+test = primEraseEquality refl
+
+thm : test ≡ refl
+thm = refl
+
+-- Should succeed
+-- WAS: primEraseEquality refl != refl