[Agda] I want implicit coercions in Agda

[Nicolas Pouillard]

If the goal is to have *implicit* coercions, then one should not see the
call to coerce.
Moreover, I think it would be too invasive to have coercions applied
everywhere.
Therefor I was thinking of a special mode/scope (here [| ... |]) where you
want coercions to be implicitly inserted.

For example:
   [| x + y |]
 would mean:
   coerce x + coerce y

Then this reminded me of idiom brackets when using the following definition
for _<*>_:
  f <*> x = coerce f (coerce x)

I have not pushed the idea further.

On Fri, Nov 23, 2018 at 11:21 AM Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 23/11/2018 10.34, Nicolas Pouillard wrote:
> > To me a concrete first step would build around a Coerce record and
> > instance arguments plus some syntactic help to use it. Would it make
> > sense to reuse idiom brackets?
>
> Why do you need new syntax for this?
>
> --
> /NAD
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181125/a73ed838/attachment.html>