fix: Make datatype cycle detection independent of auto-init

Source/DafnyCore/AST/Expressions/Conditional/Patterns/ExtendedPattern.cs

@@ -93,6 +93,8 @@ public void CheckLinearExtendedPattern(Type type, ResolutionContext resolutionCo
         return;
       }
 
+      Contract.Assert(tupleTypeDecl.Ctors.Count == 1);
+      Contract.Assert(tupleTypeDecl.Ctors[0] == tupleTypeDecl.GroundingCtor);
       idpat.Ctor = tupleTypeDecl.GroundingCtor;
 
       //We expect the number of arguments in the type of the matchee and the provided pattern to match, except if the pattern is a bound variable

Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs

@@ -1,17 +1,33 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Linq;
 
 namespace Microsoft.Dafny;
 
 public class IndDatatypeDecl : DatatypeDecl {
   public override string WhatKind { get { return "datatype"; } }
-  public DatatypeCtor GroundingCtor;  // set during resolution
+  [FilledInDuringResolution] public DatatypeCtor GroundingCtor; // set during resolution (possibly to null)
 
   public override DatatypeCtor GetGroundingCtor() {
-    return GroundingCtor;
+    return GroundingCtor ?? Ctors.FirstOrDefault(ctor => ctor.IsGhost, Ctors[0]);
   }
 
-  public bool[] TypeParametersUsedInConstructionByGroundingCtor;  // set during resolution; has same length as the number of type arguments
+  private bool[] typeParametersUsedInConstructionByGroundingCtor;
+
+  public bool[] TypeParametersUsedInConstructionByGroundingCtor {
+    get {
+      if (typeParametersUsedInConstructionByGroundingCtor == null) {
+        typeParametersUsedInConstructionByGroundingCtor = new bool[TypeArgs.Count];
+        for (var i = 0; i < typeParametersUsedInConstructionByGroundingCtor.Length; i++) {
+          typeParametersUsedInConstructionByGroundingCtor[i] = true;
+        }
+      }
+      return typeParametersUsedInConstructionByGroundingCtor;
+    }
+    set {
+      typeParametersUsedInConstructionByGroundingCtor = value;
+    }
+  }
 
   public enum ES { NotYetComputed, Never, ConsultTypeArguments }
   public ES EqualitySupport = ES.NotYetComputed;

Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs

@@ -49,6 +49,39 @@ public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Bo
     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/AST/TypeDeclarations/TupleTypeDecl.cs

@@ -39,6 +39,7 @@ private TupleTypeDecl(ModuleDefinition systemModule, List<TypeParameter> typeArg
       new List<Type>(), new List<MemberDecl>(), attributes, false) {
     Contract.Requires(systemModule != null);
     Contract.Requires(typeArgs != null);
+    Contract.Assert(Ctors.Count == 1);
     ArgumentGhostness = argumentGhostness;
     foreach (var ctor in Ctors) {
       ctor.EnclosingDatatype = this;  // resolve here
@@ -63,6 +64,10 @@ private static List<TypeParameter> CreateCovariantTypeParameters(int dims) {
     }
     return ts;
   }
+
+  /// <summary>
+  /// Creates the one and only constructor of the tuple type.
+  /// </summary>
   private static List<DatatypeCtor> CreateConstructors(List<TypeParameter> typeArgs, List<bool> argumentGhostness) {
     Contract.Requires(typeArgs != null);
     var formals = new List<Formal>();

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -1272,6 +1272,26 @@ void CheckIfCompilable(RedirectingTypeDecl declWithConstraint) {
         FillInPostConditionsAndBodiesOfPrefixLemmas(declarations);
       }
 
+      // 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. Therefore,
+      // we search for such type declarations and give error messages if something is found.
+      if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
+        foreach (var dtd in declarations.ConvertAll(decl => decl as IndDatatypeDecl).Where(dtd => dtd != null && dtd.Ctors.Count != 0)) {
+          if (AreThereAnyObviousSignsOfEmptiness(UserDefinedType.FromTopLevelDecl(dtd.tok, dtd), new HashSet<IndDatatypeDecl>())) {
+            reporter.Error(MessageSource.Resolver, dtd,
+              $"because of cyclic dependencies among constructor argument types, no instances of datatype '{dtd.Name}' can be constructed");
+          }
+        }
+      }
+
       // Perform the stratosphere check on inductive datatypes, and compute to what extent the inductive datatypes require equality support
       if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { // because SccStratosphereCheck depends on subset-type/newtype base types being successfully resolved
         foreach (var dtd in datatypeDependencies.TopologicallySortedComponents()) {
@@ -2850,6 +2870,35 @@ private void CheckOverride_ResolvedParameters(IToken tok, List<Formal> old, List
       }
     }
 
+    private bool AreThereAnyObviousSignsOfEmptiness(Type type, ISet<IndDatatypeDecl> beingVisited) {
+      type = type.NormalizeExpandKeepConstraints(); // 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 (ArrowType.IsTotalArrowTypeName(cl.Name)) {
+          return AreThereAnyObviousSignsOfEmptiness(udt.TypeArgs.Last(), beingVisited);
+        } else if (cl is SubsetTypeDecl subsetTypeDecl) {
+          return AreThereAnyObviousSignsOfEmptiness(subsetTypeDecl.RhsWithArgument(udt.TypeArgs), beingVisited);
+        } else if (cl is NewtypeDecl newtypeDecl) {
+          return AreThereAnyObviousSignsOfEmptiness(newtypeDecl.RhsWithArgument(udt.TypeArgs), beingVisited);
+        }
+        if (cl is IndDatatypeDecl datatypeDecl) {
+          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), 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.
@@ -2879,7 +2928,7 @@ void SccStratosphereCheck(IndDatatypeDecl startingPoint, Graph<IndDatatypeDecl/*
           if (dt.GroundingCtor != null) {
             // previously cleared
           } else if (ComputeGroundingCtor(dt)) {
-            Contract.Assert(dt.GroundingCtor != null);  // should have been set by the successful call to StratosphereCheck)
+            Contract.Assert(dt.GroundingCtor != null);  // should have been set by the successful call to ComputeGroundingCtor)
             clearedThisRound++;
             totalCleared++;
           }
@@ -2890,27 +2939,21 @@ void SccStratosphereCheck(IndDatatypeDecl startingPoint, Graph<IndDatatypeDecl/*
         } 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;
         }
       }
     }
 
     /// <summary>
-    /// Check that the datatype has some constructor all whose argument types can be constructed.
+    /// Check if the datatype has some constructor all whose argument types can be constructed.
     /// Returns 'true' and sets dt.GroundingCtor if that is the case.
     /// </summary>
     bool ComputeGroundingCtor(IndDatatypeDecl dt) {
       Contract.Requires(dt != null);
       Contract.Requires(dt.GroundingCtor == null);  // the intention is that this method be called only when GroundingCtor hasn't already been set
       Contract.Ensures(!Contract.Result<bool>() || dt.GroundingCtor != null);
 
-      // Stated differently, check that there is some constuctor where no argument type goes to the same stratum.
+      // Stated differently, check that there is some constructor where no argument type goes to the same stratum.
       DatatypeCtor groundingCtor = null;
       ISet<TypeParameter> lastTypeParametersUsed = null;
       foreach (DatatypeCtor ctor in dt.Ctors) {

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy

@@ -20,7 +20,7 @@ class C {
 
 datatype D = A
 
-datatype NeverendingList = Cons(int, NeverendingList)  // error: no grounding constructor
+
 
 datatype MutuallyRecursiveDataType<T> =
   FromANumber(int) |  // this is the base case
@@ -246,7 +246,36 @@ module OtherCycles1 {
 }
 
 module OtherCycles2 {
-  datatype CycleW = CycleW(CycW)
+  // the next line uses a general arrow
+  datatype CycleW = CycleW(int ~> CycW)
   type CycW = c: CycleW | true witness W()  // error: dependency cycle W -> CycW -> CycleW
   function W(): CycleW
 }
+
+module OtherCycles3 {
+  // the next line uses a partial arrow
+  datatype CycleW = CycleW(int -> CycW) // error: dependency cycle W -> CycW -> CycleW
+  type CycW = c: CycleW | true witness W()
+  function W(): CycleW
+}
+
+module OtherCycles4 {
+  // the next line uses a total arrow
+  datatype CycleW = CycleW(int -> CycW) // error: because of cycle among constructor argument types, 'CycleW' is empty
+  type CycW = c: CycleW | true witness W()
+  function W(): CycleW
+}
+
+module OtherCycles5 {
+  // the next line uses a subset type over a total arrow
+  type MyTotalArrow<X, Y> = f: X -> Y | true
+  datatype CycleW = CycleW(MyTotalArrow<int, CycW>) // error: because of cycle among constructor argument types, 'CycleW' is empty
+  type CycW = c: CycleW | true witness W()
+  function W(): CycleW
+}
+
+module NE {
+  datatype NeverendingList = Cons(int, NeverendingList)  // error: empty type
+  datatype Growing<X> = Make(Growing<array<X>>) // error: empty type
+  datatype MaybeGrowing<X> = Make(array<MaybeGrowing<X>>) // okay, since it does not violate the cycle rule
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy.expect

@@ -37,5 +37,10 @@ TypeTests.dfy(238,20): Error: using the type being defined ('B') here would caus
 TypeTests.dfy(243,20): Error: using the type being defined ('E') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
 TypeTests.dfy(244,20): Error: using the type being defined ('F') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
 TypeTests.dfy(245,20): Error: using the type being defined ('G') here would cause a logical inconsistency by defining a type whose cardinality exceeds itself (like the Continuum Transfunctioner, you might say its power would then be exceeded only by its mystery)
-TypeTests.dfy(250,7): Error: recursive constraint dependency involving a subset type: CycW -> W -> CycleW -> CycW
-40 resolution/type errors detected in TypeTests.dfy
+TypeTests.dfy(251,7): Error: recursive constraint dependency involving a subset type: CycW -> W -> CycleW -> CycW
+TypeTests.dfy(257,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'CycleW' can be constructed
+TypeTests.dfy(264,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'CycleW' can be constructed
+TypeTests.dfy(272,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'CycleW' can be constructed
+TypeTests.dfy(278,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
+TypeTests.dfy(279,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Growing' can be constructed
+45 resolution/type errors detected in TypeTests.dfy

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

@@ -1,17 +1,24 @@
 // RUN: %exits-with 2 %verify "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-datatype T = T(T, T) {
-  ghost predicate P() {
-    match this
-      case T(0, 1) => false
+module A {
+  datatype T = T(T, T)
+  {
+    ghost predicate P() {
+      match this
+      case T(0, 1) => false // error (x2): neither constant pattern of constructor pattern has the right type
+    }
   }
-}
-method a() 
-{
-    var tok := (0,0);
+
+  method M() {
+    var tok := (0, 0);
     match tok {
-      case "B" => 
+      case "B" => // error: "B" is not of type (int, int)
       case _ => 
     }
+  }
+}
+
+module B {
+  datatype T = T(T, T) // error (masked by other errors in module A): cycle prevents instances
 }

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

@@ -1,4 +1,5 @@
-git-issue-2139.dfy(14,11): Error: pattern doesn't correspond to a tuple
-git-issue-2139.dfy(7,13): Error: Constant pattern used in place of datatype
-git-issue-2139.dfy(7,16): Error: Constant pattern used in place of datatype
-3 resolution/type errors detected in git-issue-2139.dfy
+git-issue-2139.dfy(16,11): Error: pattern doesn't correspond to a tuple
+git-issue-2139.dfy(9,13): Error: Constant pattern used in place of datatype
+git-issue-2139.dfy(9,16): Error: Constant pattern used in place of datatype
+git-issue-2139.dfy(23,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'T' can be constructed
+4 resolution/type errors detected in git-issue-2139.dfy