fix: Always parse parentheses for predicates

Source/DafnyCore/Dafny.atg

@@ -1771,8 +1771,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
                   "a formal [ ] declaration is only allowed for least and greatest predicates");
         .)
       ]
-      [ Formals<true, true, isTwoState, true, formals>
-      ]
+      Formals<true, true, isTwoState, true, formals>
       [ PredicateResult<"predicate", out result> ]
     | ellipsis   (. signatureEllipsis = t; .)
     )

Source/DafnyLanguageServer.Test/Lookup/WorkspaceSymbolTest.cs

@@ -65,7 +65,7 @@ method TestMethod() returns (x: int) {
 
 trait TestTrait {}
 
-predicate TestPredicate { false }", "test-workspace-symbols.dfy", false);
+predicate TestPredicate() { false }", "test-workspace-symbols.dfy", false);
 
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy

@@ -273,6 +273,26 @@ module ArrowTypes {
   }
 }
 
+// ---------------------- missing parentheses for `predicate` -----------------------------------
+
+module MissingPredicateParens0 {
+  predicate P<A>
+} // error: expecting open paren
+
+module MissingPredicateParens1 {
+  predicate P<A> { // error: expecting open paren
+    true
+  }
+}
+
+module MissingPredicateParens2 {
+  predicate P<A> { // error: expecting open paren
+    true
+  } by method {
+    return true;
+  }
+}
+
 // ---------------------- invalid newtype definition -----------------------------------
 
 newtype T {} // error: newtype is expected to have an '='

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy.expect

@@ -79,5 +79,8 @@ ParseErrors.dfy(261,28): Error: formal cannot be declared 'older' in this contex
 ParseErrors.dfy(267,12): Error: arrow-type arguments may not be declared as 'ghost'
 ParseErrors.dfy(272,18): Error: arrow-type arguments may not be declared as 'ghost'
 ParseErrors.dfy(272,35): Error: arrow-type arguments may not be declared as 'ghost'
-ParseErrors.dfy(278,10): Error: invalid NewtypeDecl
-77 parse errors detected in ParseErrors.dfy
+ParseErrors.dfy(280,0): Error: openparen expected
+ParseErrors.dfy(283,17): Error: openparen expected
+ParseErrors.dfy(289,17): Error: openparen expected
+ParseErrors.dfy(298,10): Error: invalid NewtypeDecl
+80 parse errors detected in ParseErrors.dfy

docs/dev/news/5069.fix

@@ -0,0 +1 @@
+The syntax of a predicate definition must always include parentheses.