fix(library/compiler/csimp): we may have partially applied cases_on applications in the computationally irrelevant part

src/library/compiler/csimp.cpp

@@ -233,7 +233,9 @@ class csimp_fn {
                 if (is_proj(s) && proj_expr(s) == x) {
                     found = true;
                     return false;
-                } else if (is_cases_on_app(env(), s) && get_cases_on_app_major(env(), s) == x) {
+                } else if (is_cases_on_app(env(), s) &&
+                           get_app_num_args(s) == get_cases_on_arity(env(), const_name(get_app_fn(s))) &&
+                           get_cases_on_app_major(env(), s) == x) {
                     found = true;
                     return false;
                 }

src/library/compiler/util.cpp

@@ -125,6 +125,15 @@ bool is_cases_on_recursor(environment const & env, name const & n) {
     return ::lean::is_aux_recursor(env, n) && n.get_string() == "cases_on";
 }
 
+unsigned get_cases_on_arity(environment const & env, name const & c) {
+    lean_assert(is_cases_on_recursor(env, c));
+    inductive_val I_val = get_cases_on_inductive_val(env, c);
+    unsigned nparams    = I_val.get_nparams();
+    unsigned nindices   = I_val.get_nindices();
+    unsigned nminors    = I_val.get_ncnstrs();
+    return nparams + 1 /* motive */ + nindices + 1 /* major */ + nminors;
+}
+
 expr get_cases_on_app_major(environment const & env, expr const & c) {
     lean_assert(is_cases_on_app(env, c));
     buffer<expr> args;

src/library/compiler/util.h

@@ -30,6 +30,16 @@ expr unfold_macro_defs(environment const & env, expr const & e);
 inline bool is_lc_mdata(expr const &) { return false; }
 
 bool is_cases_on_recursor(environment const & env, name const & n);
+/* We defined the "arity" of a cases_on application as the sum:
+   ```
+     number of inductive parameters +
+     1 +    // motive
+     number of inductive indices +
+     1 +    // major premise
+     number of constructors // cases_on has a minor premise for each constructor
+   ```
+   \pre is_cases_on_recursor(env, c) */
+unsigned get_cases_on_arity(environment const & env, name const & c);
 /* Return the `inductive_val` for the cases_on constant `c`. */
 inline inductive_val get_cases_on_inductive_val(environment const & env, name const & c) {
     lean_assert(is_cases_on_recursor(env, c));