canonical instances

Stream: lean4

[Sébastien Gouëzel]

I've found the reason for the need for backward.synthInstance.canonInstances false in probability theory in many places in mathlib:

import Mathlib.Init.Logic

class FooClass (α : Type _) : Prop where

set_option backward.synthInstance.canonInstances false in -- if you comment this line, the instance is not found
lemma bar (α ι : Type _) [FooClass α] (f : ι → FooClass α) : FooClass α := by infer_instance

In this example, when looking for FooClass α, typeclass inference tries to apply f ?m.36, but it can not guess ?m.36, so it decides (rightly) that the instance can not be found here. Then it caches that there is no instance, and does not try to apply the main instance. I can't really decide if this is a bug (if typeclass inference fails because it can not guess a metavariable, then it shouldn't cache the failure) or a feature (after all, in the assumptions of bar one may argue that there are many different instances of FooClass α floating around, which shouldn't be allowed). Thoughts welcome!

This shows up often in probability theory, where there is a main instance [mΩ : MeasurableSpace Ω], and sub-sigma-algebras parameterized by time, i.e., 𝓕 : ℕ → MeasurableSpace Ω. A workaround is to declare mΩ after 𝓕 to make sure it's the one which is tried first, but for instance if you define a sequence of sub-sigma-algebras inside a proof this won't work. Not so bad when you're aware of the issue, but newcomers may easily get bitten by this.

[Michael Stoll]

It is not clear to me why lean4#4003 has the effect that there is no backtracking here. My understanding is that it should not backtrack to search for solutions of an instance search problem after one had been found already, but here no instance has been found at the relevant point.

[Sébastien Gouëzel]

Reported as lean#4213.

[Kim Morrison]

This has been fixed in lean#4216, and will land in v4.9.0-rc1 at the beginning of June (but if you tell me you want it now, v4.8.0-rc2 is probably okay, which will land in a day or two).

[Sébastien Gouëzel]

It can definitely wait for 4.9. Thanks!