diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out
index 6ec49bfbd..73c113c0c 100644
--- a/tests/lean/elab1.lean.expected.out
+++ b/tests/lean/elab1.lean.expected.out
@@ -1,39 +1,138 @@
   Set: pp::colors
   Set: pp::unicode
   Assumed: f
-Error (line: 4, pos: 6) type mismatch at application
-    f 10 ⊤
-Function type:
-    Π (A : Type), A → A → A
-Arguments types:
-    ℕ : Type
-    10 : ℕ
-    ⊤ : Bool
+Failed to solve
+ ⊢ (?M3::1 ≈ λ x : ℕ, x) ⊕ (?M3::1 ≈ nat_to_int) ⊕ (?M3::1 ≈ nat_to_real)
+    (line: 4: pos: 8) Coercion for
+        10
+    Failed to solve
+     ⊢ Bool ≺ ℕ
+        Substitution
+         ⊢ Bool ≺ ?M3::0
+            (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
+                f::explicit
+            with arguments:
+                ?M3::0
+                ?M3::1 10
+                ⊤
+            Assignment
+             ⊢ ℕ ≺ ?M3::0
+                Substitution
+                 ⊢ (?M3::5[inst:0 (10)]) 10 ≺ ?M3::0
+                    (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
+                        f::explicit
+                    with arguments:
+                        ?M3::0
+                        ?M3::1 10
+                        ⊤
+                    Assignment
+                    x : ℕ ⊢ λ x : ℕ, ℕ ≈ ?M3::5
+                        Destruct/Decompose
+                        x : ℕ ⊢ ℕ ≈ ?M3::5 x
+                            Destruct/Decompose
+                             ⊢ ℕ → ℕ ≈ Π x : ?M3::4, ?M3::5 x
+                                Substitution
+                                 ⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x
+                                     Function expected at
+                                        ?M3::1 10
+                                    Assignment
+                                     ⊢ ℕ → ℕ ≺ ?M3::3
+                                        Propagate type, ?M3::1 : ?M3::3
+                                            Assignment
+                                             ⊢ ?M3::1 ≈ λ x : ℕ, x
+                                                assumption 0
+    Failed to solve
+     ⊢ Bool ≺ ℤ
+        Substitution
+         ⊢ Bool ≺ ?M3::0
+            (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
+                f::explicit
+            with arguments:
+                ?M3::0
+                ?M3::1 10
+                ⊤
+            Assignment
+             ⊢ ℤ ≺ ?M3::0
+                Substitution
+                 ⊢ (?M3::5[inst:0 (10)]) 10 ≺ ?M3::0
+                    (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
+                        f::explicit
+                    with arguments:
+                        ?M3::0
+                        ?M3::1 10
+                        ⊤
+                    Assignment
+                    _ : ℕ ⊢ λ x : ℕ, ℤ ≈ ?M3::5
+                        Destruct/Decompose
+                        _ : ℕ ⊢ ℤ ≈ ?M3::5 _
+                            Destruct/Decompose
+                             ⊢ ℕ → ℤ ≈ Π x : ?M3::4, ?M3::5 x
+                                Substitution
+                                 ⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x
+                                     Function expected at
+                                        ?M3::1 10
+                                    Assignment
+                                     ⊢ ℕ → ℤ ≺ ?M3::3
+                                        Propagate type, ?M3::1 : ?M3::3
+                                            Assignment
+                                             ⊢ ?M3::1 ≈ nat_to_int
+                                                assumption 1
+    Failed to solve
+     ⊢ Bool ≺ ℝ
+        Substitution
+         ⊢ Bool ≺ ?M3::0
+            (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
+                f::explicit
+            with arguments:
+                ?M3::0
+                ?M3::1 10
+                ⊤
+            Assignment
+             ⊢ ℝ ≺ ?M3::0
+                Substitution
+                 ⊢ (?M3::5[inst:0 (10)]) 10 ≺ ?M3::0
+                    (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
+                        f::explicit
+                    with arguments:
+                        ?M3::0
+                        ?M3::1 10
+                        ⊤
+                    Assignment
+                    _ : ℕ ⊢ λ x : ℕ, ℝ ≈ ?M3::5
+                        Destruct/Decompose
+                        _ : ℕ ⊢ ℝ ≈ ?M3::5 _
+                            Destruct/Decompose
+                             ⊢ ℕ → ℝ ≈ Π x : ?M3::4, ?M3::5 x
+                                Substitution
+                                 ⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x
+                                     Function expected at
+                                        ?M3::1 10
+                                    Assignment
+                                     ⊢ ℕ → ℝ ≺ ?M3::3
+                                        Propagate type, ?M3::1 : ?M3::3
+                                            Assignment
+                                             ⊢ ?M3::1 ≈ nat_to_real
+                                                assumption 2
   Assumed: g
 Error (line: 7, pos: 6) unsolved placeholder at term
     g 10
   Assumed: h
-Error (line: 11, pos: 27) application type mismatch during term elaboration
-    h A x
-Function type:
-    Π (A : Type), A → A
-Arguments types:
-    A : Type
-    x : ?M0[lift:0:2]
-Elaborator state
-    #0 ≈ ?M0[lift:0:2]
+Failed to solve
+x : ?M3::0, A : Type ⊢ ?M3::0[lift:0:2] ≺ A
+    (line: 11: pos: 27) Type of argument 2 must be convertible to the expected type in the application of
+        h
+    with arguments:
+        A
+        x
   Assumed: eq
-Error (line: 15, pos: 51) application type mismatch during term elaboration
-    eq C a b
-Function type:
-    Π (A : Type), A → A → Bool
-Arguments types:
-    C : Type
-    a : ?M0[lift:0:3]
-    b : ?M2[lift:0:2]
-Elaborator state
-    #0 ≈ ?M2[lift:0:2]
-    #0 ≈ ?M0[lift:0:3]
+Failed to solve
+A : Type, B : Type, a : ?M3::0, b : ?M3::1, C : Type ⊢ ?M3::0[lift:0:3] ≺ C
+    (line: 15: pos: 51) Type of argument 2 must be convertible to the expected type in the application of
+        eq
+    with arguments:
+        C
+        a
+        b
   Assumed: a
   Assumed: b
   Assumed: H
diff --git a/tests/lean/ex3.lean.expected.out b/tests/lean/ex3.lean.expected.out
index 0c16b4034..c48adb645 100644
--- a/tests/lean/ex3.lean.expected.out
+++ b/tests/lean/ex3.lean.expected.out
@@ -4,21 +4,41 @@
 myeq Bool ⊤ ⊥
   Assumed: T
   Assumed: a
-Error (line: 5, pos: 6) type mismatch at application
-    myeq Bool ⊤ a
-Function type:
-    Π (A : Type), A → A → Bool
-Arguments types:
-    Bool : Type
-    ⊤ : Bool
-    a : T
+Failed to solve
+ ⊢ Bool ≺ T
+    Substitution
+     ⊢ Bool ≺ ?M3::0
+        (line: 5: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
+            myeq
+        with arguments:
+            ?M3::0
+            ⊤
+            a
+        Assignment
+         ⊢ T ≺ ?M3::0
+            (line: 5: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
+                myeq
+            with arguments:
+                ?M3::0
+                ⊤
+                a
   Assumed: myeq2
   Set: lean::pp::implicit
-Error (line: 9, pos: 15) type mismatch at application
-    myeq2::explicit Bool ⊤ a
-Function type:
-    Π (A : Type), A → A → Bool
-Arguments types:
-    Bool : Type
-    ⊤ : Bool
-    a : T
+Failed to solve
+ ⊢ Bool ≺ T
+    Substitution
+     ⊢ Bool ≺ ?M3::0
+        (line: 9: pos: 15) Type of argument 2 must be convertible to the expected type in the application of
+            myeq2::explicit
+        with arguments:
+            ?M3::0
+            ⊤
+            a
+        Assignment
+         ⊢ T ≺ ?M3::0
+            (line: 9: pos: 15) Type of argument 3 must be convertible to the expected type in the application of
+                myeq2::explicit
+            with arguments:
+                ?M3::0
+                ⊤
+                a
diff --git a/tests/lean/let4.lean.expected.out b/tests/lean/let4.lean.expected.out
index a56ff82d8..e5a2f6177 100644
--- a/tests/lean/let4.lean.expected.out
+++ b/tests/lean/let4.lean.expected.out
@@ -1,20 +1,47 @@
   Set: pp::colors
   Set: pp::unicode
-Error (line: 4, pos: 15) type mismatch at definition 'a', expected type
-    ℤ
-Given type:
-    Bool
+let b := ⊤, a : ℤ := b in a
   Assumed: vector
   Assumed: const
 let a := 10, v1 := const a ⊤, v2 := v1 in v2 : vector Bool 10
 let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2
 let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2 : vector Bool 10
-Error (line: 31, pos: 26) type mismatch at definition 'v2', expected type
-    vector ℤ a
-Given type:
-    vector Bool a
+Failed to solve
+a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ Bool ≈ ℤ
+    Substitution
+    a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ ?M3::0[lift:0:1] ≈ ℤ
+        Destruct/Decompose
+        a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ vector (?M3::0[lift:0:1]) a ≺ vector ℤ a
+            (line: 31: pos: 26) Type of definition 'v2' must be convertible to expected type.
+        Assignment
+        a : ℕ := 10 ⊢ ?M3::0 ≈ Bool
+            Destruct/Decompose
+            a : ℕ := 10 ⊢ vector ?M3::0 a ≺ vector Bool a
+                (line: 30: pos: 26) Type of definition 'v1' must be convertible to expected type.
   Assumed: foo
   Coercion foo
-let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector ℤ a := v1 in v2 : vector ℤ 10
+Failed to solve
+a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ Bool ≈ ℤ
+    Substitution
+    a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ ?M3::0[lift:0:1] ≈ ℤ
+        Destruct/Decompose
+        a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ vector (?M3::0[lift:0:1]) a ≺ vector ℤ a
+            (line: 40: pos: 26) Type of definition 'v2' must be convertible to expected type.
+        Assignment
+        a : ℕ := 10 ⊢ ?M3::0 ≈ Bool
+            Destruct/Decompose
+            a : ℕ := 10 ⊢ vector ?M3::0 a ≺ vector Bool a
+                (line: 39: pos: 26) Type of definition 'v1' must be convertible to expected type.
   Set: lean::pp::coercion
-let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector ℤ a := foo v1 in v2
+Failed to solve
+a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ Bool ≈ ℤ
+    Substitution
+    a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ ?M3::0[lift:0:1] ≈ ℤ
+        Destruct/Decompose
+        a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ vector (?M3::0[lift:0:1]) a ≺ vector ℤ a
+            (line: 48: pos: 26) Type of definition 'v2' must be convertible to expected type.
+        Assignment
+        a : ℕ := 10 ⊢ ?M3::0 ≈ Bool
+            Destruct/Decompose
+            a : ℕ := 10 ⊢ vector ?M3::0 a ≺ vector Bool a
+                (line: 47: pos: 26) Type of definition 'v1' must be convertible to expected type.
diff --git a/tests/lean/overload2.lean.expected.out b/tests/lean/overload2.lean.expected.out
index bbb07930b..6e198a93e 100644
--- a/tests/lean/overload2.lean.expected.out
+++ b/tests/lean/overload2.lean.expected.out
@@ -1,13 +1,108 @@
   Set: pp::colors
   Set: pp::unicode
-Error (line: 1, pos: 10) application type mismatch, none of the overloads can be used
-Candidates:
-    Real::add : ℝ → ℝ → ℝ
-    Int::add : ℤ → ℤ → ℤ
-    Nat::add : ℕ → ℕ → ℕ
-Arguments:
-    1 : ℕ
-    ⊤ : Bool
+Failed to solve
+ ⊢ (?M3::0 ≈ Nat::add) ⊕ (?M3::0 ≈ Int::add) ⊕ (?M3::0 ≈ Real::add)
+    (line: 1: pos: 10) Overloading at
+        (Real::add | Int::add | Nat::add) 1 ⊤
+    Failed to solve
+     ⊢ Bool ≺ ℕ
+        Substitution
+         ⊢ Bool ≺ ?M3::8
+            (line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of
+                ?M3::0
+            with arguments:
+                ?M3::1 1
+                ⊤
+            Assignment
+             ⊢ ℕ ≈ ?M3::8
+                Destruct/Decompose
+                 ⊢ ℕ → ℕ ≈ Π x : ?M3::8, ?M3::9 x
+                    Substitution
+                     ⊢ (?M3::7[inst:0 (?M3::1 1)]) (?M3::1 1) ≈ Π x : ?M3::8, ?M3::9 x
+                        (line: 1: pos: 10) Function expected at
+                            ?M3::0 (?M3::1 1) ⊤
+                        Assignment
+                        _ : ℕ ⊢ λ x : ℕ, ℕ → ℕ ≈ ?M3::7
+                            Destruct/Decompose
+                            _ : ℕ ⊢ ℕ → ℕ ≈ ?M3::7 _
+                                Destruct/Decompose
+                                 ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M3::6, ?M3::7 x
+                                    Substitution
+                                     ⊢ ?M3::2 ≈ Π x : ?M3::6, ?M3::7 x
+                                        (line: 1: pos: 10) Function expected at
+                                            ?M3::0 (?M3::1 1) ⊤
+                                        Assignment
+                                         ⊢ ℕ → ℕ → ℕ ≺ ?M3::2
+                                            Propagate type, ?M3::0 : ?M3::2
+                                                Assignment
+                                                 ⊢ ?M3::0 ≈ Nat::add
+                                                    assumption 0
+    Failed to solve
+     ⊢ Bool ≺ ℤ
+        Substitution
+         ⊢ Bool ≺ ?M3::8
+            (line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of
+                ?M3::0
+            with arguments:
+                ?M3::1 1
+                ⊤
+            Assignment
+             ⊢ ℤ ≈ ?M3::8
+                Destruct/Decompose
+                 ⊢ ℤ → ℤ ≈ Π x : ?M3::8, ?M3::9 x
+                    Substitution
+                     ⊢ (?M3::7[inst:0 (?M3::1 1)]) (?M3::1 1) ≈ Π x : ?M3::8, ?M3::9 x
+                        (line: 1: pos: 10) Function expected at
+                            ?M3::0 (?M3::1 1) ⊤
+                        Assignment
+                        _ : ℤ ⊢ λ x : ℤ, ℤ → ℤ ≈ ?M3::7
+                            Destruct/Decompose
+                            _ : ℤ ⊢ ℤ → ℤ ≈ ?M3::7 _
+                                Destruct/Decompose
+                                 ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M3::6, ?M3::7 x
+                                    Substitution
+                                     ⊢ ?M3::2 ≈ Π x : ?M3::6, ?M3::7 x
+                                        (line: 1: pos: 10) Function expected at
+                                            ?M3::0 (?M3::1 1) ⊤
+                                        Assignment
+                                         ⊢ ℤ → ℤ → ℤ ≺ ?M3::2
+                                            Propagate type, ?M3::0 : ?M3::2
+                                                Assignment
+                                                 ⊢ ?M3::0 ≈ Int::add
+                                                    assumption 2
+    Failed to solve
+     ⊢ Bool ≺ ℝ
+        Substitution
+         ⊢ Bool ≺ ?M3::8
+            (line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of
+                ?M3::0
+            with arguments:
+                ?M3::1 1
+                ⊤
+            Assignment
+             ⊢ ℝ ≈ ?M3::8
+                Destruct/Decompose
+                 ⊢ ℝ → ℝ ≈ Π x : ?M3::8, ?M3::9 x
+                    Substitution
+                     ⊢ (?M3::7[inst:0 (?M3::1 1)]) (?M3::1 1) ≈ Π x : ?M3::8, ?M3::9 x
+                        (line: 1: pos: 10) Function expected at
+                            ?M3::0 (?M3::1 1) ⊤
+                        Assignment
+                        _ : ℝ ⊢ λ x : ℝ, ℝ → ℝ ≈ ?M3::7
+                            Destruct/Decompose
+                            _ : ℝ ⊢ ℝ → ℝ ≈ ?M3::7 _
+                                Destruct/Decompose
+                                 ⊢ ℝ → ℝ → ℝ ≈ Π x : ?M3::6, ?M3::7 x
+                                    Substitution
+                                     ⊢ ?M3::2 ≈ Π x : ?M3::6, ?M3::7 x
+                                        (line: 1: pos: 10) Function expected at
+                                            ?M3::0 (?M3::1 1) ⊤
+                                        Assignment
+                                         ⊢ ℝ → ℝ → ℝ ≺ ?M3::2
+                                            Propagate type, ?M3::0 : ?M3::2
+                                                Assignment
+                                                 ⊢ ?M3::0 ≈ Real::add
+                                                    assumption 5
   Assumed: R
   Assumed: T
   Assumed: r2t
diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out
index 02126cf3d..1d2b09ca0 100644
--- a/tests/lean/tst1.lean.expected.out
+++ b/tests/lean/tst1.lean.expected.out
@@ -26,7 +26,7 @@ Definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2
 Definition map::explicit (A B C : Type) (n : N) (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n :=
     map f v1 v2
 select (update (const three ⊥) two ⊤) two two_lt_three : Bool
-⊤
+if Bool (two = two) ⊤ ⊥
 update (const three ⊥) two ⊤ : vector Bool three
 
 --------
diff --git a/tests/lean/tst7.lean.expected.out b/tests/lean/tst7.lean.expected.out
index a3b944564..4207f5347 100644
--- a/tests/lean/tst7.lean.expected.out
+++ b/tests/lean/tst7.lean.expected.out
@@ -2,15 +2,13 @@
   Set: pp::unicode
   Assumed: f
 λ (A B : Type) (a : B), f B a
-Error (line: 4, pos: 40) application type mismatch during term elaboration
-    f B a
-Function type:
-    Π (A : Type), A → Bool
-Arguments types:
-    B : Type
-    a : ?M0[lift:0:2]
-Elaborator state
-    #0 ≈ ?M0[lift:0:2]
+Failed to solve
+A : Type, a : ?M3::0, B : Type ⊢ ?M3::0[lift:0:2] ≺ B
+    (line: 4: pos: 40) Type of argument 2 must be convertible to the expected type in the application of
+        f
+    with arguments:
+        B
+        a
   Assumed: myeq
 myeq (Π (A : Type), A → A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b)
 myeq (Π (A : Type), A → A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b) : Bool