fix: Make datatype cycle detection independent of auto-init

[RustanLeino]

This PR makes the "datatype has no instances" checks more liberal.

Fixes #4939

Description

An inductive datatype is allowed to be defined as an empty type. For example, in

predicate P(x: int) { false }
type Subset = x: int | P(x) witness *
datatype Record = Record(Subset)

Record is an empty type, because Subset is, since P(x) is always false. But if P(x) was instead defined to be true for some x's, then Record would be nonempty. Determining whether or not Record is empty goes well beyond the syntactic checks of the type system.

However, if a datatype is empty because of some "obvious" cycle among datatype definitions, then that is both detectable by syntactic checks and likely unintended by the programmer. By this PR, Dafny will search for such type declarations and give error messages if an inductive datatype is necessarily involved in such an "obvious" cycle.

Previous behavior

Dafny had attempted this check before, too, but then the rule was too strict. The check had been implemented as part of the machinery that computed "grounding constructors". That search consulted the auto-init status of the types that a datatype depends on. Since traits are of the "possibly empty" auto-init category, if every constructor of a datatype depended on a trait (that is, the constructors had a parameter whose type is a trait), then Dafny would report an error.

This PR removes the error reporting done by the machinery that computes grounding constructors. It adds a new, separate check in the resolver to determine the "obvious" cycles.

Grounding constructors

The name "grounding constructor" was originally to mean "a constructor that can be used to construct an instance of the datatype". This name is rather outdated, because Dafny's syntactic checks do not ensure datatypes to be nonempty anyway (case in point: type Record above). A name like "initializing constructor" would be more to the point--the compiler uses this constructor in a generated method for creating an arbitrary value of the type. (At run time, this method will never be called if the datatype really is empty, but since the compiler does not know this, it still has to generate valid target code for this method.)

Alternative designs

One alternative design would be to change the new "because of a cycle, this datatype has no instances" error message to be just a warning. This alternative has some merit, since Dafny already supports empty types.

Another alternative would be to not perform the check at all, and to report neither an error nor a warning for datatypes with no instances. This would give more flexibility. However, since there are simple ways to write an empty type, a program where a datatype cycle causes a type to have no instances is most likely a mistake that the programmer would want to know about and fix.

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

[RustanLeino]

This PR also fixes #4983. Tests for that issue have been added in PR #5058.