viperproject
Supertrait limitations of auto traits
As part of #1249, I repeatedly found myself writing code like this:
https://github.com/viperproject/prusti-dev/blob/d7ce8c77fe527a0efcaa6cbfb384f06f22775934/prusti-contracts/prusti-contracts/src/core_spec/default.rs#L3-L7
Note the Copy + PureDefault, rather than simply PureDefault. This is because PureDefault is an auto trait expressing that a type's Default implementation is pure. Unfortunately, auto traits cannot have supertraits, so unless we want users to explicitly opt non-Copy types out of this refinement, we need to further constraint PureDefault to be Copy at the use site.
One possible solution would be to implement our own auto-style system, which could even allow defining PureDefault: Copy + Default as a regular trait that Prusti considers implemented on all applicable types unless otherwise stated.
An alternative solution is to tackle this specific purity issue by providing an alternative to pure, or making it take an argument, that makes it only apply when the necessary types implement Copy. This could look something like pure_if_applicable or pure(ignore_invalid_generics), respectively. This would not eliminate the need for marker traits like PureDefault entirely, as it's still possible for a type to be Copy but provide an impure implementation of default(), but it would streamline specs like this not just for us but also for users.
