[Agda] I want implicit coercions in Agda

[Stefan Monnier]

> I completely disagree.  Ambiguous notation is one of the gravest sins that
> continue to be inflicted upon students of mathematics.

This question is not binary: Agda already has forms of
coercions/overloading (e.g. implicit arguments are a form of coercion
and type classes are a form of overloading, which happens to also handle
the kind of examples shown by Sergei who uses the term coercions).

So the question should maybe better be phrased as:
which kinds of coercions/overloading are more beneficial than harmful?

        Stefan