Cannot synthesize an instance in v4.8.0-rc1

Stream: general

[Peiran Wu]

I was trying to bump a project to v4.8.0-rc1 but encountered a strange error. It looked to me like a bug.

MWE:

import Mathlib.Algebra.Module.Submodule.Basic

variable (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M] (N : Submodule R M)

#synth Nonempty N -- succeeds with `instNonemptyOfInhabited`
#synth Zero N.toAddSubgroup -- succeeds with `N.toAddSubgroup.zero`
#synth Nonempty N.toAddSubgroup -- fails

example : Nonempty N.toAddSubgroup :=
  Zero.instNonempty

As commented on above, the third #synth fails, even though the statement given can be exactly proved with the instance Zero.instNonempty, which in turn relies on the instance in the second #synth.

Such an error did not occur in v4.7.0.

[Kim Morrison]

Thanks. We've noticed previously a problem with Nonempty instances, but I don't think we have a minimization.

[Kim Morrison]

If you @Peiran Wu, or anyone else, would be interested in trying to extract a Mathlib free minimization of this problem, that would be really helpful.

[Kim Morrison]

(I can try too, but might not get to it immediately.)

[Peiran Wu]

I see. I'll play around with this later and see if I can avoid Mathlib dependency. But other people's help would definitely be appreciated.