<div dir="ltr"><div>Because they are different types? If they were equal, whether a term is well-typed or not would depend on which order Agda solves constraints, something that is generally very undesirable. For example, consider the following program:</div><div><br></div><div>```<br></div>open import Agda.Builtin.Nat<br>open import Agda.Builtin.Equality<br><br>X : Set<br>explicit : X ≡ (Nat → Nat)<br>implicit : X ≡ ({Nat} → Nat)<br><br>X = _<br>explicit = refl<br>implicit = refl<br><br>test : (f : X) → Nat<br><div>test f = f 42   -- or f {42}?</div><div>```</div><div><br></div><div>Depending on the order in which Agda checks `explicit` and `implicit`, the type of `f` will be an explicit or implicit function type, so the user has to write either `f 42` or `f {42}`. In this case it is still relatively easy to tell the order in which Agda will check things, but in general Agda's typechecker relies a lot on postponing and such so the order is not predictable.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, May 21, 2020 at 5:26 PM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">





<div lang="EN-GB">
<div class="gmail-m_-8148551956358821683WordSection1">
<p class="MsoNormal"><span style="font-size:11pt">Why are implicit and explicit Pi-types not convertible?
<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">eq : ({_ : Set} → Set) ≡ (Set → Set)<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">eq = {!refl!}<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">{_ : Set} → Set != Set → Set because one is an implicit function<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">type and the other is an explicit function type<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">when checking that the expression refl has type<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11pt">({_ : Set} → Set) ≡ (Set → Set)<u></u><u></u></span></p>
</div>
<pre>This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.



</pre></div>

_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>