From 163577c23ac6387c5f753ca5ab7f12951080797a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 May 2015 18:34:51 -0700
Subject: [PATCH] fix(library/normalize): fixes #599

---
 src/library/normalize.cpp |  2 +-
 src/library/util.cpp      | 10 +++++++---
 src/library/util.h        |  3 +++
 tests/lean/hott/599.hlean |  8 ++++++++
 4 files changed, 19 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/hott/599.hlean

diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index d195e720d..63ef05469 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -194,7 +194,7 @@ class normalize_fn {
             return some_expr(e);
         expr const & f = get_app_fn(e);
         if (is_constant(f) && has_constructor_hint(m_tc.env(), const_name(f))) {
-            if (auto r = unfold_app(m_tc.env(), e))
+            if (auto r = unfold_term(m_tc.env(), e))
                 return r;
             else
                 return some_expr(e);
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 0f84d9d2c..ec38c61d3 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -21,9 +21,7 @@ bool is_standard(environment const & env) {
     return env.prop_proof_irrel() && env.impredicative();
 }
 
-optional<expr> unfold_app(environment const & env, expr const & e) {
-    if (!is_app(e))
-        return none_expr();
+optional<expr> unfold_term(environment const & env, expr const & e) {
     expr const & f = get_app_fn(e);
     if (!is_constant(f))
         return none_expr();
@@ -36,6 +34,12 @@ optional<expr> unfold_app(environment const & env, expr const & e) {
     return some_expr(apply_beta(d, args.size(), args.data()));
 }
 
+optional<expr> unfold_app(environment const & env, expr const & e) {
+    if (!is_app(e))
+        return none_expr();
+    return unfold_term(env, e);
+}
+
 optional<level> dec_level(level const & l) {
     switch (kind(l)) {
     case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
diff --git a/src/library/util.h b/src/library/util.h
index 3e90bcf88..96eaedb1e 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -10,6 +10,9 @@ Author: Leonardo de Moura
 
 namespace lean {
 typedef std::unique_ptr<type_checker> type_checker_ptr;
+/** \brief Unfold constant \c e or constant application (i.e., \c e is of the form (f ....),
+    where \c f is a constant */
+optional<expr> unfold_term(environment const & env, expr const & e);
 /** \brief If \c e is of the form <tt>(f a_1 ... a_n)</tt>, where \c f is
     a non-opaque definition, then unfold \c f, and beta reduce.
     Otherwise, return none.
diff --git a/tests/lean/hott/599.hlean b/tests/lean/hott/599.hlean
new file mode 100644
index 000000000..32c385936
--- /dev/null
+++ b/tests/lean/hott/599.hlean
@@ -0,0 +1,8 @@
+structure pointed [class] (A : Type) := (point : A)
+
+open unit pointed
+
+definition pointed_unit [instance] [constructor] : pointed unit :=
+mk star
+
+example : point unit = point unit := by esimp