Typeclass inference question

Stream: new members

[VayusElytra]

Hi, I am curious about this snipper of code from Mathematics in Lean:
image.png

The comment from the authors is that : α is necessary, otherwise Lean takes issue with the code. If I understand right, this is because if we do not write this down, Lean does not know what instance of the typeclass to retrieve the one attribute from. Is this correct?
What happens when we type : α that solves this issue?

[Mario Carneiro]

The type of One₁.one is ∀ {α : Type} [One₁ α], α, meaning that it is supposed to produce an element of some type, and will figure out both α and the instance of One₁ α from context. Without knowing what type to produce, it will not be able to find the One₁ ?α instance since it doesn't know what to look for

[Mario Carneiro]

When you say the expected type is α, this gives the necessary context because this α unifies with the return type of One₁.one so it knows to set ?α := α and look for One₁ α (which it finds in the context). But you could also write e.g. Nat instead of α, and it would instead try to find a One₁ Nat instance

[VayusElytra]

Thank you, this is clear now!