Given that we have some long-standing consistency bugs related to sized types it makes sense to disallow sized types when --safe is active. However, I have quite a bit of code that uses sized types, and I'd like Agda to check that I'm not using other unsafe features. Thus it might make sense to add a flag like --safe-except-for-sized-types.
An alternative would be to add a more general flag with support for other unsafe features: --safe-except-for=…. Does anyone see a use for the more general variant?
A different approach would be to list the features that are allowed: --language=…. Then one could enumerate features like "user-defined data types", "pattern matching", and so on. However, implementing this option might be non-trivial.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4