Eta expand implicit arguments

Stream: general

[Jannis Limperg]

Suppose I have an expression e with type ∀ (x : T) {y : U}, V. From this, I'm generating something of the form λ (x' : T'), e (f x'), which I'd like to have type ∀ (x' : T') {y : U}, V. However, when elaborating this generated expression, Lean eagerly creates a metavariable for {y : U}, so the actual type is ∀ (x' : T'), V[y/?m].

To avoid this, I thought I'd eta-expand the implicit argument, generating λ (x' : T') {y : U}, @e (f x') y. However, I can't find the incantation that gives me @e for an arbitrary e. (In the application, e is a local constant, if that helps.) Any pointers?

(Unrelated question but I'm hijacking my own thread: Can I match on a level in an expression pattern? `(eq.{%%u} ...) doesn't seem to be a valid pattern.)

[Mario Carneiro]

You can write @e if e is a local constant though

[Reid Barton]

You could also consider changing the type of e to ∀ (x : T) {{y : U}}, V

[Jannis Limperg]

Mario Carneiro said:

You can write @e if e is a local constant though

In surface Lean, yes, but how do I represent this as an expr? I tried variations of `(@%%e ...), but that doesn't seem to work. In general, what is the expr corresponding to @h if h is a local const?

Reid Barton said:

You could also consider changing the type of e to ∀ (x : T) {{y : U}}, V

Yeah, I thought about that as well. This would be a slightly confusing change for users, but if nothing else works, I'll take it.

[Mario Carneiro]

as an expr, you don't have to do anything because you can just call expr.app and so on, elaboration doesn't happen unless you tell it to

[Mario Carneiro]

You don't have to use `(%%e ...) to construct exprs, in fact I wouldn't recommend it because it's not very general

[Mario Carneiro]

but I would need to see more precisely what you are trying to do to give more targeted advice

[Jannis Limperg]

Mario Carneiro said:

as an expr, you don't have to do anything because you can just call expr.app and so on, elaboration doesn't happen unless you tell it to

Okay, that makes sense. I thought I'd tried that, but I'll have to go back and check what exactly went wrong. Anyway, thanks!

[Gabriel Ebner]

Pro-tip: expr has a function coercion, so you can write e (f (var 0)).

[Jannis Limperg]

That is equal parts beautiful and horrifying.

[Jannis Limperg]

Okay, here's why my code doesn't work: I'm constructing a pexpr as above, not an expr. So, the real question: Is there a way to apply a local const to an implicit argument in a pexpr?

[Rob Lewis]

Not sure I'm interpreting your question right, are you looking for docs#pexpr.mk_explicit ?

[Jannis Limperg]

Don't know -- is mk_explicit e the equivalent of surface @e?

[Jannis Limperg]

Yes it is! Awesome, thanks.