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

5 files changed, 26 insertions, 6 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index a44491de..01ef0a4b 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3399,12 +3399,11 @@ namespace Microsoft.Dafny
       Contract.Requires(ctor != null);

       Contract.Requires(ctor.EnclosingDatatype != null);

       Contract.Requires(dtTypeArguments != null);

-      ResolveTypeOption option = dtTypeArguments.Count == 0 ? new ResolveTypeOption(ctor) : new ResolveTypeOption(ResolveTypeOptionEnum.AllowPrefix);

       foreach (Formal p in ctor.Formals) {

         // In the following, we pass in a NoContext, because any cycle formed by newtype constraints would have to

         // involve a non-null object in order to get to the field and its type, and there is no way in a newtype constraint

         // to obtain a non-null object.

-        ResolveType(p.tok, p.Type, new NoContext(ctor.EnclosingDatatype.Module), option, dtTypeArguments);

+        ResolveType(p.tok, p.Type, new NoContext(ctor.EnclosingDatatype.Module), ResolveTypeOptionEnum.AllowPrefix, dtTypeArguments);

       }

     }

 

@@ -3894,7 +3893,7 @@ namespace Microsoft.Dafny
               t.ResolvedClass = dd;

             } else {

               // d is a class or datatype, and it may have type parameters

-              what = "class/datatype";

+              what = isArrow ? "function type" : "class/datatype";

               t.ResolvedClass = d;

             }

             if (option.Opt == ResolveTypeOptionEnum.DontInfer) {

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);