Writing a grammar for lambda calculus I'm trying to write a context-free grammar (to be feeded to lark) for parsing lambda calculus expressions. Basic version of it, as presented by most sources, looks like:

expr: variable | "(" expr ")" | application | abstraction
abstraction: "λ" variable "." expr
application: expr expr


I'd like the grammar to unambiguously parse expressions taking advantage of the notational conventions mentioned here on Wikipedia.
While I'm able to modify the grammar to follow most of them, I got stuck with implementing this one: "The body of an abstraction extends as far right as possible".

For example, there are two parse trees for λx.x λa.a - it can be both an application of two abstractions ( (λx.x)(λa.a) ) or an abstraction with an application in its body ( λx.(x(λa.a)) ).
If the abstraction was greedy as it should be, only the second one would be correct.

Is it possible to write a grammar that would force (i.e., make it the only choice) greedy interpretation of abstractions? If so, how to do it?
As @chi wrote, one good solution would be to enforce parenthesis around both applications and abstractions. 

Because I want to be as close to "handwritten" lambda calculus (so I'd like to eliminate parenthesis as much as possible), I tried another approach, which eventually worked. I blocked applications from having abstractions (not parenthesised abstractions, just abstractions) on their left side, so that λx.x M will never parse to
(λx.x)M. This will force the greedy parsing of abstractions - λx.(xM), exactly as I want.

The grammar doing that might look like this:

atom: "(" expression ")" | variable
expr: atom | abstraction | application
abstraction: "λ" variable "." expr
application: atom | application (atom | abstraction)