[Agda] Typeclasses again in release-candidate/master

[Andrea Vezzosi]

In Haskell you would hack this sort of thing with an equality
constraint, so that the instance matches any level, including metas,
but then the constraint solver sets the level to lzero:

instance (l ~ lzero) => Order l ℕ where { ... }







On Sat, Feb 20, 2016 at 9:05 AM, Ulf Norell <ulf.norell at gmail.com> wrote:
> Yes that might be something to consider.
>
> / Ulf
>
> On Sat, Feb 20, 2016 at 8:33 AM, effectfully <effectfully at gmail.com> wrote:
>>
>> Ulf Norell, would it make sense to give a special treatment for level
>> metas wrt instance search? Records are very often parameterized by
>> levels and it doesn't feel good to choose between universe
>> polymorphism and instance search.
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>