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

3 files changed, 66 insertions, 5 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 1ca5e4d9..4b8ede60 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -697,12 +697,28 @@ namespace Microsoft.Dafny {
     }

 

     public override string TypeName(ModuleDefinition context) {

-      string s = "", closeparen = "";

-      if (Args.Count != 1 || Args[0].Normalize() is ArrowType) {

-        s += "("; closeparen = ")";

+      var domainNeedsParens = false;

+      if (Arity != 1) {

+        // 0 or 2-or-more arguments:  need parentheses

+        domainNeedsParens = true;

+      } else {

+        var arg = Args[0].Normalize();  // note, we do Normalize(), not NormalizeExpand(), since the TypeName will use any synonym

+        if (arg is ArrowType) {

+          // arrows are right associative, so we need parentheses around the domain type

+          domainNeedsParens = true;

+        } else {

+          // if the domain type consists of a single tuple type, then an extra set of parentheses is needed

+          // Note, we do NOT call .AsDatatype or .AsIndDatatype here, because those calls will do a NormalizeExpand().  Instead, we do the check manually.

+          var udt = arg as UserDefinedType;

+          if (udt != null && udt.ResolvedClass is TupleTypeDecl) {

+            domainNeedsParens = true;

+          }

+        }

       }

+      string s = "";

+      if (domainNeedsParens) { s += "("; }

       s += Util.Comma(Args, arg => arg.TypeName(context));

-      s += closeparen;

+      if (domainNeedsParens) { s += ")"; }

       s += " -> ";

       s += Result.TypeName(context);

       return s;

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