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

1 files changed, 19 insertions, 0 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

+}