conv’s arg fails with subsingleton parameters

[nomeata]

Consider

opaque foo (p : Prop) [Decidable p] : Prop

/--
error: tactic 'rfl' failed, equality expected
  Decidable ?m.58
p : Prop
inst✝ : Decidable p
⊢ Decidable ?m.58
-/
#guard_msgs in
example  [Decidable p] : foo p := by
  conv => arg 1
  sorry

The problem seems to be this code:

private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i : Int) :
  TacticM Unit := do
  if i >= 0 then
    let i := i.toNat
    if h : i < mvarIds.length then
      for mvarId? in mvarIds, j in [:mvarIds.length] do
        match mvarId? with
        | none => pure ()
        | some mvarId =>
          if i != j then
            mvarId.refl
      match mvarIds[i] with
      | none => throwError "cannot select argument"
      | some mvarId => replaceMainGoal [mvarId]
      return ()
  throwError "invalid '{tacticName}' conv tactic, application has only {mvarIds.length} (nondependent) argument(s)"

This assumes that all goals in mvarIds, which is the result of

def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) :
    MetaM (List (Option MVarId))

are equality goals, but due to

      | .subsingletonInst =>
        proof := mkApp proof arg
        let rhs ← mkFreshExprMVar (← whnf (← inferType proof)).bindingDomain!
        proof := mkApp proof rhs
        mvarIdsNewInsts := mvarIdsNewInsts.push (some rhs.mvarId!)

there this can also contain subsingleton goals.

Probably these should be solved, once the new p is known, using type class search?

Versions

4.10.0-nightly-2024-06-07

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

I was curious so had a deeper look.

This might be a fix:

diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean
index 9060bd91d6..de4dee1bc5 100644
--- a/src/Lean/Elab/Tactic/Conv/Congr.lean
+++ b/src/Lean/Elab/Tactic/Conv/Congr.lean
@@ -75,20 +75,28 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) :
 @[builtin_tactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun _ => do
   replaceMainGoal <| List.filterMap id (← congr (← getMainGoal))

+-- mvarIds is the list of goals produced by congr. We only want to change the one at position `i`
+-- so this closes all other equality goals with `rfl.`. There are non-equality goals produced
+-- by `congr` (e.g. dependent instances), thes are kept as goals.
 private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i : Int) :
   TacticM Unit := do
   if i >= 0 then
     let i := i.toNat
     if h : i < mvarIds.length then
+      let mut otherGoals := #[]
       for mvarId? in mvarIds, j in [:mvarIds.length] do
         match mvarId? with
         | none => pure ()
         | some mvarId =>
           if i != j then
-            mvarId.refl
+            if (← mvarId.getType').isEq then
+              mvarId.refl
+            else
+              -- If its not an equality, it's likely a class constraint, to be left open
+              otherGoals := otherGoals.push mvarId
       match mvarIds[i] with
       | none => throwError "cannot select argument"
-      | some mvarId => replaceMainGoal [mvarId]
+      | some mvarId => replaceMainGoal (mvarId :: otherGoals.toList)
       return ()
   throwError "invalid '{tacticName}' conv tactic, application has only {mvarIds.length} (nondependent) argument(s)"

But while testing it I found this:

class Foo (n : Nat) where
opaque P (n : Nat) [Foo n] : Prop
/-- error: cannot select argument -/
#guard_msgs in
example (n : Nat) [Foo n] : P n := by conv => arg 1

Why does this behave differently than the Prop variant above? Digging deeper I find that conv behaves differently depending on whether the class is type or prop valued, and whether the index of the class is prop or a nat:

import Lean
open Lean Elab Meta Tactic
opaque foo (p : Prop) [Decidable p] : Prop
class PropClass (n : Nat) : Prop where
opaque P1 (n : Nat) [PropClass n] : Prop
class TypeClass (n : Nat) : Type where
opaque P2 (n : Nat) [TypeClass n] : Prop

/--
info: thm for foo: ∀ (p p_1 : Prop), p = p_1 → ∀ {inst : Decidable p} {inst_1 : Decidable p_1}, foo p = foo p_1
kinds: #[Lean.Meta.CongrArgKind.eq, Lean.Meta.CongrArgKind.subsingletonInst]
---
info: thm for P1: ∀ (n n_1 : Nat) (e_n : n = n_1) [inst : PropClass n], P1 n = P1 n_1
kinds: #[Lean.Meta.CongrArgKind.eq, Lean.Meta.CongrArgKind.cast]
---
info: thm for P2: ∀ (n : Nat) [inst : TypeClass n], P2 n = P2 n
kinds: #[Lean.Meta.CongrArgKind.fixed, Lean.Meta.CongrArgKind.fixed]
-/
#guard_msgs in
run_meta
  #[``foo, ``P1, ``P2].forM fun n => do
    let e ← mkConstWithLevelParams n
    let some thm ← mkCongrSimp? e (subsingletonInstImplicitRhs := false) | throwError "no thm"
    let kinds ← getCongrSimpKinds e (← getFunInfo e)
    logInfo m!"thm for {e}: {thm.type}\nkinds: {repr kinds}"

So this does not work:

/-- error: cannot select argument -/
#guard_msgs in
example [TypeClass n] [TypeClass (id n)] (h : P2 n) : P2 (id n) := by
  conv => arg 1

And this worked before

example [PropClass n] [PropClass (id n)] (h : P1 n) : P1 (id n) := by
  conv => arg 1; rw [id]
  exact h

And my fix seems only to matter for .subsingletonInst, as now we can do

example [Decidable p] [Decidable (id p)] (h : foo p) : foo (id p) := by
  conv => arg 1; rw [id]
  exact h

So this looks plausible, although I certainly don’t understand the conv machinery here well enough to say that with confidence.

[nomeata]

One effect of this fix is that arg 1 can produce multiple goals. It looks like conv solves them when they are left over, but they do show up to the user, just as if they’d use the congr conv tactic:

/--
error: tactic 'fail' failed
p : Prop
inst✝ : Decidable p
⊢ Decidable (id p)
---
error: unsolved goals
p : Prop
inst✝ : Decidable p
⊢ foo (id p)
-/
#guard_msgs in
example [Decidable p] : foo p := by
  conv =>
    arg 1
    · rw [← id.eq_def p]
    · tactic => fail

Not sure if that’s intended for the arg 1 tactic.