feat: avoid [Decidable p] instance implicit parameters in congruence theorems when possible

src/Lean/Elab/Tactic/Conv/Congr.lean

@@ -30,8 +30,10 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) : MetaM (List (Option MVa
   else if lhs.isApp then
     let funInfo ← getFunInfo lhs.getAppFn
     let args := lhs.getAppArgs
-    let some congrThm ← mkCongrSimp? lhs.getAppFn | throwError "'congr' conv tactic failed to create congruence theorem"
-    unless args.size == congrThm.argKinds.size do throwError "'congr' conv tactic failed, unexpected number of arguments in congruence theorem"
+    let some congrThm ← mkCongrSimp? lhs.getAppFn (subsingletonInstImplicitRhs := false)
+      | throwError "'congr' conv tactic failed to create congruence theorem"
+    unless args.size == congrThm.argKinds.size do
+      throwError "'congr' conv tactic failed, unexpected number of arguments in congruence theorem"
     let mut proof := congrThm.proof
     let mut mvarIdsNew := #[]
     let mut mvarIdsNewInsts := #[]

src/Lean/Meta/CongrTheorems.lean

@@ -197,7 +197,7 @@ def getCongrSimpKinds (info : FunInfo) : Array CongrArgKind := Id.run do
 /--
   Create a congruence theorem that is useful for the simplifier and `congr` tactic.
 -/
-partial def mkCongrSimpCore? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) : MetaM (Option CongrTheorem) := do
+partial def mkCongrSimpCore? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) (subsingletonInstImplicitRhs : Bool := true) : MetaM (Option CongrTheorem) := do
   if let some result ← mk? f info kinds then
     return some result
   else if hasCastLike kinds then
@@ -242,9 +242,12 @@ where
               let rhs ← mkCast lhss[i]! rhsType info.paramInfo[i]!.backDeps eqs
               go (i+1) (rhss.push rhs) (eqs.push none) hyps
             | .subsingletonInst =>
-              let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss
-              withLocalDecl (← lhss[i]!.fvarId!.getDecl).userName BinderInfo.instImplicit rhsType fun rhs =>
-                go (i+1) (rhss.push rhs) (eqs.push none) (hyps.push rhs)
+              -- The `lhs` does not need to instance implicit since it can be inferred from the LHS
+              withNewBinderInfos #[(lhss[i]!.fvarId!, .implicit)] do
+                let rhsType := (← inferType lhss[i]!).replaceFVars (lhss[:rhss.size]) rhss
+                let rhsBi   := if subsingletonInstImplicitRhs then .instImplicit else .implicit
+                withLocalDecl (← lhss[i]!.fvarId!.getDecl).userName rhsBi rhsType fun rhs =>
+                  go (i+1) (rhss.push rhs) (eqs.push none) (hyps.push rhs)
         return some (← go 0 #[] #[] #[])
     catch _ =>
       return none
@@ -276,9 +279,17 @@ where
             mkLambdaFVars #[lhs, rhs] (← mkEqNDRec motive proofSub heq)
      go 0 type
 
-def mkCongrSimp? (f : Expr) : MetaM (Option CongrTheorem) := do
+/--
+Create a congruence theorem for `f`. The theorem is used in the simplifier.
+
+If `subsinglentonInstImplicitRhs = true`, the the `rhs` corresponding to `[Decidable p]` parameters
+is marked as instance implicit. It forces the simplifier to compute the new instance when applying
+the congruence theorem.
+For the `congr` tactic we set it to `false`.
+-/
+def mkCongrSimp? (f : Expr) (subsingletonInstImplicitRhs : Bool := true) : MetaM (Option CongrTheorem) := do
   let f := (← instantiateMVars f).cleanupAnnotations
   let info ← getFunInfo f
-  mkCongrSimpCore? f info (getCongrSimpKinds info)
+  mkCongrSimpCore? f info (getCongrSimpKinds info) (subsingletonInstImplicitRhs := subsingletonInstImplicitRhs)
 
 end Lean.Meta

src/Lean/Meta/Tactic/Congr.lean

@@ -45,7 +45,7 @@ def MVarId.congr? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
     let some (_, lhs, _) := target.eq? | return none
     let lhs := lhs.cleanupAnnotations
     unless lhs.isApp do return none
-    let some congrThm ← mkCongrSimp? lhs.getAppFn | return none
+    let some congrThm ← mkCongrSimp? lhs.getAppFn (subsingletonInstImplicitRhs := false) | return none
     applyCongrThm? mvarId congrThm
 
 /--

tests/lean/congrThm.lean

@@ -0,0 +1,10 @@
+import Lean
+opaque g (p : Prop) [Decidable p] (a : Nat) (h : a > 0) : Nat
+
+open Lean Meta
+def test (flag : Bool) : MetaM Unit := do
+  let some congrThm ← mkCongrSimp? (mkConst ``g) (subsingletonInstImplicitRhs := flag) | throwError "failed to generate theorem"
+  IO.println (← ppExpr congrThm.type)
+
+#eval test false
+#eval test true

tests/lean/congrThm.lean.expected.out

@@ -0,0 +1,8 @@
+∀ (p p_1 : Prop),
+  p = p_1 →
+    ∀ {inst : Decidable p} {inst_1 : Decidable p_1} (a a_1 : Nat),
+      a = a_1 → ∀ (h : a > 0), g p a h = g p_1 a_1 (_ : a_1 > 0)
+∀ (p p_1 : Prop),
+  p = p_1 →
+    ∀ {inst : Decidable p} [inst_1 : Decidable p_1] (a a_1 : Nat),
+      a = a_1 → ∀ (h : a > 0), g p a h = g p_1 a_1 (_ : a_1 > 0)