[Agda] nameless pattern-matching functions

[Noam Zeilberger]

I often run into situations where I would like to create a nameless
function using pattern-matching, but am forced to give it a name.
For example, when defining the function baz below:

  data Either (a : Set) (b : Set) : Set where
    Inl : a -> Either a b
    Inr : b -> Either a b

  data Foo (a b c : Set) : Set where
    Bar : (Either a b -> c) -> Foo a b c

  baz : {a b c : Set} -> (a -> c) -> (b -> c) -> Foo a b c
  baz {a} {b} {c} f g = Bar fg
   where
    fg : Either a b -> c
    fg (Inl x) = f x
    fg (Inr y) = g y

I would like to just write something like:

  baz : {a b c : Set} -> (a -> c) -> (b -> c) -> Foo a b c
  baz f g = Bar (\ Inl x -> f x
                 | Inr y -> g y)

instead, I'm forced to name the argument to Bar -- and worse, give fg
a typing annotation, which then necessitates carrying around the types
a, b, c.

Would it be tricky to extend Agda to allow pattern-matching in
nameless functions?

Noam