[Agda] optional dot in dot patterns?

[Peter Divianszky]

On 19/11/2012 14:00, Nils Anders Danielsson wrote:
> 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?

Yes, it should, imho.

I guess shadowing is useful in the following cases:

a) we are short of names
b) to make program transformation easier (moving a definition)
c) we would like to hide a name

My opinion regarding these:

a) we are short of names
    Is this happened ever before in Agda?

b) to make program transformation easier (moving a definition)
    If we use short identifiers for general definitions or definitions
    with very limited scope and make definitions in the right place,
    this is not an issue.
    For example, 'f A = A' above was not defined in the right place
    (it is not related to the postulate 'A').

c) we would like to hide a name
    I'm not sure but maybe modules and 'private' should be used for that.