fix: make sure Quot primitives stay in eta expanded form

fixes #716

src/library/compiler/csimp.cpp

@@ -1149,8 +1149,8 @@ class csimp_fn {
         // Example: `fun {a} => ReaderT.pure`
         if (!is_join_point_def && !top) {
             expr new_e = eta_reduce(e);
-           // Remark: we should not eta-reduce auxiliary match applications.
-            if (is_app(new_e) && !is_constructor_app(env(), new_e) && !is_proj(new_e) && !is_matcher_app(env(), new_e) && !is_cases_on_app(env(), new_e) && !is_lc_unreachable_app(new_e))
+           // Remark: we should only keep result if it is not a term must be in eta-expanded form.
+            if (is_app(new_e) && !must_be_eta_expanded(env(), new_e))
                 return visit(new_e, true);
         }
         buffer<expr> binding_fvars;

src/library/compiler/util.cpp

@@ -749,6 +749,21 @@ expr lcnf_eta_expand(type_checker::state & st, local_ctx lctx, expr e) {
     }
 }
 
+bool is_quot_primitive_app(environment const & env, expr const & e) {
+  expr const & f = get_app_fn(e);
+  return is_constant(f) && is_quot_primitive(env, const_name(f));
+}
+
+bool must_be_eta_expanded(environment const & env, expr const & e) {
+  return
+    is_constructor_app(env, e) ||
+    is_proj(e) ||
+    is_matcher_app(env, e) ||
+    is_cases_on_app(env, e) ||
+    is_lc_unreachable_app(e) ||
+    is_quot_primitive_app(env, e);
+}
+
 void initialize_compiler_util() {
     g_neutral_expr        = new expr(mk_constant("_neutral"));
     mark_persistent(g_neutral_expr->raw());

src/library/compiler/util.h

@@ -209,6 +209,12 @@ inline bool is_matcher_app(environment const & env, expr const & e) {
   return is_constant(f) && is_matcher(env, const_name(f));
 }
 
+/*
+  Return true if the given expression must be in eta-expanded form during compilation.
+  Example: constructors, `casesOn` applications must always be in eta-expanded form.
+*/
+bool must_be_eta_expanded(environment const & env, expr const & e);
+
 void initialize_compiler_util();
 void finalize_compiler_util();
 }

tests/lean/run/716.lean

@@ -23,7 +23,6 @@ namespace UProd
 
 @[noinline] def myId := @id
 
-set_option trace.compiler true
 def mk' {α : Type} : α × α → UProd α :=
   let f := @Quot.mk _ _
   myId f