4 files changed, 82 insertions, 3 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 589a43e2..ed69d5db 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -66,7 +66,6 @@ TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, g
 TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
 TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
 TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
-TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
 TypeTests.dfy(44,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
 TypeTests.dfy(53,6): Error: Duplicate local-variable name: z
 TypeTests.dfy(55,6): Error: Duplicate local-variable name: x
@@ -92,6 +91,7 @@ TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the
 TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type
 TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type
 TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
 34 resolution/type errors detected in TypeTests.dfy
 
 -------------------- NatTypes.dfy --------------------
@@ -1263,6 +1263,12 @@ Execution trace:
 
 Dafny program verifier finished with 32 verified, 6 errors
 
+-------------------- Coinductive.dfy --------------------
+Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
+Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
+Coinductive.dfy(51,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
+3 resolution/type errors detected in Coinductive.dfy
+
 -------------------- TypeAntecedents.dfy --------------------
 TypeAntecedents.dfy(32,13): Error: assertion violation
 Execution trace:
@@ -1848,3 +1854,6 @@ Execution trace:
     (0,0): anon11_Then
 
 Dafny program verifier finished with 19 verified, 2 errors
+
+Dafny program verifier finished with 2 verified, 0 errors
+Compiled assembly into Compilation.dll
diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy
new file mode 100644
index 00000000..fdb8c06b
--- /dev/null
+++ b/Test/dafny0/Coinductive.dfy
@@ -0,0 +1,55 @@
+// --------------------------------------------------
+
+module TestInductiveDatatypes
+{
+  // The following types test for cycles that go via instantiated type arguments
+
+  datatype Record<T> = Ctor(T);
+
+  datatype RecInt = Ctor(Record<int>);  // this is fine
+  datatype Rec_Forever = Ctor(Record<Rec_Forever>);  // error
+  datatype Rec_Stops = Cons(Record<Rec_Stops>, Rec_Stops) | Nil;  // this is okay
+
+  datatype D<T> = Ctor(E<D<T>>);  // error: illegal cycle
+  datatype E<T> = Ctor(T);
+
+  // the following is okay
+  datatype MD<T> = Ctor(ME<T>);
+  datatype ME<T> = Ctor(T);
+  method M()
+  {
+    var d: MD<MD<int>>;
+  }
+
+  datatype A = Ctor(B);  // superficially looks like a cycle, but can still be constructed
+  datatype B = Ctor(List<A>);
+  datatype List<T> = Nil | Cons(T, List);
+}
+
+// --------------------------------------------------
+
+module TestCoinductiveDatatypes
+{
+  codatatype InfList<T> = Done | Continue(T, InfList);
+
+  codatatype Stream<T> = More(T, Stream<T>);
+
+  codatatype BinaryTreeForever<T> = BNode(val: T, left: BinaryTreeForever<T>, right: BinaryTreeForever<T>);
+
+  datatype List<T> = Nil | Cons(T, List);
+
+  codatatype BestBushEver<T> = Node(value: T, branches: List<BestBushEver<T>>);
+
+  codatatype LazyRecord<T> = Lazy(contents: T);
+  class MyClass<T> { }
+  datatype GenericDt<T> = Blue | Green(T);
+  datatype GenericRecord<T> = Rec(T);
+
+  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
+
+}
+
+// --------------------------------------------------
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
new file mode 100644
index 00000000..301a4e94
--- /dev/null
+++ b/Test/dafny0/Compilation.dfy
@@ -0,0 +1,13 @@
+// The tests in this file are designed to run through the compiler.  They contain
+// program snippets that are tricky to compile or whose compilation once was buggy.
+
+datatype MyDt<T> = Nil | Cons(T, MyDt<T>);
+
+method M<U>(x: MyDt<int>)
+{
+  match (x) {
+    case Cons(head, tail) =>
+      var y: int := head;
+    case Nil =>
+  }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 608b7358..f9cd5a89 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -17,8 +17,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             ModulesCycle.dfy Modules0.dfy Modules1.dfy BadFunction.dfy
             Comprehensions.dfy Basics.dfy ControlStructures.dfy
             Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy
-            TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy NoTypeArgs.dfy
-            SplitExpr.dfy
+            TypeParameters.dfy Datatypes.dfy Coinductive.dfy
+            TypeAntecedents.dfy NoTypeArgs.dfy SplitExpr.dfy
             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
@@ -34,3 +34,5 @@ for %%f in (SmallTests.dfy LetExpr.dfy) do (
   %DAFNY_EXE% /compile:0 /dprint:out.tmp.dfy %* %%f
   %DAFNY_EXE% /compile:0 %* out.tmp.dfy
 )
+
+%DAFNY_EXE% %* Compilation.dfy