Resolving a reduce/reduce conflict in a parser for lambda calculus

I've been trying for the past couple of days write a menhir (yacc) grammar for this seemingly simple language with some syntax sugar, but can't figure out to do so without ambiguities.

The relevant constructs from the language are:

• Application is juxtaposition: x y z is a valid expression.
• Allow type annotations: given some expression e and type t, you can write e : t. the : should be a non-associative operator.
• You can (and sometimes need to) wrap certain expressions in parentheses
• Arrow types: expressions of the form (x y z : a) -> b, which is sugar for (x : a) -> (y : a) -> (z : a) -> b (-> is right-associative). here x y z are identifiers, a and b are other expressions
• Arrows can also be written as just a -> b, which is sugar for (_ : a) -> b.

My initial strategy was to split the expressions to two types based on the intuitive question "does it need to be wrapped in parentheses when used in application?", if the answer is yes I call it an "atom", otherwise it's an expression.
For example variables are atoms, because I can write x y. Parenthesized expressions are also atoms because they can be juxtaposed. Lambda abstraction is not an atom because it's too ambiguous (even for a human reader) to parse λx . y z - you have to write (λx . y) z. The (minimal error reproducing) grammar can be outlined as follows

%token EOF
%token <string> IDENT
%token LPAREN RPAREN COLON ARROW BOOL

%nonassoc COLON
%right ARROW

%start program
%type <expr> program
%type <expr> expr
%type <expr> atom

%%
program:
  | e=expr; EOF { e }

expr:
  | es=nonempty_list(atom) { unfoldApp es }           // application
  | e=expr; COLON; t=expr { Annot (e, t) }            // annotation
  | LPAREN; xs=nonempty_list(IDENT); COLON;
    a=expr; RPAREN; ARROW; b=expr { unfoldPi xs a b } // arrow types
  | a=expr; ARROW; b=expr { Pi ("_", a, b) }          // sugar (not necessary to reproduce)
  // more cases for lambda, let abstractions, etc...

atom:
  | x=IDENT { Var x }                                 // variable
  | LPAREN; e=expr; RPAREN { e }                      // parentheses
  | BOOL { Bool }
  // more constants and atoms

There's clearly an undeniable ambiguity here. After the parser sees ( x with lookahead : it might be a variable x, annotated and parenthesized. Or, it could be the start of an arrow with just one variable. Even with more variables, it could be an annotated application, so the ambiguity remains. I want to prioritize the latter, meaning if it can be an arrow type, choose that.
I could probably check in the AST later if it's something like Annot (App (App (Var "x", Var "y"), Var "z"), a) and then convert manually to the correct result, but that feels sketchy and unreliable.

Is there some clean and easy way to do it with a LALR generator such as menhir?