test: document another elab issue

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