We don't currently have a flag for erasure, and the reason is that parameters are always erased in the types of constructors and projections for non-indexed data types and record types. However, we could disallow users from writing @0 unless an infective flag --erasure is used. In that case erasure is still present in the type system if --erasure is not used, but in a (presumably) very limited way. What do you think, should we add such a flag?

I at least want to add a second flag, --single-constructor-matching. Agda currently allows matching in erased positions for non-indexed data types that have one constructor. Given that this feature is less well-explored than some other things I think we should hide it behind a flag. The flag should be infective, and I think it should be implied by --with-K (because we currently allow this kind of matching also for indexed types when --with-K is used).