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

@@ -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 ...)`.

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