Zulip Chat Archive

Stream: mathlib4

Topic: instance loop?


Winston Yin (Nov 22 2022 at 07:34):

Can somebody shed some light on why coe_mul in this file is giving the error:

(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

Also, coe_one just before this compiles but quite slowly. The problem goes away when the Monoid (Monoid.EndCat M) instance a little above is removed, so it's probably some instance loop I'm not seeing. The corresponding part in mathlib3 obviously has no such problem.

Eric Wieser (Nov 22 2022 at 09:34):

An aside; do we really want Monoid.EndCat and not just Monoid.End?

Eric Wieser (Nov 22 2022 at 09:35):

I assume EndCat is just an automated choice by mathport due to casing, and not a conscious decision (cc @Mario Carneiro)

Scott Morrison (Nov 22 2022 at 18:05):

Yes, EndCat here is certainly incorrect.

Winston Yin (Nov 22 2022 at 23:48):

Is there some command to see the instance search steps to catch this loop?

Scott Morrison (Nov 30 2022 at 18:26):

Could I summon some help on this question? mathlib4#659 is holding up pretty much everything at the moment.

The problem we're having is an instance loop once we define instance : Monoid (AddMonoid.End A).

Adding set_option trace.Meta.synthInstance true before the timeout, the typeclass search that is spiralling out of control is here.

It begins [] new goal CoeFun (AddMonoid.End A) _tc.0 ▶, and ends with the obviously broken:

[resume] propagating Monoid
        (Monoid.End
          (Monoid.End
            (Monoid.End
              (Monoid.End
                (Monoid.End
                  (Monoid.End
                    (Monoid.End
                      (Monoid.End
                        (Monoid.End
                          (Monoid.End
                            (Monoid.End
                              (Monoid.End
                                (AddMonoid.End A))))))))))))) to subgoal Monoid ?m.218081 of MulOneClass ?m.218081 

Gabriel Ebner (Nov 30 2022 at 19:14):

Things start going wrong here with the MonoidHomClass.toOneHomClass instance:

def MonoidHomClass.toOneHomClass.{u_1, u_2, u_3} : {F : Type u_1} 
  {M : outParam (Type u_2)} 
    {N : outParam (Type u_3)} 
      [inst : outParam (MulOneClass M)] 
        [inst_1 : outParam (MulOneClass N)]  [self : MonoidHomClass F M N]  OneHomClass F M N :=

What happens is that during function coercion, we need to synthesize an instance of FunLike E ?a ?b, then we're looking for OneHomClass E ?a ?b, and then we apply the instance above, which causes Lean to search for an instance of MulOneClass ?M. Or in other words, enumerate all reasonable multiplicative structures.

Gabriel Ebner (Nov 30 2022 at 19:15):

In Lean 3 we skipped arguments that were already assigned via unification, so we didn't run into this issue.

Scott Morrison (Nov 30 2022 at 20:07):

Is this something we can/should change in Lean 4? Should I start making a MWE?

Gabriel Ebner (Nov 30 2022 at 20:08):

MWE:

class Zero (A : Type u) where zero : A
class One (M : Type u) where one : M
class AddZeroClass (M : Type u) extends Zero M, Add M
class MulOneClass (M : Type u) extends One M, Mul M
structure ZeroHom (M : Type u) (N : Type v) [Zero M] [Zero N] where toFun : M  N
structure OneHom (M : Type u) (N : Type v) [One M] [One N] where toFun : M  N
structure AddMonoidHom (M) (N) [AddZeroClass M] [AddZeroClass N] extends ZeroHom M N
structure MonoidHom (M) (N) [MulOneClass M] [MulOneClass N] extends OneHom M N
class AddMonoid (M : Type u) extends AddZeroClass M
class Monoid (M : Type u) extends MulOneClass M
def AddMonoid.End (A) [AddZeroClass A] := AddMonoidHom A A
instance [AddZeroClass A] : Monoid (AddMonoid.End A) where
  one := {toFun := fun _ => Zero.zero}
  mul _ _ := {toFun := fun _ => Zero.zero}
def Monoid.End (M) [MulOneClass M] := MonoidHom M M
instance [MulOneClass M] : Monoid (Monoid.End M) where
  one := {toFun := fun _ => One.one}
  mul _ _ := {toFun := fun _ => One.one}

class FunLike (F : Sort u) (α : outParam (Sort v)) (β : outParam <| α  Sort w) where toFun : F   a, β a
class MulHomClass (F : Type u) (M N : outParam (Type _)) [outParam (Mul M)] [outParam (Mul N)] extends FunLike F M fun _ => N
class OneHomClass (F : Type u) (M N : outParam (Type _)) [outParam (One M)] [outParam (One N)] extends FunLike F M fun _ => N
class MonoidHomClass (F : Type u) (M N : outParam (Type _)) [outParam (MulOneClass M)] [outParam (MulOneClass N)]
  extends MulHomClass F M N, OneHomClass F M N
instance [FunLike F α β] : CoeFun F fun _ =>  a : α, β a where coe := FunLike.toFun
instance [AddZeroClass A] : Monoid (AddMonoid.End A) where one.toFun := id

set_option trace.Meta.synthInstance true
example {A} [AddZeroClass A] (f : AddMonoidHom A A) (a : A) : f a = f a := rfl

Scott Morrison (Nov 30 2022 at 20:29):

We can shrink that a bit to

class One (M : Type u) where one : M
class MulOneClass (M : Type u) extends One M, Mul M
structure OneHom (M : Type u) (N : Type v) [One M] [One N] where toFun : M  N
structure MonoidHom (M) (N) [MulOneClass M] [MulOneClass N] extends OneHom M N
class Monoid (M : Type u) extends MulOneClass M
def Monoid.End (M) [MulOneClass M] := MonoidHom M M
instance [MulOneClass M] : Monoid (Monoid.End M) where
  one := {toFun := fun _ => One.one}
  mul _ _ := {toFun := fun _ => One.one}

class FunLike (F : Sort u) (α : outParam (Sort v)) (β : outParam <| α  Sort w) where toFun : F   a, β a
class MulHomClass (F : Type u) (M N : outParam (Type _)) [Mul M] [Mul N] extends FunLike F M fun _ => N
class OneHomClass (F : Type u) (M N : outParam (Type _)) [One M] [One N] extends FunLike F M fun _ => N
class MonoidHomClass (F : Type u) (M N : outParam (Type _)) [MulOneClass M] [MulOneClass N]
  extends MulHomClass F M N, OneHomClass F M N
instance [FunLike F α β] : CoeFun F fun _ =>  a : α, β a where coe := FunLike.toFun
instance [MulOneClass A] : Monoid (Monoid.End A) where one.toFun := id

set_option trace.Meta.synthInstance true
example {A} [MulOneClass A] (f : MonoidHom A A) (a : A) : f a = f a := rfl

Scott Morrison (Nov 30 2022 at 20:30):

(removing the outParams on the typeclasses, after https://github.com/leanprover/lean4/issues/1852 was solved, and removed the additive structures, which aren't necessary to the example)

Scott Morrison (Nov 30 2022 at 20:41):

And further minimized:

class A (M : Type u) where m : M
structure Hom (M : Type u) (N : Type v) [A M] [A N] where toFun : M  N
def End (M) [A M] := Hom M M
instance [A M] : A (End M) where
  m := {toFun := fun _ => A.m}

class FunLike (F : Sort u) (α : outParam (Sort v)) (β : outParam <| α  Sort w) where
  toFun : F   a, β a
class HomClass (F : Type u) (M N : outParam (Type _)) [A M] [A N]
  extends FunLike F M fun _ => N
instance [FunLike F α β] : CoeFun F fun _ =>  a : α, β a where
  coe := FunLike.toFun

set_option trace.Meta.synthInstance true
example {X} [A X] (f : Hom X X) (a : X) : f a = f a := rfl

Gabriel Ebner (Nov 30 2022 at 20:44):

We're thinking alike. :smile: The End is a red herring, any instance that allows you to construct larger structures will do:

class Funny (F : Type _) (A B : outParam (Type _)) where toFun : F  A  B
instance [Funny F A B] : CoeFun F fun _ => A  B where coe := Funny.toFun
class MulHomClass (F) (A B : outParam _) [Mul A] [Mul B] extends Funny F A B
class Monoid (M) extends Mul M
instance [Mul A] : Mul (Id A) := _
set_option trace.Meta.synthInstance true
example [Monoid A] [Monoid B] [MulHomClass F A B] (f : F) (a : A) : f a = f a := rfl

Scott Morrison (Nov 30 2022 at 20:45):

Great!

Scott Morrison (Nov 30 2022 at 21:37):

I'm going to assume that either you'll work on diagnosing this, or make a lean 4 issue for it, or tell me that I should make a lean 4 issue.

Scott Morrison (Nov 30 2022 at 21:38):

In the meantime since this file is holding up other things, I'm going to comment out some instances and leave porting notes pointing to this thread, then hopefully merge the file.

Gabriel Ebner (Nov 30 2022 at 21:53):

You'd need to comment out a lot of stuff, or is this going to blow up really big. Note that the MulHomClass extends FunLike is enough to trigger the issue.

Gabriel Ebner (Nov 30 2022 at 21:54):

I've opened lean4#1901, but I don't think this is going to be fixed today.

Scott Morrison (Nov 30 2022 at 21:54):

Hmm... okay.

Yakov Pechersky (Nov 30 2022 at 22:16):

Should lean4 go back to is_monoid_hom style because of this?

Kevin Buzzard (Nov 30 2022 at 22:17):

I always thought that the reason we moved away from it was precisely because lean 3 had problems with it and we didn't want to wait for lean 4 which apparently wouldn't.

Winston Yin (Nov 30 2022 at 23:33):

Is the suggestion to switch from bundled hom structures back to mixins? Isn't it unavoidable to use bundled structures?

Eric Wieser (Dec 01 2022 at 00:04):

My understanding is that we would keep the bundled structures but discard instance : bundled_hom_class (bundled_hom A B) A B in favor of instance (h : bundled_hom A B) : is_hom f, where the latter has the advantage that you can do things like is_hom prod.fst too

Sebastien Gouezel (Dec 01 2022 at 14:59):

I'm trying to understand the difference between Lean 3 and Lean 4. In the issue, Gabriel explains that this comes from the instance

MulHomClass.toFunny [Mul A] [Mul B] [MulHomClass F A B] : Funny F A B

Is that related to the difference in instance resolution order (i.e., in Lean 3 we start with the last instance parameter, [MulHomClass F A B], and then this fixes A and B, while in Lean 4 we start with the first instance parameter [Mul A]and then since A is not fixed this goes crazy)?

If so, could we add an attribute to say that, in some lemma, one should start by the right-most instance instead of the leftmost? Or a crazy syntax like

MulHomClass.toFunny [Mul A] [Mul B] [MulHomClass F A B].{0} : Funny F A B

where one would start with the instance marked with .{0} if it exists, then the one marked with .{1} if it exists, and then the remaining ones (which are not solved by unification) from left to right?

Mario Carneiro (Dec 01 2022 at 15:00):

This actually already exists

Mario Carneiro (Dec 01 2022 at 15:00):

@[infer_tc_goals_rl]

Sebastian Ullrich (Dec 01 2022 at 15:00):

Not the crazy one though :)

Sebastien Gouezel (Dec 01 2022 at 15:01):

Does it help on this issue?

Mario Carneiro (Dec 01 2022 at 15:01):

I would prefer that any crazy extensions have crazy syntax confined to the attribute itself

Sebastien Gouezel (Dec 01 2022 at 15:07):

The crazy syntax would have been helpful to me once in mathlib 3. There was an [is_R_or_C 𝕜] field in the middle of assumptions, and it would have been helpful to start with this one because this can not blow up, restricting 𝕜 to be reals or complexes, while a later assumption was of the form [module 𝕜 F] not imposing anything on 𝕜, so Lean 3 would start with this instance search not knowing anything on 𝕜 and it would try all the rings it could imagine...

I think this one is solved by the left-to-right rule. But for performance reasons I can imagine situations where one would like to start with a middle instance because that would be the one that imposes the most restrictions and thus be the quickest to solve.

Eric Wieser (Dec 01 2022 at 15:41):

while in Lean 4 we start with the first instance parameter

Is this behavior desirable?

Floris van Doorn (Dec 01 2022 at 18:12):

Gabriel Ebner said:

I've opened lean4#1901, but I don't think this is going to be fixed today.

For people in certain time zones it was fixed the same day :tada: Thanks Leo!

Scott Morrison (Dec 02 2022 at 04:05):

Unfortunately it looks like the fix may need a fix: lean4#1907. This is holding up Algebra.Hom.Group in mathlib4#659 now.

Scott Morrison (Dec 02 2022 at 19:47):

Phew, this is finally solved! There's a little bit of version hell to deal with (we need to wait for nightly-2022-12-03, and also https://github.com/JLimperg/aesop/pull/32) before we can merge, but all the instance loops are gone now, solved by fixes in Lean 4 core.

Scott Morrison (Dec 02 2022 at 22:07):

If we don't mind working with an intermediate-between-nightlies commit of Lean 4, we could merge this today. Otherwise I'll be offline all of tomorrow, but hopefully someone could bump to 2022-12-03 when it is available and merge.

Jireh Loreaux (Dec 02 2022 at 22:10):

I'm fine with an intermediate Lean 4 version.

Gabriel Ebner (Dec 02 2022 at 22:12):

Yeah, let's go with the intermediate version. We've decided yesterday that waiting 24h+ is just slowing us down with no upsides.

Scott Morrison (Dec 02 2022 at 23:21):

Merged!


Last updated: Dec 20 2023 at 11:08 UTC