Parsing error with record update

[gancherj]

Hi all -- is the following undesired behavior?

module Test

type t = 
  { x : nat; y : nat}
  
// Parses correctly
let tst (f : t -> bool) (a : t) = 
  f ({a with x = 3})

// Parse error -- note the lack of parens around the argument to f
let tst2 (f : t -> bool) (a : t) = 
  f {a with x = 3}

[tahina-pro]

Thank you for asking. The F* parser currently requires all record literals uniformly (with or without with) passed as function arguments to be enclosed in parentheses, because of a parsing conflict with refinement types. I left a note at https://github.com/FStarLang/FStar/wiki/Parsing-and-operator-precedence#record-literals to illustrate the parsing conflict. We might want to relax this restriction for record literals with the with clause, which does not seem to exercise this parsing conflict. What do others think?