Report error if type of a quantified variable cannot be inferred

3 files changed, 22 insertions, 2 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index cd5529fe..ddabad3d 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -508,6 +508,7 @@ ResolutionErrors.dfy(466,7): Error: RHS (of type List<A>) not assignable to LHS
 ResolutionErrors.dfy(471,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

 ResolutionErrors.dfy(485,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)

 ResolutionErrors.dfy(497,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree

+ResolutionErrors.dfy(532,18): Error: type of bound variable 'z' could not determined; please specify the type explicitly

 ResolutionErrors.dfy(396,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

@@ -577,7 +578,7 @@ ResolutionErrors.dfy(510,7): Error: let-such-that expressions are allowed only i
 ResolutionErrors.dfy(510,20): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(512,7): Error: let-such-that expressions are allowed only in ghost contexts

 ResolutionErrors.dfy(513,18): Error: unresolved identifier: w

-73 resolution/type errors detected in ResolutionErrors.dfy

+74 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 69b8ea38..6c86e7a8 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -513,3 +513,22 @@ method LetSuchThat(ghost z: int, n: nat)
   x := var w := 2*w; w;  // error: the 'w' in the RHS of the assignment is not in scope

   ghost var xg := var w :| w == 2*w; w;

 }

+

+// ------------ quantified variables whose types are not inferred ----------

+

+module NonInferredType {

+  predicate P<T>(x: T)

+

+  method NonInferredType0(x: int)

+  {

+    var t;

+    assume forall z :: P(z) && z == t;

+    assume t == x;  // this statement determined the type of z

+  }

+

+  method NonInferredType1(x: int)

+  {

+    var t;

+    assume forall z :: P(z) && z == t;  // error: the type of z is not determined

+  }

+}

diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
index 19e0645f..777be464 100644
--- a/Test/dafny2/Calculations.dfy
+++ b/Test/dafny2/Calculations.dfy
@@ -121,7 +121,7 @@ ghost method Lemma_Revacc(xs: List, ys: List)
       assert concat(revacc(xrest, Cons(x, Nil)), ys)

           == revacc(xrest, concat(Cons(x, Nil), ys));

 

-      assert forall g, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);

+      assert forall g: _T0, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);

 

       assert revacc(xrest, concat(Cons(x, Nil), ys))

           == // the assert lemma just above