Implicit lambda arguments

[clayrat]

(This is more of a feature request, but it's been a long-standing stumbling block for me in Idris 1, and I hope it's fairly uncontroversial)

Steps to Reproduce

module Temp

import Data.Vect 

All : (a : i -> Type) -> Type
All a {i} = {j : i} -> a j

Vect' : Type -> Nat -> Type
Vect' = flip Vect 

infixr 1 :->
(:->) : (a, b : i -> Type) -> (i -> Type)
(:->) a b i = a i -> b i

showAll : All (Vect' Integer :-> Vect' String)
showAll = map show

justShowAll : Maybe (All (Vect' Integer :-> Vect' String))
justShowAll = Just ?hole

Expected Behavior

justShowAll = Just $ \{j} => map show

Observed Behavior

There doesn't seem to be a way to introduce the implicit to finish filling the hole.

[edwinb]

Internally, these exist, but there's no syntax yet. There is a possible complication - implicits might appear in a different order than the lambdas, so perhaps there needs to be a way to indicate which implicit argument you mean (in much the same way as you write {n = foo} in a function call) and so it might need to be able to handle lambdas appearing in a different order than in the type.

On the other hand, a simple approach would be to say that if you have an implicit lambda, it needs to be "the next one".

Anyway, all of that is why I've never implemented it. But it would be nice to have.

[clayrat]

Yeah I think going for a simpler solution and assuming a fixed order might be good enough for a start. This is what happens when matching on auto implicits already anyway, right?