Feature request: implicit lambda arguments syntax

[andreykl]

I faced a strange behavior when I was trying to get an implicit variable.

Steps to Reproduce

module ImplicitCatchImp

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

infixr 1 :->

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

record Parser (a : Type) (n : Nat) where
  constructor MkParser
  RunParser : List Char -> List a

guardM : (a -> Maybe b) -> All (Parser a :-> Parser b)
guardM f {a} {b} = ?guardM_rhs

This is how the hole looks like

 ImplicitCatchImp.guardM_rhs [P]
 `--                            b : Type
                                a : Type
                                f : a -> Maybe b
                                j : Nat
     --------------------------------------------------------
      ImplicitCatchImp.guardM_rhs : Parser a j -> Parser b j

So, everything is just as it should be (as I see). Now, I try to access j:

guardM : (a -> Maybe b) -> All (Parser a :-> Parser b)
guardM f {a} {b} {j} = ?guardM_rhs

And this is how the hole looks like now

- + ImplicitCatchImp.guardM_rhs [P]
 `--                            j : Type
                                b : Type
                                a : b -> Maybe j
                               j1 : Nat
                                f : Parser b j1
     --------------------------------------------
      ImplicitCatchImp.guardM_rhs : Parser j j1

So, it renamed j to j1 and I'm not able to get access to it. When I try to get j1 it answers that j1 is not an implicit argument of ImplicitCatchImp.guardM. That is true...

Expected Behavior

j of type Nat should be in scope

Observed Behavior

j has type Type and needed variable is ranamed to j1

There are many issues with implicit arguments but I think most close to this one are #2258 and #4206

[clayrat]

The syntax you need here is guardM f {a} {b} = \{j} => ... aka implicit lambda arguments, but this is currently not supported and, from what I understand, is likely to not be added before Idris 2.

[andreykl]

Thank you! I was confused with this a bit. Should I leave the issue as a feature request?