Add tests, and adjust for ordering for checks

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

@@ -22,7 +22,6 @@ TypeTests.dfy(10,14): Error: incorrect argument type at index 1 for function par
 TypeTests.dfy(16,16): Error: incorrect argument type for method in-parameter 'x' (expected int, found bool)
 TypeTests.dfy(16,16): Error: incorrect return type at index 1 for method out-parameter 'c' (expected C, got int)
 TypeTests.dfy(17,12): Error: incorrect return type at index 1 for method out-parameter 'c' (expected C, got int)
-TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
 TypeTests.dfy(169,7): Error: non-ghost variable cannot be assigned a value that depends on a ghost
 TypeTests.dfy(179,6): Error: cannot assign to non-ghost variable in a ghost context
 TypeTests.dfy(180,9): Error: cannot assign to non-ghost variable in a ghost context
@@ -38,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
-41 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,5 +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(4,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'T' can be constructed
+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