[Agda] optional dot in dot patterns?

[Nils Anders Danielsson]

On 2012-11-19 13:26, Peter Divianszky wrote:
> I don't see that shadowing is a problem.
> If we have a pattern (f x) such that f is a function in scope, then
> the compiler could replace (f x) by .(f x), couldn't it?
> And I ask the same for more than one or zero arguments.

Currently accepted code:

   postulate
     A : Set

   f : Set → Set
   f A = A

Should A be dotted here?

-- 
/NAD