<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; color: rgb(0, 0, 0); font-size: 14px; font-family: Calibri, sans-serif; "><div>This looks like a bug – please add it to the bug tracker.</div><div><br></div><div>We really need to understand what we are doing when checking wether pattern satisfy the —without-K condition. It seems that Conor's work on translating pattern matching to eliminators (with J and K) would be a good starting point. </div><div><br></div><div>At the same time we know that many types support UIP by structure. Michael Hedberg showed that all types with a decidable equality support UIP and it is not hard to see that this can be extended to stable equality (non-not closed). (Little puzzle: without extensionality – are there any types which have stable but not decidable equality ?)</div><div><br></div><div>We also want to quantify over all HSets (I.e. types with UIP) and so on.</div><div><br></div><div>Thorsten</div><div><br></div><span id="OLK_SRC_BODY_SECTION"><div style="font-family:Calibri; font-size:11pt; text-align:left; color:black; BORDER-BOTTOM: medium none; BORDER-LEFT: medium none; PADDING-BOTTOM: 0in; PADDING-LEFT: 0in; PADDING-RIGHT: 0in; BORDER-TOP: #b5c4df 1pt solid; BORDER-RIGHT: medium none; PADDING-TOP: 3pt"><span style="font-weight:bold">From: </span> Jason Reed <<a href="mailto:jcreed@gmail.com">jcreed@gmail.com</a>><br><span style="font-weight:bold">Date: </span> Tue, 9 Jul 2013 16:31:22 +0100<br><span style="font-weight:bold">To: </span> "<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br><span style="font-weight:bold">Subject: </span> [Agda] another possible without-K problem<br></div><div><br></div><blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;"><div dir="ltr"><span style="font-family: arial, sans-serif; font-size: 13px; ">I'm experiencing something that I think is a violation of the intent of the --without-K flag, similar to what Thorsten was talking about in </span><a href="https://lists.chalmers.se/pipermail/agda/2012/004104.html" target="_blank" style="font-family:arial,sans-serif;font-size:13px">https://lists.chalmers.se/pipermail/agda/2012/004104.html</a><span style="font-family: arial, sans-serif; font-size: 13px; ">.</span><div style="font-family:arial,sans-serif;font-size:13px"><br></div><div style="font-family:arial,sans-serif;font-size:13px">The following file checks fine for me under current darcs Agda:</div><div style="font-family:arial,sans-serif;font-size:13px"><br></div><div style="font-family:arial,sans-serif;font-size:13px">
<<<begin>>></div><div style="font-family:arial,sans-serif;font-size:13px"><div class="im"><div><font face="courier new,monospace">{-# OPTIONS --without-K #-}</font></div><div><font face="courier new,monospace"><br></font></div><div><font face="courier new,monospace">module Test where</font></div><div><font face="courier new,monospace"><br></font></div><div><font face="courier new,monospace">data S1 : Set where</font></div><div><font face="courier new,monospace"> base : S1</font></div><div><font face="courier new,monospace"><br></font></div><div><font face="courier new,monospace">module test where</font></div><div><font face="courier new,monospace"> data _¡Ý_ {A : Set} (a : A) : A ¡÷ Set where</font></div><div><font face="courier new,monospace"> refl : a ¡Ý a</font></div><div><font face="courier new,monospace"><br></font></div><div><font face="courier new,monospace"> bad : (p q : base ¡Ý base) -> p ¡Ý q</font></div><div><font face="courier new,monospace"> bad refl refl = refl</font></div><div><font face="courier new,monospace"><br></font></div><div><font face="courier new,monospace">module test2 where</font></div><div><font face="courier new,monospace"> data _¡Ý_ {A : Set} : A ¡÷ A ¡÷ Set where</font></div><div><font face="courier new,monospace"> refl : {x : A} ¡÷ x ¡Ý x</font></div><div><font face="courier new,monospace"><br></font></div><div><font face="courier new,monospace"> bad : (p q : base ¡Ý base) -> p ¡Ý q</font></div><div><font face="courier new,monospace"> bad refl refl = refl</font></div></div><div><span style="font-size:small"><<<end>>></span><br></div><div><span style="font-size:small"><br></span></div><div><span style="font-size:small">Note that this covers both the possible definitions of the identity type mentioned by Guillaume in </span><a href="https://lists.chalmers.se/pipermail/agda/2012/004105.html" target="_blank">https://lists.chalmers.se/pipermail/agda/2012/004105.html</a></div><div><br></div><div>Any ideas what should be done here? Does the K-check need to be further strengthened when there aren't parameters around? Am I misunderstanding something trivial?</div></div></div></blockquote></span>
<br><p>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 send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.</p><p>This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.</p>
<br></body></html>