stuck typeclass problem in try/catch

Stream: mathlib4

[Matthew Ballard]

In mathlib4#2109, I made an attempt at porting slice and its descendants. While it is not the most pretty, I am reasonably confident it is executing properly, at least on rewrites.

I am encountering a typeclass instance problem is stuck error which I do not completely understand.

For my best an awful #mwe example, see below. I have included a similar example in Slice.lean in the branch and have included a worked-on Equivalence.lean file with similar behavior (sliceLHS can be used to solve the goal modulo this).

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.Tactic.Conv

open CategoryTheory
open Lean Parser.Tactic Elab Command Elab.Tactic Meta

def test : TacticM Unit := do
   iterateUntilFailure do
    ``(Category.assoc) >>= fun e => rewriteTarget' e (symm := false)

elab "test" : tactic => test

variable (C : Type) [Category C] (X Y Z W : C)
variable (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W)

example : (f ≫ g) ≫ h = ((f ≫ g) ≫ h := by
  test — typeclass instance problem is stuck
  rfl

Replacing iterateUntilFailure with iterateAtMost 1removes the error. iterateAtMost 2 brings it back.

[Matthew Ballard]

I can try to minimize this further later this evening after teaching/dinner but it appears the error is coming from the catch branch in the iteration tactics.

[Matthew Ballard]

unit_inverse_comp in the equivalences file in that branch is a fun illustration.

[Thomas Murrills]

Interesting! (Btw, I've just moved the test from Slice.lean into test/slice.lean, where it can stay forever as a useful test of this issue!)

[Matthew Ballard]

Here is a better #mwe:

import Lean.Elab.Tactic
open Lean Parser.Tactic Elab Command Elab.Tactic Meta

class Assoc (α : Type) extends Mul α where
  assoc : ∀ a₁ a₂ a₃ : α , (a₁ * a₂) * a₃ = a₁ * (a₂ * a₃)

variable [Monad m] [MonadExceptOf Exception m]

partial def iterateUntilFailure (tac : m Unit) : m Unit :=
  try tac; iterateUntilFailure tac catch _ => pure ()

def iterateAtMost : Nat → m Unit → m Unit
| 0, _ => pure ()
| n + 1, tac => try tac; iterateAtMost n tac catch _ => pure ()

def test : TacticM Unit := do
  iterateUntilFailure do
    evalTactic <| ← `(conv| rw [Assoc.assoc])

elab "test" : conv => test

variable (α : Type) [Assoc α]

example (a₁ a₂ a₃ : α) : (a₁ * a₂) * a₃ = a₁ * (a₂ * a₃) := by
  conv =>
    lhs
    test -- typeclass instance problem is stuck, it is often due to metavariables Assoc ?m.7325

Add rfl to the example

example (a₁ a₂ a₃ : α) : (a₁ * a₂) * a₃ = a₁ * (a₂ * a₃) := by
  conv =>
    lhs
    test
  rfl -- no goals to be solved

Replacing iterateUntilFailure with iterateAtMost 1 removes the original error. With iterateAtMost 2 it returns.

[Matthew Ballard]

Specializing m to TacticM seems to have fixed the issue.

[Adam Topaz]

If you change MonadExceptOf to MonadExcept then it also works.

[Adam Topaz]

I guess the metavariable that lean is complaining about is Exception in the MonadExceptOf variable

[Matthew Ballard]

Is that where the Category metavariable would land?

[Adam Topaz]

I'm not sure what you mean

[Matthew Ballard]

Sorry. For this one, it complains about finding an instance of Assoc.

[Adam Topaz]

Oh

[Adam Topaz]

Okay now I'm confused. This also works:

import Lean.Elab.Tactic
open Lean Parser.Tactic Elab Command Elab.Tactic Meta

class Assoc (α : outParam Type) extends Mul α where
  assoc : ∀ a₁ a₂ a₃ : α , (a₁ * a₂) * a₃ = a₁ * (a₂ * a₃)

variable [Monad m] [MonadExceptOf Exception m]

partial def iterateUntilFailure (tac : m Unit) : m Unit :=
  try tac; iterateUntilFailure tac catch _ => pure ()

def test : TacticM Unit := do
  iterateUntilFailure do
    evalTactic <| ← `(conv| rw [Assoc.assoc])

elab "test" : conv => test

variable (α : Type) [Assoc α]

example (a₁ a₂ a₃ : α) : (a₁ * a₂) * a₃ = a₁ * (a₂ * a₃) := by
  conv =>
    lhs
    test

[Adam Topaz]

It seems that typeclass search just gets stuck even though it shouldn't?

[Matthew Ballard]

Yes. It seems so. Putting rfl at the end convinces Lean that all goals are cleared.

[Adam Topaz]

what's the set_option for typeclass tracing?

[Thomas Murrills]

Nice catch, because this is really weird to me. Even specifying the monad with iterateUntilFailure (m := TacticM) ... in the calls doesn't help—it actually has to be in the type declaration.

[Matthew Ballard]

set_option trace.Meta.synthInstance true only for #synth?

[Adam Topaz]

no that's the one

[Adam Topaz]

I don't really know why it's failing.

[Matthew Ballard]

(aside: slice is working well enough now that I am trying to kill off !4#1287 before bed)

[Adam Topaz]

Is there any reason why one should not just use MonadExcept here?

[Matthew Ballard]

I took the tactic iterators from Mathlib.Tactic.Corewithout much thought

[Adam Topaz]

Oh I see.

[Matthew Ballard]

But I doubt you would have much to break if you changed them there

[Adam Topaz]

I'll leave that to the tactic writing experts to decide.

[Thomas Murrills]

It's strange to me that making everything explicit doesn't work either. I wouldn't have expected this—but I guess that's the magic of outparams, which I don't understand yet.

def inst : MonadExceptOf Exception TacticM := inferInstance

partial def iterateUntilFailure' {m : Type _ → Type u} [m₀ : Monad m] [m₁ : MonadExceptOf Exception m] (tac : m Unit) : m Unit :=
  try tac; @iterateUntilFailure' m m₀ m₁ tac catch _ => pure ()

def test : TacticM Unit := do
  @iterateUntilFailure' TacticM instMonadTacticM inst do
    rewriteTarget' (← ``(Category.assoc)) (symm := false)

-- same issues occur

[Thomas Murrills]

Btw, the defs in that block of Mathlib.Tactic.Core which depend on [MonadExceptOf Exception m] are only used in slice and tauto. If tauto works with the change, I would hope we could just change it to [MonadExcept Exception m]—but I'm not sure why that choice was made in the first place, so we should confirm with an expert.

[Thomas Murrills]

In any case, it's great that it's working! Thanks for porting it! :)

[Thomas Murrills]

In terms of git organization (which you might be planning to do already, but just mentioning since I don’t see it on GitHub): I think !4#1287 should be made to depend on !4#2109, and !4#2109 shouldn’t include Equivalence.

[Matthew Ballard]

Agreed. Once I get equivalences working or give up, I will clean and arrange things.

[Thomas Murrills]

Another thing you might be planning already anyway, but: I think we should go ahead and change MonadExceptOf to MonadExcept in that spot in Tactic.Core, check that nothing breaks, link to this thread in the PR description, and the change will get seen and confirmed by an expert during review.

[Matthew Ballard]

This should be done now. Please check my work.