<div dir="ltr">The --type-in-type option completely drops all level arguments to Set, which means that combining it with universe polymorphism will lead to lots of unsolved levels. For instance (untested code),<div><br></div><div>id : {a : Level} {A : Set a} -&gt; A -&gt; A</div><div>id x = x</div><div><br></div><div>fail : Nat</div><div>fail = id 4  -- fails to solve the level argument to &#39;id&#39;</div><div><br></div><div>/ Ulf</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Dec 30, 2015 at 7:32 AM, Andrés Sicard-Ramírez <span dir="ltr">&lt;<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 29 December 2015 at 23:00, effectfully &lt;<a href="mailto:effectfully@gmail.com">effectfully@gmail.com</a>&gt; wrote:<br>
&gt;&gt; I created a branch allowing type in type and universe polymorphism.<br>
&gt;<br>
&gt; I tried it, but I&#39;m using Agda 2.5 and my code doesn&#39;t typecheck with<br>
&gt; Agda 2.4.2.6.<br>
<br>
</span>You can try the issue-1764-master branch:<br>
<span class=""><br>
  $ git clone <a href="https://github.com/agda/agda.git" rel="noreferrer" target="_blank">https://github.com/agda/agda.git</a><br>
  $ cd agda<br>
</span>  $ git checkout issue-1764-master<br>
  $ make install-bin<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
Andrés<br>
</font></span><div class="HOEnZb"><div class="h5">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">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>
</div></div></blockquote></div><br></div>