<div dir="ltr"><div dir="ltr"><div>Hi Agda people,</div><div><br></div><div>In the <a href=" https://github.com/agda/agda/issues/3334#issuecomment-433730080">comments on issue #3334</a>, Wolfram wrote:</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">

I consider it counterproductive to be able to declare irreleveance,
and even more counterproductive to have to do it for efficiency reasons,
because that encourages premature optimisations.
The compiler (including the type checker) should detect it whenever possible,
and optimise it away as soon as possible.

</blockquote><div><br></div><div>To which I replied:</div><div><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></div><div>
Often the fact that a certain term is irrelevant is obvious to <em>you</em>
 as the Agda programmer but there's no way for Agda to figure this out 
from the code. If it's possible that you will use the term at any point 
in the future, Agda cannot (and should not) erase it. So any automatic 
detection of irrelevance would probably be very disappointing. (The 
alternative where Agda would eagerly erase things without asking and 
then complaining later when you try to use them is arguably worse). 
Another advantage of annotating irrelevant things, is that Agda can warn
 you when you use it accidentally in a non-erased position, instead of 
removing the irrelevance silently and causing hard-to-explain 
performance regressions.

</div></blockquote><div><br></div><div>But I realized this is based mostly on speculation and not hard facts. Historically, Agda has focused on the annotated style of proof-irrelevance (Andreas' irrelevant functions and irrelevant fields, and more recently my implementation of Prop). 
Maybe inferred proof irrelevance would work better than expected?<br></div><div><br></div><div>So now my question to <i>you</i>, the Agda community is this: do you prefer Agda's current style of annotated proof-irrelevance, or would you rather have Agda infer things for you (and perhaps fail to do so in some cases)? <br></div><div><br></div><div>I won't promise I will remove Prop and focus all my attention on inferring irrelevance even if everyone votes for the latter option, but it would be interesting to know going forward what you think.</div><div><br></div><div>-- Jesper<br></div><div> </div></div></div>