From 104b4a1ce2da525f3686d362ca2f0b3ba12606c7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 15 Oct 2019 09:40:44 -0700
Subject: [PATCH] test: document another elab issue

---
 tests/elabissues/issues8.lean | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 tests/elabissues/issues8.lean

diff --git a/tests/elabissues/issues8.lean b/tests/elabissues/issues8.lean
new file mode 100644
index 0000000000..fea4289061
--- /dev/null
+++ b/tests/elabissues/issues8.lean
@@ -0,0 +1,24 @@
+def forceNat (a : Nat) := true
+def forceInt (a : Int) := false
+
+def f1 :=
+/-
+The following example works, but it adds a coercion at `forceInt i`.
+The elaborated term is
+```
+fun (n i : Nat) => if n == i then forceNat n else forceInt (coe i)
+-/
+fun n i => if n == i then forceNat n else forceInt i -- works
+
+def f2 :=
+fun n i => if coe n == i then forceInt i else forceNat n -- works
+
+#check f1 -- Nat → Nat → Bool
+#check f2 -- Nat → Int → Bool
+
+def f3 :=
+/- Fails.
+   - `n == i` generates type constraint enforcing `n` and `i` to have the same type.
+   - `forceInt i` forces `i` (and consequently `n`) to have type `Int`.
+   - `forceNat n` fails because there is no coercion from `Nat` to `Int`. -/
+fun n i => if n == i then forceInt i else forceNat n