fix(library/normalize): fixes #640

src/kernel/environment.h

@@ -56,6 +56,7 @@ public:
     bool eta() const { return m_eta; }
     bool impredicative() const { return m_impredicative; }
     normalizer_extension const & norm_ext() const { return *(m_norm_ext.get()); }
+    bool is_recursor(environment const & env, name const & n) const { return m_norm_ext->is_recursor(env, n); }
 };
 
 class environment_extension {
@@ -134,6 +135,8 @@ public:
     /** \brief Return true iff the environment assumes Eta-reduction */
     bool eta() const { return m_header->eta(); }
 
+    bool is_recursor(name const & n) const { return m_header->is_recursor(*this, n); }
+
     /** \brief Return true iff the environment treats universe level 0 as an impredicative Prop */
     bool impredicative() const { return m_header->impredicative(); }
 

src/kernel/hits/hits.cpp

@@ -129,6 +129,10 @@ bool hits_normalizer_extension::supports(name const & feature) const {
     return feature == *g_hits_extension;
 }
 
+bool hits_normalizer_extension::is_recursor(environment const &, name const & n) const {
+    return n == *g_trunc_rec || n == *g_type_quotient_rec;
+}
+
 bool is_hits_decl(environment const & env, name const & n) {
     if (!get_extension(env).m_initialized)
         return false;

src/kernel/hits/hits.h

@@ -17,6 +17,7 @@ public:
     virtual optional<pair<expr, constraint_seq>> operator()(expr const & e, extension_context & ctx) const;
     virtual optional<expr> is_stuck(expr const & e, extension_context & ctx) const;
     virtual bool supports(name const & feature) const;
+    virtual bool is_recursor(environment const & env, name const & n) const;
 };
 
 /** \brief The following function must be invoked to register the builtin HITs computation rules in the kernel. */

src/kernel/inductive/inductive.cpp

@@ -953,6 +953,10 @@ auto inductive_normalizer_extension::operator()(expr const & e, extension_contex
     return some_ecs(r, cs);
 }
 
+bool inductive_normalizer_extension::is_recursor(environment const & env, name const & n) const {
+    return static_cast<bool>(is_elim_rule(env, n));
+}
+
 template<typename Ctx>
 optional<expr> is_elim_meta_app_core(Ctx & ctx, expr const & e) {
     inductive_env_ext const & ext = get_extension(ctx.env());

src/kernel/inductive/inductive.h

@@ -19,6 +19,7 @@ public:
     virtual optional<pair<expr, constraint_seq>> operator()(expr const & e, extension_context & ctx) const;
     virtual optional<expr> is_stuck(expr const & e, extension_context & ctx) const;
     virtual bool supports(name const & feature) const;
+    virtual bool is_recursor(environment const & env, name const & n) const;
 };
 
 /** \brief Introduction rule */

src/kernel/normalizer_extension.cpp

@@ -14,6 +14,7 @@ public:
     }
     virtual optional<expr> is_stuck(expr const &, extension_context &) const { return none_expr(); }
     virtual bool supports(name const &) const { return false; }
+    virtual bool is_recursor(environment const &, name const &) const { return false; }
 };
 
 std::unique_ptr<normalizer_extension> mk_id_normalizer_extension() {
@@ -44,6 +45,10 @@ public:
     virtual bool supports(name const & feature) const {
         return m_ext1->supports(feature) || m_ext2->supports(feature);
     }
+
+    virtual bool is_recursor(environment const & env, name const & n) const {
+        return m_ext1->is_recursor(env, n) || m_ext2->is_recursor(env, n);
+    }
 };
 
 std::unique_ptr<normalizer_extension> compose(std::unique_ptr<normalizer_extension> && ext1, std::unique_ptr<normalizer_extension> && ext2) {

src/kernel/normalizer_extension.h

@@ -25,6 +25,7 @@ public:
     /** \brief Return true iff the extension supports a feature with the given name,
         this method is only used for sanity checking. */
     virtual bool supports(name const & feature) const = 0;
+    virtual bool is_recursor(environment const & env, name const & n) const = 0;
 };
 
 inline optional<pair<expr, constraint_seq>> none_ecs() { return optional<pair<expr, constraint_seq>>(); }

src/kernel/quotient/quotient.cpp

@@ -122,6 +122,10 @@ bool quotient_normalizer_extension::supports(name const & feature) const {
     return feature == *g_quotient_extension;
 }
 
+bool quotient_normalizer_extension::is_recursor(environment const &, name const & n) const {
+    return n == *g_quotient_lift || n == *g_quotient_ind;
+}
+
 bool is_quotient_decl(environment const & env, name const & n) {
     if (!get_extension(env).m_initialized)
         return false;

src/kernel/quotient/quotient.h

@@ -15,6 +15,7 @@ public:
     virtual optional<pair<expr, constraint_seq>> operator()(expr const & e, extension_context & ctx) const;
     virtual optional<expr> is_stuck(expr const & e, extension_context & ctx) const;
     virtual bool supports(name const & feature) const;
+    virtual bool is_recursor(environment const & env, name const & n) const;
 };
 
 /** \brief The following function must be invoked to register the quotient type computation rules in the kernel. */

src/library/normalize.cpp

@@ -282,7 +282,7 @@ class normalize_fn {
         if (!modified)
             return e;
         expr r = mk_rev_app(f, args);
-        if (is_constant(f) && inductive::is_elim_rule(env(), const_name(f))) {
+        if (is_constant(f) && env().is_recursor(const_name(f))) {
             return normalize(r);
         } else {
             return r;

src/tests/kernel/environment.cpp

@@ -136,6 +136,7 @@ public:
     }
     virtual optional<expr> is_stuck(expr const &, extension_context &) const { return none_expr(); }
     virtual bool supports(name const &) const { return false; }
+    virtual bool is_recursor(environment const &, name const &) const { return false; }
 };
 
 static void tst3() {

tests/lean/640.hlean

@@ -0,0 +1,26 @@
+import hit.type_quotient
+
+open type_quotient eq sum
+
+  constants {A : Type} (R : A → A → Type)
+
+  local abbreviation C := type_quotient R
+
+  definition f [unfold-c 2] (a : A) (x : unit) : C :=
+  !class_of a
+
+  inductive S : C → C → Type :=
+  | Rmk {} : Π(a : A) (x : unit), S (f a x) (!class_of a)
+
+  set_option pp.notation false
+  set_option pp.beta false
+
+  definition rec {P : type_quotient S → Type} (x : type_quotient S) : P x :=
+  begin
+    induction x with c c c' H,
+    { induction c with b b b' H,
+      { apply sorry},
+      { apply sorry}},
+    { cases H, esimp, induction x,
+      { state, esimp, state, esimp, state, apply sorry}},
+  end

tests/lean/640.hlean.expected.out

@@ -0,0 +1,17 @@
+640.hlean:25:8: proof state
+P : type_quotient S → Type,
+c c' : C,
+a : A
+⊢ pathover P (type_quotient.rec (λ (b : A), sorry) (λ (b b' : A) (H : R b b'), sorry) (f a unit.star))
+    (eq_of_rel S (S.Rmk a unit.star))
+    sorry
+640.hlean:25:22: proof state
+P : type_quotient S → Type,
+c c' : C,
+a : A
+⊢ pathover P sorry (eq_of_rel S (S.Rmk a unit.star)) sorry
+640.hlean:25:36: proof state
+P : type_quotient S → Type,
+c c' : C,
+a : A
+⊢ pathover P sorry (eq_of_rel S (S.Rmk a unit.star)) sorry