## Stream: new members

### Topic: extending structures with implicit parameters

#### Arjun Pitchanathan (Feb 21 2020 at 19:55):

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 (Feb 21 2020 at 20:02):

so make \a in foo explicit

#### Arjun Pitchanathan (Feb 21 2020 at 20:02):

So is it impossible to have it implicit?

#### Kevin Buzzard (Feb 21 2020 at 20:03):

How is Lean supposed to guess the implicit argument?

#### Arjun Pitchanathan (Feb 21 2020 at 20:04):

So is there any way to specify it explicitly?

#### Kevin Buzzard (Feb 21 2020 at 20:04):

Maybe make the \a in foo explicit?

lol

#### Kevin Buzzard (Feb 21 2020 at 20:04):

I don't know of any other way

#### Arjun Pitchanathan (Feb 21 2020 at 20:04):

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 (Feb 21 2020 at 20:05):

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 (Feb 21 2020 at 20:07):

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 (Feb 21 2020 at 20:14):

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 (Feb 21 2020 at 21:18):

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

#### Mario Carneiro (Feb 21 2020 at 21:20):

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 (Feb 21 2020 at 22:10):

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 (Feb 21 2020 at 22:13):

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 (Feb 21 2020 at 22:15):

I notice you put a type ascription on b though

Ah, right

#### Arjun Pitchanathan (Feb 21 2020 at 22:16):

But it also seems to work without it

#### Mario Carneiro (Feb 21 2020 at 22:20):

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 (Feb 21 2020 at 23:16):

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 (Feb 22 2020 at 02:20):

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 (Feb 22 2020 at 02:20):

(which is not true for a lemma)

Last updated: May 13 2021 at 18:26 UTC