Type parameters in method/function signatures are no longer auto-declared. Although

convenient and concise, the auto-declare behavior has on many occasions caused
confusion when a type name has accidentally been mistyped (and Dafny had then
accepted and auto-declared the name).
Note, the behavior of filling in missing type parameters is still supported.  This
mode, although unusual (even original?) in languages, is different from the auto-
declare behavior.  For auto-declare, identifiers could be used in the program
without having a declaration.  For fill-in parameters, the implicitly declared
type parameters remain anonymous.

18 files changed, 166 insertions, 152 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 29e36ccd..7c78c1e2 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -8469,12 +8469,6 @@ namespace Microsoft.Dafny
           r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);

         }

 #endif

-      } else if (option.Opt == ResolveTypeOptionEnum.AllowPrefixExtend && expr.OptTypeArguments == null) {

-        // it woulc plausibly be a type parameter, but isn't; we will declare it automatically

-        tp = new TypeParameter(expr.tok, expr.Name, defaultTypeArguments.Count, option.Parent);

-        defaultTypeArguments.Add(tp);

-        r = new Resolver_IdentifierExpr(expr.tok, tp);

-        allTypeParameters.Push(expr.Name, tp);

       } else {

         // ----- None of the above

         Error(expr.tok, "Undeclared top-level type or type parameter: {0} (did you forget to qualify a name?)", expr.Name);

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index c8fa76c8..89b0f02a 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -100,7 +100,7 @@ method ExpliesAssociativityM(A: bool, B: bool, C: bool) {
   }

 }

 

-method ExpliesShortCircuiting(a: array<T>)

+method ExpliesShortCircuiting(a: array)

 {

   assert a == null || 0 <= a.Length;  // (W)

   assert a != null ==> 0 <= a.Length;  // (X) -- same as (W)

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index 34aba3de..dbbffd87 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -71,16 +71,17 @@ module X1 {
 }

 

 module X2 {

+  import opened X1

   class MyClass2 {

-    method Down(x1: MyClass1, x0: MyClass0) {

+    method Down(x1: MyClass1, x0: X0'.MyClass0) {

       x1.Down(x0);

     }

-    method WayDown(x0: MyClass0) {

+    method WayDown(x0: X0'.MyClass0) {

       x0.Down();

     }

     method Up() {

     }

-    method Somewhere(y: MyClassY) {

+    method Somewhere(y: MyClassY) {  // error: no such type in scope

       y.M();

     }

   }

@@ -97,8 +98,7 @@ module YY {
 class ClassG {

   method T() { }

   function method TFunc(): int { 10 }

-  method V(y: MyClassY) {  // Note, MyClassY is in scope, since we are in the _default

-                           // module, which imports everything

+  method V(y: MyClassY) {

     y.M();

   }

 }

@@ -141,10 +141,10 @@ class AClassWithSomeField {
     SomeField := SomeField + 4;

     var a := old(SomeField);  // error: old can only be used in ghost contexts

     var b := fresh(this);  // error: fresh can only be used in ghost contexts

-    var c := allocated(this);  // error: allocated can only be used in ghost contexts

+//    var c := allocated(this);  // error: allocated can only be used in ghost contexts

     if (fresh(this)) {  // this guard makes the if statement a ghost statement

       ghost var x := old(SomeField);  // this is a ghost context, so it's okay

-      ghost var y := allocated(this);  // this is a ghost context, so it's okay

+//      ghost var y := allocated(this);  // this is a ghost context, so it's okay

     }

   }

 }

diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect
index 5d11f9c9..d2f0bcc8 100644
--- a/Test/dafny0/Modules0.dfy.expect
+++ b/Test/dafny0/Modules0.dfy.expect
@@ -9,13 +9,8 @@ Modules0.dfy(15,11): Error: Duplicate name of top-level declaration: WazzupB
 Modules0.dfy(56,21): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?)

 Modules0.dfy(57,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

 Modules0.dfy(68,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)

-Modules0.dfy(76,9): Error: type MyClass1 does not have a member Down

-Modules0.dfy(76,13): Error: expected method call, found expression

-Modules0.dfy(79,9): Error: type MyClass0 does not have a member Down

-Modules0.dfy(79,13): Error: expected method call, found expression

-Modules0.dfy(84,8): Error: type MyClassY does not have a member M

-Modules0.dfy(84,9): Error: expected method call, found expression

-Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)

+Modules0.dfy(84,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)

+Modules0.dfy(93,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)

 Modules0.dfy(226,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

 Modules0.dfy(226,8): Error: new can be applied only to reference types (got X)

 Modules0.dfy(235,13): Error: module 'B' does not declare a type 'X'

@@ -35,11 +30,5 @@ Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup
 Modules0.dfy(321,17): Error: module 'Q_Imp' does not declare a type 'Edon'

 Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)

 Modules0.dfy(324,30): Error: member Create does not exist in class Klassy

-Modules0.dfy(102,6): Error: type MyClassY does not have a member M

-Modules0.dfy(102,7): Error: expected method call, found expression

-Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts

-Modules0.dfy(142,13): Error: old expressions are allowed only in specification and ghost contexts

-Modules0.dfy(143,13): Error: fresh expressions are allowed only in specification and ghost contexts

-Modules0.dfy(144,13): Error: unresolved identifier: allocated

-Modules0.dfy(147,21): Error: unresolved identifier: allocated

-42 resolution/type errors detected in Modules0.dfy

+Modules0.dfy(101,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)

+31 resolution/type errors detected in Modules0.dfy

diff --git a/Test/dafny0/NestedMatch.dfy b/Test/dafny0/NestedMatch.dfy
index e6e7c489..81319b4a 100644
--- a/Test/dafny0/NestedMatch.dfy
+++ b/Test/dafny0/NestedMatch.dfy
@@ -28,7 +28,7 @@ function last<T>(xs: List<T>): T
   case Cons(y, Cons(z, zs)) => last(Cons(z, zs))

 }

 

-method checkLast(y: T) {

+method checkLast<T>(y: T) {

   assert last(Cons(y, Nil)) == y;

   assert last(Cons(y, Cons(y, Nil))) == last(Cons(y, Nil));

 }

diff --git a/Test/dafny0/NestedPatterns.dfy b/Test/dafny0/NestedPatterns.dfy
index ef597936..d1d88b2a 100644
--- a/Test/dafny0/NestedPatterns.dfy
+++ b/Test/dafny0/NestedPatterns.dfy
@@ -69,7 +69,7 @@ method MethodG<T>(xs: List<T>) returns (xxs: List<List<T>>)
   case Cons(h, Cons(ht, tt)) => 

 }

 

-method AssertionFailure(xs: List<T>)

+method AssertionFailure(xs: List)

 {

   match xs

   case (Nil) =>  // BUG: this line causes an assertion in the Dafny implementation (what should happen is that "(Nil)" should not be allowed here)

@@ -100,7 +100,7 @@ method DuplicateIdentifierInPattern2<T>(xs: List<T>)
   case Cons(h, Cons(e, e)) =>  // BUG:  here, the duplicate identifier is detected, but the error message is shown 3 times, which is less than ideal

 }

 

-method Tuples0(xs: List<T>, ys: List<T>)

+method Tuples0(xs: List, ys: List)

 {

   match (xs, ys)

   case (Nil, Nil) =>

@@ -110,14 +110,14 @@ method Tuples0(xs: List<T>, ys: List<T>)
                                     // only the identifiers in the last constructors are

 }

 

-method Tuples1(xs: List<T>, ys: List<T>)

+method Tuples1(xs: List, ys: List)

 {

   match (xs, ys, 4)

   case (Nil, Nil) =>  // BUG: the mismatch of 3 versus 2 arguments in the previous line and this line causes Dafny to crash with an

                       // assertion failure "mc.CasePatterns.Count == e.Arguments.Count"

 }

 

-method Tuples2(xs: List<T>, ys: List<T>)

+method Tuples2(xs: List, ys: List)

 {

   match (xs, ys, ())

   case (Nil, Nil, ()) =>  // BUG: Dafny crashes with an assertion failure "e.Arguments.Count >= 1"

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 761cffa0..8c910959 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1253,14 +1253,14 @@ module SignatureCompletion {
   datatype Dt = Ctor(X -> Dt)  // error: X is not a declared type

   datatype Et<Y> = Ctor(X -> Et, Y)  // error: X is not a declared type

 

-  // For methods and functions, signatures can auto-declare type parameters

-  method My0(s: set, x: A -> B)

-  method My1(x: A -> B, s: set)

+

+  method My0<A,B>(s: set, x: A -> B)

+  method My1<A,B>(x: A -> B, s: set)

   method My2<A,B>(s: set, x: A -> B)

   method My3<A,B>(x: A -> B, s: set)

 

-  function F0(s: set, x: A -> B): int

-  function F1(x: A -> B, s: set): int

+  function F0<A,B>(s: set, x: A -> B): int

+  function F1<A,B>(x: A -> B, s: set): int

   function F2<A,B>(s: set, x: A -> B): int

   function F3<A,B>(x: A -> B, s: set): int

 }

diff --git a/Test/hofs/Examples.dfy b/Test/hofs/Examples.dfy
index be2672f5..306d278d 100644
--- a/Test/hofs/Examples.dfy
+++ b/Test/hofs/Examples.dfy
@@ -1,14 +1,14 @@
 // RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-function Apply(f: A -> B, x: A): B
+function Apply<A,B>(f: A -> B, x: A): B
   reads f.reads(x);
   requires f.requires(x);
 {
   f(x)
 }
 
-function Apply'(f: A -> B) : A -> B
+function Apply'<A,B>(f: A -> B) : A -> B
 {
   x reads f.reads(x)
     requires f.requires(x)
@@ -16,7 +16,7 @@ function Apply'(f: A -> B) : A -> B
 }
 
 
-function Compose(f: B -> C, g:A -> B): A -> C
+function Compose<A,B,C>(f: B -> C, g:A -> B): A -> C
 {
   x reads g.reads(x)
     reads if g.requires(x) then f.reads(g(x)) else {}
@@ -25,21 +25,21 @@ function Compose(f: B -> C, g:A -> B): A -> C
     => f(g(x))
 }
 
-function W(f : (A,A) -> A): A -> A
+function W<A>(f : (A,A) -> A): A -> A
 {
   x requires f.requires(x,x)
     reads f.reads(x,x)
     => f(x,x)
 }
 
-function Curry(f : (A,B) -> C) : A -> B -> C
+function Curry<A,B,C>(f : (A,B) -> C) : A -> B -> C
 {
   x => y requires f.requires(x,y)
          reads f.reads(x,y)
          => f(x,y)
 }
 
-function Uncurry(f : A -> B -> C) : (A,B) -> C
+function Uncurry<A,B,C>(f : A -> B -> C) : (A,B) -> C
 {
   (x,y) requires f.requires(x)
         requires f(x).requires(y)
@@ -48,7 +48,7 @@ function Uncurry(f : A -> B -> C) : (A,B) -> C
         => f(x)(y)
 }
 
-function S(f : (A,B) -> C, g : A -> B): A -> C
+function S<A,B,C>(f : (A,B) -> C, g : A -> B): A -> C
 {
   x requires g.requires(x)
     requires f.requires(x,g(x))
diff --git a/Test/hofs/Fold.dfy b/Test/hofs/Fold.dfy
index 6ca2d3b1..9bcd9e02 100644
--- a/Test/hofs/Fold.dfy
+++ b/Test/hofs/Fold.dfy
@@ -13,7 +13,7 @@ function method Eval(e : Expr): int
     case Lit(i)  => i
 }
 
-function method Fold(xs : List<A>, unit : B, f : (A,B) -> B): B
+function method Fold<A,B>(xs : List<A>, unit : B, f : (A,B) -> B): B
   reads f.reads;
   requires forall x, y :: x < xs ==> f.requires(x,y);
 {
diff --git a/Test/hofs/Monads.dfy b/Test/hofs/Monads.dfy
index 3598d2b3..633dd339 100644
--- a/Test/hofs/Monads.dfy
+++ b/Test/hofs/Monads.dfy
@@ -4,29 +4,29 @@
 abstract module Monad {
   type M<A>
 
-  function method Return(x: A): M<A>
-  function method Bind(m: M<A>, f:A -> M<B>):M<B>
-    reads f.reads;
-    requires forall a :: f.requires(a);
+  function method Return<A>(x: A): M<A>
+  function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B>
+    reads f.reads
+    requires forall a :: f.requires(a)
 
   // return x >>= f = f x
-  lemma LeftIdentity(x : A, f : A -> M<B>)
-    requires forall a :: f.requires(a);
-    ensures Bind(Return(x),f) == f(x);
+  lemma LeftIdentity<A,B>(x : A, f : A -> M<B>)
+    requires forall a :: f.requires(a)
+    ensures Bind(Return(x),f) == f(x)
 
   // m >>= return = m
-  lemma RightIdentity(m : M<A>)
-    ensures Bind(m,Return) == m;
+  lemma RightIdentity<A>(m : M<A>)
+    ensures Bind(m,Return) == m
 
   // (m >>= f) >>= g = m >>= (x => f(x) >>= g)
-  lemma Associativity(m : M<A>, f:A -> M<B>, g: B -> M<C>)
-    requires forall a :: f.requires(a);
-    requires forall b :: g.requires(b);
+  lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>)
+    requires forall a :: f.requires(a)
+    requires forall b :: g.requires(b)
 	ensures Bind(Bind(m,f),g) ==
 	        Bind(m,x reads f.reads(x)
 	                 reads g.reads
 					 requires f.requires(x)
-					 requires forall b :: g.requires(b) => Bind(f(x),g));
+					 requires forall b :: g.requires(b) => Bind(f(x),g))
 }
 
 module Identity refines Monad {
@@ -101,21 +101,21 @@ module List refines Monad {
   function method Return<A>(x: A): M<A>
   { Cons(x,Nil) }
 
-  function method Concat(xs: M<A>, ys: M<A>): M<A>
+  function method Concat<A>(xs: M<A>, ys: M<A>): M<A>
   {
     match xs
 	  case Nil => ys
 	  case Cons(x,xs) => Cons(x,Concat(xs,ys))
   }
 
-  function method Join(xss: M<M<A>>) : M<A>
+  function method Join<A>(xss: M<M<A>>) : M<A>
   {
     match xss
 	  case Nil => Nil
 	  case Cons(xs,xss) => Concat(xs,Join(xss))
   }
 
-  function method Map(xs: M<A>, f: A -> B):M<B>
+  function method Map<A,B>(xs: M<A>, f: A -> B):M<B>
     reads f.reads;
 	requires forall a :: f.requires(a);
   {
@@ -170,7 +170,7 @@ module List refines Monad {
     ensures Concat(Concat(xs,ys),zs) == Concat(xs,Concat(ys,zs));
   {}
 
-  lemma BindMorphism(xs : M<A>, ys: M<A>, f : A -> M<B>)
+  lemma BindMorphism<A,B>(xs : M<A>, ys: M<A>, f : A -> M<B>)
     requires forall a :: f.requires(a);
 	ensures Bind(Concat(xs,ys),f) == Concat(Bind(xs,f),Bind(ys,f));
   {
diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy
index e11473bd..a6f8d922 100644
--- a/Test/hofs/ReadsReads.dfy
+++ b/Test/hofs/ReadsReads.dfy
@@ -2,58 +2,58 @@
 // RUN: %diff "%s.expect" "%t"
 
 module ReadsRequiresReads {
-  function MyReadsOk(f : A -> B, a : A) : set<object>
-    reads f.reads(a);
+  function MyReadsOk<A,B>(f : A -> B, a : A) : set<object>
+    reads f.reads(a)
   {
     f.reads(a)
   }
 
-  function MyReadsOk2(f : A -> B, a : A) : set<object>
-    reads f.reads(a);
+  function MyReadsOk2<A,B>(f : A -> B, a : A) : set<object>
+    reads f.reads(a)
   {
     (f.reads)(a)
   }
 
-  function MyReadsOk3(f : A -> B, a : A) : set<object>
-    reads (f.reads)(a);
+  function MyReadsOk3<A,B>(f : A -> B, a : A) : set<object>
+    reads (f.reads)(a)
   {
     f.reads(a)
   }
 
-  function MyReadsOk4(f : A -> B, a : A) : set<object>
-    reads (f.reads)(a);
+  function MyReadsOk4<A,B>(f : A -> B, a : A) : set<object>
+    reads (f.reads)(a)
   {
     (f.reads)(a)
   }
 
-  function MyReadsBad(f : A -> B, a : A) : set<object>
+  function MyReadsBad<A,B>(f : A -> B, a : A) : set<object>
   {
     f.reads(a)  // error: MyReadsBad does not have permission to read what f.reads(a) reads
   }
 
-  function MyReadsBad2(f : A -> B, a : A) : set<object>
+  function MyReadsBad2<A,B>(f : A -> B, a : A) : set<object>
   {
     (f.reads)(a)  // error: MyReadsBad2 does not have permission to read what f.reads(a) reads
   }
 
-  function MyReadsOk'(f : A -> B, a : A, o : object) : bool
-    reads f.reads(a);
+  function MyReadsOk'<A,B>(f : A -> B, a : A, o : object) : bool
+    reads f.reads(a)
   {
     o in f.reads(a)
   }
 
-  function MyReadsBad'(f : A -> B, a : A, o : object) : bool
+  function MyReadsBad'<A,B>(f : A -> B, a : A, o : object) : bool
   {
     o in f.reads(a)  // error: MyReadsBad' does not have permission to read what f.reads(a) reads
   }
 
-  function MyRequiresOk(f : A -> B, a : A) : bool
-    reads f.reads(a);
+  function MyRequiresOk<A,B>(f : A -> B, a : A) : bool
+    reads f.reads(a)
   {
     f.requires(a)
   }
 
-  function MyRequiresBad(f : A -> B, a : A) : bool
+  function MyRequiresBad<A,B>(f : A -> B, a : A) : bool
   {
     f.requires(a)  // error: MyRequiresBad does not have permission to read what f.requires(a) reads
   }
@@ -72,11 +72,11 @@ module WhatWeKnowAboutReads {
   }
 
   class S {
-    var s : S;
+    var s : S
   }
 
   function ReadsSomething(s : S):()
-    reads s;
+    reads s
   {()}
 
   method MaybeSomething() {
@@ -105,29 +105,29 @@ module WhatWeKnowAboutReads {
 
 module ReadsAll {
   function A(f: int -> int) : int
-    reads set o,x | o in f.reads(x) :: o;
-    requires forall x :: f.requires(x);
+    reads set o,x | o in f.reads(x) :: o
+    requires forall x :: f.requires(x)
   {
     f(0) + f(1) + f(2)
   }
 
   function method B(f: int -> int) : int
-    reads set o,x | o in f.reads(x) :: o;
-    requires forall x :: f.requires(x);
+    reads set o,x | o in f.reads(x) :: o
+    requires forall x :: f.requires(x)
   {
     f(0) + f(1) + f(2)
   }
 
   function C(f: int -> int) : int
-    reads f.reads;
-    requires forall x :: f.requires(x);
+    reads f.reads
+    requires forall x :: f.requires(x)
   {
     f(0) + f(1) + f(2)
   }
 
   function method D(f: int -> int) : int
-    reads f.reads;
-    requires forall x :: f.requires(x);
+    reads f.reads
+    requires forall x :: f.requires(x)
   {
     f(0) + f(1) + f(2)
   }
diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy
index 3c0d7cd9..ae838eb3 100644
--- a/Test/hofs/ResolveError.dfy
+++ b/Test/hofs/ResolveError.dfy
@@ -3,9 +3,9 @@
 
 
 method ResolutionErrors() {
-    var x;
-    var g5 := x, y => (y, x);   // fail at resolution
-    var g6 := x, (y => (y, x)); // fail at resolution
+  var x;
+  var g5 := x, y => (y, x);   // fail at resolution
+  var g6 := x, (y => (y, x)); // fail at resolution
 }
 
 // cannot assign functions
@@ -23,20 +23,20 @@ method Nope3() {
 
 method RequiresFail(f : int -> int)
   // ok
-  requires f(0) == 0;
-  requires f.requires(0);
-  requires f.reads(0) == {};
+  requires f(0) == 0
+  requires f.requires(0)
+  requires f.reads(0) == {}
 
   // fail
-  requires f(0) == true;
-  requires f(1,2) == 0;
-  requires f(true) == 0;
-  requires f.requires(true);
-  requires f.requires(1) == 0;
-  requires f.requires(1,2);
-  requires f.reads(true) == {};
-  requires f.reads(1) == 0;
-  requires f.reads(1,2) == {};
+  requires f(0) == true
+  requires f(1,2) == 0
+  requires f(true) == 0
+  requires f.requires(true)
+  requires f.requires(1) == 0
+  requires f.requires(1,2)
+  requires f.reads(true) == {}
+  requires f.reads(1) == 0
+  requires f.reads(1,2) == {}
 {
 }
 
@@ -56,7 +56,7 @@ method Bla() {
   assert Bool;
 }
 
-method Pli(f : A -> B) requires f != null;
+method Pli<A,B>(f : A -> B) requires f != null
 {
   var o : object;
   assert f != o;
@@ -102,7 +102,7 @@ module AritySituations {
     w := V;  // error
   }
 
-  method P(r: T -> U, x: T) returns (u: U)
+  method P<T,U>(r: T -> U, x: T) returns (u: U)
     requires r.requires(x);
   {
     u := r(x);
diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect
index c3e0c242..11471ffd 100644
--- a/Test/hofs/ResolveError.dfy.expect
+++ b/Test/hofs/ResolveError.dfy.expect
@@ -2,8 +2,8 @@ ResolveError.dfy(86,6): Error: RHS (of type ((int,bool)) -> real) not assignable
 ResolveError.dfy(91,15): Error: incorrect type of method in-parameter 0 (expected ? -> ?, got (int,bool) -> real)

 ResolveError.dfy(101,6): Error: RHS (of type (()) -> real) not assignable to LHS (of type () -> real)

 ResolveError.dfy(102,6): Error: RHS (of type () -> real) not assignable to LHS (of type (()) -> real)

-ResolveError.dfy(7,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment

-ResolveError.dfy(8,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment

+ResolveError.dfy(7,9): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment

+ResolveError.dfy(8,9): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment

 ResolveError.dfy(21,6): Error: LHS of assignment must denote a mutable field

 ResolveError.dfy(31,16): Error: arguments must have the same type (got int and bool)

 ResolveError.dfy(32,12): Error: wrong number of arguments to function application (function type 'int -> int' expects 1, got 2)

@@ -17,7 +17,7 @@ ResolveError.dfy(39,18): Error: wrong number of arguments to function applicatio
 ResolveError.dfy(46,15): Error: a reads-clause expression must denote an object or a collection of objects (instead got int)

 ResolveError.dfy(47,7): Error: Precondition must be boolean (got int)

 ResolveError.dfy(56,9): Error: condition is expected to be of type bool, but is () -> bool

-ResolveError.dfy(59,34): Error: arguments must have the same type (got A -> B and ?)

+ResolveError.dfy(59,39): Error: arguments must have the same type (got A -> B and ?)

 ResolveError.dfy(62,11): Error: arguments must have the same type (got A -> B and object)

 ResolveError.dfy(68,24): Error: unresolved identifier: _

 22 resolution/type errors detected in ResolveError.dfy

diff --git a/Test/hofs/Simple.dfy b/Test/hofs/Simple.dfy
index c27fa82c..6d98531e 100644
--- a/Test/hofs/Simple.dfy
+++ b/Test/hofs/Simple.dfy
@@ -50,7 +50,7 @@ method Main() {
 }
 
 function method succ(x : int) : int
-  requires x > 0;
+  requires x > 0
 {
   x + 1
 }
@@ -74,24 +74,24 @@ method Main3() {
 }
 
 
-function P(f: A -> B, x : A): B
-  reads (f.reads)(x);
-  requires (f.requires)(x);
+function P<A,B>(f: A -> B, x : A): B
+  reads (f.reads)(x)
+  requires (f.requires)(x)
 {
   f(x)
 }
 
 
-function Q(f: U -> V, x : U): V
-  reads P.reads(f,x);
-  requires f.requires(x);  // would be nice to be able to write P.requires(f,x)
+function Q<U,V>(f: U -> V, x : U): V
+  reads P.reads(f,x)
+  requires f.requires(x)  // would be nice to be able to write P.requires(f,x)
 {
   P(f,x)
 }
 
-function QQ(f: U -> V, x : U): V
-  reads ((() => ((()=>f)()).reads)())((()=>x)());
-  requires ((() => ((()=>f)()).requires)())((()=>x)());
+function QQ<U,V>(f: U -> V, x : U): V
+  reads ((() => ((()=>f)()).reads)())((()=>x)())
+  requires ((() => ((()=>f)()).requires)())((()=>x)())
 {
   ((() => P)())((()=>f)(),(()=>x)())
 }
diff --git a/Test/hofs/TreeMapSimple.dfy b/Test/hofs/TreeMapSimple.dfy
index a853b82c..6b8f1377 100644
--- a/Test/hofs/TreeMapSimple.dfy
+++ b/Test/hofs/TreeMapSimple.dfy
@@ -6,7 +6,7 @@ datatype List<A> = Nil | Cons(head: A,tail: List<A>)
 datatype Tree<A> = Branch(val: A,trees: List<Tree<A>>)
 
 function ListData(xs : List) : set
-  ensures forall x :: x in ListData(xs) ==> x < xs;
+  ensures forall x :: x in ListData(xs) ==> x < xs
 {
   match xs
     case Nil => {}
@@ -14,32 +14,32 @@ function ListData(xs : List) : set
 }
 
 function TreeData(t0 : Tree) : set
-  ensures forall t :: t in TreeData(t0) ==> t < t0;
+  ensures forall t :: t in TreeData(t0) ==> t < t0
 {
   var Branch(x,ts) := t0;
   {x} + set t, y | t in ListData(ts) && y in TreeData(t) :: y
 }
 
-function Pre(f : A -> B, s : set<A>) : bool
-  reads (set x, y | x in s && y in f.reads(x) :: y);
+function Pre<A,B>(f : A -> B, s : set<A>) : bool
+  reads (set x, y | x in s && y in f.reads(x) :: y)
 {
   forall x :: x in s ==> f.reads(x) == {} && f.requires(x)
 }
 
-function method Map(xs : List<A>, f : A -> B): List<B>
-  reads Pre.reads(f, ListData(xs));
-  requires Pre(f, ListData(xs));
-  decreases xs;
+function method Map<A,B>(xs : List<A>, f : A -> B): List<B>
+  reads Pre.reads(f, ListData(xs))
+  requires Pre(f, ListData(xs))
+  decreases xs
 {
   match xs
     case Nil => Nil
     case Cons(x,xs) => Cons(f(x),Map(xs,f))
 }
 
-function method TMap(t0 : Tree<A>, f : A -> B) : Tree<B>
-  reads Pre.reads(f, TreeData(t0));
-  requires Pre(f, TreeData(t0));
-  decreases t0;
+function method TMap<A,B>(t0 : Tree<A>, f : A -> B) : Tree<B>
+  reads Pre.reads(f, TreeData(t0))
+  requires Pre(f, TreeData(t0))
+  decreases t0
 {
   var Branch(x,ts) := t0;
   Branch(f(x),Map(ts, t  requires t in ListData(ts)
diff --git a/Test/hofs/Twice.dfy b/Test/hofs/Twice.dfy
index add7e83c..5d948a58 100644
--- a/Test/hofs/Twice.dfy
+++ b/Test/hofs/Twice.dfy
@@ -1,7 +1,7 @@
 // RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-function method Twice(f : A -> A): A -> A
+function method Twice<A>(f : A -> A): A -> A
 {
   x requires f.requires(x) && f.requires(f(x))
     reads f.reads(x) reads if f.requires(x) then f.reads(f(x)) else {}
@@ -29,7 +29,7 @@ method WithReads() {
 }
 
 
-function method Twice_bad(f : A -> A): A -> A
+function method Twice_bad<A>(f : A -> A): A -> A
 {
   x requires f.requires(x) && f.requires(f(x))
     reads f.reads(x) + f.reads(f(x))
diff --git a/Test/hofs/VectorUpdate.dfy b/Test/hofs/VectorUpdate.dfy
index 96edbe77..ca6b20b3 100644
--- a/Test/hofs/VectorUpdate.dfy
+++ b/Test/hofs/VectorUpdate.dfy
@@ -1,28 +1,59 @@
 // RUN: %dafny /compile:3 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-method VectorUpdate(N: int, a : array<A>, f : (int,A) -> A)
-  requires a != null;
-  requires N == a.Length;
-  requires forall j :: 0 <= j < N ==> f.requires(j,a[j]);
-  requires forall j :: 0 <= j < N ==> a !in f.reads(j,a[j]);
-  modifies a;
-  ensures forall j :: 0 <= j < N ==> a[j] == f(j,old(a[j]));
+// this is a rather verbose version of the VectorUpdate method
+method VectorUpdate<A>(N: int, a : array<A>, f : (int,A) -> A)
+  requires a != null
+  requires N == a.Length
+  requires forall j :: 0 <= j < N ==> f.requires(j,a[j])
+  requires forall j :: 0 <= j < N ==> a !in f.reads(j,a[j])
+  modifies a
+  ensures forall j :: 0 <= j < N ==> a[j] == f(j,old(a[j]))
 {
   var i := 0;
-  while (i < N)
-    invariant 0 <= i <= N;
-    invariant forall j :: i <= j < N ==> f.requires(j,a[j]);
-    invariant forall j :: 0 <= j < N ==> f.requires(j,old(a[j]));
-    invariant forall j :: i <= j < N ==> a !in f.reads(j,a[j]);
-    invariant forall j :: i <= j < N ==> a[j] == old(a[j]);
-    invariant forall j :: 0 <= j < i ==> a[j] == f(j,old(a[j]));
+  while i < N
+    invariant 0 <= i <= N
+    invariant forall j :: i <= j < N ==> f.requires(j,a[j])
+    invariant forall j :: 0 <= j < N ==> f.requires(j,old(a[j]))
+    invariant forall j :: i <= j < N ==> a !in f.reads(j,a[j])
+    invariant forall j :: i <= j < N ==> a[j] == old(a[j])
+    invariant forall j :: 0 <= j < i ==> a[j] == f(j,old(a[j]))
   {
     a[i] := f(i,a[i]);
     i := i + 1;
   }
 }
 
+// here's a shorter version of the method above
+method VectorUpdate'<A>(a : array<A>, f : (int,A) -> A)
+  requires a != null
+  requires forall j :: 0 <= j < a.Length ==> a !in f.reads(j,a[j]) && f.requires(j,a[j])
+  modifies a
+  ensures forall j :: 0 <= j < a.Length ==> a[j] == f(j,old(a[j]))
+{
+  var i := 0;
+  while i < a.Length
+    invariant 0 <= i <= a.Length
+    invariant forall j :: i <= j < a.Length ==> a[j] == old(a[j])
+    invariant forall j :: 0 <= j < i ==> a[j] == f(j,old(a[j]))
+  {
+    a[i] := f(i,a[i]);
+    i := i + 1;
+  }
+}
+
+// here's yet another version
+method VectorUpdate''<A>(a : array<A>, f : (int,A) -> A)
+  requires a != null
+  requires forall j :: 0 <= j < a.Length ==> a !in f.reads(j,a[j]) && f.requires(j,a[j])
+  modifies a
+  ensures forall j :: 0 <= j < a.Length ==> a[j] == f(j,old(a[j]))
+{
+  forall i | 0 <= i < a.Length {
+    a[i] := f(i,a[i]);
+  }
+}
+
 method Main() 
 {
   var v := new int[10];
@@ -46,11 +77,11 @@ method Main()
 }
 
 method PrintArray(a : array<int>)
-  requires a != null;
+  requires a != null
 {
   var i := 0;
-  while (i < a.Length) {
-    if (i != 0) {
+  while i < a.Length {
+    if i != 0 {
 	  print ", ";
 	}
     print a[i];
diff --git a/Test/hofs/VectorUpdate.dfy.expect b/Test/hofs/VectorUpdate.dfy.expect
index b01ace00..18a7b110 100644
--- a/Test/hofs/VectorUpdate.dfy.expect
+++ b/Test/hofs/VectorUpdate.dfy.expect
@@ -1,5 +1,5 @@
 

-Dafny program verifier finished with 6 verified, 0 errors

+Dafny program verifier finished with 10 verified, 0 errors

 Program compiled successfully

 Running...