Class instance problem

Stream: maths

[Roman Fedorov]

Can anybody tell me why this code does not work (it says it fails to synthesize instance of add_monoid M):
example : Prop := ∀ (M : Type 0) [add_monoid M] (f : M →+ MM), true. Thanks!

[Johan Commelin]

Tip: use #backticks to format code on Zulip

[Kevin Buzzard]

It's because add_monoid is after the colon.

[Jalex Stark]

example (M : Type 0) [add_monoid M] (f : M →+ M) : Prop := true

gives no errors for me

[Reid Barton]

You can write it like this:
example : Prop := ∀ (M : Type 0) [add_monoid M], by exactI ∀ (f : M →+ M), true

[Reid Barton]

More obscurely, this version also works for some reason:

structure ex : Prop :=
(h : ∀ (M : Type 0) [add_monoid M] (f : M →+ M), true)

[Reid Barton]

The reason the original doesn't work is there is something called the "instance cache" where Lean looks for instances (like add_monoid M), and variables introduced by ∀ and other binders don't get added to the cache automatically, only variables that appear in the arguments before the : like in Jalex's example.

[Reid Barton]

exactI is a tactic that's like exact but first causes everything in scope to get added to the instance cache.
(There are some other related tactics.)

[Roman Fedorov]

Thanks for the answers! But is there a better way to quantify over a module (or more generally, over something inferred by class resolution)?

[Kenny Lau]

what's wrong with ∀ (M : Type 0) [add_monoid M], by exactI ∀ (f : M →+ M), true as suggested by Reid?

[Reid Barton]

Well it's a bit inconvenient of course. I wonder whether the behavior will change in Lean 4.