From 85cf20a5b4ecf1fecc7944cef9b784d59c7fc2e6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 30 Aug 2016 08:13:58 -0700
Subject: [PATCH] fix(library/type_context): missing case: stuck projections

type_context only unfolds projections when they reduce.
---
 src/library/type_context.cpp | 15 +++++++++++++++
 src/library/type_context.h   |  1 +
 2 files changed, 16 insertions(+)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 236f1e9c2d..1da8c6ff38 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -599,9 +599,24 @@ expr type_context::relaxed_whnf(expr const & e) {
     return whnf(e);
 }
 
+optional<expr> type_context::is_stuck_projection(expr const & e) {
+    expr const & f = get_app_fn(e);
+    if (!is_constant(f)) return none_expr(); // it is not projection app
+    projection_info const * info = m_cache->m_proj_info.find(const_name(f));
+    if (!info) return none_expr(); // it is not projection app
+    buffer<expr> args;
+    get_app_args(e, args);
+    if (args.size() <= info->m_nparams) return none_expr(); // partially applied projection
+    unsigned mkidx  = info->m_nparams;
+    expr mk         = args[mkidx];
+    return is_stuck(mk);
+}
+
 optional<expr> type_context::is_stuck(expr const & e) {
     if (is_meta(e)) {
         return some_expr(e);
+    } else if (auto r = is_stuck_projection(e)) {
+        return r;
     } else {
         return env().norm_ext().is_stuck(e, *this);
     }
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 9b5d300edc..05966ffdde 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -250,6 +250,7 @@ public:
     virtual expr relaxed_whnf(expr const & e) override;
     virtual bool relaxed_is_def_eq(expr const & e1, expr const & e2) override;
 
+    optional<expr> is_stuck_projection(expr const & e);
     virtual optional<expr> is_stuck(expr const &) override;
 
     virtual expr push_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) override;