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.

1 files changed, 5 insertions, 5 deletions

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

 }