Fix #5816: skip generating cubical clauses for Prop stuff

[andreasabel]

Fix #5816: skip generating cubical clauses for Prop stuff

TODO:

• [ ] disallow --cubical and --prop together?

[Saizan]

The models of CTT support a Prop universe. What one should do for indexed families and/or HITs in Prop would require more thought though. It does not seem like you should be able to support the same eliminators in general.

[andreasabel]

Thanks for chiming in, @Saizan.
Current master contributes indexed inductive types to Cubical Agda, but the development isn't finished yet. We need a plan what to do about it for the 2.6.3 release. This PR is a clumsy attempt to work around an internal error introduced by the new code for indexed inductive cubicality. Any help to do better appreciated.

[nad]

Thanks for chiming in, @Saizan. Current master contributes indexed inductive types to Cubical Agda, but the development isn't finished yet. We need a plan what to do about it for the 2.6.3 release.

One option is perhaps to disallow the combination of --prop and --cubical/--erased-cubical when --safe is active. However, if the combination of --prop and --cubical can lead to lots of broken invariants, then perhaps it should be ruled out entirely.

[andreasabel]

@mergifyio rebase

[mergify[bot]]

rebase

✅ Branch has been successfully rebased

[plt-amy]

The fix looks good; In the future we'd have to revisit generation of hcomp clauses into types living in Prop if we were to e.g. make Prop univalent. For the 2.6.3 release, I think the cleanest option is to lock support for cubical indexed inductives behind a flag: it has a tendency to explode (#5816, #6005, #6001) and Injectivity is a very popular unification step.

[nad]

For the 2.6.3 release, I think the cleanest option is to lock support for cubical indexed inductives behind a flag

Should that flag be compatible with --safe?

[plt-amy]

It doesn't let you prove anything new, so it's not not --safe... but it's not entirely safe since there's a lot of __IMPOSSIBLE__ to run into? So I'd say "no"

[nad]

If the only problem is that Agda might crash, then I think it is fine to make the flag compatible with --safe. The idea of that flag is that when it is used, then any logical or runtime errors are Agda bugs.

[jespercockx]

In the past we have often made experimental flags not compatible with --safe, even though in principle they do not add any inconsistencies (see for example --prop). If this is still the policy, I would suggest making this new flag incompatible with --safe until it is fully implemented (in particular with support for Injectivity and Prop).

[plt-amy]

Actually, do we still need this after #6153? I don't think so

[andreasabel]

Since the problems reported in #5816 are fixed (and a testcase has been added), I don't see a reason to keep this PR.