diff --git a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/ExtendedPattern.cs b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/ExtendedPattern.cs
index 43a94fe1b36..e745cb7fc71 100644
--- a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/ExtendedPattern.cs
+++ b/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
diff --git a/Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs
index dd9749718a7..6af1191fe99 100644
--- a/Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs
+++ b/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;
diff --git a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs
index ce41305f19b..8ff7a2f43de 100644
--- a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs
+++ b/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; }
 
diff --git a/Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs
index 0e6b8673243..590e4915204 100644
--- a/Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs
+++ b/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>();
diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs
index c9188e490fe..b4a60bff93f 100644
--- a/Source/DafnyCore/Resolver/ModuleResolver.cs
+++ b/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,19 +2652,13 @@ 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) {
@@ -2623,7 +2666,7 @@ public ReportOtherAdditionalInformation_Visitor(ModuleResolver resolver)
       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) {
diff --git a/Source/DafnyCore/Resolver/ResolutionErrors.cs b/Source/DafnyCore/Resolver/ResolutionErrors.cs
index 5c0eac59c62..69a6fa57649 100644
--- a/Source/DafnyCore/Resolver/ResolutionErrors.cs
+++ b/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() {
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
index 5494a3a705c..810e22102dd 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
+++ b/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>();
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs
index d740e699064..02af1554a10 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs
+++ b/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,7 +1370,6 @@ 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#");
@@ -1377,7 +1377,7 @@ private record ReadsCheckDelayer(ExpressionTranslator etran, Function selfCallsA
           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");
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs
index d5d67116770..2c445f9c5c8 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs
+++ b/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)));
     }
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs
index c8d09035bcb..31defc234b2 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs
+++ b/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}");
     }
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs
index 5c75bffc2f5..18c4f0c2efa 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.cs
+++ b/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)"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Coinductive.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Coinductive.dfy
index 3615f08e749..fff9f324eae 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Coinductive.dfy
+++ b/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
 
 }
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Coinductive.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Coinductive.dfy.expect
index 9f58bc94721..5a5f281ae11 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Coinductive.dfy.expect
+++ b/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
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors.dfy
index dabc4a9fdf2..fe0aefea006 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors.dfy
+++ b/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
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors.dfy.expect
index 9782a2aecd0..e6086abf38e 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors.dfy.expect
@@ -133,7 +133,8 @@ ResolutionErrors.dfy(1023,22): Error: Type or type parameter is not declared in
 ResolutionErrors.dfy(1030,7): Error: type-synonym cycle: A -> A
 ResolutionErrors.dfy(1033,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A
 ResolutionErrors.dfy(1037,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1046,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
+ResolutionErrors.dfy(1046,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
+ResolutionErrors.dfy(1043,8): Error: class 'C' with fields without known initializers, like 'a' of type 'A', must declare a constructor
 ResolutionErrors.dfy(1049,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A
 ResolutionErrors.dfy(1054,7): Error: cycle among redirecting types (newtypes, subset types, type synonyms): A -> B -> A
 ResolutionErrors.dfy(1059,7): Error: type-synonym cycle: A -> A
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy
index 1950c3ea51b..9b61908c456 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy
+++ b/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
@@ -226,11 +226,11 @@ module ArrayTests {
 // ---------------------
 
 module OtherCycles0 {
-  datatype A = Ctor(A -> A)  // error: cannot be constructed
-  datatype B = Ctor(int -> B)  // error: cannot be constructed
+  datatype A = Ctor(A -> A)  // warning: empty datatype
+  datatype B = Ctor(int -> B)  // warning: empty datatype
 
-  datatype Cycle = Cycle(Cyc)  // error: cannot be constructed
-  type Cyc = c: Cycle | true
+  datatype Cycle = Cycle(Cyc)  // warning: empty datatype
+  type Cyc = c: Cycle | true // error: dependency: Cyc -> Cycle -> Cyc
 }
 
 module OtherCycles1 {
@@ -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) // warning: no instance possible
+  type CycW = c: CycleW | true witness W() // error: dependency cycle W -> CycW -> CycleW
+  function W(): CycleW
+}
+
+module OtherCycles4 {
+  // the next line uses a total arrow
+  datatype CycleW = CycleW(int -> CycW) // warning: because of cycle among constructor argument types, 'CycleW' is empty
+  type CycW = c: CycleW | true witness W() // error: dependency cycle: CycW -> W -> CycleW -> CycW
+  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>) // warning: because of cycle among constructor argument types, 'CycleW' is empty
+  type CycW = c: CycleW | true witness W() // error: dependency cycle: CycW -> W -> CycleW -> CycW
+  function W(): CycleW
+}
+
+module NE {
+  datatype NeverendingList = Cons(int, NeverendingList)  // warning: empty type
+  datatype Growing<X> = Make(Growing<array<X>>) // warning: empty type
+  datatype MaybeGrowing<X> = Make(array<MaybeGrowing<X>>) // okay, since it does not violate the cycle rule
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy.expect
index 1aa4950a6ab..6b858119876 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy.expect
@@ -29,13 +29,22 @@ TypeTests.dfy(198,10): Error: incorrect argument type for datatype constructor p
 TypeTests.dfy(204,10): Error: incorrect argument type for datatype constructor parameter (expected ? -> Dt<?>, found Dt<?> -> Dt<?>) (contravariance for type parameter at index 0 expects ? <: Dt<?>)
 TypeTests.dfy(211,10): Error: incorrect argument type for function parameter 'x' (expected ?, found set<?>)
 TypeTests.dfy(222,9): Error: assignment to array element is not allowed in this context, because this is a ghost method
-TypeTests.dfy(229,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'A' can be constructed
-TypeTests.dfy(230,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'B' can be constructed
-TypeTests.dfy(232,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Cycle' can be constructed
+TypeTests.dfy(229,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'A' can be constructed
+TypeTests.dfy(230,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'B' can be constructed
+TypeTests.dfy(232,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'Cycle' can be constructed
+TypeTests.dfy(233,7): Error: recursive constraint dependency involving a subset type: Cyc -> Cycle -> Cyc
 TypeTests.dfy(237,20): Error: using the type being defined ('A') 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(238,20): Error: using the type being defined ('B') 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(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): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'CycleW' can be constructed
+TypeTests.dfy(258,7): Error: recursive constraint dependency involving a subset type: CycW -> W -> CycleW -> CycW
+TypeTests.dfy(264,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'CycleW' can be constructed
+TypeTests.dfy(265,7): Error: recursive constraint dependency involving a subset type: CycW -> W -> CycleW -> CycW
+TypeTests.dfy(272,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'CycleW' can be constructed
+TypeTests.dfy(273,7): Error: recursive constraint dependency involving a subset type: CycW -> W -> CycleW -> CycW
+TypeTests.dfy(278,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
+TypeTests.dfy(279,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'Growing' can be constructed
+41 resolution/type errors detected in TypeTests.dfy
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2139.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2139.dfy
index 48c26d1a596..3666ff043db 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2139.dfy
+++ b/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) // warnin: cycle prevents instances (module A has the same problem, but the warning is masked by other errors there)
 }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2139.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2139.dfy.expect
index 420313f1329..356acecd947 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2139.dfy.expect
+++ b/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
+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): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'T' can be constructed
 3 resolution/type errors detected in git-issue-2139.dfy
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939a.dfy
new file mode 100644
index 00000000000..ea1d9cf37ec
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939a.dfy
@@ -0,0 +1,220 @@
+// RUN: %exits-with 4 %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(); // error: cannot prove termination
+      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) // error: cannot prove termination
+    }
+  }
+
+  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) // error: cannot prove termination
+    }
+  }
+}
+
+module SimpleExample0 {
+  trait GeneralTrait {
+  }
+
+  datatype Wrapper = Wrapper(g: GeneralTrait) // this once gave the cyclic-dependency error
+}
+
+module SimpleExample1 {
+  trait ReferenceTrait extends object {
+  }
+
+  datatype Wrapper = Wrapper(g: ReferenceTrait) // 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) // warning: empty datatype
+
+  datatype Mutual = M0(Nutual) | M1(Mutual) // warning: empty datatype
+  datatype Nutual = N0(Mutual) // warning: empty datatype
+}
+
+// The following module contains tests for some previous boxing translation errors
+module RegressionTest {
+  trait Interface { }
+
+  datatype Wrapper = Wrapper(inner: Interface)
+
+  method Test0(ww: Wrapper) {
+    var w: Wrapper;
+    w := ww as Wrapper;
+  }
+
+  method Test1(i: Interface) {
+    var w: Wrapper;
+    w := Wrapper(i) as Wrapper;
+  }
+
+  predicate P(x: int) { true }
+
+  method Test() returns (ghost h: bool)  {
+    h := forall i: int :: P(i) ==> var j: int :| true; false;
+  }
+}
+
+// The following module also contains tests for some previous boxing translation errors
+module OtherRegressionTests {
+  trait Parent extends object { }
+  class MyClass extends Parent { }
+
+  datatype Brapper = Brapper(inner: Parent)
+
+  method Testx(c: MyClass) {
+    var kw :=
+      var jj: Parent := c;
+      Brapper(jj);
+    assert true;
+  }
+
+  // ----
+
+  trait Interface { }
+
+  datatype Wrapper extends Interface = Wrapper(inner: Interface)
+
+  datatype DetectZero extends Interface  = DetectZero
+
+  function getWrappedDetectZero(): Interface {
+    var i: Interface := DetectZero;
+    var w: Wrapper := Wrapper(i);
+    w
+  }
+
+  method Test(w: Wrapper) returns (i: Interface) {
+    i := w;
+    i :=
+      var k: Wrapper := Wrapper(i);
+      k;
+    var j: Interface :=
+      var i: Interface := DetectZero;
+      var w: Wrapper := Wrapper(i);
+      w;
+  }
+
+  method SameTest() returns () {
+    var ui: Interface := DetectZero;
+    var e := Wrapper(ui);
+
+    var kw :=
+      var jj: Interface := DetectZero;
+      Wrapper(jj);
+
+    assert true;
+  }
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939a.dfy.expect
new file mode 100644
index 00000000000..bd0861ef22f
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939a.dfy.expect
@@ -0,0 +1,12 @@
+git-issue-4939a.dfy(142,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'T' can be constructed
+git-issue-4939a.dfy(144,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'Mutual' can be constructed
+git-issue-4939a.dfy(145,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nutual' can be constructed
+git-issue-4939a.dfy(25,32): Error: cannot prove termination; try supplying a decreases clause
+git-issue-4939a.dfy(68,12): Error: cannot prove termination; try supplying a decreases clause
+git-issue-4939a.dfy(68,12): Error: decreases expression must be bounded below by 0
+git-issue-4939a.dfy(67,23): Related location
+git-issue-4939a.dfy(105,27): Error: cannot prove termination; try supplying a decreases clause
+git-issue-4939a.dfy(105,27): Error: decreases expression must be bounded below by 0
+git-issue-4939a.dfy(104,23): Related location
+
+Dafny program verifier finished with 12 verified, 5 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939b.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939b.dfy
new file mode 100644
index 00000000000..28b4d43cda7
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939b.dfy
@@ -0,0 +1,31 @@
+// RUN: %exits-with 4 %verify --type-system-refresh --general-traits=datatype "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module NoAutoInit {
+  trait GeneralTrait { }
+  trait ReferenceTrait extends object { }
+
+  datatype A = A(g: GeneralTrait)
+  datatype B = B(h: ReferenceTrait)
+
+  method Test() {
+    var a: A := *;
+    var b: B := *;
+
+    if * {
+      print a, "\n"; // error: A is a possibly empty type, so "a" is subject to definite assignment
+    } else {
+      print b, "\n"; // error: B is a possibly empty type, so "b" is subject to definite assignment
+    }
+  }
+}
+
+module ProvablyEmpty {
+  datatype BadList<X> = Cons(head: X, tail: BadList<X>) // warning: no instances
+
+  lemma NeverGetHere<X>(xs: BadList<X>)
+    ensures false
+  {
+    NeverGetHere(xs.tail);
+  }
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939b.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939b.dfy.expect
new file mode 100644
index 00000000000..f38e41b4de0
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939b.dfy.expect
@@ -0,0 +1,5 @@
+git-issue-4939b.dfy(24,11): Warning: because of cyclic dependencies among constructor argument types, no instances of datatype 'BadList' can be constructed
+git-issue-4939b.dfy(16,12): Error: variable 'a', which is subject to definite-assignment rules, might be uninitialized here
+git-issue-4939b.dfy(18,12): Error: variable 'b', which is subject to definite-assignment rules, might be uninitialized here
+
+Dafny program verifier finished with 1 verified, 2 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939c.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939c.dfy
new file mode 100644
index 00000000000..815a713da73
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939c.dfy
@@ -0,0 +1,16 @@
+// RUN: %testDafnyForEachCompiler "%s" -- --general-traits=datatype
+
+module NoAutoInit {
+  trait GeneralTrait { }
+  trait ReferenceTrait extends object { }
+
+  datatype A = A(g: GeneralTrait)
+  datatype B = B(h: ReferenceTrait)
+
+  method Main() {
+    // Test that code generation succeeds, even thought "a" and "b" are never defined or used
+    var a: A := *;
+    var b: B := *;
+    print "done\n";
+  }
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939c.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939c.dfy.expect
new file mode 100644
index 00000000000..19f86f493ab
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4939c.dfy.expect
@@ -0,0 +1 @@
+done
diff --git a/docs/dev/news/4997.fix b/docs/dev/news/4997.fix
new file mode 100644
index 00000000000..9f4163953c2
--- /dev/null
+++ b/docs/dev/news/4997.fix
@@ -0,0 +1 @@
+Allow a datatype to depend on traits without being told "datatype has no instances"