4 files changed, 24 insertions, 7 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 0ca8c4f8..d2ddc057 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -357,6 +357,8 @@ ResolutionErrors.dfy(606,10): Error: ghost variables are allowed only in specifi
 ResolutionErrors.dfy(615,17): Error: 'new' is not allowed in ghost contexts
 ResolutionErrors.dfy(617,20): Error: only ghost methods can be called from this context
 ResolutionErrors.dfy(619,8): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(637,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.
+ResolutionErrors.dfy(637,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.
 ResolutionErrors.dfy(427,2): Error: More than one default constructor
 ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context
 ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts
@@ -429,7 +431,7 @@ ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only i
 ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specification contexts
 ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts
 ResolutionErrors.dfy(544,18): Error: unresolved identifier: w
-89 resolution/type errors detected in ResolutionErrors.dfy
+91 resolution/type errors detected in ResolutionErrors.dfy
 
 -------------------- ParseErrors.dfy --------------------
 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -703,7 +705,7 @@ Basics.dfy(110,16): Error: assertion violation
 Execution trace:
     (0,0): anon0
     (0,0): anon10_Then
-Basics.dfy(129,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must have the same value
+Basics.dfy(129,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value
 Execution trace:
     (0,0): anon0
     (0,0): anon10_Then
@@ -712,7 +714,7 @@ Execution trace:
     (0,0): anon6
     (0,0): anon12_Then
     (0,0): anon9
-Basics.dfy(143,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value
+Basics.dfy(143,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
 Execution trace:
     (0,0): anon0
 Basics.dfy(155,19): Error: assertion violation
@@ -743,7 +745,7 @@ Execution trace:
     (0,0): anon13_Then
     (0,0): anon8
     (0,0): anon14_Then
-Basics.dfy(236,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value
+Basics.dfy(235,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
 Execution trace:
     (0,0): anon0
 
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index ccd55fa3..b451cdf1 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -207,7 +207,6 @@ method m()
 {
   var i: int, j: int;
   i, j := 3, 6;
-  i, i := 3, 3;
 }
 
 method swap(a: array<int>, i: nat, j: nat)
diff --git a/Test/dafny0/Maps.dfy b/Test/dafny0/Maps.dfy
index 1c245952..b23a3750 100644
--- a/Test/dafny0/Maps.dfy
+++ b/Test/dafny0/Maps.dfy
@@ -103,13 +103,13 @@ method m7()
 }
 method m8()
 {
-   var a := map[];
+   var a: map<int,int> := map[];
    assert forall i :: i !in a; // check emptiness
    var i,n := 0, 100;
    while(i < n)
       invariant 0 <= i <= n;
       invariant forall i | i in a :: a[i] == i * i;
-	  invariant forall k :: 0 <= k < i <==> k in a;
+      invariant forall k :: 0 <= k < i <==> k in a;
    {
       a := a[i := i * i];
       i := i + 1;
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 696a583f..60314836 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -626,3 +626,19 @@ module GhostAllocationTests {
   {
   }
 }
+
+// ------------------------- underspecified types ------------------------------
+
+module UnderspecifiedTypes {
+  method M(S: set<int>) {
+    var n, p, T0 :| 12 <= n && n in T0 && 10 <= p && p in T0 && T0 <= S && p % 2 != n % 2;
+    var T1 :| 12 in T1 && T1 <= S;
+    var T2 :| T2 <= S && 12 in T2;
+    var T3 :| 120 in T3;  // error: underspecified type
+    var T3'0: set<int> :| 120 in T3'0;
+    var T3'1: multiset<int> :| 120 in T3'1;
+    var T3'2: map<int,bool> :| 120 in T3'2;
+    var T3'3: seq<int> :| 120 in T3'3;
+    var T4 :| T4 <= S;
+  }
+}