diff --git a/golden-tests/tests/eta-singleton/eta-sing.quox b/golden-tests/tests/eta-singleton/eta-sing.quox
index c3b1fc3..5ae2daf 100644
--- a/golden-tests/tests/eta-singleton/eta-sing.quox
+++ b/golden-tests/tests/eta-singleton/eta-sing.quox
@@ -27,7 +27,7 @@ namespace unrestricted {
 namespace linear {
   def0 ZZA : ★ = 1.ZZ → A
 
-  #[fail]
+  #[fail "λ _ ⇒ x reflZ is not equal to x"]
   def defeq : 0.(P : ZZA → ★) → 0.(x : ZZA) → P (λ _ ⇒ x reflZ) → P x =
     λ P x p ⇒ p
 }