From 1cdadba4b251bda889062203e41ebc834ddadaac Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Jun 2019 17:36:10 -0700
Subject: [PATCH] fix(library/compiler/csimp): type error

@kha This is another instance of a problem we discussed last summer.
I guess there are many more instances like this one that we are not handling.
Recall that we want to preserve types at `csimp` because we eventually
want to allow users to use equational theorems as rewriting rules during
compilation.
However, some of the transformations that `csimp` perform do not
preserve typeability in CIC.
Moreover, some of the optimizations require type inference.

I see the possible long term solutions:

1- Erase types and proofs as soon as possible. The main drawback here is
that we would have to develop an approach for translating Lean theorems
into valid rewriting rules for lambda pure. For example, the following
theorem should not be used as a rewriting rule after we erase types.
```
forall (xs : List Unit) (f : Unit -> Unit), List.map f xs = List.map id xs
```
BTW, I don't want to abandon the idea of using lemmas as rewriting rules in
the compiler.

2- Go over `csimp` and other compiler steps and make sure they work
properly even when `type_checker::infer_type` fails.
---
 src/library/compiler/csimp.cpp       | 31 ++++++++++++++++------------
 tests/lean/run/csimp_type_error.lean | 17 +++++++++++++++
 2 files changed, 35 insertions(+), 13 deletions(-)
 create mode 100644 tests/lean/run/csimp_type_error.lean

diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp
index 2b2fd45eaf..4227ad9eb4 100644
--- a/src/library/compiler/csimp.cpp
+++ b/src/library/compiler/csimp.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/inductive.h"
+#include "kernel/kernel_exception.h"
 #include "library/util.h"
 #include "library/constants.h"
 #include "library/class.h"
@@ -1318,21 +1319,25 @@ class csimp_fn {
     optional<expr> try_inline_proj_instance(expr const & e, bool is_let_val) {
         lean_assert(is_proj(e));
         if (!m_before_erasure) return none_expr();
-        expr e_type = infer_type(e);
-        if (is_type_class(e_type)) {
-            /* If `typeof(e)` is a type class, then we should not instantiate it.
-               See comment above. */
+        try {
+            expr e_type = infer_type(e);
+            if (is_type_class(e_type)) {
+                /* If `typeof(e)` is a type class, then we should not instantiate it.
+                   See comment above. */
+                return none_expr();
+            }
+
+            unsigned saved_fvars_size = m_fvars.size();
+            if (optional<expr> new_s = try_inline_proj_instance_aux(proj_expr(e))) {
+                lean_assert(is_constructor_app(env(), *new_s));
+                expr r = proj_constructor(*new_s, proj_idx(e).get_small_value());
+                return some_expr(visit(r, is_let_val));
+            }
+            m_fvars.resize(saved_fvars_size);
+            return none_expr();
+        } catch (kernel_exception &) {
             return none_expr();
         }
-
-        unsigned saved_fvars_size = m_fvars.size();
-        if (optional<expr> new_s = try_inline_proj_instance_aux(proj_expr(e))) {
-            lean_assert(is_constructor_app(env(), *new_s));
-            expr r = proj_constructor(*new_s, proj_idx(e).get_small_value());
-            return some_expr(visit(r, is_let_val));
-        }
-        m_fvars.resize(saved_fvars_size);
-        return none_expr();
     }
 
     /* Return true iff `e` is of the form `fun (xs), let ys := ts in (ctor ...)`.
diff --git a/tests/lean/run/csimp_type_error.lean b/tests/lean/run/csimp_type_error.lean
new file mode 100644
index 0000000000..ff5b52081e
--- /dev/null
+++ b/tests/lean/run/csimp_type_error.lean
@@ -0,0 +1,17 @@
+namespace scratch
+
+inductive type
+| bv (w:Nat) : type
+
+open type
+
+def value : type -> Type
+  | (bv w) := {n // n < w}
+
+def tester_fails : Π {tp : type}, value tp -> Bool
+  | (bv _) v1 := decide (v1.val = 0)
+
+def tester_ok : Π{tp : type}, value tp -> Prop
+  | (bv _) v1 := v1.val = 0
+
+end scratch