From 81729d96f9cee6fc815f76720ae06a63eaa2994f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 8 Oct 2021 09:28:58 -0700
Subject: [PATCH] fix: make sure `Quot` primitives stay in eta expanded form

fixes #716
---
 src/library/compiler/csimp.cpp |  4 ++--
 src/library/compiler/util.cpp  | 15 +++++++++++++++
 src/library/compiler/util.h    |  6 ++++++
 tests/lean/run/716.lean        |  1 -
 4 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp
index 14c91bc408..0dcd4d46bb 100644
--- a/src/library/compiler/csimp.cpp
+++ b/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;
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index 5f77bdc781..00ac11a659 100644
--- a/src/library/compiler/util.cpp
+++ b/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());
diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h
index 31672107bb..e5d358c442 100644
--- a/src/library/compiler/util.h
+++ b/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();
 }
diff --git a/tests/lean/run/716.lean b/tests/lean/run/716.lean
index c9a844a366..b2ad907ff9 100644
--- a/tests/lean/run/716.lean
+++ b/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