fix: Fix parsing error and a crash with non-reference-trait base type

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -1273,18 +1273,22 @@ void CheckIfCompilable(RedirectingTypeDecl declWithConstraint) {
  }
 
  // Perform the stratosphere check on inductive datatypes, and compute to what extent the inductive datatypes require equality support
- foreach (var dtd in datatypeDependencies.TopologicallySortedComponents()) {
- if (datatypeDependencies.GetSCCRepresentative(dtd) == dtd) {
- // do the following check once per SCC, so call it on each SCC representative
- SccStratosphereCheck(dtd, datatypeDependencies);
- DetermineEqualitySupport(dtd, datatypeDependencies);
+ if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { // because SccStratosphereCheck depends on subset-type/newtype base types being successfully resolved
+ foreach (var dtd in datatypeDependencies.TopologicallySortedComponents()) {
+ if (datatypeDependencies.GetSCCRepresentative(dtd) == dtd) {
+ // do the following check once per SCC, so call it on each SCC representative
+ SccStratosphereCheck(dtd, datatypeDependencies);
+ DetermineEqualitySupport(dtd, datatypeDependencies);
+ }
  }
  }
 
  // Set the SccRepr field of codatatypes
- foreach (var repr in codatatypeDependencies.TopologicallySortedComponents()) {
- foreach (var codt in codatatypeDependencies.GetSCC(repr)) {
- codt.SscRepr = repr;
+ if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
+ foreach (var repr in codatatypeDependencies.TopologicallySortedComponents()) {
+ foreach (var codt in codatatypeDependencies.GetSCC(repr)) {
+ codt.SscRepr = repr;
+ }
  }
  }
 

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs

@@ -28,15 +28,15 @@ protected override void VisitOneDeclaration(TopLevelDecl decl) {
  if (decl is NewtypeDecl newtypeDecl) {
  if (newtypeDecl.Var != null) {
  if (!IsDetermined(newtypeDecl.BaseType.NormalizeExpand())) {
- resolver.ReportError(ResolutionErrors.ErrorId.r_newtype_base_undetermined, newtypeDecl.tok, "newtype's base type is not fully determined; add an explicit type for '{0}'",
- newtypeDecl.Var.Name);
+ resolver.ReportError(ResolutionErrors.ErrorId.r_newtype_base_undetermined, newtypeDecl.tok,
+ $"{newtypeDecl.WhatKind}'s base type is not fully determined; add an explicit type for bound variable '{newtypeDecl.Var.Name}'");
  }
  }
 
  } else if (decl is SubsetTypeDecl subsetTypeDecl) {
  if (!IsDetermined(subsetTypeDecl.Rhs.NormalizeExpand())) {
  resolver.ReportError(ResolutionErrors.ErrorId.r_subset_type_base_undetermined, subsetTypeDecl.tok,
- "subset type's base type is not fully determined; add an explicit type for '{0}'", subsetTypeDecl.Var.Name);
+ $"{subsetTypeDecl.WhatKind}'s base type is not fully determined; add an explicit type for bound variable '{subsetTypeDecl.Var.Name}'");
  }
 
  } else if (decl is DatatypeDecl datatypeDecl) {

Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs

@@ -55,6 +55,9 @@ public void Check(List<TopLevelDecl> declarations) {
 
  } else if (d is SubsetTypeDecl) {
  var dd = (SubsetTypeDecl)d;
+ if (!DetectUnderspecificationVisitor.IsDetermined(dd.Var.PreType)) {
+ ReportError(dd, $"{dd.WhatKind}'s base type is not fully determined; add an explicit type for bound variable '{dd.Var.Name}'");
+ }
  CheckExpression(dd.Constraint, context);
  if (dd.Witness != null) {
  CheckExpression(dd.Witness, context);
@@ -64,7 +67,7 @@ public void Check(List<TopLevelDecl> declarations) {
  var dd = (NewtypeDecl)d;
  if (dd.Var != null) {
  if (!DetectUnderspecificationVisitor.IsDetermined(dd.BasePreType)) {
- ReportError(dd, "newtype's base type is not fully determined; add an explicit type for '{0}'", dd.Var.Name);
+ ReportError(dd, $"{dd.WhatKind}'s base type is not fully determined; add an explicit type for bound variable '{dd.Var.Name}'");
  }
  CheckExpression(dd.Constraint, context);
  if (dd.Witness != null) {

Source/DafnyCore/Verifier/BoogieGenerator.Types.cs

@@ -862,6 +862,9 @@ Expression Zero(IToken tok, Type typ) {
  return null;
  } else if (typ.IsAbstractType || typ.IsInternalTypeSynonym) {
  return null;
+ } else if (typ.IsTraitType) {
+ Contract.Assert(options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy);
+ return null;
  } else {
  Contract.Assume(false); // unexpected type
  return null;

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

@@ -1,5 +1,5 @@
-// RUN: %exits-with 2 %verify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s"
+
 
 module A {
  newtype int0 = x | true // newtype's base type is not fully determined; add an explicit type for 'x'
@@ -10,3 +10,6 @@ module B {
  const x: int0 := 0 // type for constant 'x' is 'int0', but its initialization value type is 'int'
 }
 
+module C {
+ type int0 = x | true // subset type's base type is not fully determined; add an explicit type for 'x'
+}

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

@@ -1,3 +1,4 @@
-git-issue-2303.dfy(5,10): Error: newtype's base type is not fully determined; add an explicit type for 'x'
+git-issue-2303.dfy(5,10): Error: newtype's base type is not fully determined; add an explicit type for bound variable 'x'
 git-issue-2303.dfy(10,8): Error: type for constant 'x' is 'int0', but its initialization value type is 'int'
-2 resolution/type errors detected in git-issue-2303.dfy
+git-issue-2303.dfy(14,7): Error: subset type's base type is not fully determined; add an explicit type for bound variable 'x'
+3 resolution/type errors detected in git-issue-2303.dfy

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

@@ -0,0 +1,4 @@
+git-issue-2303.dfy(5,10): Error: newtype's base type is not fully determined; add an explicit type for bound variable 'x'
+git-issue-2303.dfy(10,19): Error: integer literal used as if it had type int0
+git-issue-2303.dfy(14,7): Error: subset type's base type is not fully determined; add an explicit type for bound variable 'x'
+3 resolution/type errors detected in git-issue-2303.dfy

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

@@ -0,0 +1,23 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=datatype
+
+trait ProgramTrait {
+ method Compute() returns (r: Result)
+}
+
+type Program = ProgramTrait | true // error: 'ProgramTrait' is a bound variable here, and its type is undetermined
+
+newtype NewProgram = ProgramTrait | true // error: 'ProgramTrait' is a bound variable here, and its type is undetermined
+
+datatype Result =
+ | Bounce(next: Program)
+ | NewBounce(newNext: NewProgram)
+ | Done()
+
+datatype Trivial extends ProgramTrait =
+ Trivial()
+{
+ method Compute() returns (r: Result)
+ {
+ return Done();
+ }
+}

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

@@ -0,0 +1,3 @@
+git-issue-4946a.dfy(7,5): Error: subset type's base type is not fully determined; add an explicit type for bound variable 'ProgramTrait'
+git-issue-4946a.dfy(9,8): Error: newtype's base type is not fully determined; add an explicit type for bound variable 'ProgramTrait'
+2 resolution/type errors detected in git-issue-4946a.dfy

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

@@ -0,0 +1,7 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --general-traits=legacy
+
+trait GeneralTrait { }
+trait ReferenceTrait extends object { }
+
+type SubsetType = x: GeneralTrait | true // error: cannot find witness (tried null)
+type Reference = x: ReferenceTrait | true // error: cannot find witness (tried null)

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

@@ -0,0 +1,4 @@
+git-issue-4946b.dfy(6,5): Error: trying witness null: value of expression (of type 'GeneralTrait?') is not known to be an instance of type 'GeneralTrait', because it might be null
+git-issue-4946b.dfy(7,5): Error: trying witness null: value of expression (of type 'ReferenceTrait?') is not known to be an instance of type 'ReferenceTrait', because it might be null
+
+Dafny program verifier finished with 0 verified, 2 errors

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

@@ -0,0 +1,7 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --general-traits=datatype
+
+trait GeneralTrait { }
+trait ReferenceTrait extends object { }
+
+type SubsetType = x: GeneralTrait | true // error: cannot find witness (didn't try anything)
+type Reference = x: ReferenceTrait | true // error: cannot find witness (tried null)

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

@@ -0,0 +1,4 @@
+git-issue-4946c.dfy(6,5): Error: cannot find witness that shows type is inhabited; try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
+git-issue-4946c.dfy(7,5): Error: trying witness null: value of expression (of type 'ReferenceTrait?') is not known to be an instance of type 'ReferenceTrait', because it might be null
+
+Dafny program verifier finished with 0 verified, 2 errors

docs/dev/news/4956.fix

@@ -0,0 +1,3 @@
+Fix: check that subset-type variable's type is determined (resolver refresh).
+Fix crash in verifier when there was a previous error in determining subset-type/newtype base type.
+Fix crash in verifier when a subset type has no explicit `witness` clause and has a non-reference trait as its base type.