<div dir="ltr">Matteo,<br><div><div class="gmail_extra"><div class="gmail_quote"><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">PS. I still do not understand why by using a parameterised module the<br>



file is not accepted, as that is the way I most often assume<br>
&quot;postulates&quot; and I thought the outcome would be the same. However, I<br>
admit I do *not* understand the details of the problem.<br></blockquote><div><br></div><div>I think the reason why your version with the parametrized module is not accepted, is that Agda treats data types inside a parametrized module as parametrized data types. I.e. the definition of Foo in your version your version is equivalent with<br>


<br> <span style="font-family:courier new,monospace">data Foo (mySpace : Set) (myPoint : mySpace) : myPoint ≡ myPoint → Set where<br>  foo : Foo refl<br><br></span></div><div><span style="font-family:arial,helvetica,sans-serif">For parametrized data types, the current --without-K implementation performs parameter reconstruction (as implemented by Nils). I.e. for the purpose of checking --without-K, the constructor foo is considered to have type &quot;(mySpace : Set) (myPoint : mySpace) -&gt; Foo refl&quot;. Now we cannot eliminate the argument of type &quot;foo mySpace myPoint </span><span style="font-family:arial,helvetica,sans-serif">≡ foo mySpace myPoint&quot; because the variables mySpace and myPoint are not used linearly.<br>

<br></span></div><div><span style="font-family:arial,helvetica,sans-serif">In contrast, in my example there are no parameters (of the module or the data kind), so parameter reconstruction does not help. In fact, you can replace my postulates of mySpace and myPoint by any concrete values (for example a sphere) as long as they do not contain parameters or free variables, and the file still typechecks. This is clearly not what we want.<br>

<br></span></div><div><span style="font-family:courier new,monospace"><span style="font-family:arial,helvetica,sans-serif">Jesper</span><br></span></div></div></div></div></div>