[Agda] Is it possible to switch off universes checking?

[Ulf Norell]

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

id : {a : Level} {A : Set a} -> A -> A
id x = x

fail : Nat
fail = id 4  -- fails to solve the level argument to 'id'

/ Ulf


On Wed, Dec 30, 2015 at 7:32 AM, Andrés Sicard-Ramírez <asr at eafit.edu.co>
wrote:

> On 29 December 2015 at 23:00, effectfully <effectfully at gmail.com> wrote:
> >> I created a branch allowing type in type and universe polymorphism.
> >
> > I tried it, but I'm using Agda 2.5 and my code doesn't typecheck with
> > Agda 2.4.2.6.
>
> You can try the issue-1764-master branch:
>
>   $ git clone https://github.com/agda/agda.git
>   $ cd agda
>   $ git checkout issue-1764-master
>   $ make install-bin
>
> --
> Andrés
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151230/8f5dd95b/attachment.html