How to specify implicit arguments for infix operators?

Question

Suppose I have an operator

infixl 9 @@

(@@) : Tensor [S n] t -> Tensor (S n :: tail) t -> Tensor tail t

(where Tensor takes a Vect and a type, but that's not important here). If I want to specify tail, I know that I can add to a @@ b by turning @@ into a function (@@) like

(@@) {tail=[]} a b

but that somewhat defeats the point of it being infix. What's idiomatic?

Answer 1

You could try using a postfix projection operator:

(.f) : Tensor [S n] t -> Tensor (S n :: tail) t -> Tensor tail t

a.f {tail=[]} b