1 files changed, 14 insertions, 4 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 520b2e38..9f6c948a 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1007,20 +1007,20 @@ module CycleError2 {
   type A = B  // error: cycle: A -> B -> A
   type B = set<A>
 }
-module Good0 {
+module CycleErrors3 {
   type A = (B, D<bool>)
   type B = C
   class C {
     var a: A;  // this is fine
   }
-  datatype D<X> = Make(A, B, C)  // this is fine, too
+  datatype D<X> = Make(A, B, C)  // error: cannot construct a D<X>
 }
-module CycleError3 {
+module CycleError4 {
   type A = B  // error: cycle: A -> B -> A
   type B = C<A>
   class C<T> { }
 }
-module CycleError4 {
+module CycleError5 {
   type A = B  // error: cycle: A -> B -> A
   type B = Dt<A>
   datatype Dt<T> = Make(T)
@@ -1090,3 +1090,13 @@ module OpaqueTypes1 {
     assert p != q;  // error: types must be the same in order to do compare
   }
 }
+
+// ----- new trait -------------------------------------------
+
+
+trait J { }
+type JJ = J
+method TraitSynonym()
+{
+  var x := new JJ;  // error: new cannot be applied to a trait
+}