Can't infer type from instance

Stream: new members

[Vasily Nesterov]

Hello! I'm working on my project and faced with the following problem.

universes u v

class foo (α : Type u) (β : Type v)

instance bar : foo ℤ ℕ := foo.mk

def buz {β : Type v} (α : Type u) [foo α β] : Type v := β

def γ : Type v := (buz ℤ : Type v) -- error: don't know how to synthesize placeholder

(toy example for simplicity)

I want Lean to infer both ℤ as β and bar as an instance for foo α β from bar in the last line, but it can't. Is there any fundamental reason why this is impossible? Anyway, is it possible to work around the problem without using explicit arguments? (there are too many of them in my project)

[Eric Wieser]

Yes, make β an out_param (Type v) on line 3

[Vasily Nesterov]

Wow, it works, thank you! But it looks like magic, сan you please give a link to something where out_param and its usage are explained?

[Eric Wieser]

docs#out_param might have something

[Vasily Nesterov]

Yes, but it haven't :smile:
I have found only this, it's about Lean 4, but may still be useful for someone (like me)

[Eric Wieser]

I think the description there likely applies roughly to lean 3 too