From f723550d33f1ce60f42e9c502be650cbff5cdc28 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 24 Apr 2015 14:58:15 -0700
Subject: [PATCH] feat(frontends/lean/elaborator): decorates error message with
 free variables introduced by the left-hand-side of the equation

closes #528
---
 src/frontends/lean/elaborator.cpp          | 28 ++++++++++++++++++++--
 tests/lean/528.lean                        |  7 ++++++
 tests/lean/528.lean.expected.out           |  6 +++++
 tests/lean/error_loc_bug.lean.expected.out |  2 ++
 4 files changed, 41 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/528.lean
 create mode 100644 tests/lean/528.lean.expected.out

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index e858e8527..644386596 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1100,15 +1100,39 @@ expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) {
     optional<expr> first_eq;
     for (expr const & eq : eqs) {
         expr new_eq;
+        constraint_seq new_cs;
+        buffer<expr> fns_locals;
+        fun_to_telescope(m_ngen, eq, fns_locals, optional<binder_info>());
+        list<expr> locals = to_list(fns_locals.begin() + num_fns, fns_locals.end());
         if (first_eq) {
             // Replace first num_fns domains of eq with the ones in first_eq.
             // This is a trick/hack to ensure the fns in each equation have
             // the same elaborated type.
-            new_eq = visit(copy_domain(num_fns, *first_eq, eq), cs);
+            new_eq = visit(copy_domain(num_fns, *first_eq, eq), new_cs);
         } else {
-            new_eq = visit(eq, cs);
+            new_eq = visit(eq, new_cs);
             first_eq = new_eq;
         }
+        // To produce more helpful error messages, we decorate all
+        // justifications created when processing eq with the list of local variables declared in the
+        // left-hand-side of the equation.
+        buffer<constraint> tmp_cs;
+        new_cs.linearize(tmp_cs);
+        for (constraint const & c : tmp_cs) {
+            justification j = c.get_justification();
+            auto pp_fn      = [=](formatter const & fmt, pos_info_provider const * pp, substitution const & s) {
+                format r = j.pp(fmt, pp, s);
+                r += compose(line(), format("The following identifier(s) are introduced as free variables by the "
+                                            "left-hand-side of the equation:"));
+                format aux;
+                for (expr const & l : locals)
+                    aux += compose(format(local_pp_name(l)), space());
+                r += nest(get_pp_indent(fmt.get_options()), compose(line(), aux));
+                return r;
+            };
+            justification new_j = mk_wrapper(j, j.get_main_expr(), pp_fn);
+            cs += update_justification(c, new_j);
+        }
         new_eqs.push_back(new_eq);
     }
 
diff --git a/tests/lean/528.lean b/tests/lean/528.lean
new file mode 100644
index 000000000..c66498133
--- /dev/null
+++ b/tests/lean/528.lean
@@ -0,0 +1,7 @@
+variables {P : bool → Type} {x : P bool.tt} {y : P bool.ff}
+
+example (b : bool) : P b :=
+match b with
+| tt := x
+| ff := y
+end
diff --git a/tests/lean/528.lean.expected.out b/tests/lean/528.lean.expected.out
new file mode 100644
index 000000000..175e20fa1
--- /dev/null
+++ b/tests/lean/528.lean.expected.out
@@ -0,0 +1,6 @@
+528.lean:6:5: error: type mismatch at definition 'match', has type
+  P bool.ff
+but is expected to have type
+  P bool.tt
+The following identifier(s) are introduced as free variables by the left-hand-side of the equation:
+  ff 
diff --git a/tests/lean/error_loc_bug.lean.expected.out b/tests/lean/error_loc_bug.lean.expected.out
index d4545e5a1..8b4b890f7 100644
--- a/tests/lean/error_loc_bug.lean.expected.out
+++ b/tests/lean/error_loc_bug.lean.expected.out
@@ -6,3 +6,5 @@ has type
   Γ ⊢ A ∨ B
 but is expected to have type
   Γ ⊢ A ∧ B
+The following identifier(s) are introduced as free variables by the left-hand-side of the equation:
+  Γ A B Δ H Hs