extending structures with implicit parameters

Stream: new members

[Arjun Pitchanathan]

How does one extend a structure that has implicit parameters? Consider

structure foo {α : Type} := (a : α)
structure bar {α : Type} extends foo :=
(b : α)

Lean apparently will not infer the parameter:

don't know how to synthesize placeholder
context:
α : Type
⊢ Type

And neither are we able to specify it explicitly:

structure foo {α : Type} := (a : α)
structure bar {α : Type} extends @foo α :=
(b : α)

gives the error:

invalid 'structure', expression must be a 'parent' structure

I found this but there doesn't seem to be a resolution there

[Kenny Lau]

so make \a in foo explicit

[Arjun Pitchanathan]

So is it impossible to have it implicit?

[Kevin Buzzard]

How is Lean supposed to guess the implicit argument?

[Arjun Pitchanathan]

So is there any way to specify it explicitly?

[Kevin Buzzard]

Maybe make the \a in foo explicit?

[Kenny Lau]

lol

[Kevin Buzzard]

I don't know of any other way

[Arjun Pitchanathan]

As in, can I have it implicit in both foo and bar and specify it explicitly in the extends part, like I'm trying to do with the @foo

[Kevin Buzzard]

Right, I don't know how to make that work. You can see in the conversation you linked to that Chris fixed it by making the argument explicit. How can Lean guess the implicit argument? It might be foo nat or something, that would be a valid solution right?

[Arjun Pitchanathan]

True, I was hoping there would be a way to at least specify it ourselves -- seems there isn't. Thanks for your help.

[Kevin Buzzard]

Aah I see, yeah that makes sense. I don't know how to do it, perhaps some more CS person than me can suggest a fix. Nice question!

[Mario Carneiro]

I think it would make sense for the @foo α to work. That should be filed as a bug

[Mario Carneiro]

But as Kenny and Kevin say, I can't see any reason for foo as defined to make sense. Lean can never infer that argument so it should not be implicit

[Arjun Pitchanathan]

Okay, I just figured out that \a is always implicit infoo.mk, which was what I was really trying to do. I now realize that Kevin was probably asking how lean could infer \a in a general context when one uses foo rather than in my snippet, after extends. It makes sense to me now, thanks!

[Arjun Pitchanathan]

Also, here is one possible example where lean can infer the argument

inductive option {α : Type} : Type
| none {} : option
| some (a : α) : option
def has_val {α : Type} (a : α) : option → Prop
| option.none := false
| (option.some (b : α)) := a = b

[Mario Carneiro]

I notice you put a type ascription on b though

[Arjun Pitchanathan]

Ah, right

[Arjun Pitchanathan]

But it also seems to work without it

[Mario Carneiro]

I guess this is an instance of the fact that lean can infer the argument to foo in F in the following pattern:

variable (foo : ∀ {α : Type}, Type)
variable (bar : Type → Type)
variable (f : ∀ {α}, @foo α → bar α)

#check λ (F : foo) (b : bar ℕ), f F = b

In your case, f is foo.rec

[Arjun Pitchanathan]

Yes, I guess it should work for basically any expression that forces the types to be equal

variable (foo : ∀ {α : Type}, Type)
variable (bar : Type → Type)
variable (r : ∀ {α β}, @foo α → bar α → β)
#check λ (F : foo) (b : bar ℕ), r F b

Thanks a lot!

[Reid Barton]

This has_val example also only works because it is a def and the body of a def is taken into account when checking the type.

[Reid Barton]

(which is not true for a lemma)

[Nicolò Cavalleri]

Is there still no solution to this? I need to extend a structure by putting implicit parameters in spots that are filled by type class inference

[Kevin Buzzard]

If the type of a parameter is a class then surely it should be in square brackets at all times?

This is a weird thread, it's people complaining that they can't do things which I can't ever imagine one would need to do. Is this a big #xy issue?

[Kevin Buzzard]

Can you post an #mwe?