From 2cbdd637c7c8a4b1c44f835a862fcff0a66b20fe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 25 Apr 2021 10:35:23 -0700
Subject: [PATCH] test: add second example for issue #423

---
 tests/lean/423.lean              |  2 ++
 tests/lean/423.lean.expected.out | 24 ++++++++++++++++++++++++
 2 files changed, 26 insertions(+)

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