[Agda] How experimental is Cumulativity?

[Jesper Cockx]

Hi Joey,

The note that it is experimental mainly refers to the fact that there is no
proper solver yet for level (in)equalities, so there will be (possibly
quite frequent) cases where you have to fill in implicit level arguments
that Agda is able to infer without --cumulativity. That being said, it is
also a new feature in Agda and it hasn't been tested very extensively yet
so there may also still be bugs of the "make Agda unsound" kind. Running
Agda with the --double-check flag enabled might catch some of these bugs
when they occur.

-- Jesper

ps: If anyone is interested in implementing a proper solver for universe
levels, please get in touch! There may be some interesting research
questions lurking there.

On Fri, Jan 3, 2020 at 8:28 PM Joey Eremondi <joey.eremondi at gmail.com>
wrote:

> I see that Cumulativity is listed as an experimental feature in 2.6.1. Is
> this "the compiler might crash or reject valid programs" experimental? Or
> "Cumulativity might make Agda unsound" experimental? How much can I trust
> proofs that use cumulative Agda?
>
> Thanks!
> _______________________________________________
> 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/20200104/1ede8f93/attachment.html>