Funcs with implicit parameters hard to read

Stream: lean4

[Max Nowak 🐉]

I have the following minimized problem. For some reason, taker nop renders as taker fun {A} => nop in the infoview, which is very distracting and hard to read. In some places I can fix this by writing taker @nop instead.
It's eta equivalent, but annoying.

inductive Ty : Type | ty
inductive Tm : Ty -> Type | tm : Tm .ty

def Subb : Type _ := {A : Ty} -> (var_idx : Nat) -> Tm A
def nop : Subb := fun {A} idx => .tm
def taker : Subb -> String := sorry
#check taker nop -- taker fun {A} => nop : String

set_option pp.all true
def ohno := taker nop
def ohyes := taker @nop
#print ohno -- taker fun {A : Ty} => @nop A
#print ohyes -- taker @nop

I assume that would be very hard to fix and would require the elaborator or delaborator to be changed.
Is there a better way of handling these? Does someone have a delaborator for this written already? Maybe there is a tactic which will eta-simplify?

[Eric Wieser]

The fact that these two print in different ways suggests that what you want is an elaborator change, not a delaborator change.

[Max Nowak 🐉]

Yeah... I take it there is no easy solution, other than just not using implicit arguments like this?

[Kyle Miller]

I find this to be surprising behavior. Why is the elaborator unfolding Subb? The type of nop is Subb, so where is it getting the idea that it needs to see that there is an implicit argument hidden behind the definition of Subb?

[Max Nowak 🐉]

Oh yeah I didn't even notice that, that's even weirder.

[Mario Carneiro]

I think implicit lambdas always do this?

[Mario Carneiro]

they are eagerly inserted and then canceled using implicit arguments (producing an eta redex) if needed

[Kyle Miller]

That would make sense to me if there were any implicit lambdas that the elaborator could immediately see in the types of taker or nop, but does it see that nop is an implicit lambda? Or that Subb is a type with an implicit forall?

[Mario Carneiro]

Max Nowak 🐉 said:

Yeah... I take it there is no easy solution, other than just not using implicit arguments like this?

well, implicit foralls in definitions are generally avoided for exactly this reason. Normally when you want this in a definition like src#Set.Subset you use semi-implicits instead (this is their main motivation)

[Kyle Miller]

Oh, the implicit lambda feature does whnf on the expected type, right? Actually, never mind, this doesn't explain the behavior of nop for me, since it's not a lambda unless you unfold it.

[Mario Carneiro]

implicit lambda triggers basically whenever you call elabTerm, it doesn't require there to be a lambda expected or a forall goal

[Mario Carneiro]

it's an optional parameter to the function: docs#Lean.Elab.Term.elabTerm

[Max Nowak 🐉]

I think the semi implicit binders are exactly what I was looking for