Compute IsObviouslyEmpty for inductive datatypes

Fixes #4939

Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs

@@ -49,6 +49,39 @@ public class NewtypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, Redirect
  this.NewSelfSynonym();
  }
 
+ /// <summary>
+ /// Return .BaseType instantiated with "typeArgs", but only look at the part of .BaseType that is in scope.
+ /// </summary>
+ public Type RhsWithArgument(List<Type> typeArgs) {
+ Contract.Requires(typeArgs != null);
+ Contract.Requires(typeArgs.Count == TypeArgs.Count);
+ var scope = Type.GetScope();
+ var rtd = BaseType.AsRevealableType;
+ if (rtd != null) {
+ Contract.Assume(rtd.AsTopLevelDecl.IsVisibleInScope(scope));
+ if (!rtd.IsRevealedInScope(scope)) {
+ // type is actually hidden in this scope
+ return rtd.SelfSynonym(typeArgs);
+ }
+ }
+ return RhsWithArgumentIgnoringScope(typeArgs);
+ }
+ /// <summary>
+ /// Returns the declared .BaseType but with formal type arguments replaced by the given actuals.
+ /// </summary>
+ public Type RhsWithArgumentIgnoringScope(List<Type> typeArgs) {
+ Contract.Requires(typeArgs != null);
+ Contract.Requires(typeArgs.Count == TypeArgs.Count);
+ // Instantiate with the actual type arguments
+ if (typeArgs.Count == 0) {
+ // this optimization seems worthwhile
+ return BaseType;
+ } else {
+ var subst = TypeParameter.SubstitutionMap(TypeArgs, typeArgs);
+ return BaseType.Subst(subst);
+ }
+ }
+
  public TopLevelDecl AsTopLevelDecl => this;
  public TypeDeclSynonymInfo SynonymInfo { get; set; }
 

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -1273,6 +1273,13 @@ public partial class ModuleResolver {
  }
 
  // Perform the stratosphere check on inductive datatypes, and compute to what extent the inductive datatypes require equality support
+ var inductiveDatatypesCheckedForEmptiness = new Dictionary<IndDatatypeDecl, bool>();
+ foreach (var dtd in declarations.ConvertAll(decl => decl as IndDatatypeDecl).Where(dtd => dtd != null)) {
+ if (IsObviouslyEmpty(dtd, inductiveDatatypesCheckedForEmptiness)) {
+ reporter.Error(MessageSource.Resolver, dtd,
+ $"because of cyclic dependencies among constructor argument types, no instances of datatype '{dtd.Name}' can be constructed");
+ }
+ }
  foreach (var dtd in datatypeDependencies.TopologicallySortedComponents()) {
  if (datatypeDependencies.GetSCCRepresentative(dtd) == dtd) {
  // do the following check once per SCC, so call it on each SCC representative
@@ -2846,6 +2853,47 @@ public ReportOtherAdditionalInformation_Visitor(ModuleResolver resolver)
  }
  }
 
+ /// <summary>
+ /// Determine if "datatypeDecl" is involved in a cycle in such a way that it is obvious that the type has no instances.
+ /// Return the answer.
+ ///
+ /// "informationSoFar" is used as a cache of computed information. The method updates the cache for "datatypeDecl".
+ /// </summary>
+ bool IsObviouslyEmpty(IndDatatypeDecl datatypeDecl, IDictionary<IndDatatypeDecl, bool> informationSoFar) {
+ var datatype = UserDefinedType.FromTopLevelDecl(datatypeDecl.tok, datatypeDecl);
+ var isEmpty = AreThereAnyObviousSignsOfEmptiness(datatype, informationSoFar, new HashSet<IndDatatypeDecl>());
+ informationSoFar.Add(datatypeDecl, isEmpty);
+ return isEmpty;
+ }
+
+ private bool AreThereAnyObviousSignsOfEmptiness(Type type, IDictionary<IndDatatypeDecl, bool> informationSoFar, ISet<IndDatatypeDecl> beingVisited) {
+ type = type.NormalizeExpand(); // cut through type proxies, type synonyms, but being mindful of what's in scope
+ if (type is UserDefinedType { ResolvedClass: var cl} udt) {
+ Contract.Assert(cl != null);
+ if (cl is NewtypeDecl newtypeDecl) {
+ return AreThereAnyObviousSignsOfEmptiness(newtypeDecl.RhsWithArgument(udt.TypeArgs), informationSoFar, beingVisited);
+ }
+ if (cl is IndDatatypeDecl datatypeDecl) {
+ if (informationSoFar.TryGetValue(datatypeDecl, out var isObviouslyEmpty)) {
+ return isObviouslyEmpty;
+ }
+ if (beingVisited.Contains(datatypeDecl)) {
+ // This datatype may be empty, but it's definitely empty if we consider only the constructors that have been visited
+ // since AreThereAnyObviousSignsOfEmptiness was called from IsObviouslyEmpty.
+ return true;
+ }
+ beingVisited.Add(datatypeDecl);
+ var typeMap = TypeParameter.SubstitutionMap(datatypeDecl.TypeArgs, udt.TypeArgs);
+ var isEmpty = datatypeDecl.Ctors.TrueForAll(ctor =>
+ ctor.Formals.Exists(formal => AreThereAnyObviousSignsOfEmptiness(formal.Type.Subst(typeMap), informationSoFar, beingVisited)));
+ beingVisited.Remove(datatypeDecl);
+ return isEmpty;
+ }
+ }
+
+ return false;
+ }
+
  /// <summary>
  /// Check that the SCC of 'startingPoint' can be carved up into stratospheres in such a way that each
  /// datatype has some value that can be constructed from datatypes in lower stratospheres only.
@@ -2886,12 +2934,6 @@ public ReportOtherAdditionalInformation_Visitor(ModuleResolver resolver)
  } else if (clearedThisRound != 0) {
  // some progress was made, so let's keep going
  } else {
- // whatever is in scc-cleared now failed to pass the test
- foreach (var dt in scc) {
- if (dt.GroundingCtor == null) {
- reporter.Error(MessageSource.Resolver, dt, "because of cyclic dependencies among constructor argument types, no instances of datatype '{0}' can be constructed", dt.Name);
- }
- }
  return;
  }
  }

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939.dfy

@@ -0,0 +1,148 @@
+// RUN: %exits-with 2 %verify --type-system-refresh --general-traits=datatype "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module FromIssue0 {
+ trait Program {
+ method Compute() returns (r: Result)
+ }
+
+ datatype Result =
+ | Bounce(next: Program)
+ | Done()
+
+ datatype Trivial extends Program =
+ Trivial()
+ {
+ method Compute() returns (r: Result) {
+ return Done();
+ }
+ }
+
+ datatype Seq extends Program =
+ Seq(left: Program, right: Program) // this once gave an error, saying Seq is empty because of cyclic dependencies
+ {
+ method Compute() returns (r: Result) {
+ var result := left.Compute();
+ match result
+ case Done() => r := right.Compute();
+ case Bounce(next) =>
+ var next' := Seq(next, right);
+ assert next' is Program;
+ return Bounce(next');
+ }
+ }
+}
+
+module FromIssue1 {
+ trait Program {
+ }
+
+ datatype Trivial extends Program =
+ Trivial()
+
+ datatype Seq extends Program =
+ Seq(left: Program, right: Program) // this once gave an error, saying Seq is empty because of cyclic dependencies
+}
+
+module FromIssue2 {
+ // NoInstances has no instances
+ class NoInstances {
+ constructor ()
+ requires false
+ {
+ }
+ }
+
+ // ... and therefore, neither does D. However, this is not detected syntactically, so there are no complaints.
+ datatype D = D(n: NoInstances)
+}
+
+module FromIssue3 {
+ trait Interface {
+ function getString(i: int): string
+ }
+
+ datatype Wrapper extends Interface = Wrapper(inner: Interface) // this once gave the cyclic-dependency error
+ {
+ function getString(i: int): string {
+ inner.getString(i+1)
+ }
+ }
+
+ datatype DetectZero extends Interface = DetectZero
+ {
+ function getString(i: int): string {
+ if i == 0
+ then "zero"
+ else "I don't know"
+ }
+ }
+
+ function getWrappedDetectZero(): Interface {
+ Wrapper(DetectZero)
+ }
+}
+
+module FromIssue4 {
+ trait Interface {
+ function GetString(i: int): string
+ }
+
+ class {:extern} Store {
+ var interface: Interface
+
+ constructor (interface: Interface) {
+ this.interface := interface;
+ }
+
+ function GetInterface(): (res: Interface)
+ ensures res == interface
+ }
+
+ datatype Wrapper extends Interface = Wrapper(inner: Store)
+ {
+ function GetString(i: int): string {
+ inner.GetInterface().GetString(i + 1)
+ }
+ }
+}
+
+module SimpleExample0 {
+ trait GeneralTrait {
+ function F(): int { 5 }
+ }
+
+ datatype Wrapper = Wrapper(g: GeneralTrait) // this once gave the cyclic-dependency error
+}
+
+module SimpleExample1 {
+ trait GeneralTrait extends object {
+ function F(): int { 5 }
+ }
+
+ datatype Wrapper = Wrapper(g: GeneralTrait) // this was always fine
+}
+
+module Standard {
+ datatype List<X> = Nil | Cons(X, List<X>)
+
+ datatype Op = Plus | Times
+ datatype Expr = Value(int) | Node(operator: Op, arguments: List<Expr>)
+}
+
+module Good0 {
+ datatype Mutual = M0(Nutual) | M1(Mutual)
+ datatype Nutual = N0(Mutual) | Easy
+}
+
+module Good1 {
+ datatype Nutual = N0(Mutual) | Easy
+ datatype Mutual = M0(Nutual) | M1(Mutual)
+}
+
+module Bad {
+ datatype T = Make(T, T) // error: obviously empty
+
+ datatype Mutual = M0(Nutual) | M1(Mutual) // error: empty
+ datatype Nutual = N0(Mutual) // error: empty
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939.dfy.expect

@@ -0,0 +1,4 @@
+git-issue-4939.dfy(144,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'T' can be constructed
+git-issue-4939.dfy(146,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Mutual' can be constructed
+git-issue-4939.dfy(147,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nutual' can be constructed
+3 resolution/type errors detected in git-issue-4939.dfy