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

2 files changed, 46 insertions, 1 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);
+  }
+}
diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect
index 994d78f2..2cf19369 100644
--- a/Test/hofs/ResolveError.dfy.expect
+++ b/Test/hofs/ResolveError.dfy.expect
@@ -1,3 +1,7 @@
+ResolveError.dfy(86,6): Error: RHS (of type ((int,bool)) -> real) not assignable to LHS (of type (int,bool) -> real)

+ResolveError.dfy(91,14): Error: incorrect type of method in-parameter 0 (expected ? -> ?, got (int,bool) -> real)

+ResolveError.dfy(101,6): Error: RHS (of type (()) -> real) not assignable to LHS (of type () -> real)

+ResolveError.dfy(102,6): Error: RHS (of type () -> real) not assignable to LHS (of type (()) -> real)

 ResolveError.dfy(7,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment

 ResolveError.dfy(8,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment

 ResolveError.dfy(21,6): Error: LHS of assignment must denote a mutable field

@@ -16,4 +20,4 @@ ResolveError.dfy(56,9): Error: condition is expected to be of type bool, but is
 ResolveError.dfy(59,34): Error: arguments must have the same type (got A -> B and ?)

 ResolveError.dfy(62,11): Error: arguments must have the same type (got A -> B and object)

 ResolveError.dfy(68,24): Error: unresolved identifier: _

-18 resolution/type errors detected in ResolveError.dfy

+22 resolution/type errors detected in ResolveError.dfy