Add examples that demonstrate limitations of the current elaborator. The new design, we are working on, will be able to solve them.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

tests/lean/bad/t1.lean

@@ -0,0 +1,24 @@
+Variable g : Pi A : Type, A -> A.
+Variables a b : Int
+(*
+The following example demonstrates a limitation in the current elaborator.
+The current elaborator decides overloads before filling holes.
+The symbol '>' is overloaded. The possible overloads are:
+    Nat::lt   Nat -> Nat -> Nat
+    Int::lt   Int -> Int -> Int
+    Real::lt  Real -> Real -> Real
+The type of (g _ a) is not available when the overload is decided, and
+0 has type Nat. Then, the overload resolver selects
+    Nat::lt   Nat -> Nat -> Nat
+Now, when we fill the holes, (g _ a) is elaborated to (g Int a) which
+has type Int, and we fail.
+If the hole elaborator and overload resolver are executed simultaneously,
+we would get the fully elaborated term:
+
+    Int::le (g Int a) (nat_to_int 0)
+*)
+Axiom H1 : g _ a > 0
+(*
+One workaround consists in manually providing the coercion.
+*)
+Axiom H1 : g _ a > (nat_to_int 0)

tests/lean/bad/t2.lean

@@ -0,0 +1,36 @@
+Variable list : Type -> Type
+Variable nil  {A : Type} : list A
+Variable cons {A : Type} (head : A) (tail : list A) : list A
+Definition n1 : list Int := cons (nat_to_int 10) nil
+Definition n2 : list Nat := cons 10 nil
+(*
+The following example demonstrates that the expected type (list Int)
+does not influece whether coercions are used or not.
+*)
+Definition n3 : list Int := cons 10 nil
+
+(*
+Here are some workarounds for the example above.
+The 'let' construct is one of the main tools for providing
+hints.
+*)
+Definition n3a : list Int :=
+           let a : Int := 10
+           in cons a nil
+
+(* Solution b: we manually provide the coercion *)
+Definition n3b : list Int := cons (nat_to_int 10) nil
+
+(* The folowing example works *)
+Definition n4 : list Int := nil
+
+(*
+The following example demonstrates that we do not do type inference.
+In the current implementation, we first elaborate the type and
+then the body.
+*)
+Definition n5 : _ := cons 10 nil
+
+Set pp::coercion true
+Set pp::implicit true
+Show Environment 1.

tests/lean/bad/t3.lean

@@ -0,0 +1,12 @@
+Variable list : Type -> Type
+Variable nil  {A : Type} : list A
+Variable cons {A : Type} (head : A) (tail : list A) : list A
+Variables a b : Int
+Variables n m : Nat
+(*
+Here are other examples showing that coercions and implicit arguments
+do not "interact well with each other" in the current implementation.
+*)
+Definition l1 : list Int := cons a (cons b (cons n nil))
+Definition l2 : list Int := cons a (cons n (cons b nil))
+Check cons a (cons b (cons n nil))