fix: Make datatype cycle detection independent of auto-init

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

@@ -93,6 +93,8 @@ public abstract class ExtendedPattern : TokenNode {
  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 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/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 TupleTypeDecl(ModuleDefinition systemModule, List<TypeParameter> typeArg
  }
  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 @@ public partial class ModuleResolver {
  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 @@ public ReportOtherAdditionalInformation_Visitor(ModuleResolver resolver)
  }
  }
 
+ 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 @@ public ReportOtherAdditionalInformation_Visitor(ModuleResolver resolver)
  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 @@ 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;
  }
  }
  }
 
  /// <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