From 1ecb234a9fbff80525d15857ee8628cea065007a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 21 Sep 2019 10:17:26 -0700
Subject: [PATCH] test(elabissues): document some of the known problems

---
 tests/elabissues/issues1.lean | 48 +++++++++++++++++++++++++++++++++++
 tests/elabissues/issues2.lean | 39 ++++++++++++++++++++++++++++
 tests/elabissues/issues3.lean | 23 +++++++++++++++++
 3 files changed, 110 insertions(+)
 create mode 100644 tests/elabissues/issues1.lean
 create mode 100644 tests/elabissues/issues2.lean
 create mode 100644 tests/elabissues/issues3.lean

diff --git a/tests/elabissues/issues1.lean b/tests/elabissues/issues1.lean
new file mode 100644
index 0000000000..a8e8cce4eb
--- /dev/null
+++ b/tests/elabissues/issues1.lean
@@ -0,0 +1,48 @@
+def f : List Int → Bool := fun _ => true
+
+def ex1 : Bool :=
+f [1, 2, 3]  -- Works
+
+def ex2 : Bool :=
+let xs := [1, 2, 3];
+/- The following application fails.
+   In the Lean3 elaborator, the `;` after `have` and `let` expressions is a "check-point".
+   The elaborator will resolve type class instances and force pending numeral types to `Nat` if they
+   have not been assigned yet.
+   So, `xs` will have type `List Nat`.
+   Solution: remove "check-point" from `let`, but keep the one on `have`. We use `have` expressions
+   when proving, and it is nice to make sure the proposition does not have meta-variables before continuing. -/
+f xs
+
+def ex3 : IO Bool :=
+do
+xs ← pure [1, 2, 3];
+pure $ f xs -- Works
+
+def ex4 :=
+[1, 2, 3].map $ fun x => x+1
+
+def ex5 (xs : List String) :=
+/- `r.push x` fails because we don't know the type of `r`.
+   Potential solution: the elaborator should suspend the elaboration of `fun r x => r.push x`,
+   elaborate `Array.empty`, and then resume the suspension.
+-/
+xs.foldl (fun r x => r.push x) Array.empty
+
+inductive Expr
+| val : Nat → Expr
+| app : Expr → Expr → Expr
+
+instance : HasCoe Nat Expr := ⟨Expr.val⟩
+
+def foo : Expr → Expr := fun e => e
+
+def ex6 :=
+/- `1` is elaborated to `HasOne.one ?A ?S : ?A`.
+    Typing constraints unify `?A =?= Expr`, and
+    we fail to synthesize `HasOne Expr`.
+    Users get confused since they have defined `HasCoe Nat Expr`.
+    Solution: elaborate `1` into `Expr.lit (Literal.natVal 1) : Nat`,
+    and rely on coercions.
+-/
+foo 1
diff --git a/tests/elabissues/issues2.lean b/tests/elabissues/issues2.lean
new file mode 100644
index 0000000000..9842c31f17
--- /dev/null
+++ b/tests/elabissues/issues2.lean
@@ -0,0 +1,39 @@
+inductive Syntax
+| atom : String → Syntax
+| node : String → Array Syntax → Syntax
+
+instance coe1 : HasCoe String Syntax := ⟨Syntax.atom⟩
+instance coe2 {α} : HasCoe (List α) (Array α) := ⟨List.toArray⟩
+
+def ex7 : Syntax :=
+/-
+We try to elaborate `["bla"]` with expected type `Array Syntax`.
+The expected type is "discarded" since we fail to unify `Array Syntax =?= List ?A`
+where `List ?A` is the resulting type for `List.cons` application before we process its children.
+Remark: the elaborator does **not** try to use coercions here. Even if it tried, it would fail since
+`List ?A` contains a meta-variable.
+Then, we elaborate `["bla"]` without an expected type and produce a term of type `List String`.
+Finally, we fail with a type mismatch between `List String` and `Array Nat`.
+We can make it work by using:
+```
+instance coe3 {α β} [HasCoe α β] : HasCoe (List α) (Array β) := ⟨fun xs => (xs.map (fun x => (coe x : β))).toArray⟩
+```
+-/
+Syntax.node "foo" ["bla"]
+
+def ex8 : Syntax :=
+Syntax.node "foo" (List.toArray ["boo"]) -- Works
+
+def ex9 : Syntax :=
+/-
+We need the type of `["boo"]` to be able to apply `.toArray`.
+So, we elaborate `["boo"]` first without expected type, and then
+obtain `Array String`, and then a type mismatch between
+`Array String` and `Array Syntax`.
+We can make it work by using:
+```
+instance coe3 {α β} [HasCoe α β] : HasCoe (Array α) (Array β) := ⟨fun xs => (xs.map (fun x => (coe x : β)))⟩
+```
+But, the behavior is still confusing to users.
+-/
+Syntax.node "foo" ["boo"].toArray
diff --git a/tests/elabissues/issues3.lean b/tests/elabissues/issues3.lean
new file mode 100644
index 0000000000..76e0af5166
--- /dev/null
+++ b/tests/elabissues/issues3.lean
@@ -0,0 +1,23 @@
+inductive Syntax
+| atom : String → Syntax
+| node : String → Array Syntax → Syntax
+
+instance coe1 : HasCoe String Syntax := ⟨Syntax.atom⟩
+instance coe2 {α} : HasCoe (List α) (Array α) := ⟨List.toArray⟩
+
+def ex10 (s : Syntax) : Syntax :=
+Syntax.node "foo" (List.toArray ["boo", s]) -- Works
+
+def ex11 (s : Syntax) :=
+[s, "foo"] -- Works
+
+def ex12 (s : Syntax) :=
+/-
+We don't know the expected type. Before elaborating the `List.cons` applications we know
+that the resulting type is `List ?A`. Then, we elaborate `"foo"`, and set `?A := String`.
+Then, we fail when we try to elaborate `s` since there is not coercion from `Syntax` to `String`.
+Potential solution: add special support for polymorphic nested applications such as `List.cons`, `HasAdd.add`, etc.
+Disclaimer: not sure whether we will create even more problems since all nested arguments would have to
+be elaborated without an expected type. Perhaps, combined with the "suspension" mechanism it will work great.
+-/
+["foo", s]