2 files changed, 82 insertions, 7 deletions
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 141e48cb..01c2a0a5 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -114,6 +114,55 @@ method K() {
   var d: MutuallyRecursiveDataType<nat>;  // error: not allowed to instantiate with 'nat'
   var a := new nat[100];  // error: not allowed the type array<nat>
   var b := new nat[100,200];  // error: not allowed the type array2<nat>
+
+  // constructors
+  var ci0 := new Expl_Class.Init<nat>(0, 0);  // error: subrange not allowed here
+  var ci1 := new Expl_Class<nat>;  // error
+  var ci2 := new Expl_Class<nat>.Init(0, 0);  // error
+
+  // collection types (sets are above) and array types
+  var m0: multiset<nat>;  // error
+  var m1: seq<nat>;  // error
+  var m2: map<nat,int>;  // error
+  var m3: map<int,nat>;  // error
+  var n: seq<MutuallyRecursiveDataType<nat>>;  // error
+  var o: array<nat>;  // error
+  var o': array2<nat>;  // error
+
+  // tuple types
+  var tu0: (nat);  // no problem, this just means 'nat'
+  var tu1: (nat,int);  // error
+  var tu2: (int,nat);  // error
+
+  // function types
+  var fn: nat -> int;  // error
+  var gn: int -> nat;  // error
+  var hn: (int,nat) -> int;  // error
+
+  // the following tests test NameSegment and ExprDotName in types:
+  var k: Expl_Class<nat>;  // error
+  var k': Expl_Module.E<nat>;  // error
+
+  // the following tests test NameSegment and ExprDotName in expressions:
+  var e0 := Expl_M<nat>(0);  // error
+  var e1 := Expl_F<nat>(0);  // error
+  var ec := new Expl_Class<int>;
+  ec.Init<nat>(0, 0);  // error
+  Expl_Class.DoIt<nat>(0, 0);  // error
+  Expl_Class<nat>.DoIt(0, 0);  // error
+  Expl_Module.E.N<nat>(0, 0);  // error
+  Expl_Module.E<nat>.N(0, 0);  // error
+}
+method Expl_M<T>(x: T) returns (y: T)
+function method Expl_F<T>(x: T): T
+class Expl_Class<T> {
+  method Init<U>(t: T, u: U)
+  static method DoIt<U>(t: T, u: U)
+}
+module Expl_Module {
+  class E<T> {
+    static method N<U>(t: T, u: U)
+  }
 }
 
 // --------------------- more ghost tests, for assign-such-that statements
diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect
index e40f2c35..500b1af9 100644
--- a/Test/dafny0/TypeTests.dfy.expect
+++ b/Test/dafny0/TypeTests.dfy.expect
@@ -1,6 +1,6 @@
-TypeTests.dfy(156,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
-TypeTests.dfy(162,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
-TypeTests.dfy(169,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
+TypeTests.dfy(205,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
+TypeTests.dfy(211,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
+TypeTests.dfy(218,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
 TypeTests.dfy(7,17): Error: type mismatch for argument 0 (function expects C, got D)
 TypeTests.dfy(7,20): Error: type mismatch for argument 1 (function expects D, got C)
 TypeTests.dfy(8,15): Error: type mismatch for argument 0 (function expects C, got int)
@@ -30,8 +30,34 @@ TypeTests.dfy(113,6): Error: sorry, cannot instantiate collection type with a su
 TypeTests.dfy(114,9): Error: sorry, cannot instantiate type parameter with a subrange type
 TypeTests.dfy(115,8): Error: sorry, cannot instantiate type parameter with a subrange type
 TypeTests.dfy(116,8): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(128,15): Error: ghost variables are allowed only in specification contexts
-TypeTests.dfy(138,4): Error: cannot assign to non-ghost variable in a ghost context
-TypeTests.dfy(139,7): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(119,28): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(119,28): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(120,17): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(120,10): Error: new can be applied only to reference types (got Expl_Class<nat>)
+TypeTests.dfy(121,17): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(124,6): Error: sorry, cannot instantiate collection type with a subrange type
+TypeTests.dfy(125,6): Error: sorry, cannot instantiate collection type with a subrange type
+TypeTests.dfy(126,6): Error: sorry, cannot instantiate collection type with a subrange type
+TypeTests.dfy(127,6): Error: sorry, cannot instantiate collection type with a subrange type
+TypeTests.dfy(128,13): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(129,9): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(130,10): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(134,11): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(135,11): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(138,14): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(139,14): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(140,20): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(143,9): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(144,22): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(147,12): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(148,12): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(150,5): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(151,13): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(152,2): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(153,16): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(154,14): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(177,15): Error: ghost variables are allowed only in specification contexts
+TypeTests.dfy(187,4): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(188,7): Error: cannot assign to non-ghost variable in a ghost context
 TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
-36 resolution/type errors detected in TypeTests.dfy
+62 resolution/type errors detected in TypeTests.dfy