When refining a goal, the given term sometimes loses parentheses when it is inserted in the buffer.
As a trivial example, consider the function
foo : (A : Set) -> (f : A -> A) -> A -> A.
I first define it as
foo A f x = ? and then type check. When I refine with
f (f x), Agda inserts
f f x into the buffer instead, which is, of course, not correct.
Fixed. -- Ulf