Why are implicit arguments inserted eagerly?

Stream: lean4

[Michael Jam]

I was reading this https://leanprover.github.io/theorem_proving_in_lean4/interacting_with_lean.html?highlight=semi%20implicit#more-on-implicit-arguments
Until now, I naturally assumed that implicit arguments behaved like semi-implicit arguments, but now my view of the world is collapsing.
Looking at the example it sounds like semi-implicit arguments are more desirable, and I feel like I should use them everywhere.
Why are implicit arguments inserted eagerly by default?
What is an example where regular implicit arguments are more desirable than semi-implicit ones?

[Henrik Böving]

This feature is called autoImplicit and you can shut it off if you want.

The reason we have it is quite simply convenience. If you say write a function that has 4 type parameters do you want to figure out all of the universe stuff etc. Yourself? I doubt it. The autoImplicit feature allows us to have generic type notation like Haskell with the most general universes possible for free.

[Michael Jam]

@Henrik Böving I don't think you're answering my question, I wasn't talking about auto implicits. I'm talking about semi-implicits vs implicit (double curly brackets vs single curly brackets)

[Michael Jam]

Now that I discovered that the difference exists, I feel like i'd prefer using double curly brackets everywhere which is weird. That's why I'm wondering if there are examples where it's clearly better to use single curly brackets over double curly brackets

[Eric Wieser]

What about a function that takes no explicit arguments? How are you supposed to tell lean to fill out the semi-implicits?

[Sebastian Ullrich]

With only strict-implicit parameters (I haven't seen them called semi-implicit before), we e.g. wouldn't have id : Nat -> Nat, i.e. implicit parameters are closer to usual polymorphism in e.g. Haskell

[Michael Jam]

My personal habit so far has been to make sure that the functions I write, always have some (at least one) explicit parameters, so that all the function's implicit parameters can be inferred from explicit inputs only, and not from the expected type at the use site.
I remember getting lots of type inference problems when I didn't follow that principle.
It also makes my life easier when thinking about how to write a proof because I can just write have := f x y z ... without having to think of a return type or immediately plug it in something else.
Do you think it's a bad principle to follow? Are functions with only implicit parameters really that useful?

[Floris van Doorn]

In Lean 3 mathlib we prefer eagerly inserted arguments. There are lots of lemmas without explicit arguments, where it would be inconvenient to use strict-implicit arguments.
Most definitions indeed have at least one explicit argument (there are a couple of exceptions, like list.nil and set.univ). But even with functions with explicit arguments it can still be nice to have eagerly inserted arguments if the function itself is the argument of another function, like in congr_arg2 prod.mk h1 h2 or list.map option.some.

[Kyle Miller]

Eric Wieser said:

What about a function that takes no explicit arguments? How are you supposed to tell lean to fill out the semi-implicits?

This is definitely a limitation of strict implicits. If there were a way to force strict implicits (maybe a special kind of pseudo-argument token?) it would make them more useful.

[Michael Jam]

OK I understand Floris' point. Some functions unavoidably end up having only implicit parameters because they are sometimes passed without being fully applied.
In general, what's a good rule of thumb to decide if one should make a parameter strict-implicit?