ensures/requires on traits and impls: better ergonomics

[W95Psp]

We can right ensures and requires on methods in impls and traits, but that requires putting a #[hax_lib::attributes] on the impl or trait block.

That is fine, but when the user forgets to put that #[hax_lib::attributes], we should output a nice error message with hints (the hint being: add hax_lib::attribtue).

[github-actions]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

Would still be useful

[github-actions]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.