Zulip Chat Archive

Stream: new members

Topic: Can't infer type from instance

Vasily Nesterov (Nov 17 2022 at 08:53):

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 (Nov 17 2022 at 09:07):

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

Vasily Nesterov (Nov 17 2022 at 12:03):

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 (Nov 17 2022 at 12:25):

docs#out_param might have something

Vasily Nesterov (Nov 17 2022 at 14:55):

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 (Nov 17 2022 at 16:45):

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

Last updated: Dec 20 2023 at 11:08 UTC