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.Warning(MessageSource.Resolver, ResolutionErrors.ErrorId.r_empty_cyclic_datatype, dtd.tok,
+ $"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()) {
@@ -2563,6 +2583,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.
@@ -2592,7 +2641,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++;
  }
@@ -2603,27 +2652,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/DafnyCore/Resolver/ResolutionErrors.cs

@@ -82,7 +82,8 @@ public enum ErrorId {
  r_assert_only_before_after,
  r_failure_methods_deprecated,
  r_member_only_assumes_other,
- r_member_only_has_no_before_after
+ r_member_only_has_no_before_after,
+ r_empty_cyclic_datatype
  }
 
  static ResolutionErrors() {

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -1551,7 +1551,10 @@ public ExpressionTranslator(ExpressionTranslator etran, Boogie.Expr heap)
  Contract.Requires(let != null);
  var substMap = new Dictionary<IVariable, Expression>();
  for (int i = 0; i < let.LHSs.Count; i++) {
- BoogieGenerator.AddCasePatternVarSubstitutions(let.LHSs[i], TrExpr(let.RHSs[i]), substMap);
+ var rhs = TrExpr(let.RHSs[i]);
+ var toType = let.LHSs[i].Var?.Type ?? let.LHSs[i].Expr.Type;
+ rhs = BoogieGenerator.CondApplyBox(rhs.tok, rhs, let.RHSs[i].Type, toType);
+ BoogieGenerator.AddCasePatternVarSubstitutions(let.LHSs[i], rhs, substMap);
  }
  lhss = new List<Boogie.Variable>();
  rhss = new List<Boogie.Expr>();

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs

@@ -1229,7 +1229,8 @@ private record ReadsCheckDelayer(ExpressionTranslator etran, Function selfCallsA
  Contract.Assert(resultType != null);
  var bResult = etran.TrExpr(expr);
  CheckSubrange(expr.tok, bResult, expr.Type, resultType, builder);
- builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, expr.tok, expr, e => Bpl.Expr.Eq(result, e),
+ builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, expr.tok, expr,
+ e => Bpl.Expr.Eq(result, CondApplyBox(expr.tok, e, expr.Type, resultType)),
  resultDescription));
  builder.Add(TrAssumeCmd(expr.tok, etran.CanCallAssumption(expr)));
  builder.Add(new CommentCmd("CheckWellformedWithResult: any expression"));
@@ -1369,15 +1370,14 @@ private record ReadsCheckDelayer(ExpressionTranslator etran, Function selfCallsA
  void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr result, Type resultType, List<Bpl.Variable> locals,
  BoogieStmtListBuilder builder, ExpressionTranslator etran, bool checkRhs) {
  if (e.Exact) {
- var uniqueSuffix = "#Z" + defaultIdGenerator.FreshNumericId("#Z");
  var substMap = SetupBoundVarsAsLocals(e.BoundVars.ToList<BoundVar>(), builder, locals, etran, "#Z");
  Contract.Assert(e.LHSs.Count == e.RHSs.Count); // checked by resolution
  var varNameGen = CurrentIdGenerator.NestedFreshIdGenerator("let#");
  for (int i = 0; i < e.LHSs.Count; i++) {
  var pat = e.LHSs[i];
  var rhs = e.RHSs[i];
  var nm = varNameGen.FreshId(string.Format("#{0}#", i));
- var r = new Bpl.LocalVariable(pat.tok, new Bpl.TypedIdent(pat.tok, nm, TrType(rhs.Type)));
+ var r = new Bpl.LocalVariable(pat.tok, new Bpl.TypedIdent(pat.tok, nm, TrType(pat.Expr.Type)));
  locals.Add(r);
  var rIe = new Bpl.IdentifierExpr(rhs.tok, r);
  CheckWellformedWithResult(e.RHSs[i], wfOptions, rIe, pat.Expr.Type, locals, builder, etran, "let expression binding RHS well-formed");

Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs

@@ -876,7 +876,7 @@ public partial class BoogieGenerator {
  }
 
  var etranBody = layer == null ? etran : etran.LimitedFunctions(f, ly);
- var trbody = etranBody.TrExpr(bodyWithSubst);
+ var trbody = CondApplyBox(f.tok, etranBody.TrExpr(bodyWithSubst), f.Body.Type, f.ResultType);
  tastyVegetarianOption = BplAnd(etranBody.CanCallAssumption(bodyWithSubst),
  BplAnd(TrFunctionSideEffect(bodyWithSubst, etranBody), Bpl.Expr.Eq(funcAppl, trbody)));
  }

Source/DafnyCore/Verifier/BoogieGenerator.Types.cs

@@ -1156,6 +1156,8 @@ void AddRedirectingTypeDeclAxioms<T>(bool is_alloc, T dd, string fullName)
  } else if (fromType.IsTraitType) {
  // cast from a non-reference trait
  return UnboxIfBoxed(r, toType);
+ } else if (fromType.Equals(toType)) {
+ return r;
  } else {
  Contract.Assert(false, $"No translation implemented from {fromType} to {toType}");
  }

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -3271,17 +3271,12 @@ class BoilerplateTriple { // a triple that is now a quintuple
 
  if (!ModeledAsBoxType(fromType) && (toType == null || ModeledAsBoxType(toType))) {
  // if "e" denotes "Unbox(E): T", then just return "E"
- var coerce = e as Bpl.NAryExpr;
- if (coerce != null && coerce.Fun is Bpl.TypeCoercion) {
+ if (e is Bpl.NAryExpr { Fun: Bpl.TypeCoercion } coerce) {
  Contract.Assert(coerce.Args.Count == 1);
- Contract.Assert(Bpl.Type.Equals(((Bpl.TypeCoercion)coerce.Fun).Type, TrType(fromType))); ;
- var call = coerce.Args[0] as Bpl.NAryExpr;
- if (call != null && call.Fun is Bpl.FunctionCall) {
- var fn = (Bpl.FunctionCall)call.Fun;
- if (fn.FunctionName == "$Unbox") {
- Contract.Assert(call.Args.Count == 1);
- return call.Args[0];
- }
+ Contract.Assert(Bpl.Type.Equals(((Bpl.TypeCoercion)coerce.Fun).Type, TrType(fromType)));
+ if (coerce.Args[0] is Bpl.NAryExpr { Fun: Bpl.FunctionCall { FunctionName: "$Unbox" } } call) {
+ Contract.Assert(call.Args.Count == 1);
+ return call.Args[0];
  }
  }
  // return "Box(e)"

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

@@ -10,10 +10,10 @@ module TestInductiveDatatypes
  datatype Record<T> = Ctor(T)
 
  datatype RecInt = Ctor(Record<int>) // this is fine
- datatype Rec_Forever = Ctor(Record<Rec_Forever>) // error
+ datatype Rec_Forever = Ctor(Record<Rec_Forever>) // warning: no instances
  datatype Rec_Stops = Cons(Record<Rec_Stops>, Rec_Stops) | Nil // this is okay
 
- datatype D<T> = Ctor(E<D<T>>) // error: illegal cycle
+ datatype D<T> = Ctor(E<D<T>>) // warning: no instances
  datatype E<T> = Ctor(T)
 
  // the following is okay
@@ -35,7 +35,7 @@ module MoreInductive {
 
  datatype M = All(List<M>)
  datatype H<'a> = HH('a, Tree<'a>)
- datatype K<'a> = KK('a, Tree<K<'a>>) // error
+ datatype K<'a> = KK('a, Tree<K<'a>>) // warning: no instances
  datatype L<'a> = LL('a, Tree<List<L<'a>>>)
 }
 
@@ -61,7 +61,7 @@ module TestCoinductiveDatatypes
  datatype FiniteEnough_Class = Ctor(MyClass<FiniteEnough_Class>)
  datatype FiniteEnough_Co = Ctor(LazyRecord<FiniteEnough_Co>)
  datatype FiniteEnough_Dt = Ctor(GenericDt<FiniteEnough_Dt>) // fine
- datatype NotFiniteEnough_Dt = Ctor(GenericRecord<NotFiniteEnough_Dt>) // error
+ datatype NotFiniteEnough_Dt = Ctor(GenericRecord<NotFiniteEnough_Dt>) // warning: no instances
 
 }
 

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

@@ -1,7 +1,7 @@
-Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
-Coinductive.dfy(16,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
-Coinductive.dfy(38,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
-Coinductive.dfy(64,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
+Coinductive.dfy(13,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
+Coinductive.dfy(16,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
+Coinductive.dfy(38,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
+Coinductive.dfy(64,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
 Coinductive.dfy(93,8): Error: a greatest predicate can be called recursively only in positive positions
 Coinductive.dfy(94,8): Error: a greatest predicate can be called recursively only in positive positions
 Coinductive.dfy(95,8): Error: a greatest predicate can be called recursively only in positive positions
@@ -38,4 +38,4 @@ Coinductive.dfy(355,19): Error: a greatest predicate can be called recursively o
 Coinductive.dfy(355,44): Error: a greatest predicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
 Coinductive.dfy(358,19): Error: a greatest predicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
 Coinductive.dfy(358,46): Error: a greatest predicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
-40 resolution/type errors detected in Coinductive.dfy
+36 resolution/type errors detected in Coinductive.dfy

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

@@ -1040,10 +1040,10 @@ module CycleError2 {
 module CycleErrors3 {
  type A = (B, D<bool>)
  type B = C
- class C {
+ class C { // error: since A is not auto-init, class C needs a constructor
  var a: A // this is fine
  }
- datatype D<X> = Make(A, B, C) // error: cannot construct a D<X>
+ datatype D<X> = Make(A, B, C) // warning: D<X> is empty
 }
 module CycleError4 {
  type A = B // error: cycle: A -> B -> A