fix(library/congr_lemma_manager): bug in congruence lemma generator

src/library/congr_lemma_manager.cpp

@@ -320,7 +320,8 @@ public:
             if (std::find(result_deps.begin(), result_deps.end(), i) != result_deps.end()) {
                 kinds[i] = congr_arg_kind::Fixed;
             } else if (pinfos[i].is_subsingleton()) {
-                if (empty(pinfos[i].get_dependencies()))
+                // See comment at mk_congr.
+                if (!pinfos[i].is_prop() && pinfos[i].is_dep())
                     kinds[i] = congr_arg_kind::Fixed;
                 else
                     kinds[i] = congr_arg_kind::Cast;

tests/lean/congr_lemma_bug.lean

@@ -0,0 +1,6 @@
+constant P : Type₁
+constant P_sub : subsingleton P
+attribute P_sub [instance]
+constant q : P → Prop
+
+#congr q

tests/lean/congr_lemma_bug.lean.expected.out

@@ -0,0 +1,4 @@
+[cast]
+λ (a a_1 : P), eq.trans (eq.refl (q a)) (congr (eq.refl q) (subsingleton.elim a a_1))
+:
+∀ (a a_1 : P), q a = q a_1

tests/lean/run/blast_congr_bug.lean

@@ -0,0 +1,21 @@
+constant P : Type₁
+constant P_sub : subsingleton P
+attribute P_sub [instance]
+constant q : P → Prop
+
+section
+set_option blast.simp true
+set_option blast.cc   false
+
+example (h₁ h₂ : P) : q h₁ = q h₂ :=
+by blast
+end
+
+
+section
+set_option blast.simp false
+set_option blast.cc   true
+
+example (h₁ h₂ : P) : q h₁ = q h₂ :=
+by blast
+end