3 files changed, 22 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 15cec24f..9de11371 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -640,6 +640,12 @@ Dafny program verifier finished with 7 verified, 1 error
 -------------------- Modules0.dfy --------------------
 Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
 Modules0.dfy(13,7): Error: module T named among imports does not exist
+Modules0.dfy(196,8): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(197,11): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(198,7): Error: Duplicate name of top-level declaration: WazzupA
+Modules0.dfy(201,7): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(202,8): Error: Duplicate name of top-level declaration: WazzupB
+Modules0.dfy(203,11): Error: Duplicate name of top-level declaration: WazzupB
 Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G
 Modules0.dfy(51,8): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)
 Modules0.dfy(62,9): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
@@ -651,7 +657,7 @@ Modules0.dfy(131,11): Error: fresh expressions are allowed only in specification
 Modules0.dfy(132,11): Error: allocated expressions are allowed only in specification and ghost contexts
 Modules0.dfy(148,10): Error: match source expression 'tree' has already been used as a match source expression in this context
 Modules0.dfy(187,12): Error: match source expression 'l' has already been used as a match source expression in this context
-13 resolution/type errors detected in Modules0.dfy
+19 resolution/type errors detected in Modules0.dfy
 
 -------------------- Modules1.dfy --------------------
 Modules1.dfy(52,3): Error: decreases expression must be bounded below by 0
diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 17500c97..d8bffce4 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -136,7 +136,7 @@ class A {
   }
 }
 
-class B { }
+type B;
 
 // -------------------------------
 
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index c14aece6..4eb02905 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -188,3 +188,17 @@ function NestedMatch3(tree: Tree): int
       case Nil => 0
       case Cons(h1,l1,r1) => h + h0 + h1
 }
+
+// ---------------------- more duplicates
+
+module Wazzup {
+  class WazzupA { }
+  class WazzupA { }  // error: duplicate type
+  datatype WazzupA = W_A_X;  // error: duplicate type
+  type WazzupA;  // error: duplicate type
+
+  type WazzupB;
+  type WazzupB;  // error: duplicate type
+  class WazzupB { }  // error: duplicate type
+  datatype WazzupB = W_B_X;  // error: duplicate type
+}