Embellish release notes of PR 4928 (#5016)

Embellish release notes of PR #4928. The release note now try to make it
clear that any new errors (for this issue) on previous programs are
intentional.


<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

docs/dev/news/4928.fix

@@ -1 +1,3 @@
-Check for correct usage of type characteristics in specifications and other places where they were missing
+Check for correct usage of type characteristics in specifications and other places where they were missing.
+
+This fix will cause build breaks for programs with missing type characteristics (like `(!new)` and `(0)`). Any such error message is accompanied with a hint about what type characterics need to be added where.