From 9d5b69ad5cc9bfe2ef99ce3983e63caf690f1d83 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 12 Jun 2017 20:32:15 -0700
Subject: [PATCH] fix(library/compiler/preprocess): compile_lemma =>
 compile_irrelevant

We can also ignore functions that return types at compile_lemma (now
called compile_irrelevant).

fixes #1658
---
 src/library/compiler/preprocess.cpp | 19 +++++++++++--------
 tests/lean/run/1658.lean            | 14 ++++++++++++++
 2 files changed, 25 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/run/1658.lean

diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp
index d80aaacd56..7e370aa61e 100644
--- a/src/library/compiler/preprocess.cpp
+++ b/src/library/compiler/preprocess.cpp
@@ -203,15 +203,14 @@ class preprocess_fn {
     }
 #endif
 
-    /* If type of d is a proposition, we don't need to compile it.
+    /* If type of d is a proposition or return a type, we don't need to compile it.
        We can just generate (fun args, neutral_expr)
 
-       This procedure returns true if type of d is a proposition,
+       This procedure returns true if type of d is a proposition or return a type,
        and store the dummy code above in */
-    bool compile_lemma(declaration const & d, buffer<procedure> & procs) {
+    bool compile_irrelevant(declaration const & d, buffer<procedure> & procs) {
         type_context ctx(m_env, transparency_mode::All);
         expr type = d.get_type();
-        if (!ctx.is_prop(type)) return false;
         type_context::tmp_locals locals(ctx);
         while (true) {
             type = ctx.relaxed_whnf(type);
@@ -220,9 +219,13 @@ class preprocess_fn {
             expr local = locals.push_local_from_binding(type);
             type       = instantiate(binding_body(type), local);
         }
-        expr r = locals.mk_lambda(mk_neutral_expr());
-        procs.emplace_back(d.get_name(), optional<pos_info>(), r);
-        return true;
+        if (ctx.is_prop(type) || is_sort(type)) {
+            expr r = locals.mk_lambda(mk_neutral_expr());
+            procs.emplace_back(d.get_name(), optional<pos_info>(), r);
+            return true;
+        } else {
+            return false;
+        }
     }
 
 public:
@@ -230,7 +233,7 @@ public:
         m_env(env) {}
 
     void operator()(declaration const & d, buffer<procedure> & procs) {
-        if (compile_lemma(d, procs))
+        if (compile_irrelevant(d, procs))
             return;
         expr v = d.get_value();
         lean_trace(name({"compiler", "input"}), tout() << "\n" << v << "\n";);
diff --git a/tests/lean/run/1658.lean b/tests/lean/run/1658.lean
new file mode 100644
index 0000000000..7ef87ee1e8
--- /dev/null
+++ b/tests/lean/run/1658.lean
@@ -0,0 +1,14 @@
+constant p : bool → bool
+constant P : bool → Prop
+
+noncomputable def lp : bool → bool
+| ff := p ff
+| tt := p tt
+
+def foo (b : bool) : Prop :=
+P (lp b)
+
+constant T : bool → Type
+
+def boo (b : bool) : Type :=
+T (lp b)