<div dir="ltr">If the goal is to have *implicit* coercions, then one should not see the call to coerce.<div>Moreover, I think it would be too invasive to have coercions applied everywhere.</div><div>Therefor I was thinking of a special mode/scope (here [| ... |]) where you want coercions to be implicitly inserted.</div><div><br></div><div>For example:</div><div>   [| x + y |]</div><div> would mean:</div><div>   coerce x + coerce y</div><div><br></div><div>Then this reminded me of idiom brackets when using the following definition for _<*>_:</div><div>  f <*> x = coerce f (coerce x)</div><div><br></div><div>I have not pushed the idea further.</div></div><br><div class="gmail_quote"><div dir="ltr">On Fri, Nov 23, 2018 at 11:21 AM Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 23/11/2018 10.34, Nicolas Pouillard wrote:<br>
> To me a concrete first step would build around a Coerce record and<br>
> instance arguments plus some syntactic help to use it. Would it make<br>
> sense to reuse idiom brackets?<br>
<br>
Why do you need new syntax for this?<br>
<br>
-- <br>
/NAD<br>
</blockquote></div>