instance synth failure

Stream: mathlib4

[Kevin Buzzard]

This surprised me. I am running a Lean alg geom workshop next week so I thought I'd try and make the scheme associated to an elliptic curve. I made two affine patches but when attempting to glue them I ran into an error which I've minimised to this:

import Mathlib

suppress_compilation

inductive S : Type
| x : S
| y : S

abbrev R : Type := MvPolynomial S ℂ

abbrev R.x : R := MvPolynomial.X S.x
abbrev R.y : R := MvPolynomial.X S.y

open R in
abbrev I : Ideal R := Ideal.span {y^2 - x^3 - 1}

abbrev Q := R ⧸ I

variable (A : Type) [CommRing A] in
#synth DistribMulAction A A -- works

#synth CommRing Q -- works
-- #synth DistribMulAction Q Q -- fails

set_option maxSynthPendingDepth 37 in
#synth DistribMulAction Q Q -- still fails

My experience was that setting maxSynthPendingDepth to be something like 2 would usually solve these problems.

[Matthew Ballard]

That seems to step just outside of the default limits for synthesis

[Eric Wieser]

set_option synthInstance.maxHeartbeats 21000 fixes it

[Kevin Buzzard]

Oh I'm a fool, thanks.

[Matthew Ballard]

Eric Wieser said:

set_option synthInstance.maxHeartbeats 21000 fixes it

Even 20150 works for me :)

[Matthew Ballard]

As does not using the abbrev. Lean doesn't want to peak into R for the matching on the keys which results in a ton of hits

[Matthew Ballard]

But the difference in heartbeats isn't very big without abbrev

[Kevin Buzzard]

I went with abbrevs everywhere because I wanted notation and didn't want to write weird stuff in front of the students justifying that things which were obviously rings, were rings. Maybe that's my mistake

[Matthew Ballard]

No I would expect the matching on keys to look into the abbrev. Notation makes sense