I would argue no, they are only necessary for reducing the suffering caused by other issues. In particular, one of the largest reasons we need implicits are various issues caused by bundling problems.
To see what I mean by this, let's consider an example. We might define a monoid like so:
record Monoid : Set where
field
Carrier : Set
unit : Carrier -> Carrier -> Carrier
mul : Carrier
...
However, we will run into trouble if we try to use only this definition. Namely, we don't have a way of talking about a monoid on a specific carrier set! To do this, we need to introduce yet another definition:
record MonoidOn (Carrier : Set) : Set where
field
unit : Carrier -> Carrier -> Carrier
mul : Carrier
...
Now, once we start working with these, we need to start using implicits, lest we drown in a pile of arguments that are totally redundant. However, if we had some way of definitionally constraining the Carrier field from our original Monoid definition, then we wouldn't be in a position where we even needed implicits!
Another thing that makes use reach for implicits are families of types. As an example, consider the definition of a category:
record Category : Set where
field
Obj : Set
Hom : Obj -> Obj -> Set
id : (X : Obj) -> Hom X X
seq : (X Y Z : Obj) -> Hom X Y -> Hom Y Z -> Hom X Y
...
Here we run into similar issues: if we don't have implicits, then the laws are going to be brutal to state. Associativity will require 4 (!!!) redundant arguments, which is a show-stopper. However, if we look closely, we can see that this too is a bundling issue. If we work with the total space of Hom, and had our imaginary way of constraining things definitionally, then we wouldn't have our parameter explosion, and thus would not need implicits. With these ingredients, we might write Category like so:
record Category where
field
Obj : Set
Hom : (s : Obj) -> (t : Obj) -> Set
id : (x : Obj) -> Hom [ s = x, t = x ]
seq : (f : Hom) -> (g : Hom [ s = f.t ]) -> Hom [ s = f.s, t = g.t ]
assoc (f : Hom) -> (g : Hom [ s = f.t ]) (h : Hom [ s = g.t ]) ->
Id (Hom [ s = f.s, t = h.t]) (seq (seq f g) h) (seq f (seq g h))
...
Luckily, our magic imaginary way of constraining things does exist under the guise of singleton types, or, more generally, extension types. Currently, cooltt supports all of these tricks, and allows us to write things concisely without using any implicits at all. This is also very easy to implement: we already had extension types, and the elaborator tricks required slide in at under 100 lines.
To summarize, implicits let us hide the fact that some parameter explosion occurred because we unbundled a bunch of stuff. Instead, let's try to prevent the explosion from happening in the first place by bundling as often as we can.
