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.