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, 7 insertions, 7 deletions

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

     }

   }

 }