diff --git a/tests/lean/423.lean b/tests/lean/423.lean
index deb28a5bbb..2332ef6f67 100644
--- a/tests/lean/423.lean
+++ b/tests/lean/423.lean
@@ -1,3 +1,5 @@
 universe u
 
 #check fun {T : Sort u} (a : T) => a + 0
+
+#check fun {T : Sort u} (a : T) [Add T] [OfNat T 0] => a + 0
diff --git a/tests/lean/423.lean.expected.out b/tests/lean/423.lean.expected.out
index a47588e229..72f19f0263 100644
--- a/tests/lean/423.lean.expected.out
+++ b/tests/lean/423.lean.expected.out
@@ -6,3 +6,27 @@ has type
   T : Sort u
 but is expected to have type
   Nat : Type
+423.lean:5:33-5:38: error: application type mismatch
+  Add T
+argument
+  T
+has type
+  Sort u : Type u
+but is expected to have type
+  Type ?u : Type (?u + 1)
+423.lean:5:41-5:50: error: application type mismatch
+  OfNat T
+argument
+  T
+has type
+  Sort u : Type u
+but is expected to have type
+  Type ?u : Type (?u + 1)
+423.lean:5:55-5:60: error: application type mismatch
+  HAdd.hAdd a
+argument
+  a
+has type
+  T : Sort u
+but is expected to have type
+  Nat : Type