Allow array-type parameters to be filled in automatically.

Enhanced filling in of datatype parameters:  allow places that need only a prefix of the parameters of the datatype

1 files changed, 22 insertions, 0 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 35c17112..74405fa5 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -943,3 +943,25 @@ method TupleResolution(x: int, y: int, r: real)
   var pp: (int) := x;

   var qq: int := pp;

 }

+

+// --- filling in type arguments and checking that there aren't too many ---

+

+module TypeArgumentCount {

+  class C<T> {

+    var f: T;

+  }

+

+  method R0(a: array3, c: C)

+

+  method R1()

+  {

+    var a: array3;

+    var c: C;

+  }

+

+  method R2<T>()

+  {

+    var a: array3<T,int>;  // error: too many type arguments

+    var c: C<T,int>;  // error: too many type arguments

+  }

+}