Print arrow types with parentheses around the domain type when the domain consists of one tuple type.

1 files changed, 41 insertions, 0 deletions

diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy
index 410842b3..3c0d7cd9 100644
--- a/Test/hofs/ResolveError.dfy
+++ b/Test/hofs/ResolveError.dfy
@@ -67,3 +67,44 @@ method Underscores() {
   var v := (_, _) => 0;
   var w := (_, _, _) => _;
 }
+
+module AritySituations {
+  // In addition to testing type checking, these tests check that error messages
+  //  print the types correctly
+  function method F(x: int, b: bool): real    // F:  (int,bool) -> real
+  function method G(pair: (int, bool)): real  // G:  ((int,bool)) -> real
+  function method V(): real                   // V:  () -> real
+  function method W(unit: ()): real           // W:  (()) -> real
+
+  method M()
+  {
+    var f: (int, bool) -> real;
+    var g: ((int, bool)) -> real;
+    var h: (int, bool) -> real;
+    f := F;
+    g := G;
+    h := G;  // error
+
+    var f' := F;
+    var g' := G;
+  
+    var s0 := P(F, 5);  // error: F takes 2 arguments, but P expect a function that takes 1
+    var s1 := P(G, (2,true));  // fine
+
+    var v: () -> real;
+    var w: (()) -> real;
+    v := V;
+    w := W;
+    var v': () -> real := V;
+    var w': (()) -> real := W;
+    var w'': ((((((())))))) -> real := W;
+    v := W;  // error
+    w := V;  // error
+  }
+
+  method P(r: T -> U, x: T) returns (u: U)
+    requires r.requires(x);
+  {
+    u := r(x);
+  }
+}