This PR fixes and closes three reported bugs related to datatypes extending traits:

• Reference-type traits used with import opened were not recognized as reference types (issue Reference trait not recognized in separate modules with opened #4936).
• Implicit conversions from a datatype to a parent trait had caused malformed Boogie (issue Boogie crash: Error: invalid argument types (Box and DatatypeType) to binary operator == #4983). This was actually fixed in PR fix: Make datatype cycle detection independent of auto-init #4997, but the present PR adds tests for it.
• Equality (and disequality) comparisons with a datatype (or codatatype) on the left and a parent trait on the right had caused malformed Boogie (issue Malformed Boogie when comparing datatype with parent trait #4994).

Fixes #4936
Closes #4983
Fixes #4994

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.