Recursive constraint dep

Source/DafnyCore/AST/Expressions/Heap/WildcardExpr.cs

@@ -7,6 +7,7 @@ public class WildcardExpr : Expression, ICloneable<WildcardExpr> {  // a Wildcar
   public WildcardExpr(Cloner cloner, WildcardExpr original) : base(cloner, original) {
   }
 
+  [SyntaxConstructor]
   public WildcardExpr(IOrigin origin)
     : base(origin) {
     Contract.Requires(origin != null);

Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs

@@ -1,3 +1,4 @@
+#nullable enable
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using Microsoft.Dafny.Auditor;
@@ -12,7 +13,8 @@ public AssumeStmt Clone(Cloner cloner) {
   public AssumeStmt(Cloner cloner, AssumeStmt original) : base(cloner, original) {
   }
 
-  public AssumeStmt(IOrigin origin, Expression expr, Attributes attributes)
+  [SyntaxConstructor]
+  public AssumeStmt(IOrigin origin, Expression expr, Attributes? attributes)
     : base(origin, expr, attributes) {
     Contract.Requires(origin != null);
     Contract.Requires(expr != null);
@@ -43,7 +45,7 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext co
 
   public override void ResolveGhostness(ModuleResolver resolver, ErrorReporter reporter, bool mustBeErasable,
     ICodeContext codeContext,
-    string proofContext, bool allowAssumptionVariables, bool inConstructorInitializationPhase) {
+    string? proofContext, bool allowAssumptionVariables, bool inConstructorInitializationPhase) {
     IsGhost = true;
   }
 }

Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs

@@ -306,6 +306,22 @@ public CharLiteralExpr ReadCharLiteralExprOption()
             return ReadCharLiteralExpr();
         }
 
+        public WildcardExpr ReadWildcardExpr()
+        {
+            var parameter0 = ReadAbstract<IOrigin>();
+            return new WildcardExpr(parameter0);
+        }
+
+        public WildcardExpr ReadWildcardExprOption()
+        {
+            if (ReadIsNull())
+            {
+                return default;
+            }
+
+            return ReadWildcardExpr();
+        }
+
         public UnchangedExpr ReadUnchangedExpr()
         {
             var parameter0 = ReadAbstract<IOrigin>();
@@ -587,6 +603,24 @@ public ExpectStmt ReadExpectStmtOption()
             return ReadExpectStmt();
         }
 
+        public AssumeStmt ReadAssumeStmt()
+        {
+            var parameter0 = ReadAbstract<IOrigin>();
+            var parameter2 = ReadAttributesOption();
+            var parameter1 = ReadAbstract<Expression>();
+            return new AssumeStmt(parameter0, parameter1, parameter2);
+        }
+
+        public AssumeStmt ReadAssumeStmtOption()
+        {
+            if (ReadIsNull())
+            {
+                return default;
+            }
+
+            return ReadAssumeStmt();
+        }
+
         public AssertStmt ReadAssertStmt()
         {
             var parameter0 = ReadAbstract<IOrigin>();
@@ -2319,6 +2353,11 @@ private object ReadObject(System.Type actualType)
                 return ReadCharLiteralExpr();
             }
 
+            if (actualType == typeof(WildcardExpr))
+            {
+                return ReadWildcardExpr();
+            }
+
             if (actualType == typeof(UnchangedExpr))
             {
                 return ReadUnchangedExpr();
@@ -2394,6 +2433,11 @@ private object ReadObject(System.Type actualType)
                 return ReadExpectStmt();
             }
 
+            if (actualType == typeof(AssumeStmt))
+            {
+                return ReadAssumeStmt();
+            }
+
             if (actualType == typeof(AssertStmt))
             {
                 return ReadAssertStmt();

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -1696,7 +1696,8 @@ private void ComputeGhostInterestAndMisc(List<TopLevelDecl> declarations) {
 
     private void CheckForCyclesAmongRedirectingTypes(RedirectingTypeDecl dd, HashSet<ICallable> cycleErrorHasBeenReported) {
       var enclosingModule = dd.EnclosingModule;
-      if (enclosingModule.CallGraph.GetSCCSize(dd) != 1) {
+      if (enclosingModule.CallGraph.GetSCCSize(dd) != 1 ||
+          enclosingModule.CallGraph.FindVertex(dd).Successors.Any(v => v.N == dd)) {
         var r = enclosingModule.CallGraph.GetSCCRepresentative(dd);
         if (cycleErrorHasBeenReported.Contains(r)) {
           // An error has already been reported for this cycle, so don't report another.

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -4222,15 +4222,14 @@ public ResolveTypeReturn ResolveTypeLenient(IOrigin tok, Type type, ResolutionCo
               t.ResolvedClass = d;  // Store the decl, so the compiler will generate the fully qualified name
             } else if (d is RedirectingTypeDecl) {
               var dd = (RedirectingTypeDecl)d;
-              var caller = CodeContextWrapper.Unwrap(resolutionContext.CodeContext) as ICallable;
-              if (caller != null && !(d is SubsetTypeDecl && caller is SpecialFunction)) {
-                if (caller != d) {
-                } else if (d is TypeSynonymDecl && !(d is SubsetTypeDecl)) {
-                  // detect self-loops here, since they don't show up in the graph's SCC methods
-                  reporter.Error(MessageSource.Resolver, d.Origin, "type-synonym cycle: {0} -> {0}", d.Name);
-                } else {
-                  // detect self-loops here, since they don't show up in the graph's SCC methods
-                  reporter.Error(MessageSource.Resolver, d.Origin, "recursive constraint dependency involving a {0}: {1} -> {1}", d.WhatKind, d.Name);
+              var parent = CodeContextWrapper.Unwrap(resolutionContext.CodeContext) as ICallable;
+              if (parent != null && !(d is SubsetTypeDecl && parent is SpecialFunction)) {
+                var cycleFound = parent == d;
+                if (cycleFound) {
+                  if (d is TypeSynonymDecl && !(d is SubsetTypeDecl)) {
+                    // detect self-loops here, since they don't show up in the graph's SCC methods
+                    reporter.Error(MessageSource.Resolver, d.Origin, "type-synonym cycle: {0} -> {0}", d.Name);
+                  }
                 }
               }
               t.ResolvedClass = d;

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy

@@ -0,0 +1,11 @@
+// RUN: ! %testDafnyForEachResolver "%s" -- --allow-axioms=false
+
+type Even = x: int | x % 2 == 0
+opaque const ten: Even := 10
+
+const twoHundred: LessThanTwoHundred := 200
+type LessThanTwoHundred = k | 0 <= k < twoHundred
+
+const twoHundred_2: LessThanHundredNinetyNine := 200
+const hundredNinetyNine: int := twoHundred_2 as int - 1
+type LessThanHundredNinetyNine = k | 0 <= k < hundredNinetyNine

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy.expect

@@ -0,0 +1,3 @@
+constResolution.dfy(7,5): Error: recursive constraint dependency involving a subset type: LessThanTwoHundred -> twoHundred -> LessThanTwoHundred
+constResolution.dfy(11,5): Error: recursive constraint dependency involving a subset type: LessThanHundredNinetyNine -> hundredNinetyNine -> twoHundred_2 -> LessThanHundredNinetyNine
+2 resolution/type errors detected in constResolution.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy

@@ -0,0 +1,9 @@
+// RUN: ! %verify --type-system-refresh --general-traits=datatype %s &> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Stmt =
+  | Skip
+  | Block(stmts: seq<Stmt>)
+  | If(b: bool, thn: BlockStmt, els: BlockStmt)
+
+type BlockStmt = s: Stmt | s.Block? witness Block([])

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy.expect

@@ -0,0 +1,2 @@
+cycles.dfy(9,5): Error: recursive constraint dependency involving a subset type: BlockStmt -> Stmt -> BlockStmt
+1 resolution/type errors detected in cycles.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy

@@ -0,0 +1,8 @@
+// RUN: %verify --type-system-refresh --general-traits=datatype %s &> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait SelfConstraintDep<T extends SelfConstraintDep<T>> {}
+trait SelfConstraintDep2<T extends SelfConstraintDep2<T>> extends object {}
+
+datatype D extends SelfConstraintDep<D> = D {}
+class C extends SelfConstraintDep2<C> {}

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 0 verified, 0 errors

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

@@ -191,11 +191,13 @@ GeneralNewtypeResolution.dfy(927,4): Error: type parameter 'ZZ' is not allowed t
 GeneralNewtypeResolution.dfy(932,5): Error: type parameter 'A' is not allowed to change variance (here, from '+' to '-')
 GeneralNewtypeResolution.dfy(933,5): Error: type parameter 'B' is not allowed to change variance (here, from '=' to '+')
 GeneralNewtypeResolution.dfy(934,4): Error: type parameter 'C' is not allowed to change variance (here, from '-' to '=')
-GeneralNewtypeResolution.dfy(940,10): Error: recursive constraint dependency involving a newtype: A -> A
-GeneralNewtypeResolution.dfy(945,10): Error: recursive constraint dependency involving a newtype: A -> A
+GeneralNewtypeResolution.dfy(939,10): Error: a newtype ('W') must be based on some numeric type (got X)
+GeneralNewtypeResolution.dfy(940,10): Error: Cyclic dependency among declarations: A -> A
+GeneralNewtypeResolution.dfy(944,10): Error: a newtype ('W') must be based on some numeric type (got X)
+GeneralNewtypeResolution.dfy(945,10): Error: Cyclic dependency among declarations: A -> A
 GeneralNewtypeResolution.dfy(950,7): Error: type-synonym cycle: A -> A
-GeneralNewtypeResolution.dfy(955,10): Error: recursive constraint dependency involving a newtype: A -> A
-197 resolution/type errors detected in GeneralNewtypeResolution.dfy
+GeneralNewtypeResolution.dfy(955,10): Error: Cyclic dependency among declarations: A -> A
+199 resolution/type errors detected in GeneralNewtypeResolution.dfy
 GeneralNewtypeResolution.dfy(34,10): Error: a newtype ('MyOrdinal') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got ORDINAL)
 GeneralNewtypeResolution.dfy(40,10): Error: a newtype ('MyObject') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got object)
 GeneralNewtypeResolution.dfy(41,10): Error: a newtype ('MyTrait') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got Trait)
@@ -355,8 +357,8 @@ GeneralNewtypeResolution.dfy(927,4): Error: type parameter 'ZZ' is not allowed t
 GeneralNewtypeResolution.dfy(932,5): Error: type parameter 'A' is not allowed to change variance (here, from '+' to '-')
 GeneralNewtypeResolution.dfy(933,5): Error: type parameter 'B' is not allowed to change variance (here, from '=' to '+')
 GeneralNewtypeResolution.dfy(934,4): Error: type parameter 'C' is not allowed to change variance (here, from '-' to '=')
-GeneralNewtypeResolution.dfy(940,10): Error: recursive constraint dependency involving a newtype: A -> A
-GeneralNewtypeResolution.dfy(945,10): Error: recursive constraint dependency involving a newtype: A -> A
+GeneralNewtypeResolution.dfy(940,10): Error: Cyclic dependency among declarations: A -> A
+GeneralNewtypeResolution.dfy(945,10): Error: Cyclic dependency among declarations: A -> A
 GeneralNewtypeResolution.dfy(950,7): Error: type-synonym cycle: A -> A
-GeneralNewtypeResolution.dfy(955,10): Error: recursive constraint dependency involving a newtype: A -> A
+GeneralNewtypeResolution.dfy(955,10): Error: Cyclic dependency among declarations: A -> A
 162 resolution/type errors detected in GeneralNewtypeResolution.dfy

Source/Scripts/Syntax.cs-schema

@@ -184,6 +184,10 @@ class CharLiteralExpr : LiteralExpr
 {
 }
 
+class WildcardExpr : Expression
+{
+}
+
 class UnchangedExpr : Expression
 {
     List<FrameExpression> frame;
@@ -313,6 +317,10 @@ class ExpectStmt : PredicateStmt
     Expression? message;
 }
 
+class AssumeStmt : PredicateStmt
+{
+}
+
 class AssertStmt : PredicateStmt
 {
     AssertLabel? label;