fix(library/normalize): fixes #599

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);

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) {
+optional<expr> unfold_term(environment const & env, expr const & e) {
-    if (!is_app(e))
-        return none_expr();
     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:

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.

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