typeclass timeout

Stream: mathlib4

[Winston Yin]

import Mathlib.Algebra.Hom.Group
import Mathlib.Logic.Equiv.Basic
import Mathlib.Data.Pi.Algebra -- commenting this out makes #synth below work

structure MulEquiv (M N : Type _) [Mul M] [Mul N] extends M ≃ N, M →ₙ* N

infixl:25 " ≃* " => MulEquiv

class MulEquivClass (F A B : Type _) [outParam <| Mul A] [outParam <| Mul B] extends EquivLike F A B where
  map_mul : ∀ (f : F) (a b), f (a * b) = f a * f b

instance (priority := 100) [Mul M] [Mul N] [h : MulEquivClass F M N] : MulHomClass F M N :=
  { h with coe := h.coe, coe_injective' := FunLike.coe_injective' }

instance [Mul M] [Mul N] : MulEquivClass (M ≃* N) M N where
  coe f := f.toFun
  inv f := f.invFun
  left_inv f := f.left_inv
  right_inv f := f.right_inv
  coe_injective' f g h₁ h₂ := by
    cases f
    cases g
    congr
    apply Equiv.coe_fn_injective h₁
  map_mul := MulEquiv.map_mul'

variable [Mul M] [Mul N]
#synth MulHomClass (M ≃* N) M N -- succeeds/fails depending on Mathlib.Data.Pi.Algebra

[Winston Yin]

Something in the recently merged Data.Pi.Algebra causes some typeclass problems to end in a timeout. How can I debug this?

[Winston Yin]

(For Algebra.Hom.Group one would need to merge mathlib4#659)

[Winston Yin]

If I set_option trace.Meta.synthInstance true, it just tells me my MulHomClass typeclass problem has exploded :boom:, and then the VSCode Infoview crashed

[Jon Eugster]

Random guess, is that maybe a problem of instance priorities? I ported that file. it's been lying around in review for a while, I think instance priority wasn't available at all when I started it.
Can debug this later today!

[Winston Yin]

Thanks for looking into this. I don't really understand instance priorities yet, so I would love it if you found a fix and could help me understand it!

[Jon Eugster]

The error seems to come from the MulHomClass in Algebra.Hom.Group:

class MulHomClass (F : Type _) (M N : outParam (Type _)) [outParam (Mul M)] [outParam (Mul N)]
  extends FunLike F M fun _ => N where [...]

If (M N : Type _) are not marked with outParam, then your example works fine:

class MulHomClass (F : Type _) (M N : Type _) [outParam (Mul M)] [outParam (Mul N)]
  extends FunLike F M fun _ => N where [...]

Since they are marked with outParam it tries to find MulHomClass (M ≃* N) ?m.10225 ?m.10226 and then tries literally everything for the two unknowns (which schould be M N), starting with things like MulHomClass (M ≃* N) N Rat and other non-sense.

The reason that Data.Pi.Algebra causes a timeout is that it ends up trying something like MulHomClass (M ≃* N) N (?m.10699 →ₙ* ?m.10700) at which point it would fail without Pi.instMul, but with it, it goes mayham.

Lean 3 code was:

class mul_hom_class (F : Type*) (M N : out_param $ Type*)
  [has_mul M] [has_mul N] extends fun_like F M (λ _, N) :=

So I guess my question is why does it seem that the outParam should move from M, N to Mul M, Mul N in Lean4? I know very little about outParam

[Jon Eugster]

(I added this comment to mathlib4#659 but I don't know for sure if that's the correct approach)

[Jon Eugster]

Winston Yin said:

If I set_option trace.Meta.synthInstance true, it just tells me my MulHomClass typeclass problem has exploded :boom:, and then the VSCode Infoview crashed

As for the debugging, I used

set_option trace.Meta.synthInstance true
set_option synthInstance.maxHeartbeats 800

that avoids the crash you mentioned :)

[Winston Yin]

Above problem still persists in mathlib4#835, after lean4#1901 and lean4#1907 :sad:

[Eric Wieser]

Those outParams on M and N should definition be there, I think there is another thread on this

[Kevin Buzzard]

(deleted)

[Scott Morrison]

This typeclass timeout is still a problem at mathlib4#835. @Jon Eugster has suggested a fix above, but it just doesn't make sense to me (and causes other errors).

[Scott Morrison]

The typeclass search spiralling out of control can be viewed at https://gist.github.com/semorrison/2d5249762d6ea4ed6b07cf0b555acd32

[Scott Morrison]

@Gabriel Ebner, if you'd have a chance to look at this sometime...?

[Gabriel Ebner]

Can we merge mathlib4#865 first and then see what the linter has to say?

[Scott Morrison]

Your conversation with Mario there is tangential right, and merging doesn't need to wait for it?

[Scott Morrison]

I'm trying out the combination of mathlib4#865 and mathlib4#835 on branch hom_equiv_basic_2.

[Gabriel Ebner]

Yeah, nobody has objected to the PR yet. All the objectionable parts are already merged in std4 after all. :smile:

[Scott Morrison]

Okay, so

import Mathlib.Data.FunLike.Equiv

class AddEquivClass (F A B : Type _) [Add A] [Add B] extends EquivLike F A B where
  map_add : ∀ (f : F) (a b), f (a + b) = f a + f b

#lint

now says:

/- The `dangerousInstance` linter reports:
SOME INSTANCES ARE DANGEROUS
During type-class search, they produce subgoals like `Group ?M`.
Try marking the dangerous arguments as implicit instead. -/
#check @AddEquivClass.toEquivLike /- generates subgoals with metavariables: argument 4 inst✝¹ : Add
  ?A, argument 5 inst✝ : Add ?B -/

[Gabriel Ebner]

It needs to be:

class AddEquivClass (F : Type _) (A B : outParam (Type _)) [Add A] [Add B] extends EquivLike F A B where

[Scott Morrison]

Hooray, that, and changing a few arguments to implicits later, solves all the problems in this PR.

[Scott Morrison]

... besides a bunch of linting problems, if anyone feels like tackling those. :-)

[Jon Eugster]

writing

instance (priority := 100) {_ : Mul M} {_ : Mul N} [h : MulEquivClass F M N] : MulHomClass F M N :=

instead of

instance (priority := 100) [Mul M] [Mul N] [h : MulEquivClass F M N] : MulHomClass F M N :=

is definitely a trick I didn't know about, cool :partying_face:

[Eric Wieser]

Didn't we use to do that all the time in Lean 3, but then typeclass search changed and now it has basically no effect there?

[Winston Yin]

I ported Algebra.Hom.Group and kept a few of these { _ : Mul A} in there. Not needed anymore?

[Jon Eugster]

Really? But looking at the last PR by Scott it seems that's been done in about 3-4 places? and in the above mwe it is one way to synth the instance.
I'd be curious to understand things better :)