evil instances?

Stream: general

[Jireh Loreaux]

Is there something evil about the instances docs#algebra.elemental_algebra.comm_ring docs#elemental_star_algebra.comm_semiring docs#elemental_star_algebra.comm_ring, like maybe because they are declared using a reducible def?

Reason I ask: I'm trying to fix the timeout in #17164 and I traced it to these instances (which weren't imported before where the timeout occurs, but are now). Easiest way to reproduce the timeout: On master, add import topology.algebra.star_subalgebra to number_theory.modular_forms.slash_actions. If you deinstance the aforementioned declarations locally then the timeout disappears.

[Eric Wieser]

Is docs#subalgebra.comm_ring_topological_closure already ported?

[Jireh Loreaux]

No. Why?

[Eric Wieser]

Sorry, I though I was looking at a porting stream, ignore that comment

[Eric Wieser]

Does adding mul := (*) etc to subalgebra.comm_ring_topological_closure help?

[Jireh Loreaux]

No.

[Jireh Loreaux]

Hmmm, it doesn't timeout here (with or without the mul) but instead gives the error

maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

almost immediately, which makes me feel like it's looping or something.

[Floris van Doorn]

Those three instances look completely fine to me. The assumptions are all type-classes on R and A, both of which occur in the conclusion.
What is declared using a reducible def?

[Floris van Doorn]

It is probably looping, you can try set_option trace.class_instances true and looking at all of the instances in the loop (look at the [nn] numbers to see how deep you are in the loop.

[Jireh Loreaux]

Huh, I don't entirely understand the issue, but removing the local notation ↑ₘ on γ here solves the problem. This local notation has some holes, so perhaps it's sending Lean down the wrong path somehow. (I think because it needs to find a chain of several coercions). @Chris Birkbeck : since you authored the file, do you have any obejctions if I replace ↑ₘγ with just γ here (assuming everything later works fine)?

[Jireh Loreaux]

And Floris, I didn't see any clear looping (although instance search did go deep into over a thousand metavariables), but it seemed to be spending all it's time looking for coercions, consistent with the above.

[Chris Birkbeck]

Oh I have no problem changing it if its helps (and doesnt break anything). This notation is also used in ...number_theory.modular and ...matrix.special_linear_group. But I'm guessing there are no issues there.

[Eric Wieser]

Is thisthe matrix coe notation?

[Eric Wieser]

The problem is that if you write g 0 1 you get ⇑g 0 1 which isn't simp-normal

[Eric Wieser]

But the only way to get the simp-normal ↑g 0 1 is with painful annotations

[Eric Wieser]

Making matrix a structure would solve this

[Jireh Loreaux]

@Chris Birkbeck : given the simp normal form issue Eric raised, how do you feel about an additional local notation ↑ₘ[R] that allows you to specify the ring R? This seems to also solve the issue. I'll leave the ↑ₘ notation where it works and add a note where ↑ₘ[R] is declared stating that it exists to help Lean elaborate in certain contexts.

[Chris Birkbeck]

Oh yeah thats better! It really is just a convenience since we dont want to keep writing (M : matrix n n R) or something, but I didn't know it would cause issues, so I'm for any change that fixes this.