Parser: accept `f {field = ...}` (no need for `f ({field = ...})` anymore)

[W95Psp]

Hi,

This PR changes a bit the parser rules related to function application so that the expression f {foo = 123} is now allowed. Previously, f {foo = 123} was rejected, and we were forced to wrap the record into parenthesis, writing f ({foo = 123}).

[tahina-pro]

Thank you for your proposal. However, it might introduce a parser conflict, as I described in https://github.com/FStarLang/FStar/wiki/Parsing-and-operator-precedence#record-literals :

module V
type u = {x : unit}
let ffalse (_: u) = nat
let f (b: bool) : (if b then Type0 else (u → Type0)) = if b then unit else ffalse
type dummy =
  | Dummy1 : x: f true { x = () } → dummy
  | Dummy2 : x: f false ({ x = () }) → dummy

[W95Psp]

Hi @tahina-pro, thank you for your answer, I didn't see that note on that wiki page earlier actually, nor issue #2417! Thanks for pointing me to it!

Though, I think the changes I made with this PR are safe and yield no such conflict: I intentionally make a distinction between parsing record expressions that are within a refinement context and those outside of such a context. To do so, I split the rule appTerm into two different rules appTermNoRecordExp and appTerm. In presence of refinement, I only allow appTermNoRecordExp, so that we avoid any conflict.

I think that would be really nice to be able to drop those parentheses! Do you think that might break other things? (theoretically it shouldn't -- menhir is not complaining at least)

EDIT: forgot to say I empirically tested just now the snipped of that wiki page with the PR: it is parsed correctly.

[nikswamy]

Thanks Lucas! This improves the record syntax significantly ... the need for the additional parenthesis has been a long-standing wart.

That said, for the record, the wart isn't completely gone, as Tahina's example points out. Due to the inherent ambiguity in the syntax between refinements and records, in some cases, like Dummy2 : x: f false ({ x = () }) → dummy, you do still need the parens.

Thanks again!