fix(library/compiler/simp_inductive): fix an assertion violation… (#173)

* fix(simp_inductive): fix an assertion violoation for compiling `cases_on`

this was added for the test `tests/lean/crash2.lean`.
in `option.cases_on x none f`, we would get an assertion violation
because it isn't expecting a partially applied function.
I am not sure why this only seems to occur in record introductions.

* Fix bad file reference in comment

src/library/compiler/simp_inductive.cpp

@@ -89,12 +89,17 @@ class simp_inductive_core_fn : public compiler_step_visitor {
     pair<expr, bool> visit_minor_premise(expr e, buffer<bool> const & rel_fields) {
         type_context_old::tmp_locals locals(ctx());
         for (unsigned i = 0; i < rel_fields.size(); i++) {
-            lean_assert(is_lambda(e));
-            if (rel_fields[i]) {
-                expr l = locals.push_local_from_binding(e);
-                e = instantiate(binding_body(e), l);
+            if (!is_lambda(e)) {
+                /* [note] this was added for the test `tests/lean/172.lean`.  */
+                break;
             } else {
-                e = instantiate(binding_body(e), mk_neutral_expr());
+                lean_assert(is_lambda(e));
+                if (rel_fields[i]) {
+                    expr l = locals.push_local_from_binding(e);
+                    e = instantiate(binding_body(e), l);
+                } else {
+                    e = instantiate(binding_body(e), mk_neutral_expr());
+                }
             }
         }
         e = visit(e);

tests/lean/172.lean

@@ -0,0 +1,7 @@
+-- see issue: https://github.com/leanprover-community/lean/issues/172
+
+instance its_a_monad : monad option :=
+{ pure := λ _, some
+, bind := λ α β x f, option.rec_on x option.none f}
+
+#eval @has_bind.bind option (@monad.to_has_bind _ its_a_monad) _ _ (some 4) some

tests/lean/172.lean.expected.out

@@ -0,0 +1 @@
+(some 4)