Disallow automatic completion of type arguments to the LHS of datatype declarations

4 files changed, 24 insertions, 3 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 79e7ac57..e324393d 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1240,3 +1240,22 @@ module NonInferredTypeVariables {
      */

   }

 }

+

+// -------------- signature completion ------------------

+

+module SignatureCompletion {

+  // datatype signatures do not allow auto-declared type parameters on the LHS

+  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 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 F2<A,B>(s: set, x: A -> B): int

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

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 1b802687..3b768c84 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -83,6 +83,8 @@ ResolutionErrors.dfy(1220,26): Error: the type of this variable is underspecifie
 ResolutionErrors.dfy(1221,31): Error: the type of this variable is underspecified

 ResolutionErrors.dfy(1222,29): Error: the type of this variable is underspecified

 ResolutionErrors.dfy(1232,34): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1248,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

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

 ResolutionErrors.dfy(429,2): Error: More than one anonymous constructor

 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts

@@ -180,4 +182,4 @@ ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1129,2): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-182 resolution/type errors detected in ResolutionErrors.dfy

+184 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index 900b6110..aa3d7671 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -335,7 +335,7 @@ module ArrayTypeMagic {
     return b[..];

   }

 

-  datatype ArrayCubeTree = Leaf(array3) | Node(ArrayCubeTree, ArrayCubeTree)

+  datatype ArrayCubeTree<T> = Leaf(array3) | Node(ArrayCubeTree, ArrayCubeTree)

   datatype AnotherACT<T> = Leaf(array3) | Node(AnotherACT, AnotherACT)

   datatype OneMoreACT<T,U> = Leaf(array3) | Node(OneMoreACT, OneMoreACT)

 

diff --git a/Test/hofs/Fold.dfy b/Test/hofs/Fold.dfy
index 7ce99e56..50b5569b 100644
--- a/Test/hofs/Fold.dfy
+++ b/Test/hofs/Fold.dfy
@@ -1,7 +1,7 @@
 // RUN: %dafny /compile:3 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-datatype List = Nil | Cons(A,List<A>);
+datatype List<A> = Nil | Cons(A,List<A>);
 
 datatype Expr = Add(List<Expr>) | Mul(List<Expr>) | Lit(int);