[Agda] Overloading atoms and operators

[Andreas Abel]

I see why there is a need to overload operators of ,different arity by 
the same name, for instance, unary and binary minus.

postulate
   ℤ : Set
   -_ : ℤ → ℤ
   _-_ : (x y : ℤ) → ℤ

infix 10 -_
infixl 5 _-_

test : ℤ → ℤ
test x = - x - x

But what is the point of overloading and atom with an operator of the 
same name?  This is, as far as I know, not mathematical practice, and 
would only serve obfuscation.

postulate
   A B : Set
   x a : A
   _x_ : A → A → B

infix 10 _x_

There seems no way of making Agda parse

   a x a

thus, the operator is unusable.

In the light of issue 1616, it seems sensible to rule out such overloading.

An atom should be in name conflict with any operator containing this 
atom as a name part.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/