<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>