Weird Behaviour of `apply`

Stream: mathlib4

[Wang Jingting]

@Nailin Guan found the following weird behavior of apply when working on the Gorenstein ring project, and we have obtained the following mwe:

import Mathlib

axiom P : Type* → Prop
axiom hP (α : AddCommGrpCat) (h : Subsingleton α) : P α

example (α β : Type*) [AddCommGroup β] (e : α ≃ β) (h : Subsingleton α) : P (AddCommGrpCat.of β) := by
  apply hP _ (e.subsingleton_congr.mp ?_)
  -- refine hP _ (e.subsingleton_congr.mp ?_)  -- Worked!
  -- apply hP (AddCommGrpCat.of β) (e.subsingleton_congr.mp ?_) -- Worked!
  sorry

The behavior is basically that in the apply not commented out, the tactic should have given us a new goal Subsingleton α, but in fact it shows no goals. However, if I delete the sorry line, it will report don't know how to synthesize placeholder on the ?_ (which is where we expected the new goal).

For comparison, the other two alternatives in the code snippet above both worked correctly, giving us a new goal. (and the behavior is not related to Subsingleton, we can reproduce it when replacing with a custom typeclass)

[Kyle Miller]

Re sorry: The "don't know how to synthesize placeholder" is part of a check at the end of elaboration. When there are other errors already (e.g. when you have a sorry even if there are no more goals), that error is not reported.

If the sorry is for illustrating that there are no goals remaining, the fact the by itself succeeds is sufficient.

[Kyle Miller]

I agree that it's bizarre that apply isn't collecting this ?_ goal if there is a _ placeholder.

Do you think it's specifically due to typeclasses? Can you reduce this to a self-contained example that does not depend on Batteries or Mathlib?

[Wang Jingting]

Kyle Miller said:

Re sorry: The "don't know how to synthesize placeholder" is part of a check at the end of elaboration. When there are other errors already (e.g. when you have a sorry even if there are no more goals), that error is not reported.

If the sorry is for illustrating that there are no goals remaining, the fact the by itself succeeds is sufficient.

If I understand you correctly, does that mean the apply tactic actually failed to synthesize the placeholder, therefore unable to create new goals, but the sorry on no goals is reported instead (because it's considered somehow more urgent?).

[Wang Jingting]

Kyle Miller said:

I agree that it's bizarre that apply isn't collecting this ?_ goal if there is a _ placeholder.

Do you think it's specifically due to typeclasses? Can you reduce this to a self-contained example that does not depend on Batteries or Mathlib?

We've tested that it doesn't rely on Subsingleton being a typeclass, and I'm now trying to also replace AddCommGrpCat with something else.

[Wang Jingting]

OK, I now have the following example to show that at least it has something to do with typeclass:

import Mathlib

class MyInstance (α : Type*) : Type

universe u
structure MyType : Type (u + 1) where
  (carrier : Type u)
  [str : MyInstance carrier]

instance : CoeSort MyType (Type u) := ⟨fun x ↦ x.carrier⟩

axiom P : Type* → Prop
axiom Q : Type* → Prop
axiom hP (α : MyType) (h : Q α) : P α
axiom Q_congr (α β : Type*) : Q α ↔ Q β

example (α β : Type*) [MyInstance β] (h : Q α) : P (MyType.mk β) := by
  apply hP _ ((Q_congr α β).mp ?_)

The current code reproduces that behavior, but if you comment out MyInstance part in the structure, the behavior will be back to expected.

[Junyan Xu]

If you delete import Mathlib and replace Type* by Type _ you get a mathlib-free example:

class MyInstance (α : Type _) : Type

universe u
structure MyType : Type (u + 1) where
  (carrier : Type u)
  [str : MyInstance carrier]

instance : CoeSort MyType (Type u) := ⟨fun x ↦ x.carrier⟩

axiom P : Type _ → Prop
axiom Q : Type _ → Prop
axiom hP (α : MyType) (h : Q α) : P α
axiom Q_congr (α β : Type _) : Q α ↔ Q β

example (α β : Type _) [MyInstance β] (h : Q α) : P (MyType.mk β) := by
  apply hP _ ((Q_congr α β).mp ?_)