chore(tests/lean): fix tests

Remarks:
- Some tests do not produce error messages anymore because they can be
  processed using the new equation compiler preprocessor.

- Some error messages got worse because of the preprocessing step.
  We use metavariables in the preprocessing step. This information
  may "leak" to users. Another problem is that some variable names
  are lost. Example: in the following definition

  def to_nat : ∀ {n}, fi n → nat
  | (succ n) f0     := 0
  | (succ n) (fs i) := succ (to_nat i)

  The preprocessing step uses metavariables for pattern variables.
  Thus, we have

  def to_nat : ∀ {n}, fi n → nat
  | (succ ?n) (@f0 ?x)    := 0
  | (succ ?n) (@fs ?x ?i) := succ (to_nat i)

  when solving the constraint `succ ?n =?= succ ?x`, Lean assigns
        ?n := ?x
  after solving these constraints, the preprocessor converts
  metavariables into pattern variables again, and we have

  def to_nat : ∀ {n}, fi n → nat
  | (succ x) (@f0 x)   := 0
  | (succ x) (@fs x i) := succ (to_nat i)

  So, we get the following equation lemmas:

  to_nat.equations._eqn_1 : ∀ (x : ℕ), @to_nat (succ x) (@f0 x) = 0
  to_nat.equations._eqn_2 : ∀ (x : ℕ) (i : fi x), @to_nat (succ x) (@fs x i) = succ (@to_nat x i)

  instead of

  to_nat.equations._eqn_1 : ∀ (n : ℕ), @to_nat (succ n) (@f0 n) = 0
  to_nat.equations._eqn_2 : ∀ (n : ℕ) (i : fi n), @to_nat (succ n) (@fs n i) = succ (@to_nat n i)

tests/lean/bad_error2.lean

@@ -4,7 +4,8 @@ example {k n m : ℕ} (h : k + n ≤ k + m) : n ≤ m :=
 match le.dest h with
 | ⟨w, hw⟩ := @le.intro _ _ w
     begin
-      -- in the following error pp.beta is automatically disabled
+      -- hw is beta reduced after we added the equation compiler preprocessor.
+      -- So, this test is not really relevant anymore.
       rw [nat.add_assoc] at hw,
       apply nat.add_left_cancel hw
     end

tests/lean/bad_error2.lean.expected.out

@@ -1,9 +0,0 @@
-bad_error2.lean:8:6: error: rewrite tactic failed, did not find instance of the pattern in the target expression
-  ?m_1 + ?m_2 + ?m_3
-state:
-k n m : ℕ,
-h : k + n ≤ k + m,
-_match : (∃ (k_1 : ℕ), k + n + k_1 = k + m) → n ≤ m,
-w : ℕ,
-hw : (λ (k_1 : ℕ), k + n + k_1 = k + m) w
-⊢ n + w = m

tests/lean/bad_inaccessible.lean

@@ -1,3 +1,4 @@
+-- These definitions can be processed by the new equation compiler without producing errors.
 universe variables u
 definition f1 : nat → nat → nat
 | a .(a) := a

tests/lean/bad_inaccessible.lean.expected.out

@@ -1,7 +0,0 @@
-bad_inaccessible.lean:3:6: error: invalid use of inaccessible term, it is not fixed by other arguments
-bad_inaccessible.lean:6:8: error: invalid use of inaccessible term, the provided term is
-  b
-but is expected to be
-  a
-bad_inaccessible.lean:14:2: error: invalid use of inaccessible term, it is not completely fixed by other arguments
-  .?m_1 + 1

tests/lean/bad_inaccessible2.lean

@@ -8,24 +8,14 @@ open vec
 variables {A : Type u}
 variables f : A → A → A
 
-/- The following definition fails because the pattern variables are
-   introduced in the following order:
-         a va n b vb
-   However, the type of va must be (vec A n). That is, it depends
-   on a variable introduced after va.
-
-   The error message is confusing.
-
-   Alternatives:
-   1- Ignore the problem since this is a very obscure use of inaccessible terms.
-   2- Reorder variables based on their occurrence in inaccessible terms.
-      If we do that, the variables in the pattern will be ordered as:
-            n a va b vb
-      and this example will work. This is not fully satisfactor since
-      we can create another declaration where this heuristic is not the right
-      solution.
-   3- Produce a better error message.
+/- The new equation compiler can process this example.
+   So, this is not a test about error messages anymore.
 -/
-definition map_head : ∀ {n}, vec A n → vec A n → vec A n
+def map_head : ∀ {n}, vec A n → vec A n → vec A n
 | .(0)     nil nil                       := nil
 | .(n+1) (@cons .(A) .(n) a va) (@cons .(A) n b vb) := cons (f a b) va
+
+/- The following shorter version is also accepted. -/
+def map_head2 : ∀ {n}, vec A n → vec A n → vec A n
+| _ nil         nil         := nil
+| _ (cons a va) (cons b vb) := cons (f a b) va

tests/lean/bad_inaccessible2.lean.expected.out

@@ -1,9 +0,0 @@
-bad_inaccessible2.lean:31:2: error: type mismatch at application
-  map_head (cons a va) (cons b vb)
-term
-  cons b vb
-has type
-  vec .?m_1 (n + 1)
-but is expected to have type
-  vec A . (.?m_1 + 1)
-bad_inaccessible2.lean:31:52: error: ill-formed match/equations expression

tests/lean/bad_pattern2.lean.expected.out

@@ -8,4 +8,4 @@ has type
   _
 but is expected to have type
   ℕ
-bad_pattern2.lean:2:10: error: ill-formed match/equations expression
+bad_pattern2.lean:2:10: error: ill-formed match/equation expression

tests/lean/def_inaccessible_issue.lean.expected.out

@@ -1,3 +1,3 @@
 map2.equations._eqn_2 :
-  ∀ (f : bool → bool → bool) (n : ℕ) (b1 : bool) (v1 : bv n) (b2 : bool) (v2 : bv n),
-    map2 f (cons n b1 v1) (cons n b2 v2) = cons n (f b1 b2) (map2 f v1 v2)
+  ∀ (f : bool → bool → bool) (x : ℕ) (b1 : bool) (v1 : bv x) (b2 : bool) (v2 : bv x),
+    map2 f (cons x b1 v1) (cons x b2 v2) = cons x (f b1 b2) (map2 f v1 v2)

tests/lean/eqn_compiler_error_msg.lean.expected.out

@@ -1,3 +1,3 @@
-eqn_compiler_error_msg.lean:5:2: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
-  .p + .n
+eqn_compiler_error_msg.lean:5:28: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
+  .?m_1 + .?m_2
 eqn_compiler_error_msg.lean:4:6: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)

tests/lean/expr_quote.lean.expected.out

@@ -1,4 +1,5 @@
 expr_quote.lean:1:30: error: invalid quotation, contains universe metavariable
+expr_quote.lean:1:9: error: type of sorry macro is not a sort
 expr_quote.lean:1:9: error: don't know how to synthesize placeholder
 context:
 α a : expr

tests/lean/inaccessible.lean.expected.out

@@ -1,21 +1,24 @@
-inaccessible.lean:14:10: error: function expected at
-  mk
-term has type
-  ?m_1
-inaccessible.lean:14:4: error: invalid use of inaccessible term, it is not fixed by other arguments
+inaccessible.lean:14:10: error: invalid application, function expected
+inaccessible.lean:14:13: error: don't know how to synthesize placeholder
+context:
+A : Type u,
+B : Type v,
+f : A → B,
+inv_3 : Π (b : B), imf f b → A
+⊢ A
+inaccessible.lean:13:11: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 inaccessible.lean:17:12: error: invalid inaccessible annotation, it cannot be used around functions in applications
-inaccessible.lean:17:4: error: invalid use of inaccessible term, it is not fixed by other arguments
+inaccessible.lean:17:16: error: don't know how to synthesize placeholder
+context:
+A : Type u,
+B : Type v,
+f : A → B,
+inv_4 : Π (b : B), imf f b → A
+⊢ A
+inaccessible.lean:16:11: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 inaccessible.lean:25:12: error: invalid pattern, 'a' already appeared in this pattern
-inaccessible.lean:25:3: error: function expected at
-  f
-term has type
-  ?m_1
-inaccessible.lean:25:16: error: ill-formed match/equations expression
-inaccessible.lean:28:3: error: function expected at
-  f
-term has type
-  ?m_1
-inaccessible.lean:28:16: error: ill-formed match/equations expression
+inaccessible.lean:25:3: error: invalid application, function expected
+inaccessible.lean:25:16: error: ill-formed match/equation expression
+inaccessible.lean:28:3: error: invalid application, function expected
+inaccessible.lean:28:16: error: ill-formed match/equation expression
 inaccessible.lean:31:4: error: invalid pattern, 'a' already appeared in this pattern
-inaccessible.lean:82:2: error: invalid use of inaccessible term, it is not completely fixed by other arguments
-  .?m_1 + 1

tests/lean/inaccessible2.lean

@@ -12,3 +12,6 @@ definition inv_3 {A B : Sort*} (f : A → B) : ∀ (b : B), imf f b → A
 
 definition symm {A : Sort*} : ∀ a b : A, a = b → b = a
 | .(a) .(a) (eq.refl a) := rfl -- Error `a` in eq.refl must be marked as inaccessible since it is an inductive datatype parameter
+
+definition symm2 {A : Sort*} : ∀ a b : A, a = b → b = a
+| _ _ rfl := rfl -- correct version

tests/lean/inaccessible2.lean.expected.out

@@ -1,14 +1,24 @@
 inaccessible2.lean:5:8: error: invalid occurrence of 'inaccessible' annotation, it must only occur in patterns
 inaccessible2.lean:8:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
 inaccessible2.lean:8:45: error: unknown identifier 'a'
-inaccessible2.lean:8:4: error: invalid use of inaccessible term, it is not fixed by other arguments
+inaccessible2.lean:7:11: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 inaccessible2.lean:11:39: error: inaccesible pattern notation `.(t)` can only be used in patterns
 inaccessible2.lean:11:46: error: invalid expression
-inaccessible2.lean:11:4: error: function expected at
-  f
-term has type
-  ?m_1
-inaccessible2.lean:11:46: error: ill-formed match/equations expression
+inaccessible2.lean:11:4: error: invalid application, function expected
+inaccessible2.lean:11:46: error: ill-formed match/equation expression
 inaccessible2.lean:11:46: error: command expected
-inaccessible2.lean:14:13: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
-inaccessible2.lean:14:24: error: ill-formed match/equations expression
+inaccessible2.lean:14:27: error: don't know how to synthesize placeholder
+context:
+A : Sort ?,
+symm : ∀ (a b : A), a = b → b = a
+⊢ A
+inaccessible2.lean:13:11: error: equation compiler failed to create auxiliary declaration 'symm._main'
+nested exception message:
+type mismatch at application
+  eq.rec (λ (a_1 : a = a) (H_2 : a_1 == eq.refl a), id_rhs (⁇ = ⁇) rfl)
+term
+  λ (a_1 : a = a) (H_2 : a_1 == eq.refl a), id_rhs (⁇ = ⁇) rfl
+has type
+  ∀ (a_1 : a = a), a_1 == _ → ⁇ = ⁇
+but is expected to have type
+  (λ (b : A), ∀ (a_1 : a = b), a_1 == _ → b = a) a

tests/lean/inject.lean.expected.out

@@ -3,12 +3,12 @@ lift.equations._eqn_2 : ∀ {m k : ℕ} (f : fi m → fi k) (n : ℕ), @lift m k
 lift.equations._eqn_3 :
   ∀ {m k : ℕ} (f : fi m → fi k) (n : ℕ) (i : fi (m + n)),
     @lift m k f (succ n) (@fs (m + n) i) = @fs (k + n) (@lift m k f n i)
-to_nat.equations._eqn_1 : ∀ (n : ℕ), @to_nat (succ n) (@f0 n) = 0
-to_nat.equations._eqn_2 : ∀ (n : ℕ) (i : fi n), @to_nat (succ n) (@fs n i) = succ (@to_nat n i)
-inject.equations._eqn_1 : ∀ (n : ℕ) (i : fi n), @inject (succ n) (@fs n i) (@f0 (@to_nat n i)) = @f0 n
+to_nat.equations._eqn_1 : ∀ (x : ℕ), @to_nat (succ x) (@f0 x) = 0
+to_nat.equations._eqn_2 : ∀ (x : ℕ) (i : fi x), @to_nat (succ x) (@fs x i) = succ (@to_nat x i)
+inject.equations._eqn_1 : ∀ (x : ℕ) (i : fi x), @inject (succ x) (@fs x i) (@f0 (@to_nat x i)) = @f0 x
 inject.equations._eqn_2 :
-  ∀ (n : ℕ) (i : fi n) (j : fi (@to_nat n i)),
-    @inject (succ n) (@fs n i) (@fs (@to_nat n i) j) = @fs n (@inject n i j)
+  ∀ (x : ℕ) (i : fi x) (j : fi (@to_nat x i)),
+    @inject (succ x) (@fs x i) (@fs (@to_nat x i) j) = @fs x (@inject x i j)
 inject'.equations._eqn_1 : ∀ (n : ℕ) (i : fi n), @inject' (succ n) (@fs n i) (@f0 (@to_nat n i)) = @f0 n
 inject'.equations._eqn_2 :
   ∀ (n : ℕ) (i : fi n) (j : fi (@to_nat n i)),
@@ -16,10 +16,10 @@ inject'.equations._eqn_2 :
 raise.equations._eqn_1 : ∀ {m : ℕ} (i : fi m), @raise m 0 i = i
 raise.equations._eqn_2 : ∀ {m : ℕ} (n : ℕ) (i : fi m), @raise m (succ n) i = @fs (m + n) (@raise m n i)
 deg.equations._eqn_1 : ∀ (n : ℕ) (j : fi (succ n)), @deg (succ n) (@f0 (succ n)) j = @fs (succ n) j
-deg.equations._eqn_2 : ∀ (n : ℕ) (i : fi (succ n)), @deg (succ n) (@fs (succ n) i) (@f0 n) = @f0 (succ n)
+deg.equations._eqn_2 : ∀ (x : ℕ) (i : fi (succ x)), @deg (succ x) (@fs (succ x) i) (@f0 x) = @f0 (succ x)
 deg.equations._eqn_3 :
-  ∀ (n : ℕ) (i : fi (succ n)) (j : fi n), @deg (succ n) (@fs (succ n) i) (@fs n j) = @fs (succ n) (@deg n i j)
+  ∀ (x : ℕ) (i : fi (succ x)) (j : fi x), @deg (succ x) (@fs (succ x) i) (@fs x j) = @fs (succ x) (@deg x i j)
 deg'.equations._eqn_1 : ∀ (n : ℕ) (j : fi (succ n)), @deg' (succ n) (@f0 (succ n)) j = @fs (succ n) j
-deg'.equations._eqn_2 : ∀ (n : ℕ) (i : fi (succ n)), @deg' (succ n) (@fs (succ n) i) (@f0 n) = @f0 (succ n)
+deg'.equations._eqn_2 : ∀ (x : ℕ) (i : fi (succ x)), @deg' (succ x) (@fs (succ x) i) (@f0 x) = @f0 (succ x)
 deg'.equations._eqn_3 :
-  ∀ (n : ℕ) (i : fi (succ n)) (j : fi n), @deg' (succ n) (@fs (succ n) i) (@fs n j) = @fs (succ n) (@deg' n i j)
+  ∀ (x : ℕ) (i : fi (succ x)) (j : fi x), @deg' (succ x) (@fs (succ x) i) (@fs x j) = @fs (succ x) (@deg' x i j)

tests/lean/offset_is_def_eq_trick.lean.expected.out

@@ -1 +1 @@
-head.equations._eqn_1 : ∀ {α : Type u_1} (n : ℕ) (h : α) (t : Vec α n), head (Vec.cons h t) = h
+head.equations._eqn_1 : ∀ {α : Type u_1} (x : ℕ) (h : α) (t : Vec α x), head (Vec.cons h t) = h

tests/lean/string_imp.lean.expected.out

@@ -1,10 +1,18 @@
 string_imp.lean:2:2: error: invalid constructor ⟨...⟩, type is a private inductive datatype
+string_imp.lean:2:3: error: don't know how to synthesize placeholder
+context:
+f : string → list char
+⊢ list char
 string_imp.lean:1:4: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 string_imp.lean:5:3: error: invalid pattern: variable, constructor or constant tagged as pattern expected
 string_imp.lean:5:3: error: function expected at
   string_imp.mk
 term has type
   _
+string_imp.lean:5:17: error: don't know how to synthesize placeholder
+context:
+g : string → list char
+⊢ list char
 string_imp.lean:4:4: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 string_imp.lean:8:0: error: unknown identifier 'string_imp.cases_on'
 string_imp.lean:7:0: warning: declaration 'h' uses sorry