From f7ca4ede6e033a4b828de536c04259e6b5c01ee2 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Sat, 2 May 2026 22:39:25 +0000
Subject: [PATCH 01/11] Replace `!<...!>` predicate-constructor delimiters with
 `{...}`

The predicate-constructor syntax `P!<x, _!>` is replaced by `P{x, _}`,
matching the notation used in the underlying paper and aligning with
struct-literal syntax. The grammar conflict with composite literals is
resolved as follows:

- Grammar: `predConstructArgs` now uses `L_CURLY ... R_CURLY`. The
  `primaryExpr predConstructArgs` rule continues to handle non-typeName
  bases such as `(T{42}).inv3{}()` directly.
- Parser postprocessor: `IDENT { ... }` and `IDENT.IDENT { ... }`
  always parse as `PCompositeLit`. A new `PredicateConstructorPostprocessor`
  rewrites them to `PPredConstructor` whenever they are unambiguously
  predicate constructors -- either because the literal contains a `_`
  blank (illegal in composite literals) or because the named base
  resolves syntactically to a predicate declared in the current package
  or to a built-in predicate (e.g. `PredTrue`).

Limitations / migration notes:
- Cross-package predicate constructors with no `_` (e.g. `pkg.P{1}()`)
  must currently be parenthesised: `(pkg.P){1}()`. The parse-time
  postprocessor cannot know whether `pkg.P` is an imported type or
  predicate without full name resolution.
- Tests, stubs (`waitgroup.gobra`), and the tutorial have been migrated
  to the new syntax; the deprecated `!<` / `!>` lexer tokens are kept so
  that legacy uses produce clearer errors.

https://claude.ai/code/session_01DoEQdoLVWuLxD2mQUJDDRg
---
 docs/tutorial.md                              | 57 ++++++++-------
 src/main/antlr4/GobraParser.g4                |  2 +-
 src/main/resources/stubs/sync/waitgroup.gobra | 26 +++----
 .../gobra/frontend/ParseTreeTranslator.scala  |  2 +-
 .../scala/viper/gobra/frontend/Parser.scala   | 71 +++++++++++++++++++
 .../impl_errors/parallel_search_replace.gobra | 42 +++++------
 .../evaluation/impl_errors/parallel_sum.gobra | 36 +++++-----
 .../evaluation/parallel_search_replace.gobra  | 42 +++++------
 .../examples/evaluation/parallel_sum.gobra    | 36 +++++-----
 .../spec_errors/parallel_search_replace.gobra | 42 +++++------
 .../evaluation/spec_errors/parallel_sum.gobra | 36 +++++-----
 .../parallel_search_replace_shared.gobra      | 48 ++++++-------
 .../examples/tutorial-examples/channels.gobra | 22 +++---
 .../tutorial-examples/multi-channel.gobra     | 46 ++++++------
 .../examples/tutorial-examples/mutex.gobra    | 12 ++--
 .../features/channels/channel-fail4.gobra     |  8 +--
 .../features/channels/channel-fail5.gobra     |  4 +-
 .../features/channels/channel-fail6.gobra     | 10 +--
 .../channels/channel-simple-buffered1.gobra   | 12 ++--
 .../channels/channel-simple-buffered2.gobra   | 26 +++----
 .../features/channels/channel-simple5.gobra   | 12 ++--
 .../features/channels/channel-simple6.gobra   | 52 +++++++-------
 .../features/channels/channel-simple7.gobra   | 22 +++---
 .../features/channels/channel-simple8.gobra   |  4 +-
 .../features/channels/channel-simple9.gobra   | 10 +--
 .../features/channels/foo/foo.gobra           |  6 +-
 .../channels/multi-channel-simple1.gobra      | 18 ++---
 .../features/defunc/defunc-fail1.gobra        | 16 ++---
 .../regressions/features/defunc/defunc1.gobra | 20 +++---
 .../features/defunc/import-preds.gobra        |  6 +-
 .../regressions/features/defunc/mutex1.gobra  | 18 ++---
 .../defunc/pred-construct-fail1.gobra         |  4 +-
 .../features/defunc/pred-expr-base1.gobra     |  6 +-
 .../features/defunc/waitgroup-fail1.gobra     | 10 +--
 .../features/defunc/waitgroup-simple1.gobra   | 60 ++++++++--------
 .../predicateWithInterfaceParam.gobra         |  8 +--
 .../features/predicates/foldability.gobra     | 14 ++--
 .../resources/regressions/issues/000164.gobra |  4 +-
 .../resources/regressions/issues/000176.gobra | 14 ++--
 .../resources/regressions/issues/000695.gobra | 20 +++---
 .../same_package/pkg_init/concfib/fib.go      | 24 +++----
 .../pkg_init/concfib/fib_spec.gobra           |  2 +-
 42 files changed, 501 insertions(+), 429 deletions(-)

diff --git a/docs/tutorial.md b/docs/tutorial.md
index 104e87552..053e98099 100644
--- a/docs/tutorial.md
+++ b/docs/tutorial.md
@@ -611,18 +611,18 @@ The race condition in the previous example can be avoided by using concurrency p
 
 Gobra has support for first-class predicates, i.e., expressions with a predicate type. First-class predicates are of type `pred(x1 T1, ..., xn Tn)`. The types `T1, ..., Tn` define that the predicate has an arity of `n` with the corresponding parameter types. 
 
-To instantiate a first-class predicate, Gobra provides *predicate constructors*. A predicate constructor `P!<d1, ..., dn!>` partially applies a declared predicate `P` with the constructor arguments `d1, ..., dn`. A constructor argument is either an expression or a wildcard `_`, symbolizing that this argument of `P` remains unapplied. In particular, the type of `P!<d1, ..., dn!>` is `pred(u1,...,uk)`, where `u1,...,uk` are the types of the unapplied arguments. As an example, consider the declared predicate `pred sameValue(i1 int8, i2 uint32){ ... }`. The predicate constructor `sameValue!<int8(1), _!>` has type `pred(uint32)`, since the first argument is applied and the second is not. Conversely, `sameValue!<_, uint32(1)!>` has type `pred(int8)`. Finally, `sameValue!<int8(1), uint32(1)!>` and `sameValue!< _, _!>` have types `pred()` and `pred(int8, uint32)`, respectively.
+To instantiate a first-class predicate, Gobra provides *predicate constructors*. A predicate constructor `P{d1, ..., dn}` partially applies a declared predicate `P` with the constructor arguments `d1, ..., dn`. A constructor argument is either an expression or a wildcard `_`, symbolizing that this argument of `P` remains unapplied. In particular, the type of `P{d1, ..., dn}` is `pred(u1,...,uk)`, where `u1,...,uk` are the types of the unapplied arguments. As an example, consider the declared predicate `pred sameValue(i1 int8, i2 uint32){ ... }`. The predicate constructor `sameValue{int8(1), _}` has type `pred(uint32)`, since the first argument is applied and the second is not. Conversely, `sameValue{_, uint32(1)}` has type `pred(int8)`. Finally, `sameValue{int8(1), uint32(1)}` and `sameValue{ _, _}` have types `pred()` and `pred(int8, uint32)`, respectively.
 
-The equality operator for predicate constructors is defined as a point-wise comparison, that is, `P1!<d1, ..., dn!>` is equal to `P2!<d'1, ... , d'n!>` if and only if `P1` and `P2` are the same declared predicate and if `di == d'i` for all `i` ranging from 1 to `n`.
+The equality operator for predicate constructors is defined as a point-wise comparison, that is, `P1{d1, ..., dn}` is equal to `P2{d'1, ... , d'n}` if and only if `P1` and `P2` are the same declared predicate and if `di == d'i` for all `i` ranging from 1 to `n`.
 
-The body of the predicate `P!<d1, ..., dn!>` is the body of `P` with the arguments applied accordingly. Like with other predicates, `P!<d1, ..., dn!>` can be instantiated and its instances may occur in assertions and in `fold` and `unfold` statements. The fold statement `fold P!<d1, ..., dk!>(e1, ..., en)` exchanges the first-class predicate instance with its body. The unfold statement does the reverse.
+The body of the predicate `P{d1, ..., dn}` is the body of `P` with the arguments applied accordingly. Like with other predicates, `P{d1, ..., dn}` can be instantiated and its instances may occur in assertions and in `fold` and `unfold` statements. The fold statement `fold P{d1, ..., dk}(e1, ..., en)` exchanges the first-class predicate instance with its body. The unfold statement does the reverse.
 
-> **Note**: In the paper, we use the notation `P{...}` instead of `P!<...!>`. Currently, Gobra uses `!<` and `!>` as delimiters to simplify Gobra's parser. In the future, we will change to the `P{...}` syntax.
+> **Note**: Predicate constructors share their `name { args }` surface syntax with composite literals. Gobra disambiguates by treating `name { args }` as a predicate constructor whenever `name` resolves to a top-level (function or method) predicate of the current package, or whenever the argument list contains the `_` blank identifier. For predicate constructors over imported predicates whose name happens to collide with a local type, parenthesise the base, e.g. `(pkg.P){1}()`.
 
 ### Reasoning about Mutual Exclusion with `sync.Mutex`
 
 
-In the following example, we show the function `safeInc`, a data-race free version of the previously seen function `inc` in section [Concurrency](#concurrency). The snippet uses a lock `pmutex` to synchronize the write accesses to the pointer `x`. `safeInc`'s pre and postcondition assert that `pmutex` was initialized (`acc(pmutex.LockP(), _)`) with invariant `mutexInvariant` (`pmutex.LockInv() == mutexInvariant!<x!>`), protecting the access to variable `x`. In the body of `safeInc`, first `pmutex.Lock()` is called to acquire the invariant `mutexInvariant!<x!>`. Then the first-class predicate instance is unfolded to acquire `acc(x)`, required to modify the value of `x`. At the end, the invariant is folded back again, after which `pmutex` can be released via a call to method `Unlock`.
+In the following example, we show the function `safeInc`, a data-race free version of the previously seen function `inc` in section [Concurrency](#concurrency). The snippet uses a lock `pmutex` to synchronize the write accesses to the pointer `x`. `safeInc`'s pre and postcondition assert that `pmutex` was initialized (`acc(pmutex.LockP(), _)`) with invariant `mutexInvariant` (`pmutex.LockInv() == mutexInvariant{x}`), protecting the access to variable `x`. In the body of `safeInc`, first `pmutex.Lock()` is called to acquire the invariant `mutexInvariant{x}`. Then the first-class predicate instance is unfolded to acquire `acc(x)`, required to modify the value of `x`. At the end, the invariant is folded back again, after which `pmutex` can be released via a call to method `Unlock`.
 
 ```go (test/resources/regressions/tutorial-examples/mutex.gobra)
 package tutorial
@@ -633,26 +633,25 @@ pred mutexInvariant(x *int) {
 	acc(x)
 }
 
-requires acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant!<x!>
-ensures  acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant!<x!>
+requires acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant{x}
+ensures  acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant{x}
 func safeInc(pmutex *sync.Mutex, x *int) {
 	pmutex.Lock()
-	unfold mutexInvariant!<x!>()
+	unfold mutexInvariant{x}()
 	*x = *x + 1
-	fold mutexInvariant!<x!>()
+	fold mutexInvariant{x}()
 	pmutex.Unlock()
 }
 ```
-> **Note:** At this point in time, using semicolons is mandatory to terminate lines that end with the `!<` `!>` delimiters like in the pre and postcondition of `safeInc`. This is a known limitation of our current parser and it will be fixed when we adopt the `{` `}` delimeters for predicate constructors. 
 
-The snippet below shows a client. First, `mutex` is allocated and the invariant is established for the first time by folding `mutexInvariant!<&x!>()`. To bind an invariant to a mutex, the `SetInv` method is called. `SetInv` expects as argument a first-class predicate with arity zero. After the invariant is bound to `&mutex`, the mutex is initialized and the permission `&mutex.LockP()` is acquired. This permission is necessary to call `Lock` and `Unlock`. At this point, the preconditions of the goroutines are satisfied and the goroutines can be started. Note that the preconditon of `safeInc` does not require write permission to the lock and thus, after starting the first goroutine, there are sufficient permissions remaining to start the second goroutine.
+The snippet below shows a client. First, `mutex` is allocated and the invariant is established for the first time by folding `mutexInvariant{&x}()`. To bind an invariant to a mutex, the `SetInv` method is called. `SetInv` expects as argument a first-class predicate with arity zero. After the invariant is bound to `&mutex`, the mutex is initialized and the permission `&mutex.LockP()` is acquired. This permission is necessary to call `Lock` and `Unlock`. At this point, the preconditions of the goroutines are satisfied and the goroutines can be started. Note that the preconditon of `safeInc` does not require write permission to the lock and thus, after starting the first goroutine, there are sufficient permissions remaining to start the second goroutine.
 
 ```go (test/resources/regressions/tutorial-examples/mutex.gobra)
 func client() {
 	x@ := 0
 	mutex@ := sync.Mutex{}
-	fold mutexInvariant!<&x!>()
-	(&mutex).SetInv(mutexInvariant!<&x!>)
+	fold mutexInvariant{&x}()
+	(&mutex).SetInv(mutexInvariant{&x})
 	go safeInc(&mutex, &x)
 	go safeInc(&mutex, &x)
 }
@@ -660,13 +659,13 @@ func client() {
 
 ### Channels
 
-We now shift our attention to channels. Similar to mutexes, channels must be initialized before any message can be sent and received through them. This is done via a call to the method `Init`. The method has two parameters: The first parameter is a first-class predicate with type `pred(T)`, where `T` is the type of messages communicated via the channel. It specifies properties and permissions of the data that is sent through the channel. The second parameter is a first-class predicate with type `pred()` that specifies properties and permissions that the sender obtains from the receiver when it sends a message. This is useful to model a rendez-vous of permissions in synchronous communication, which happens for unbuffered channels. In this example, and whenever the channel is buffered, the second argument will always be `PredTrue!<!>`, a predicate with arity zero whose body is `true`. Initializing a channel `c` through `Init` also produces permissions `m.SendChannel()` and `m.ReceiveChannel()`. Any read fraction of `m.SendChannel()` allows a function to send messages on `m`, whereas a read fraction of `m.ReceiveChannel()` allows a function to receive from `m`.
+We now shift our attention to channels. Similar to mutexes, channels must be initialized before any message can be sent and received through them. This is done via a call to the method `Init`. The method has two parameters: The first parameter is a first-class predicate with type `pred(T)`, where `T` is the type of messages communicated via the channel. It specifies properties and permissions of the data that is sent through the channel. The second parameter is a first-class predicate with type `pred()` that specifies properties and permissions that the sender obtains from the receiver when it sends a message. This is useful to model a rendez-vous of permissions in synchronous communication, which happens for unbuffered channels. In this example, and whenever the channel is buffered, the second argument will always be `PredTrue{}`, a predicate with arity zero whose body is `true`. Initializing a channel `c` through `Init` also produces permissions `m.SendChannel()` and `m.ReceiveChannel()`. Any read fraction of `m.SendChannel()` allows a function to send messages on `m`, whereas a read fraction of `m.ReceiveChannel()` allows a function to receive from `m`.
 
-After initialization, the predicates passed as arguments to `Init` can be retrieved via several methods. The method `c.SendGivenPerm()` returns the invariant that must hold when the sender sends a message. The method `c.RecvGotPerm()` returns the invariant that the receiver of a message can assume. Currently, these are always the same. Likewise, `c.SendGotPerm()` and `c.RecvGivenPerm()` are the invariants that must hold when a message is received and that can be assumed when a message is sent, respectively. Currently, these are also always the same. Furthermore, they must be `PredTrue!<!>` unless the channel is unbuffered.
+After initialization, the predicates passed as arguments to `Init` can be retrieved via several methods. The method `c.SendGivenPerm()` returns the invariant that must hold when the sender sends a message. The method `c.RecvGotPerm()` returns the invariant that the receiver of a message can assume. Currently, these are always the same. Likewise, `c.SendGotPerm()` and `c.RecvGivenPerm()` are the invariants that must hold when a message is received and that can be assumed when a message is sent, respectively. Currently, these are also always the same. Furthermore, they must be `PredTrue{}` unless the channel is unbuffered.
 
-In the following example, the function `incChannel` receives an `*int` from channel `c` and increments the value on the received location. The first two preconditions of `incChannel` require a fraction of `c.SendChannel()` and `c.RecvChannel()` to send on and receive from channel `c`. The rest of the preconditions establish that function `incChannel` expects `c` to have been initialized with the arguments `sendInvariant!<_!>` and `PredTrue!<!>`. The predicate `sendInvariant` contains the permission to the pointer sent over the channel `c` and restricts that `*v` is positive.
+In the following example, the function `incChannel` receives an `*int` from channel `c` and increments the value on the received location. The first two preconditions of `incChannel` require a fraction of `c.SendChannel()` and `c.RecvChannel()` to send on and receive from channel `c`. The rest of the preconditions establish that function `incChannel` expects `c` to have been initialized with the arguments `sendInvariant{_}` and `PredTrue{}`. The predicate `sendInvariant` contains the permission to the pointer sent over the channel `c` and restricts that `*v` is positive.
 
-The body of `incChannel` starts by folding `PredTrue!<!>()` to be able to receive from the channel. Recall that an instance of `PredTrue` must be sent from receiver to sender. It then receives from `c` and in case of success, unfolds `sendInvariant!<_!>(res)` to acquire write permissions to `res`. It then modifies `*res` and folds back `sendInvariant!<_!>(res)` to send the reply.
+The body of `incChannel` starts by folding `PredTrue{}()` to be able to receive from the channel. Recall that an instance of `PredTrue` must be sent from receiver to sender. It then receives from `c` and in case of success, unfolds `sendInvariant{_}(res)` to acquire write permissions to `res`. It then modifies `*res` and folds back `sendInvariant{_}(res)` to send the reply.
 
 ```go (test/resources/regressions/tutorial-examples/channels.gobra)
 package tutorial
@@ -677,25 +676,25 @@ pred sendInvariant(v *int) {
 
 requires acc(c.SendChannel(), 1/2)
 requires acc(c.RecvChannel(), 1/2)
-requires c.SendGivenPerm() == sendInvariant!<_!>
-requires c.SendGotPerm() == PredTrue!<!>
-requires c.RecvGivenPerm() == PredTrue!<!>
-requires c.RecvGotPerm() == sendInvariant!<_!>
+requires c.SendGivenPerm() == sendInvariant{_}
+requires c.SendGotPerm() == PredTrue{}
+requires c.RecvGivenPerm() == PredTrue{}
+requires c.RecvGotPerm() == sendInvariant{_}
 func incChannel(c chan *int) {
-	fold PredTrue!<!>()
+	fold PredTrue{}()
 	res, ok := <- c
 	if (ok) {
-		unfold sendInvariant!<_!>(res)
+		unfold sendInvariant{_}(res)
 		// we now have write access after unfolding the invariant:
 		*res = *res + 1
 		// fold the invariant and send pointer and permission back:
-		fold sendInvariant!<_!>(res)
+		fold sendInvariant{_}(res)
 		c <- res
 	}
 }
 ```
 
-The next snippet shows a client. In the body, a channel `c` is created and initialized with `sendInvariant` and `PredTrue`. It then spawns a goroutine, executing `incChannel` with the initialized channel. Next, it folds `sendInvariant!<_!>(p)` to send `p` over the channel `c`. The subsequent fold of `PredTrue!<!>()` is required to satisfy the precondition of receive. At this point, `PredTrue!<!>()` must be sent from `clientChannel` (the receiver) to `incChannel` (the sender). After successfully receiving the reply, the receiver acquires `sendInvariant!<_!>(res)`, which can then be unfolded to obtain the permission to `res` and to check that its value is positive.
+The next snippet shows a client. In the body, a channel `c` is created and initialized with `sendInvariant` and `PredTrue`. It then spawns a goroutine, executing `incChannel` with the initialized channel. Next, it folds `sendInvariant{_}(p)` to send `p` over the channel `c`. The subsequent fold of `PredTrue{}()` is required to satisfy the precondition of receive. At this point, `PredTrue{}()` must be sent from `clientChannel` (the receiver) to `incChannel` (the sender). After successfully receiving the reply, the receiver acquires `sendInvariant{_}(res)`, which can then be unfolded to obtain the permission to `res` and to check that its value is positive.
 
 ```go (test/resources/regressions/tutorial-examples/channels.gobra)
 func clientChannel() {
@@ -703,16 +702,16 @@ func clientChannel() {
 
 	var x@ int = 42
 	var p *int = &x
-	c.Init(sendInvariant!<_!>, PredTrue!<!>)
+	c.Init(sendInvariant{_}, PredTrue{})
 	go incChannel(c)
 	assert *p == 42
-	fold sendInvariant!<_!>(p)
+	fold sendInvariant{_}(p)
 	c <- p
 
-	fold PredTrue!<!>()
+	fold PredTrue{}()
 	res, ok := <- c
 	if (ok) {
-		unfold sendInvariant!<_!>(res)
+		unfold sendInvariant{_}(res)
 		assert *res > 0
 		// we have regained write access:
 		*res = 1
diff --git a/src/main/antlr4/GobraParser.g4 b/src/main/antlr4/GobraParser.g4
index 102d1308c..375be4356 100644
--- a/src/main/antlr4/GobraParser.g4
+++ b/src/main/antlr4/GobraParser.g4
@@ -424,7 +424,7 @@ functionLit: specification closureDecl[$specification.trusted, $specification.pu
 
 closureDecl[boolean trusted, boolean pure]:  FUNC IDENTIFIER? (signature blockWithBodyParameterInfo?);
 
-predConstructArgs: L_PRED expressionList? COMMA? R_PRED;
+predConstructArgs: L_CURLY expressionList? COMMA? R_CURLY;
 
 // Added predicate spec and method specifications
 interfaceType:
diff --git a/src/main/resources/stubs/sync/waitgroup.gobra b/src/main/resources/stubs/sync/waitgroup.gobra
index 2c0335f6e..3575c2d11 100644
--- a/src/main/resources/stubs/sync/waitgroup.gobra
+++ b/src/main/resources/stubs/sync/waitgroup.gobra
@@ -58,14 +58,14 @@ func (g *WaitGroup) SetWaitMode(ghost p perm, ghost q perm)
 // latest proposal for WaitGroups (as of 21/01/2021)
 ghost
 requires P() && g.UnitDebt(P)
-ensures g.UnitDebt(PredTrue!<!>)
+ensures g.UnitDebt(PredTrue{})
 decreases _
 func (g *WaitGroup) PayDebt(ghost P pred())
 
-// Simplified version of the debt redistribution rule, instantiated with P == { PredTrue!<!> } and Q == { R }.
+// Simplified version of the debt redistribution rule, instantiated with P == { PredTrue{} } and Q == { R }.
 // This is the only rule that generates a Token.
 ghost
-requires g.UnitDebt(PredTrue!<!>)
+requires g.UnitDebt(PredTrue{})
 ensures g.UnitDebt(R) && g.Token(R)
 decreases _
 func (g *WaitGroup) GenerateTokenAndDebt(ghost R pred())
@@ -80,16 +80,16 @@ func (g *WaitGroup) GenerateToken(ghost R pred())
 requires p >= 0
 requires n > 0 && p > 0 ==> acc(g.WaitGroupP(), p) && !g.WaitMode()
 requires (n > 0 && p == 0) ==> g.UnitDebt(P)
-requires n < 0 ==> acc(g.UnitDebt(PredTrue!<!>), -n/1)
+requires n < 0 ==> acc(g.UnitDebt(PredTrue{}), -n/1)
 ensures (n > 0 && p > 0) ==> acc(g.WaitGroupP(), p)
 ensures (n > 0 && p == 0) ==> g.UnitDebt(P)
-ensures n > 0 ==> acc(g.UnitDebt(PredTrue!<!>), n/1)
+ensures n > 0 ==> acc(g.UnitDebt(PredTrue{}), n/1)
 // this is actually necessary, otherwise Gobra cannot prove that Add does not modify the wait mode
 ensures (n > 0 && p > 0) ==> g.WaitMode() == old(g.WaitMode())
 decreases _
 func (g *WaitGroup) Add(n int, ghost p perm, ghost P pred())
 
-requires g.UnitDebt(PredTrue!<!>)
+requires g.UnitDebt(PredTrue{})
 decreases _
 func (g *WaitGroup) Done()
 
@@ -120,9 +120,9 @@ pred CollectFractions(ghost P seq[pred()], ghost perms seq[perm]) {
 ghost
 requires len(P) == len(permsP)
 requires len(Q) == len(permsQ)
-requires g.UnitDebt(CollectFractions!<P ++ Q, permsP ++ permsQ!>)
-requires g.UnitDebt(PredTrue!<!>)
-ensures g.UnitDebt(CollectFractions!<P, permsP!>) && g.UnitDebt(CollectFractions!<Q, permsQ!>)
+requires g.UnitDebt(CollectFractions{P ++ Q, permsP ++ permsQ})
+requires g.UnitDebt(PredTrue{})
+ensures g.UnitDebt(CollectFractions{P, permsP}) && g.UnitDebt(CollectFractions{Q, permsQ})
 decreases _
 func (g *WaitGroup) SplitSequence(ghost P seq[pred()], ghost Q seq[pred()], ghost permsP seq[perm], ghost permsQ seq[perm])
 
@@ -133,10 +133,10 @@ requires len(P) == len(permsQ)
 requires len(P) == len(permsR)
 requires forall i int :: 0 <= i && i < len(P) ==> permsP[i] >= 0
 requires forall i int :: 0 <= i && i < len(P) ==> permsQ[i] >= 0
-requires g.UnitDebt(CollectFractions!<P, permsR!>)
-requires g.UnitDebt(PredTrue!<!>)
+requires g.UnitDebt(CollectFractions{P, permsR})
+requires g.UnitDebt(PredTrue{})
 requires forall i int :: 0 <= i && i < len(P) ==> permsP[i] + permsQ[i] == permsR[i]
-ensures g.UnitDebt(CollectFractions!<P, permsP!>)
-ensures g.UnitDebt(CollectFractions!<P, permsQ!>)
+ensures g.UnitDebt(CollectFractions{P, permsP})
+ensures g.UnitDebt(CollectFractions{P, permsQ})
 decreases _
 func (g *WaitGroup) SplitFractions(ghost P seq[pred()], ghost permsP seq[perm], ghost permsQ seq[perm], ghost permsR seq[perm])
diff --git a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala
index b118fe588..b29a442d0 100644
--- a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala
+++ b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala
@@ -1364,7 +1364,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
 
   /**
     * Visits the rule
-    * predConstructArgs: L_PRED expressionList? COMMA? R_PRED
+    * predConstructArgs: L_CURLY expressionList? COMMA? R_CURLY
     * @param ctx the parse tree
     *     */
   override def visitPredConstructArgs(ctx: PredConstructArgsContext): PredArgs = {
diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala
index 26efdf048..fd370955d 100644
--- a/src/main/scala/viper/gobra/frontend/Parser.scala
+++ b/src/main/scala/viper/gobra/frontend/Parser.scala
@@ -239,6 +239,7 @@ object Parser extends LazyLogging {
       postprocessors = Seq(
         new ImportPostprocessor(parseAst.positions.positions),
         new TerminationMeasurePostprocessor(parseAst.positions.positions, specOnly = specOnly),
+        new PredicateConstructorPostprocessor(parseAst.positions.positions),
       )
       postprocessedAst <- postprocessors.foldLeft[Either[Vector[ParserError], PPackage]](Right(parseAst)) {
         case (Right(ast), postprocessor) => postprocessor.postprocess(ast)(config)
@@ -515,6 +516,76 @@ object Parser extends LazyLogging {
     }
   }
 
+  private class PredicateConstructorPostprocessor(override val positions: Positions) extends Postprocessor {
+    /**
+      * Predicate constructors share their `name { args }` surface syntax with composite literals,
+      * so the parser conservatively builds a `PCompositeLit` for `IDENT { ... }` and
+      * `IDENT.IDENT { ... }` shapes. This postprocessor rewrites such literals into
+      * `PPredConstructor` when they are unambiguously predicate constructors:
+      *   1. They contain at least one positional `_` element (illegal in composite literals), or
+      *   2. The named/dotted base resolves syntactically to a top-level predicate declared in
+      *      the current package.
+      *
+      * Cases that depend on cross-package resolution (e.g. `pkg.P{1}()` where `P` is a predicate
+      * declared in `pkg` and not shadowed locally) are left alone and must currently be written
+      * with an explicit parenthesised base, e.g. `(pkg.P){1}()`.
+      */
+    def postprocess(pkg: PPackage)(config: Config): Either[Vector[ParserError], PPackage] = {
+      // collect names of all top-level (function and method) predicate declarations
+      val localPredicateNames: Set[String] = pkg.programs.flatMap(_.declarations.collect {
+        case d: PFPredicateDecl => d.id.name
+        case d: PMPredicateDecl => d.id.name
+      }).toSet
+      // also recognise built-in predicate identifiers (e.g. PredTrue, IsChannel, ...)
+      val builtInPredicateNames: Set[String] = viper.gobra.frontend.info.base.BuiltInMemberTag.builtInMembers().collect {
+        case t: viper.gobra.frontend.info.base.BuiltInMemberTag.BuiltInPredicateTag => t.identifier
+      }.toSet
+      val predicateNames: Set[String] = localPredicateNames ++ builtInPredicateNames
+
+      def hasKey(lit: PLiteralValue): Boolean = lit.elems.exists(_.key.isDefined)
+      def hasBlank(lit: PLiteralValue): Boolean = lit.elems.exists {
+        case PKeyedElement(None, PExpCompositeVal(_: PBlankIdentifier)) => true
+        case _ => false
+      }
+      def isPredName(id: PIdnUse): Boolean = predicateNames.contains(id.name)
+
+      def shouldRewrite(typ: PLiteralType, lit: PLiteralValue): Boolean = {
+        // composite literals with keyed elements (e.g. `T{x: 1}`) cannot be predicate constructors
+        if (hasKey(lit)) false
+        else typ match {
+          case PNamedOperand(id) => hasBlank(lit) || isPredName(id)
+          case PDot(_, id) => hasBlank(lit) || isPredName(id)
+          case _ => false
+        }
+      }
+
+      def convertArgs(lit: PLiteralValue): Vector[Option[PExpression]] = lit.elems.map {
+        case PKeyedElement(None, PExpCompositeVal(_: PBlankIdentifier)) => None
+        case PKeyedElement(None, PExpCompositeVal(e)) => Some(e)
+        case e => Violation.violation(s"unexpected element form in predicate constructor candidate: $e")
+      }
+
+      def buildBase(typ: PLiteralType): PPredConstructorBase = typ match {
+        case op@PNamedOperand(id) => PFPredBase(id).at(op)
+        case d: PDot => PDottedBase(d).at(d)
+        case t => Violation.violation(s"unexpected base for predicate constructor: $t")
+      }
+
+      val rewritePredConstructors: Strategy =
+        strategyWithName[Any]("rewritePredConstructors", {
+          case n@PCompositeLit(typ, lit) if shouldRewrite(typ, lit) =>
+            Some(PPredConstructor(buildBase(typ), convertArgs(lit)).at(n))
+          case n => Some(n)
+        })
+
+      val updatedProgs = pkg.programs.map(prog => {
+        val updatedDecls = rewrite(topdown(attempt(rewritePredConstructors)))(prog.declarations)
+        PProgram(prog.packageClause, prog.pkgInvariants, prog.imports, prog.friends, updatedDecls).at(prog)
+      })
+      Right(PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info).at(pkg))
+    }
+  }
+
   private class SyntaxAnalyzer[Rule <: ParserRuleContext, Node <: AnyRef](tokens: CommonTokenStream, source: Source, errors: ListBuffer[ParserError], pom: PositionManager, specOnly: Boolean = false) extends GobraParser(tokens){
 
 
diff --git a/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_search_replace.gobra b/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_search_replace.gobra
index feddaa55b..7b1ab0b37 100644
--- a/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_search_replace.gobra
+++ b/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_search_replace.gobra
@@ -27,20 +27,20 @@ pred replacedPerm(ghost s0 seq[int], ghost s [] int, ghost x, y int) {
 
 pred messagePerm(ghost wg *sync.WaitGroup, s []int, ghost x, y int) {
   (forall i int :: 0 <= i && i < len(s) ==> acc(&s[i])) &&
-  wg.UnitDebt(replacedPerm!<toSeq(s),s,x,y!>)
+  wg.UnitDebt(replacedPerm{toSeq(s),s,x,y})
 }
 
 requires acc(c.RecvChannel(),_)
-requires c.RecvGivenPerm() == PredTrue!<!>
-requires c.RecvGotPerm() == messagePerm!<wg,_,x,y!>
+requires c.RecvGivenPerm() == PredTrue{}
+requires c.RecvGotPerm() == messagePerm{wg,_,x,y}
 func worker(c <- chan[]int, wg *sync.WaitGroup, x, y int) {
-  fold acc(PredTrue!<!>(),2/1);
-  invariant PredTrue!<!>() && acc(c.RecvChannel(),_)
-  invariant c.RecvGivenPerm() == PredTrue!<!>
-  invariant c.RecvGotPerm() == messagePerm!<wg,_,x,y,!>
-  invariant ok ==> messagePerm!<wg,_,x,y!>(s)
+  fold acc(PredTrue{}(),2/1);
+  invariant PredTrue{}() && acc(c.RecvChannel(),_)
+  invariant c.RecvGivenPerm() == PredTrue{}
+  invariant c.RecvGotPerm() == messagePerm{wg,_,x,y,}
+  invariant ok ==> messagePerm{wg,_,x,y}(s)
   for s, ok := <- c; ok; s, ok = <-c {
-    unfold messagePerm!<wg,_,x,y!>(s)
+    unfold messagePerm{wg,_,x,y}(s)
     ghost s0 := toSeq(s)
     invariant 0 <= i && i <= len(s)
     invariant forall j int :: 0 <= j && j < len(s) ==> acc(&s[j])
@@ -51,10 +51,10 @@ func worker(c <- chan[]int, wg *sync.WaitGroup, x, y int) {
       // we forget to perform the worker's task (seeded bug):
       // if(s[i] == x) { s[i] = y }
     }
-    fold replacedPerm!<s0,s,x,y!>()
-    wg.PayDebt(replacedPerm!<s0,s,x,y!>)
+    fold replacedPerm{s0,s,x,y}()
+    wg.PayDebt(replacedPerm{s0,s,x,y})
     wg.Done()
-    fold PredTrue!<!>()
+    fold PredTrue{}()
   }
 }
 
@@ -73,13 +73,13 @@ func SearchReplace(s []int, x, y int) {
   ghost s0 := toSeq(s)
   c := make(chan []int,4)
   var wg@ sync.WaitGroup
-  ghost pr := messagePerm!<&wg,_,x,y!>
-  c.Init(pr,PredTrue!<!>)
+  ghost pr := messagePerm{&wg,_,x,y}
+  c.Init(pr,PredTrue{})
   wg.Init()
   ghost seqs := seq[seq[int]] {}
   ghost pseqs := seq[pred()] {}
   invariant acc(c.RecvChannel(),_)
-  invariant c.RecvGivenPerm() == PredTrue!<!> && c.RecvGotPerm() == pr
+  invariant c.RecvGivenPerm() == PredTrue{} && c.RecvGotPerm() == pr
   for i := 0; i != workers; i++ {
     go worker(c,&wg,x,y)
   }
@@ -98,7 +98,7 @@ func SearchReplace(s []int, x, y int) {
     0 <= j && j < len(seqs[i]) ==> seqs[i][j] == s0[i * workRange + j]
   invariant len(pseqs) == len(seqs)
   invariant forall i int :: {pseqs[i]} 0 <= i && i < len(pseqs) ==>
-    pseqs[i] == replacedPerm!<seqs[i],s[i * workRange:i * workRange + len(seqs[i])],x,y!>
+    pseqs[i] == replacedPerm{seqs[i],s[i * workRange:i * workRange + len(seqs[i])],x,y}
   invariant forall i int :: 0 <= i && i < len(pseqs) ==> wg.TokenById(pseqs[i],i)
   for offset := 0; offset != len(s); {
     nextOffset := offset + workRange;
@@ -109,16 +109,16 @@ func SearchReplace(s []int, x, y int) {
     assert forall i int :: {&section[i]} 0 <= i && i < len(s) ==>
       &section[i] == &s[i + offset]
     ghost s1 := toSeq(section)
-    ghost wpr := replacedPerm!<s1,section,x,y!>
-    wg.Add(1,1/2,PredTrue!<!>)
+    ghost wpr := replacedPerm{s1,section,x,y}
+    wg.Add(1,1/2,PredTrue{})
     ghost if(offset == 0) {
-      wg.Start(1/2,PredTrue!<!>)
+      wg.Start(1/2,PredTrue{})
     }
     wg.GenerateTokenAndDebt(wpr)
     fold wg.TokenById(wpr,len(pseqs))
     seqs = seqs ++ seq[seq[int]]{ s1 }
     pseqs = pseqs ++ seq[pred()] { wpr }
-    fold messagePerm!<&wg,_,x,y!>(section)
+    fold messagePerm{&wg,_,x,y}(section)
     c <- section
     offset = nextOffset
   }
@@ -137,7 +137,7 @@ func SearchReplace(s []int, x, y int) {
       down := i * workRange
       up := down + len(seqs[i])
       s1 := s[down:up]
-      unfold replacedPerm!<seqs[i],s1,x,y!>()
+      unfold replacedPerm{seqs[i],s1,x,y}()
       assert forall j int :: {&s[j]} down <= j && j < up ==> &s[j] == &s1[j-down]
     }
   }
diff --git a/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra b/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra
index 21b06c68d..4ded5ef23 100644
--- a/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra
+++ b/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra
@@ -19,11 +19,11 @@ requires acc(c) && acc(c.sum) && acc(c.m) && c.m.state == 0 && c.m.stema == 0
 requires *c.sum == 0
 requires forall i int :: 0 <= i && i < len(seenSlice) ==> acc(&seenSlice[i], 1/2)
 requires forall i int :: 0 <= i && i < len(seenSlice) ==> seenSlice[i] == 0
-ensures acc(c) && c.m.LockP() && c.m.LockInv() == (AccInv!<c.sum, seenSlice!>)
+ensures acc(c) && c.m.LockP() && c.m.LockInv() == (AccInv{c.sum, seenSlice})
 func (c *Accum) Init(ghost seenSlice ghost []int) {
 	assume GhostSum(seenSlice) == 0
-	fold AccInv!<c.sum, seenSlice!>()
-	c.m.SetInv(AccInv!<c.sum, seenSlice!>)
+	fold AccInv{c.sum, seenSlice}()
+	c.m.SetInv(AccInv{c.sum, seenSlice})
 }
 
 /* Creates a worker thread per element in the slice and concurrently computes the sum of all the elements */
@@ -52,19 +52,19 @@ func ParallelSum(s []int) (res int) {
 	// invariant i != 0 ==> acc(w.WaitGroupP(), 1/2) && acc(w.WaitGroupStarted(), 1/2)
 	invariant i > 0 ==> acc(w.WaitGroupP(), 1/2) && acc(w.WaitGroupStarted(), 1/2)
 	invariant forall i int :: 0 <= i && i < len(s) ==> acc(&s[i], 1/2)
-	invariant forall j int :: 0 <= j && j < i ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!>
+	invariant forall j int :: 0 <= j && j < i ==> tokens[j] == locHasVal{&seenSlice[j],s[j]}
 	invariant forall j int :: 0 <= j && j < i ==> w.TokenById(tokens[j], j)
 	invariant !w.WaitMode()
 	invariant acc(c, _)
-	invariant acc(c.m.LockP(), _) && c.m.LockInv() == AccInv!<c.sum, seenSlice!>
+	invariant acc(c.m.LockP(), _) && c.m.LockInv() == AccInv{c.sum, seenSlice}
 	invariant forall j int :: i <= j && j < n ==> acc(&seenSlice[j], 1/2)
 	invariant forall j int :: i <= j && j < n ==> seenSlice[j] == 0
 	for i := 0; i < n; i++ {
-		w.Add(1, 1/2, PredTrue!<!>)
+		w.Add(1, 1/2, PredTrue{})
 		ghost if i == 0 {
-			w.Start(1/2, PredTrue!<!>)
+			w.Start(1/2, PredTrue{})
 		}
-		tokens = tokens ++ seq[pred()]{ locHasVal!<&seenSlice[i], s[i]!> }
+		tokens = tokens ++ seq[pred()]{ locHasVal{&seenSlice[i], s[i]} }
 		w.GenerateTokenAndDebt(tokens[i])
 		fold w.TokenById(tokens[i], i)
 		go worker(w, c, s[i], seenSlice, i)
@@ -75,19 +75,19 @@ func ParallelSum(s []int) (res int) {
 	ghost {
 		invariant 0 <= i && i <= n
 		invariant forall j int :: 0 <= j && j < n ==> acc(&s[j], 1/2)
-		invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!>
+		invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal{&seenSlice[j],s[j]}
 		invariant forall j int :: 0 <= j && j < n ==> (j < i ? acc(&seenSlice[j], 1/2) && seenSlice[j] == s[j] : sync.InjEval(tokens[j], j))
 		decreases n - i
 		for i:=0; i < n; i++ {
 			unfold sync.InjEval(tokens[i], i)
-			unfold locHasVal!<&seenSlice[i],s[i]!>()
+			unfold locHasVal{&seenSlice[i],s[i]}()
 		}
 	}
 
 	c.m.Lock()
-	unfold AccInv!<c.sum, seenSlice!>()
+	unfold AccInv{c.sum, seenSlice}()
 	res = *(c.sum)
-	fold AccInv!<c.sum, seenSlice!>()
+	fold AccInv{c.sum, seenSlice}()
 	c.m.Unlock()
 	sumExtensional(s, seenSlice)
 	return res
@@ -141,19 +141,19 @@ func update(ghost s ghost []int, ghost pos, val int) {
 
 requires acc(accum, _)
 requires acc(&seenSlice[pos], 1/2) && seenSlice[pos] == 0
-requires acc(accum.m.LockP(), _) && accum.m.LockInv() == AccInv!<accum.sum, seenSlice!>
+requires acc(accum.m.LockP(), _) && accum.m.LockInv() == AccInv{accum.sum, seenSlice}
 requires 0 <= pos && pos < len(seenSlice)
-requires w.UnitDebt(locHasVal!<&seenSlice[pos],val!>)
+requires w.UnitDebt(locHasVal{&seenSlice[pos],val})
 func worker(w *sync.WaitGroup, accum *Accum, val int, ghost seenSlice ghost []int, ghost pos int) {
 	accum.m.Lock()
-	unfold AccInv!<accum.sum, seenSlice!>()
+	unfold AccInv{accum.sum, seenSlice}()
 	// we forget to increment the sum (seeded bug):
 	// *(accum.sum) += val
 	update(seenSlice, pos, val)
 	//:: ExpectedOutput(fold_error:assertion_error)
-	fold AccInv!<accum.sum, seenSlice!>()
+	fold AccInv{accum.sum, seenSlice}()
 	accum.m.Unlock()
-	fold locHasVal!<&seenSlice[pos],val!>()
-	w.PayDebt(locHasVal!<&seenSlice[pos],val!>)
+	fold locHasVal{&seenSlice[pos],val}()
+	w.PayDebt(locHasVal{&seenSlice[pos],val})
 	w.Done()
 }
\ No newline at end of file
diff --git a/src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra b/src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra
index e6dab82d3..754be59e4 100644
--- a/src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra
+++ b/src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra
@@ -25,20 +25,20 @@ pred replacedPerm(ghost s0 seq[int], ghost s [] int, ghost x, y int) {
 
 pred messagePerm(ghost wg *sync.WaitGroup, s []int, ghost x, y int) {
   (forall i int :: 0 <= i && i < len(s) ==> acc(&s[i])) &&
-  wg.UnitDebt(replacedPerm!<toSeq(s),s,x,y!>)
+  wg.UnitDebt(replacedPerm{toSeq(s),s,x,y})
 }
 
 requires acc(c.RecvChannel(),_)
-requires c.RecvGivenPerm() == PredTrue!<!>
-requires c.RecvGotPerm() == messagePerm!<wg,_,x,y!>
+requires c.RecvGivenPerm() == PredTrue{}
+requires c.RecvGotPerm() == messagePerm{wg,_,x,y}
 func worker(c <- chan[]int, wg *sync.WaitGroup, x, y int) {
-  fold acc(PredTrue!<!>(),2/1);
-  invariant PredTrue!<!>() && acc(c.RecvChannel(),_)
-  invariant c.RecvGivenPerm() == PredTrue!<!>
-  invariant c.RecvGotPerm() == messagePerm!<wg,_,x,y,!>
-  invariant ok ==> messagePerm!<wg,_,x,y!>(s)
+  fold acc(PredTrue{}(),2/1);
+  invariant PredTrue{}() && acc(c.RecvChannel(),_)
+  invariant c.RecvGivenPerm() == PredTrue{}
+  invariant c.RecvGotPerm() == messagePerm{wg,_,x,y,}
+  invariant ok ==> messagePerm{wg,_,x,y}(s)
   for s, ok := <- c; ok; s, ok = <-c {
-    unfold messagePerm!<wg,_,x,y!>(s)
+    unfold messagePerm{wg,_,x,y}(s)
     ghost s0 := toSeq(s)
     invariant 0 <= i && i <= len(s)
     invariant forall j int :: 0 <= j && j < len(s) ==> acc(&s[j])
@@ -47,11 +47,11 @@ func worker(c <- chan[]int, wg *sync.WaitGroup, x, y int) {
     for i := 0; i != len(s); i++ {
       if(s[i] == x) { s[i] = y }
     }
-    fold replacedPerm!<s0,s,x,y!>()
+    fold replacedPerm{s0,s,x,y}()
     // Gobra can detect automatically that this call is ghost. In these cases, the `ghost` annotation is not necessary
-    wg.PayDebt(replacedPerm!<s0,s,x,y!>)
+    wg.PayDebt(replacedPerm{s0,s,x,y})
     wg.Done()
-    fold PredTrue!<!>()
+    fold PredTrue{}()
   }
 }
 
@@ -70,13 +70,13 @@ func SearchReplace(s []int, x, y int) {
   ghost s0 := toSeq(s)
   c := make(chan []int,4)
   var wg@ sync.WaitGroup
-  ghost pr := messagePerm!<&wg,_,x,y!>
-  c.Init(pr,PredTrue!<!>)
+  ghost pr := messagePerm{&wg,_,x,y}
+  c.Init(pr,PredTrue{})
   wg.Init()
   ghost seqs := seq[seq[int]] {}
   ghost pseqs := seq[pred()] {}
   invariant acc(c.RecvChannel(),_)
-  invariant c.RecvGivenPerm() == PredTrue!<!> && c.RecvGotPerm() == pr
+  invariant c.RecvGivenPerm() == PredTrue{} && c.RecvGotPerm() == pr
   for i := 0; i != workers; i++ {
     go worker(c,&wg,x,y)
   }
@@ -95,7 +95,7 @@ func SearchReplace(s []int, x, y int) {
     0 <= j && j < len(seqs[i]) ==> seqs[i][j] == s0[i * workRange + j]
   invariant len(pseqs) == len(seqs)
   invariant forall i int :: {pseqs[i]} 0 <= i && i < len(pseqs) ==>
-    pseqs[i] == replacedPerm!<seqs[i],s[i * workRange:i * workRange + len(seqs[i])],x,y!>
+    pseqs[i] == replacedPerm{seqs[i],s[i * workRange:i * workRange + len(seqs[i])],x,y}
   invariant forall i int :: 0 <= i && i < len(pseqs) ==> wg.TokenById(pseqs[i],i)
   for offset := 0; offset != len(s); {
     nextOffset := offset + workRange;
@@ -106,16 +106,16 @@ func SearchReplace(s []int, x, y int) {
     assert forall i int :: {&section[i]} 0 <= i && i < len(s) ==>
       &section[i] == &s[i + offset]
     ghost s1 := toSeq(section)
-    ghost wpr := replacedPerm!<s1,section,x,y!>
-    wg.Add(1,1/2,PredTrue!<!>)
+    ghost wpr := replacedPerm{s1,section,x,y}
+    wg.Add(1,1/2,PredTrue{})
     ghost if(offset == 0) {
-      wg.Start(1/2,PredTrue!<!>)
+      wg.Start(1/2,PredTrue{})
     }
     wg.GenerateTokenAndDebt(wpr)
     fold wg.TokenById(wpr,len(pseqs))
     seqs = seqs ++ seq[seq[int]]{ s1 }
     pseqs = pseqs ++ seq[pred()] { wpr }
-    fold messagePerm!<&wg,_,x,y!>(section)
+    fold messagePerm{&wg,_,x,y}(section)
     c <- section
     offset = nextOffset
   }
@@ -134,7 +134,7 @@ func SearchReplace(s []int, x, y int) {
       down := i * workRange
       up := down + len(seqs[i])
       s1 := s[down:up]
-      unfold replacedPerm!<seqs[i],s1,x,y!>()
+      unfold replacedPerm{seqs[i],s1,x,y}()
       assert forall j int :: {&s[j]} down <= j && j < up ==> &s[j] == &s1[j-down]
     }
   }
diff --git a/src/test/resources/regressions/examples/evaluation/parallel_sum.gobra b/src/test/resources/regressions/examples/evaluation/parallel_sum.gobra
index 9bd88a507..2bc74783e 100644
--- a/src/test/resources/regressions/examples/evaluation/parallel_sum.gobra
+++ b/src/test/resources/regressions/examples/evaluation/parallel_sum.gobra
@@ -19,11 +19,11 @@ requires acc(c) && acc(c.sum) && acc(c.m) && c.m.state == 0 && c.m.stema == 0
 requires *c.sum == 0
 requires forall i int :: 0 <= i && i < len(seenSlice) ==> acc(&seenSlice[i], 1/2)
 requires forall i int :: 0 <= i && i < len(seenSlice) ==> seenSlice[i] == 0
-ensures acc(c) && c.m.LockP() && c.m.LockInv() == (AccInv!<c.sum, seenSlice!>)
+ensures acc(c) && c.m.LockP() && c.m.LockInv() == (AccInv{c.sum, seenSlice})
 func (c *Accum) Init(ghost seenSlice ghost []int) {
 	assume GhostSum(seenSlice) == 0
-	fold AccInv!<c.sum, seenSlice!>()
-	c.m.SetInv(AccInv!<c.sum, seenSlice!>)
+	fold AccInv{c.sum, seenSlice}()
+	c.m.SetInv(AccInv{c.sum, seenSlice})
 }
 
 /* Creates a worker thread per element in the slice and concurrently computes the sum of all the elements */
@@ -52,19 +52,19 @@ func ParallelSum(s []int) (res int) {
 	// invariant i != 0 ==> acc(w.WaitGroupP(), 1/2) && acc(w.WaitGroupStarted(), 1/2)
 	invariant i > 0 ==> acc(w.WaitGroupP(), 1/2) && acc(w.WaitGroupStarted(), 1/2)
 	invariant forall i int :: 0 <= i && i < len(s) ==> acc(&s[i], 1/2)
-	invariant forall j int :: 0 <= j && j < i ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!>
+	invariant forall j int :: 0 <= j && j < i ==> tokens[j] == locHasVal{&seenSlice[j],s[j]}
 	invariant forall j int :: 0 <= j && j < i ==> w.TokenById(tokens[j], j)
 	invariant !w.WaitMode()
 	invariant acc(c, _)
-	invariant acc(c.m.LockP(), _) && c.m.LockInv() == AccInv!<c.sum, seenSlice!>
+	invariant acc(c.m.LockP(), _) && c.m.LockInv() == AccInv{c.sum, seenSlice}
 	invariant forall j int :: i <= j && j < n ==> acc(&seenSlice[j], 1/2)
 	invariant forall j int :: i <= j && j < n ==> seenSlice[j] == 0
 	for i := 0; i < n; i++ {
-		w.Add(1, 1/2, PredTrue!<!>)
+		w.Add(1, 1/2, PredTrue{})
 		ghost if i == 0 {
-			w.Start(1/2, PredTrue!<!>)
+			w.Start(1/2, PredTrue{})
 		}
-		tokens = tokens ++ seq[pred()]{ locHasVal!<&seenSlice[i], s[i]!> }
+		tokens = tokens ++ seq[pred()]{ locHasVal{&seenSlice[i], s[i]} }
 		w.GenerateTokenAndDebt(tokens[i])
 		fold w.TokenById(tokens[i], i)
 		go worker(w, c, s[i], seenSlice, i)
@@ -75,19 +75,19 @@ func ParallelSum(s []int) (res int) {
 	ghost {
 		invariant 0 <= i && i <= n
 		invariant forall j int :: 0 <= j && j < n ==> acc(&s[j], 1/2)
-		invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!>
+		invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal{&seenSlice[j],s[j]}
 		invariant forall j int :: 0 <= j && j < n ==> (j < i ? acc(&seenSlice[j], 1/2) && seenSlice[j] == s[j] : sync.InjEval(tokens[j], j))
 		decreases n - i
 		for i:=0; i < n; i++ {
 			unfold sync.InjEval(tokens[i], i)
-			unfold locHasVal!<&seenSlice[i],s[i]!>()
+			unfold locHasVal{&seenSlice[i],s[i]}()
 		}
 	}
 
 	c.m.Lock()
-	unfold AccInv!<c.sum, seenSlice!>()
+	unfold AccInv{c.sum, seenSlice}()
 	res = *(c.sum)
-	fold AccInv!<c.sum, seenSlice!>()
+	fold AccInv{c.sum, seenSlice}()
 	c.m.Unlock()
 	sumExtensional(s, seenSlice)
 
@@ -142,17 +142,17 @@ func update(ghost s ghost []int, ghost pos, val int) {
 
 requires acc(accum, _)
 requires acc(&seenSlice[pos], 1/2) && seenSlice[pos] == 0
-requires acc(accum.m.LockP(), _) && accum.m.LockInv() == AccInv!<accum.sum, seenSlice!>
+requires acc(accum.m.LockP(), _) && accum.m.LockInv() == AccInv{accum.sum, seenSlice}
 requires 0 <= pos && pos < len(seenSlice)
-requires w.UnitDebt(locHasVal!<&seenSlice[pos],val!>)
+requires w.UnitDebt(locHasVal{&seenSlice[pos],val})
 func worker(w *sync.WaitGroup, accum *Accum, val int, ghost seenSlice ghost []int, ghost pos int) {
 	accum.m.Lock()
-	unfold AccInv!<accum.sum, seenSlice!>()
+	unfold AccInv{accum.sum, seenSlice}()
 	*(accum.sum) += val
 	update(seenSlice, pos, val)
-	fold AccInv!<accum.sum, seenSlice!>()
+	fold AccInv{accum.sum, seenSlice}()
 	accum.m.Unlock()
-	fold locHasVal!<&seenSlice[pos],val!>()
-	w.PayDebt(locHasVal!<&seenSlice[pos],val!>)
+	fold locHasVal{&seenSlice[pos],val}()
+	w.PayDebt(locHasVal{&seenSlice[pos],val})
 	w.Done()
 }
\ No newline at end of file
diff --git a/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra b/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra
index 264cb680f..dcbc9ddcc 100644
--- a/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra
+++ b/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra
@@ -25,22 +25,22 @@ pred replacedPerm(ghost s0 seq[int], ghost s [] int, ghost x, y int) {
 
 pred messagePerm(ghost wg *sync.WaitGroup, s []int, ghost x, y int) {
   (forall i int :: 0 <= i && i < len(s) ==> acc(&s[i])) &&
-  wg.UnitDebt(replacedPerm!<toSeq(s),s,x,y!>)
+  wg.UnitDebt(replacedPerm{toSeq(s),s,x,y})
 }
 
 requires acc(c.RecvChannel(),_)
-requires c.RecvGivenPerm() == PredTrue!<!>
-requires c.RecvGotPerm() == messagePerm!<wg,_,x,y!>
+requires c.RecvGivenPerm() == PredTrue{}
+requires c.RecvGotPerm() == messagePerm{wg,_,x,y}
 func worker(c <- chan[]int, wg *sync.WaitGroup, x, y int) {
-  fold acc(PredTrue!<!>(),2/1);
-  invariant PredTrue!<!>() && acc(c.RecvChannel(),_)
-  invariant c.RecvGivenPerm() == PredTrue!<!>
+  fold acc(PredTrue{}(),2/1);
+  invariant PredTrue{}() && acc(c.RecvChannel(),_)
+  invariant c.RecvGivenPerm() == PredTrue{}
   // we forget to specify the channel's RecvGotPerm (needed due to black-box semantics of loops) (seeded bug):
-  // invariant c.RecvGotPerm() == messagePerm!<wg,_,x,y,!>
+  // invariant c.RecvGotPerm() == messagePerm{wg,_,x,y,}
   //:: ExpectedOutput(invariant_preservation_error:permission_error)
-  invariant ok ==> messagePerm!<wg,_,x,y!>(s)
+  invariant ok ==> messagePerm{wg,_,x,y}(s)
   for s, ok := <- c; ok; s, ok = <-c {
-    unfold messagePerm!<wg,_,x,y!>(s)
+    unfold messagePerm{wg,_,x,y}(s)
     ghost s0 := toSeq(s)
     invariant 0 <= i && i <= len(s)
     invariant forall j int :: 0 <= j && j < len(s) ==> acc(&s[j])
@@ -49,10 +49,10 @@ func worker(c <- chan[]int, wg *sync.WaitGroup, x, y int) {
     for i := 0; i != len(s); i++ {
       if(s[i] == x) { s[i] = y }
     }
-    fold replacedPerm!<s0,s,x,y!>()
-    wg.PayDebt(replacedPerm!<s0,s,x,y!>)
+    fold replacedPerm{s0,s,x,y}()
+    wg.PayDebt(replacedPerm{s0,s,x,y})
     wg.Done()
-    fold PredTrue!<!>()
+    fold PredTrue{}()
   }
 }
 
@@ -71,13 +71,13 @@ func SearchReplace(s []int, x, y int) {
   ghost s0 := toSeq(s)
   c := make(chan []int,4)
   var wg@ sync.WaitGroup
-  ghost pr := messagePerm!<&wg,_,x,y!>
-  c.Init(pr,PredTrue!<!>)
+  ghost pr := messagePerm{&wg,_,x,y}
+  c.Init(pr,PredTrue{})
   wg.Init()
   ghost seqs := seq[seq[int]] {}
   ghost pseqs := seq[pred()] {}
   invariant acc(c.RecvChannel(),_)
-  invariant c.RecvGivenPerm() == PredTrue!<!> && c.RecvGotPerm() == pr
+  invariant c.RecvGivenPerm() == PredTrue{} && c.RecvGotPerm() == pr
   for i := 0; i != workers; i++ {
     go worker(c,&wg,x,y)
   }
@@ -96,7 +96,7 @@ func SearchReplace(s []int, x, y int) {
     0 <= j && j < len(seqs[i]) ==> seqs[i][j] == s0[i * workRange + j]
   invariant len(pseqs) == len(seqs)
   invariant forall i int :: {pseqs[i]} 0 <= i && i < len(pseqs) ==>
-    pseqs[i] == replacedPerm!<seqs[i],s[i * workRange:i * workRange + len(seqs[i])],x,y!>
+    pseqs[i] == replacedPerm{seqs[i],s[i * workRange:i * workRange + len(seqs[i])],x,y}
   invariant forall i int :: 0 <= i && i < len(pseqs) ==> wg.TokenById(pseqs[i],i)
   for offset := 0; offset != len(s); {
     nextOffset := offset + workRange;
@@ -107,16 +107,16 @@ func SearchReplace(s []int, x, y int) {
     assert forall i int :: {&section[i]} 0 <= i && i < len(s) ==>
       &section[i] == &s[i + offset]
     ghost s1 := toSeq(section)
-    ghost wpr := replacedPerm!<s1,section,x,y!>
-    wg.Add(1,1/2,PredTrue!<!>)
+    ghost wpr := replacedPerm{s1,section,x,y}
+    wg.Add(1,1/2,PredTrue{})
     ghost if(offset == 0) {
-      wg.Start(1/2,PredTrue!<!>)
+      wg.Start(1/2,PredTrue{})
     }
     wg.GenerateTokenAndDebt(wpr)
     fold wg.TokenById(wpr,len(pseqs))
     seqs = seqs ++ seq[seq[int]]{ s1 }
     pseqs = pseqs ++ seq[pred()] { wpr }
-    fold messagePerm!<&wg,_,x,y!>(section)
+    fold messagePerm{&wg,_,x,y}(section)
     c <- section
     offset = nextOffset
   }
@@ -135,7 +135,7 @@ func SearchReplace(s []int, x, y int) {
       down := i * workRange
       up := down + len(seqs[i])
       s1 := s[down:up]
-      unfold replacedPerm!<seqs[i],s1,x,y!>()
+      unfold replacedPerm{seqs[i],s1,x,y}()
       assert forall j int :: {&s[j]} down <= j && j < up ==> &s[j] == &s1[j-down]
     }
   }
diff --git a/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra b/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra
index dcec71c89..8c77adc4f 100644
--- a/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra
+++ b/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra
@@ -19,11 +19,11 @@ requires acc(c) && acc(c.sum) && acc(c.m) && c.m.state == 0 && c.m.stema == 0
 requires *c.sum == 0
 requires forall i int :: 0 <= i && i < len(seenSlice) ==> acc(&seenSlice[i], 1/2)
 requires forall i int :: 0 <= i && i < len(seenSlice) ==> seenSlice[i] == 0
-ensures acc(c) && c.m.LockP() && c.m.LockInv() == (AccInv!<c.sum, seenSlice!>)
+ensures acc(c) && c.m.LockP() && c.m.LockInv() == (AccInv{c.sum, seenSlice})
 func (c *Accum) Init(ghost seenSlice ghost []int) {
 	assume GhostSum(seenSlice) == 0
-	fold AccInv!<c.sum, seenSlice!>()
-	c.m.SetInv(AccInv!<c.sum, seenSlice!>)
+	fold AccInv{c.sum, seenSlice}()
+	c.m.SetInv(AccInv{c.sum, seenSlice})
 }
 
 /* Creates a worker thread per element in the slice and concurrently computes the sum of all the elements */
@@ -52,19 +52,19 @@ func ParallelSum(s []int) (res int) {
 	// invariant i != 0 ==> acc(w.WaitGroupP(), 1/2) && acc(w.WaitGroupStarted(), 1/2)
 	invariant i > 0 ==> acc(w.WaitGroupP(), 1/2) && acc(w.WaitGroupStarted(), 1/2)
 	invariant forall i int :: 0 <= i && i < len(s) ==> acc(&s[i], 1/2)
-	invariant forall j int :: 0 <= j && j < i ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!>
+	invariant forall j int :: 0 <= j && j < i ==> tokens[j] == locHasVal{&seenSlice[j],s[j]}
 	invariant forall j int :: 0 <= j && j < i ==> w.TokenById(tokens[j], j)
 	invariant !w.WaitMode()
 	invariant acc(c, _)
-	invariant acc(c.m.LockP(), _) && c.m.LockInv() == AccInv!<c.sum, seenSlice!>
+	invariant acc(c.m.LockP(), _) && c.m.LockInv() == AccInv{c.sum, seenSlice}
 	invariant forall j int :: i <= j && j < n ==> acc(&seenSlice[j], 1/2)
 	invariant forall j int :: i <= j && j < n ==> seenSlice[j] == 0
 	for i := 0; i < n; i++ {
-		w.Add(1, 1/2, PredTrue!<!>)
+		w.Add(1, 1/2, PredTrue{})
 		ghost if i == 0 {
-			w.Start(1/2, PredTrue!<!>)
+			w.Start(1/2, PredTrue{})
 		}
-		tokens = tokens ++ seq[pred()]{ locHasVal!<&seenSlice[i], s[i]!> }
+		tokens = tokens ++ seq[pred()]{ locHasVal{&seenSlice[i], s[i]} }
 		w.GenerateTokenAndDebt(tokens[i])
 		fold w.TokenById(tokens[i], i)
 		go worker(w, c, s[i], seenSlice, i)
@@ -75,19 +75,19 @@ func ParallelSum(s []int) (res int) {
 	ghost {
 		invariant 0 <= i && i <= n
 		invariant forall j int :: 0 <= j && j < n ==> acc(&s[j], 1/2)
-		invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!>
+		invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal{&seenSlice[j],s[j]}
 		invariant forall j int :: 0 <= j && j < n ==> (j < i ? acc(&seenSlice[j], 1/2) && seenSlice[j] == s[j] : sync.InjEval(tokens[j], j))
 		decreases n - i
 		for i:=0; i < n; i++ {
 			unfold sync.InjEval(tokens[i], i)
-			unfold locHasVal!<&seenSlice[i],s[i]!>()
+			unfold locHasVal{&seenSlice[i],s[i]}()
 		}
 	}
 
 	c.m.Lock()
-	unfold AccInv!<c.sum, seenSlice!>()
+	unfold AccInv{c.sum, seenSlice}()
 	res = *(c.sum)
-	fold AccInv!<c.sum, seenSlice!>()
+	fold AccInv{c.sum, seenSlice}()
 	c.m.Unlock()
 	sumExtensional(s, seenSlice)
 	return res
@@ -141,19 +141,19 @@ func update(ghost s ghost []int, ghost pos, val int) {
 
 requires acc(accum, _)
 requires acc(&seenSlice[pos], 1/2) && seenSlice[pos] == 0
-requires acc(accum.m.LockP(), _) && accum.m.LockInv() == AccInv!<accum.sum, seenSlice!>
+requires acc(accum.m.LockP(), _) && accum.m.LockInv() == AccInv{accum.sum, seenSlice}
 requires 0 <= pos && pos < len(seenSlice)
 // we forget to specify the worker's debt (seeded bug):
-// requires w.UnitDebt(locHasVal!<&seenSlice[pos],val!>)
+// requires w.UnitDebt(locHasVal{&seenSlice[pos],val})
 func worker(w *sync.WaitGroup, accum *Accum, val int, ghost seenSlice ghost []int, ghost pos int) {
 	accum.m.Lock()
-	unfold AccInv!<accum.sum, seenSlice!>()
+	unfold AccInv{accum.sum, seenSlice}()
 	*(accum.sum) += val
 	update(seenSlice, pos, val)
-	fold AccInv!<accum.sum, seenSlice!>()
+	fold AccInv{accum.sum, seenSlice}()
 	accum.m.Unlock()
-	fold locHasVal!<&seenSlice[pos],val!>()
+	fold locHasVal{&seenSlice[pos],val}()
 	//:: ExpectedOutput(precondition_error:permission_error)
-	w.PayDebt(locHasVal!<&seenSlice[pos],val!>)
+	w.PayDebt(locHasVal{&seenSlice[pos],val})
 	w.Done()
 }
\ No newline at end of file
diff --git a/src/test/resources/regressions/examples/parallel_search_replace_shared.gobra b/src/test/resources/regressions/examples/parallel_search_replace_shared.gobra
index 4d6d9e510..8b983096d 100644
--- a/src/test/resources/regressions/examples/parallel_search_replace_shared.gobra
+++ b/src/test/resources/regressions/examples/parallel_search_replace_shared.gobra
@@ -30,28 +30,28 @@ pred replacedPerm(ghost s0 seq[int], ghost s [] int, ghost x, y int) {
 
 pred messagePerm(ghost wg *sync.WaitGroup, s []int, ghost x, y int) {
   (forall i int :: 0 <= i && i < len(s) ==> acc(&s[i])) &&
-  wg.UnitDebt(replacedPerm!<toSeq(s),s,x,y!>)
+  wg.UnitDebt(replacedPerm{toSeq(s),s,x,y})
 }
 
 requires acc(c.RecvChannel(),_)
-requires c.RecvGivenPerm() == PredTrue!<!>;
-requires c.RecvGotPerm() == messagePerm!<wg,_,x,y!>;
+requires c.RecvGivenPerm() == PredTrue{};
+requires c.RecvGotPerm() == messagePerm{wg,_,x,y};
 func worker(c <- chan[]int, wg *sync.WaitGroup, x, y int) {
   share c, wg, x, y
-  fold acc(PredTrue!<!>(),2/1);
-  // assert c.RecvGivenPerm() == PredTrue!<!>;
+  fold acc(PredTrue{}(),2/1);
+  // assert c.RecvGivenPerm() == PredTrue{};
   invariant acc(&c, 1/2) && acc(&wg, 1/2) &&acc(&s) && acc(&ok) && acc(&x, 1/2) && acc(&y, 1/2)
-  invariant PredTrue!<!>() && acc(c.RecvChannel(),_)
-  invariant c.RecvGivenPerm() == PredTrue!<!>;
-  invariant c.RecvGotPerm() == messagePerm!<wg,_,x,y,!>;
-  invariant ok ==> messagePerm!<wg,_,x,y!>(s)
+  invariant PredTrue{}() && acc(c.RecvChannel(),_)
+  invariant c.RecvGivenPerm() == PredTrue{};
+  invariant c.RecvGotPerm() == messagePerm{wg,_,x,y,};
+  invariant ok ==> messagePerm{wg,_,x,y}(s)
   for s@, ok@ := <- c; ok; s, ok = <-c {
-    unfold messagePerm!<wg,_,x,y!>(s)
+    unfold messagePerm{wg,_,x,y}(s)
     ghost s0 := toSeq(s)
     invariant acc(&c, 1/4) && acc(&wg, 1/4) && acc(&x, 1/4) && acc(&y, 1/4) && acc(&s)
     invariant len(s0) == len(s)
     invariant acc(c.RecvChannel(),_)
-    invariant wg.UnitDebt(replacedPerm!<s0,s,x,y!>)
+    invariant wg.UnitDebt(replacedPerm{s0,s,x,y})
     invariant 0 <= i && i <= len(s)
     invariant forall j int :: 0 <= j && j < len(s) ==> acc(&s[j])
     invariant forall j int :: {s[j]} 0 <= j && j < len(s) ==>
@@ -59,11 +59,11 @@ func worker(c <- chan[]int, wg *sync.WaitGroup, x, y int) {
     for i := 0; i != len(s); i++ {
       if(s[i] == x) { s[i] = y }
     }
-    fold replacedPerm!<s0,s,x,y!>()
-    wg.PayDebt(replacedPerm!<s0,s,x,y!>)
+    fold replacedPerm{s0,s,x,y}()
+    wg.PayDebt(replacedPerm{s0,s,x,y})
     wg.Done()
-    fold PredTrue!<!>()
-    // assert c.RecvGivenPerm() == PredTrue!<!>;
+    fold PredTrue{}()
+    // assert c.RecvGivenPerm() == PredTrue{};
   }
 }
 
@@ -82,13 +82,13 @@ func SearchReplace(s []int, x, y int) {
   ghost s0 := toSeq(s)
   c := make(chan []int,4)
   var wg@ sync.WaitGroup
-  ghost pr := messagePerm!<&wg,_,x,y!>;
-  c.Init(pr,PredTrue!<!>)
+  ghost pr := messagePerm{&wg,_,x,y};
+  c.Init(pr,PredTrue{})
   wg.Init()
   ghost seqs := seq[seq[int]] {}
   ghost pseqs := seq[pred()] {}
   invariant acc(c.RecvChannel(),_)
-  invariant c.RecvGivenPerm() == PredTrue!<!> && c.RecvGotPerm() == pr
+  invariant c.RecvGivenPerm() == PredTrue{} && c.RecvGotPerm() == pr
   for i := 0; i != workers; i++ {
     go worker(c,&wg,x,y)
   }
@@ -107,7 +107,7 @@ func SearchReplace(s []int, x, y int) {
     0 <= j && j < len(seqs[i]) ==> seqs[i][j] == s0[i * workRange + j]
   invariant len(pseqs) == len(seqs)
   invariant forall i int :: {pseqs[i]} 0 <= i && i < len(pseqs) ==>
-    pseqs[i] == replacedPerm!<seqs[i],s[i * workRange:i * workRange + len(seqs[i])],x,y!>;
+    pseqs[i] == replacedPerm{seqs[i],s[i * workRange:i * workRange + len(seqs[i])],x,y};
   invariant forall i int :: 0 <= i && i < len(pseqs) ==> wg.TokenById(pseqs[i],i)
   for offset := 0; offset != len(s); {
     nextOffset := offset + workRange;
@@ -118,16 +118,16 @@ func SearchReplace(s []int, x, y int) {
     assert forall i int :: {&section[i]} 0 <= i && i < len(s) ==>
       &section[i] == &s[i + offset]
     ghost s1 := toSeq(section)
-    ghost wpr := replacedPerm!<s1,section,x,y!>;
-    wg.Add(1,1/2,PredTrue!<!>)
+    ghost wpr := replacedPerm{s1,section,x,y};
+    wg.Add(1,1/2,PredTrue{})
     ghost if(offset == 0) {
-      wg.Start(1/2,PredTrue!<!>)
+      wg.Start(1/2,PredTrue{})
     }
     wg.GenerateTokenAndDebt(wpr)
     fold wg.TokenById(wpr,len(pseqs))
     seqs = seqs ++ seq[seq[int]]{ s1 }
     pseqs = pseqs ++ seq[pred()] { wpr }
-    fold messagePerm!<&wg,_,x,y!>(section)
+    fold messagePerm{&wg,_,x,y}(section)
     c <- section
     offset = nextOffset
   }
@@ -146,7 +146,7 @@ func SearchReplace(s []int, x, y int) {
       down := i * workRange
       up := down + len(seqs[i])
       s1 := s[down:up]
-      unfold replacedPerm!<seqs[i],s1,x,y!>()
+      unfold replacedPerm{seqs[i],s1,x,y}()
       assert forall j int :: {&s[j]} down <= j && j < up ==> &s[j] == &s1[j-down]
     }
   }
diff --git a/src/test/resources/regressions/examples/tutorial-examples/channels.gobra b/src/test/resources/regressions/examples/tutorial-examples/channels.gobra
index d21f806df..7a9924384 100644
--- a/src/test/resources/regressions/examples/tutorial-examples/channels.gobra
+++ b/src/test/resources/regressions/examples/tutorial-examples/channels.gobra
@@ -9,19 +9,19 @@ pred sendInvariant(v *int) {
 
 requires acc(c.SendChannel(), 1/2)
 requires acc(c.RecvChannel(), 1/2)
-requires c.SendGivenPerm() == sendInvariant!<_!>
-requires c.SendGotPerm() == PredTrue!<!>
-requires c.RecvGivenPerm() == PredTrue!<!>
-requires c.RecvGotPerm() == sendInvariant!<_!>
+requires c.SendGivenPerm() == sendInvariant{_}
+requires c.SendGotPerm() == PredTrue{}
+requires c.RecvGivenPerm() == PredTrue{}
+requires c.RecvGotPerm() == sendInvariant{_}
 func incChannel(c chan *int) {
-	fold PredTrue!<!>()
+	fold PredTrue{}()
 	res, ok := <- c
 	if (ok) {
-		unfold sendInvariant!<_!>(res)
+		unfold sendInvariant{_}(res)
 		// we now have write access after unfolding the invariant:
 		*res = *res + 1
 		// fold the invariant and send pointer and permission back:
-		fold sendInvariant!<_!>(res)
+		fold sendInvariant{_}(res)
 		c <- res
 	}
 }
@@ -31,16 +31,16 @@ func clientChannel() {
 
 	var x@ int = 42
 	var p *int = &x
-	c.Init(sendInvariant!<_!>, PredTrue!<!>)
+	c.Init(sendInvariant{_}, PredTrue{})
 	go incChannel(c)
 	assert *p == 42
-	fold sendInvariant!<_!>(p)
+	fold sendInvariant{_}(p)
 	c <- p
 
-	fold PredTrue!<!>()
+	fold PredTrue{}()
 	res, ok := <- c
 	if (ok) {
-		unfold sendInvariant!<_!>(res)
+		unfold sendInvariant{_}(res)
 		assert *res > 0
 		// we have regained write access:
 		*res = 1
diff --git a/src/test/resources/regressions/examples/tutorial-examples/multi-channel.gobra b/src/test/resources/regressions/examples/tutorial-examples/multi-channel.gobra
index af5389957..1b8df0ad4 100644
--- a/src/test/resources/regressions/examples/tutorial-examples/multi-channel.gobra
+++ b/src/test/resources/regressions/examples/tutorial-examples/multi-channel.gobra
@@ -12,39 +12,39 @@ pred answer(x int,y * int,r int) { acc(y) && *y == x + 1 && r == x * x }
 pred isQuery(q query) {
 	acc(q.loc) &&
 	acc(q.ret.SendChannel(),_) &&
-	q.ret.SendGotPerm() == PredTrue!<!> &&
-	q.ret.SendGivenPerm() == answer!<*q.loc,q.loc,_!>
+	q.ret.SendGotPerm() == PredTrue{} &&
+	q.ret.SendGivenPerm() == answer{*q.loc,q.loc,_}
 }
 
 pred QueryHandler(c chan <- query) {
 	acc(c.SendChannel(),_) &&
-	c.SendGotPerm() == PredTrue!<!> &&
-	c.SendGivenPerm() == isQuery!<_!>
+	c.SendGotPerm() == PredTrue{} &&
+	c.SendGivenPerm() == isQuery{_}
 }
 
 pred ResultHandler(h <- chan int,x int,y * int) {
 	acc(h.RecvChannel(),_) &&
-	h.RecvGivenPerm() == PredTrue!<!> &&
-	h.RecvGotPerm() == answer!<x,y,_!>
+	h.RecvGivenPerm() == PredTrue{} &&
+	h.RecvGotPerm() == answer{x,y,_}
 }
 
 requires acc(c.RecvChannel(),_)
-requires c.RecvGivenPerm() == PredTrue!<!>
-requires c.RecvGotPerm() == isQuery!<_!>
+requires c.RecvGivenPerm() == PredTrue{}
+requires c.RecvGotPerm() == isQuery{_}
 func slave(c <- chan query) {
-	fold acc(PredTrue!<!>(),2/1);
-	invariant PredTrue!<!>() && acc(c.RecvChannel(),_)
-	invariant c.RecvGivenPerm() == PredTrue!<!>
-	invariant c.RecvGotPerm() == isQuery!<_!>
-	invariant ok ==> isQuery!<_!>(q)
+	fold acc(PredTrue{}(),2/1);
+	invariant PredTrue{}() && acc(c.RecvChannel(),_)
+	invariant c.RecvGivenPerm() == PredTrue{}
+	invariant c.RecvGotPerm() == isQuery{_}
+	invariant ok ==> isQuery{_}(q)
 	for q, ok := <-c; ok; q, ok = <-c {
-		unfold isQuery!<_!>(q);
+		unfold isQuery{_}(q);
 		y := *q.loc
 		r := y * y
 		*q.loc = y+1
-		fold answer!<y,q.loc,_!>(r)
+		fold answer{y,q.loc,_}(r)
 		q.ret <- r
-		fold PredTrue!<!>()
+		fold PredTrue{}()
 	}
 }
 
@@ -53,10 +53,10 @@ ensures ResultHandler(handler,old(*x),x)
 func MakeQuery(c chan <- query,x * int) (handler <- chan int) {
 	unfold acc(QueryHandler(c),_)
 	h0 := make(chan int)
-	h0.Init(answer!<*x,x,_!>,PredTrue!<!>)
+	h0.Init(answer{*x,x,_},PredTrue{})
 	handler = h0
 	q := query{ret:h0,loc:x}
-	fold isQuery!<_!>(q)
+	fold isQuery{_}(q)
 	c <- q
 	fold ResultHandler(h0, old(*x), x)
 }
@@ -65,10 +65,10 @@ requires ResultHandler(handler,x,y)
 ensures acc(y) && *y == x + 1 && r == x * x
 func GetResult(handler <- chan int,ghost x int,ghost y * int) (r int) {
 	unfold ResultHandler(handler,x,y)
-	fold PredTrue!<!>()
+	fold PredTrue{}()
 	r0, ok := <-handler
 	assume ok
-	unfold answer!<x,y,_!>(r0)
+	unfold answer{x,y,_}(r0)
 	r = r0
 }
 
@@ -76,10 +76,10 @@ requires k > 0
 ensures QueryHandler(c)
 func MakeServer(k int) (c chan <- query) {
 	c0 := make(chan query)
-	c0.Init(isQuery!<_!>,PredTrue!<!>)
+	c0.Init(isQuery{_},PredTrue{})
 	invariant acc(c0.RecvChannel(),_)
-	invariant c0.RecvGivenPerm() == PredTrue!<!>
-	invariant c0.RecvGotPerm() == isQuery!<_!>
+	invariant c0.RecvGivenPerm() == PredTrue{}
+	invariant c0.RecvGotPerm() == isQuery{_}
 	for i := 0; i != k; i++ {
 		go slave(c0)
 	}
diff --git a/src/test/resources/regressions/examples/tutorial-examples/mutex.gobra b/src/test/resources/regressions/examples/tutorial-examples/mutex.gobra
index 62e93811c..0ba1d59ae 100644
--- a/src/test/resources/regressions/examples/tutorial-examples/mutex.gobra
+++ b/src/test/resources/regressions/examples/tutorial-examples/mutex.gobra
@@ -9,21 +9,21 @@ pred mutexInvariant(x *int) {
 	acc(x)
 }
 
-requires acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant!<x!>
-ensures  acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant!<x!>
+requires acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant{x}
+ensures  acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant{x}
 func safeInc(pmutex *sync.Mutex, x *int) {
 	pmutex.Lock()
-	unfold mutexInvariant!<x!>()
+	unfold mutexInvariant{x}()
 	*x = *x + 1
-	fold mutexInvariant!<x!>()
+	fold mutexInvariant{x}()
 	pmutex.Unlock()
 }
 
 func client() {
 	x@ := 0
 	mutex@ := sync.Mutex{}
-	fold mutexInvariant!<&x!>()
-	(&mutex).SetInv(mutexInvariant!<&x!>)
+	fold mutexInvariant{&x}()
+	(&mutex).SetInv(mutexInvariant{&x})
 	go safeInc(&mutex, &x)
 	go safeInc(&mutex, &x)
 }
diff --git a/src/test/resources/regressions/features/channels/channel-fail4.gobra b/src/test/resources/regressions/features/channels/channel-fail4.gobra
index 0f36715ba..ad2859f84 100644
--- a/src/test/resources/regressions/features/channels/channel-fail4.gobra
+++ b/src/test/resources/regressions/features/channels/channel-fail4.gobra
@@ -14,13 +14,13 @@ pred testPredicate(p int)
 func closeWrongArgTypes(c chan int) {
     // last argument has to be of type `pred()`
     //:: ExpectedOutput(type_error)
-    close(c, 1, 2, testPredicate!<_!>)
+    close(c, 1, 2, testPredicate{_})
 }
 
 func closeGhostChannel(ghost c chan int) {
     // channel has to be of actual type
     //:: ExpectedOutput(type_error)
-    close(c, 1, 2, testPredicate!<0!>)
+    close(c, 1, 2, testPredicate{0})
 }
 
 func initWithWrongArgType() {
@@ -29,7 +29,7 @@ func initWithWrongArgType() {
   // and reported (i.e. without crashing Gobra)
   c := make(chan int, 1) // make a buffered channel
   //:: ExpectedOutput(type_error)
-  c.Init(1, testPredicate!<_!>, PredTrue!<!>, PredTrue!<!>, testPredicate!<_!>)
+  c.Init(1, testPredicate{_}, PredTrue{}, PredTrue{}, testPredicate{_})
   //:: ExpectedOutput(type_error)
-  c.Init(1, testPredicate!<_!>)
+  c.Init(1, testPredicate{_})
 }
diff --git a/src/test/resources/regressions/features/channels/channel-fail5.gobra b/src/test/resources/regressions/features/channels/channel-fail5.gobra
index 1bed4e56f..f086833ee 100644
--- a/src/test/resources/regressions/features/channels/channel-fail5.gobra
+++ b/src/test/resources/regressions/features/channels/channel-fail5.gobra
@@ -14,9 +14,9 @@ pred customTrue() {
 func initBufferedChannelWithWrongPredicates() {
   c0 := make(chan int, 0) // make an unbuffered channel
   // if it's an unbuffered channel one can use arbitrary predicate expressions as SendGotPerm and RecvGivenPerm
-  c0.Init(vIsOne!<_!>, customTrue!<!>)
+  c0.Init(vIsOne{_}, customTrue{})
   c1 := make(chan int, 1) // make a buffered channel
   // however, this is not possible if the channel is buffered:
   //:: ExpectedOutput(precondition_error:assertion_error)
-  c1.Init(vIsOne!<_!>, customTrue!<!>)
+  c1.Init(vIsOne{_}, customTrue{})
 }
diff --git a/src/test/resources/regressions/features/channels/channel-fail6.gobra b/src/test/resources/regressions/features/channels/channel-fail6.gobra
index 605e476ef..30e48e4bb 100644
--- a/src/test/resources/regressions/features/channels/channel-fail6.gobra
+++ b/src/test/resources/regressions/features/channels/channel-fail6.gobra
@@ -12,20 +12,20 @@ requires c.IsChannel() && c.BufferSize() == 1
 func testDependentBuiltInMembers(c chan int) {
     // PredTrue, SendChannel, RecvChannel, SendGivenPerm, SendGotPerm, RecvGivenPerm, and RecvGotPerm members have to be generated
 
-    // Init cannot be called since equality of sendInvariant!<42!> and PredTrue!<!> cannot be proved
+    // Init cannot be called since equality of sendInvariant{42} and PredTrue{} cannot be proved
     //:: ExpectedOutput(precondition_error:assertion_error)
-    c.Init(sendInvariant!<_!>, sendInvariant!<42!>)
+    c.Init(sendInvariant{_}, sendInvariant{42})
 }
 
 requires c.IsChannel() // c.BufferSize() is not specified
 func testInitWithoutBufferSize(c chan int) {
-    // as the buffer size is unknown, the second argument has to be equal to PredTrue!<!> (same situation as in the functio above)
+    // as the buffer size is unknown, the second argument has to be equal to PredTrue{} (same situation as in the functio above)
     //:: ExpectedOutput(precondition_error:assertion_error)
-    c.Init(sendInvariant!<_!>, sendInvariant!<42!>)
+    c.Init(sendInvariant{_}, sendInvariant{42})
 }
 
 requires c.IsChannel() && c.BufferSize() == 0
 func testInitWithBufferSize0(c chan int) {
     // any predicate expression can be used as second argument as it is known that the channel has buffer size 0
-    c.Init(sendInvariant!<_!>, sendInvariant!<42!>)
+    c.Init(sendInvariant{_}, sendInvariant{42})
 }
diff --git a/src/test/resources/regressions/features/channels/channel-simple-buffered1.gobra b/src/test/resources/regressions/features/channels/channel-simple-buffered1.gobra
index b7d67d1ab..191d16b0a 100644
--- a/src/test/resources/regressions/features/channels/channel-simple-buffered1.gobra
+++ b/src/test/resources/regressions/features/channels/channel-simple-buffered1.gobra
@@ -9,22 +9,22 @@ pred vIsOne(v int) {
 
 func main() {
   c := make(chan int, 1) // make a buffered channel
-  c.Init(vIsOne!<_!>, PredTrue!<!>)
+  c.Init(vIsOne{_}, PredTrue{})
   go foo(1, c)
 
-  fold PredTrue!<!>()
+  fold PredTrue{}()
   res, ok := <- c
   if (ok) {
-    unfold vIsOne!<_!>(res)
+    unfold vIsOne{_}(res)
     assert res == 1
   }
 }
 
 requires acc(c.SendChannel(), 1/2)
-requires c.SendGivenPerm() == vIsOne!<_!>
-requires c.SendGotPerm() == PredTrue!<!>
+requires c.SendGivenPerm() == vIsOne{_}
+requires c.SendGotPerm() == PredTrue{}
 requires v == 1
 func foo(v int, c chan int) {
-    fold vIsOne!<_!>(v)
+    fold vIsOne{_}(v)
     c <- v
 }
diff --git a/src/test/resources/regressions/features/channels/channel-simple-buffered2.gobra b/src/test/resources/regressions/features/channels/channel-simple-buffered2.gobra
index 1e22611ba..08e70b54d 100644
--- a/src/test/resources/regressions/features/channels/channel-simple-buffered2.gobra
+++ b/src/test/resources/regressions/features/channels/channel-simple-buffered2.gobra
@@ -13,26 +13,26 @@ pred dummy(i int) {
 
 func main() {
   c := make(chan int, 1) // make a buffered channel
-  c.Init(dummy!<_!>, PredTrue!<!>)
+  c.Init(dummy{_}, PredTrue{})
 
   var x@ int = 0
   var p *int = &x
   assert acc(p)
-  fold someLocation!<p!>()
+  fold someLocation{p}()
 
   // split someLocation{p}() into ClosureDebt and Token:
-  c.CreateDebt(1, 2 /* 1/2 */, someLocation!<p!>)
+  c.CreateDebt(1, 2 /* 1/2 */, someLocation{p})
 
   // start a separate thread to send a value back to us
   go foo(c, p)
 
   // receive will fail since other thread never sends something (however this cannot be proven right now)
-  fold PredTrue!<!>()
+  fold PredTrue{}()
   res, ok := <- c
   if (!ok) {
     // use Token from `DebtRedistribution` to regain access to p
-    c.Redeem(someLocation!<p!>)
-    unfold someLocation!<p!>()
+    c.Redeem(someLocation{p})
+    unfold someLocation{p}()
     // do something with p:
     *p = 42
     //:: ExpectedOutput(assert_error:assertion_error)
@@ -41,16 +41,16 @@ func main() {
 }
 
 requires acc(c.SendChannel(), 1/2)
-requires c.SendGivenPerm() == dummy!<_!>
-requires c.SendGotPerm() == PredTrue!<!>
-requires someLocation!<p!>()
-requires c.ClosureDebt(someLocation!<p!>, 1, 2 /* 1/2 */)
+requires c.SendGivenPerm() == dummy{_}
+requires c.SendGotPerm() == PredTrue{}
+requires someLocation{p}()
+requires c.ClosureDebt(someLocation{p}, 1, 2 /* 1/2 */)
 func foo(c chan int, p *int) {
-    unfold someLocation!<p!>()
+    unfold someLocation{p}()
     *p = 1234
-    fold someLocation!<p!>()
+    fold someLocation{p}()
 
     // close channel
-    close(c, 1, 2 /* 1/2 */, someLocation!<p!>)
+    close(c, 1, 2 /* 1/2 */, someLocation{p})
     assert c.Closed()
 }
diff --git a/src/test/resources/regressions/features/channels/channel-simple5.gobra b/src/test/resources/regressions/features/channels/channel-simple5.gobra
index a74da1d48..21624795c 100644
--- a/src/test/resources/regressions/features/channels/channel-simple5.gobra
+++ b/src/test/resources/regressions/features/channels/channel-simple5.gobra
@@ -9,22 +9,22 @@ pred vIsOne(v int) {
 
 func main() {
   c := make(chan int)
-  c.Init(vIsOne!<_!>, PredTrue!<!>)
+  c.Init(vIsOne{_}, PredTrue{})
   go foo(1, c)
 
-  fold PredTrue!<!>()
+  fold PredTrue{}()
   res, ok := <- c
   if (ok) {
-    unfold vIsOne!<_!>(res)
+    unfold vIsOne{_}(res)
     assert res == 1
   }
 }
 
 requires acc(c.SendChannel(), 1/2)
-requires c.SendGivenPerm() == vIsOne!<_!>
-requires c.SendGotPerm() == PredTrue!<!>
+requires c.SendGivenPerm() == vIsOne{_}
+requires c.SendGotPerm() == PredTrue{}
 requires v == 1
 func foo(v int, c chan int) {
-    fold vIsOne!<_!>(v)
+    fold vIsOne{_}(v)
     c <- v
 }
diff --git a/src/test/resources/regressions/features/channels/channel-simple6.gobra b/src/test/resources/regressions/features/channels/channel-simple6.gobra
index 20e0ef849..5e9282182 100644
--- a/src/test/resources/regressions/features/channels/channel-simple6.gobra
+++ b/src/test/resources/regressions/features/channels/channel-simple6.gobra
@@ -19,27 +19,27 @@ func main() {
 
   // set channel invariants
   assert c.IsChannel()
-  assert c.BufferSize() > 0 ==> PredTrue!<!> == PredTrue!<!>
-  c.Init(vIsOne!<_!>, PredTrue!<!>)
+  assert c.BufferSize() > 0 ==> PredTrue{} == PredTrue{}
+  c.Init(vIsOne{_}, PredTrue{})
   assert c.SendChannel() && c.RecvChannel()
-  assert c.SendGivenPerm() == vIsOne!<_!> && c.SendGotPerm() == PredTrue!<!>
-  assert c.RecvGivenPerm() == PredTrue!<!> && c.RecvGotPerm() == vIsOne!<_!>
+  assert c.SendGivenPerm() == vIsOne{_} && c.SendGotPerm() == PredTrue{}
+  assert c.RecvGivenPerm() == PredTrue{} && c.RecvGotPerm() == vIsOne{_}
 
   var x@ int = 0
   var p *int = &x
   assert acc(p)
-  fold someLocation!<p!>()
+  fold someLocation{p}()
 
   // split someLocation{p}() into ClosureDebt and Token:
-  assert someLocation!<p!>()
-  c.CreateDebt(1, 2 /* 1/2 */, someLocation!<p!>)
-  assert c.ClosureDebt(someLocation!<p!>, 1, 2 /* 1/2 */) && c.Token(someLocation!<p!>)
+  assert someLocation{p}()
+  c.CreateDebt(1, 2 /* 1/2 */, someLocation{p})
+  assert c.ClosureDebt(someLocation{p}, 1, 2 /* 1/2 */) && c.Token(someLocation{p})
 
   // start a separate thread to send a value back to us
   go foo(1, c, p)
 
   // receive from channel:
-  fold PredTrue!<!>()
+  fold PredTrue{}()
   assert acc(c.RecvChannel(), _) && c.RecvGivenPerm()()
   res, ok := <- c
   assert c.RecvChannel()
@@ -47,12 +47,12 @@ func main() {
   assert !ok ==> c.Closed() && res == 0
   // first receive should succeed (but we cannot prove it)
   if (ok) {
-    unfold vIsOne!<_!>(res)
+    unfold vIsOne{_}(res)
     assert res == 1
   }
 
   // receive a second time from the channel:
-  fold PredTrue!<!>()
+  fold PredTrue{}()
   assert acc(c.RecvChannel(), _) && c.RecvGivenPerm()()
   res, ok := <- c
   assert c.RecvChannel()
@@ -61,38 +61,38 @@ func main() {
   // second receive should definitely fail (but we cannot prove it)
   if (!ok) {
     // use Token from `DebtRedistribution` to regain access to p
-    assert c.Token(someLocation!<p!>)
+    assert c.Token(someLocation{p})
     assert acc(c.Closed(), _)
-    c.Redeem(someLocation!<p!>)
-    assert someLocation!<p!>()
+    c.Redeem(someLocation{p})
+    assert someLocation{p}()
 
-    unfold someLocation!<p!>()
+    unfold someLocation{p}()
     // do something with p:
     *p = 42
   }
 }
 
 requires acc(c.SendChannel(), 1/2)
-requires c.SendGivenPerm() == vIsOne!<_!>
-requires c.SendGotPerm() == PredTrue!<!>
+requires c.SendGivenPerm() == vIsOne{_}
+requires c.SendGotPerm() == PredTrue{}
 requires v == 1
-requires someLocation!<p!>()
-requires c.ClosureDebt(someLocation!<p!>, 1, 2 /* 1/2 */)
+requires someLocation{p}()
+requires c.ClosureDebt(someLocation{p}, 1, 2 /* 1/2 */)
 func foo(v int, c chan int, p *int) {
     // send something to main:
-    fold vIsOne!<_!>(v)
+    fold vIsOne{_}(v)
 
-    assert acc(c.SendChannel(), _) && vIsOne!<_!>(v)
+    assert acc(c.SendChannel(), _) && vIsOne{_}(v)
     c <- v
-    assert acc(c.SendChannel(), _) && PredTrue!<!>()
+    assert acc(c.SendChannel(), _) && PredTrue{}()
 
     // permission to p should not have been touched and thus can still be used:
-    unfold someLocation!<p!>()
+    unfold someLocation{p}()
     *p = 1234
-    fold someLocation!<p!>()
+    fold someLocation{p}()
 
     // close channel
-    assert acc(c.SendChannel(), 1/2) && c.ClosureDebt(someLocation!<p!>, 1, 2 /* 1/2 */) && someLocation!<p!>()
-    close(c, 1, 2 /* 1/2 */, someLocation!<p!>)
+    assert acc(c.SendChannel(), 1/2) && c.ClosureDebt(someLocation{p}, 1, 2 /* 1/2 */) && someLocation{p}()
+    close(c, 1, 2 /* 1/2 */, someLocation{p})
     assert c.Closed()
 }
diff --git a/src/test/resources/regressions/features/channels/channel-simple7.gobra b/src/test/resources/regressions/features/channels/channel-simple7.gobra
index 6822c2d0a..b8cc6626b 100644
--- a/src/test/resources/regressions/features/channels/channel-simple7.gobra
+++ b/src/test/resources/regressions/features/channels/channel-simple7.gobra
@@ -10,19 +10,19 @@ pred sendInvariant(v *int) {
 func main() {
   var c@ = make(chan *int)
   var pc *chan *int = &c
-  (*pc).Init(sendInvariant!<_!>, PredTrue!<!>)
+  (*pc).Init(sendInvariant{_}, PredTrue{})
   go foo(pc)
 
   var x@ int = 42
   var p *int = &x
 
-  fold sendInvariant!<_!>(p)
+  fold sendInvariant{_}(p)
   *pc <- p
 
-  fold PredTrue!<!>()
+  fold PredTrue{}()
   res, ok := <- *pc
   if (ok) {
-    unfold sendInvariant!<_!>(res)
+    unfold sendInvariant{_}(res)
     assert *res == 42
     // we have regained write access:
     *res = 1
@@ -35,22 +35,22 @@ func main() {
 requires acc(pc, 1/2)
 requires acc((*pc).SendChannel(), 1/2)
 requires acc((*pc).RecvChannel(), 1/2)
-requires (*pc).SendGivenPerm() == sendInvariant!<_!>
-requires (*pc).SendGotPerm() == PredTrue!<!>
-requires (*pc).RecvGivenPerm() == PredTrue!<!>
-requires (*pc).RecvGotPerm() == sendInvariant!<_!>
+requires (*pc).SendGivenPerm() == sendInvariant{_}
+requires (*pc).SendGotPerm() == PredTrue{}
+requires (*pc).RecvGivenPerm() == PredTrue{}
+requires (*pc).RecvGotPerm() == sendInvariant{_}
 func foo(pc *chan *int) {
-    fold PredTrue!<!>()
+    fold PredTrue{}()
     res, ok := <- *pc
     if (ok) {
-        unfold sendInvariant!<_!>(res)
+        unfold sendInvariant{_}(res)
         assert *res == 42
         // we should have write access and thus can write to it
         *res = 0
         // before being able to fold again, we have to revert the value:
         *res = 42
         // send pointer and permission back:
-        fold sendInvariant!<_!>(res)
+        fold sendInvariant{_}(res)
         *pc <- res
     }
 
diff --git a/src/test/resources/regressions/features/channels/channel-simple8.gobra b/src/test/resources/regressions/features/channels/channel-simple8.gobra
index d1f2f9501..c303725bf 100644
--- a/src/test/resources/regressions/features/channels/channel-simple8.gobra
+++ b/src/test/resources/regressions/features/channels/channel-simple8.gobra
@@ -15,8 +15,8 @@ func testIsChannelPredicateIsIndependantOfAddressability() {
   // testCall can be called with both channels:
   testCall1(c1)
   testCall1(c2)
-  c1.Init(sendInvariant!<_!>, sendInvariant!<42!>)
-  c2.Init(sendInvariant!<_!>, sendInvariant!<42!>)
+  c1.Init(sendInvariant{_}, sendInvariant{42})
+  c2.Init(sendInvariant{_}, sendInvariant{42})
   testCall2(c1)
   testCall2(c2)
 }
diff --git a/src/test/resources/regressions/features/channels/channel-simple9.gobra b/src/test/resources/regressions/features/channels/channel-simple9.gobra
index 1ddfa5f9b..4c89c12dd 100644
--- a/src/test/resources/regressions/features/channels/channel-simple9.gobra
+++ b/src/test/resources/regressions/features/channels/channel-simple9.gobra
@@ -9,15 +9,15 @@ pred sendInvariant(v int) {
 
 // tests whether some information about the channel's state can be extracted from the single return form of receive:
 requires c.RecvChannel()
-requires c.RecvGivenPerm() == PredTrue!<!>
-requires c.RecvGotPerm() == sendInvariant!<_!>
+requires c.RecvGivenPerm() == PredTrue{}
+requires c.RecvGotPerm() == sendInvariant{_}
 func testSingleReceive(c chan int) {
-  fold PredTrue!<!>()
+  fold PredTrue{}()
   res := <- c // single return form of receive
   if (res != 0) {
     // non-zero value should imply the invariant:
-    assert sendInvariant!<_!>(res)
-    unfold sendInvariant!<_!>(res)
+    assert sendInvariant{_}(res)
+    unfold sendInvariant{_}(res)
     assert res == 42
   } else {
     // channel is in theory closed since the invariant tells us that a zero-value cannot be received
diff --git a/src/test/resources/regressions/features/channels/foo/foo.gobra b/src/test/resources/regressions/features/channels/foo/foo.gobra
index beb12701a..d859d46ce 100644
--- a/src/test/resources/regressions/features/channels/foo/foo.gobra
+++ b/src/test/resources/regressions/features/channels/foo/foo.gobra
@@ -8,10 +8,10 @@ pred vIsOne(v int) {
 }
 
 requires acc(c.SendChannel(), 1/2)
-requires c.SendGivenPerm() == vIsOne!<_!>
-requires c.SendGotPerm() == PredTrue!<!>
+requires c.SendGivenPerm() == vIsOne{_}
+requires c.SendGotPerm() == PredTrue{}
 func send1(c chan<- int) {
     v := 1
-    fold vIsOne!<_!>(v)
+    fold vIsOne{_}(v)
     c <- v
 }
diff --git a/src/test/resources/regressions/features/channels/multi-channel-simple1.gobra b/src/test/resources/regressions/features/channels/multi-channel-simple1.gobra
index 8c992beb2..0f5abde89 100644
--- a/src/test/resources/regressions/features/channels/multi-channel-simple1.gobra
+++ b/src/test/resources/regressions/features/channels/multi-channel-simple1.gobra
@@ -19,23 +19,23 @@ func structChannel() {
     assert c.IsChannel()
     assert c.BufferSize() == 1
 
-    c.Init(payloadIsOne!<_!>, PredTrue!<!>)
+    c.Init(payloadIsOne{_}, PredTrue{})
     go sendMsg(c)
 
-    fold PredTrue!<!>()
+    fold PredTrue{}()
     res, ok := <- c
     if (ok) {
-        unfold payloadIsOne!<_!>(res)
+        unfold payloadIsOne{_}(res)
         assert res.payload == 1
     }
 }
 
 requires acc(c.SendChannel(), 1/2)
-requires c.SendGivenPerm() == payloadIsOne!<_!>
-requires c.SendGotPerm() == PredTrue!<!>
+requires c.SendGivenPerm() == payloadIsOne{_}
+requires c.SendGotPerm() == PredTrue{}
 func sendMsg(c chan *msg) {
     m@ := msg{1}
-    fold payloadIsOne!<_!>(&m)
+    fold payloadIsOne{_}(&m)
     c <- &m
 }
 
@@ -46,13 +46,13 @@ func intChannel() {
     assert c.IsChannel()
     assert c.BufferSize() == 0
 
-    c.Init(f.vIsOne!<_!>, PredTrue!<!>)
+    c.Init(f.vIsOne{_}, PredTrue{})
     go f.send1(c)
 
-    fold PredTrue!<!>()
+    fold PredTrue{}()
     res, ok := <- c
     if (ok) {
-        unfold f.vIsOne!<_!>(res)
+        unfold f.vIsOne{_}(res)
         assert res == 1
     }
 }
diff --git a/src/test/resources/regressions/features/defunc/defunc-fail1.gobra b/src/test/resources/regressions/features/defunc/defunc-fail1.gobra
index 13e866b12..d93b2d7d2 100644
--- a/src/test/resources/regressions/features/defunc/defunc-fail1.gobra
+++ b/src/test/resources/regressions/features/defunc/defunc-fail1.gobra
@@ -22,9 +22,9 @@ func error2(ghost inv pred()) {
 	x@ := 1
 	fold accPred(&x)
 	// y := unfolding accPred(&x) in x
-	fold accPred!<&x!>()
+	fold accPred{&x}()
 	//:: ExpectedOutput(type_error)
-	y := unfolding accPred!<&x!>() in x
+	y := unfolding accPred{&x}() in x
 }
 
 pred eq(x *int, y *int) {
@@ -37,13 +37,13 @@ func error3() {
 	x@ := 1
 	y@ := 2
 	//:: ExpectedOutput(type_error)
-	fold eq!<&x, &x, &x!>()
+	fold eq{&x, &x, &x}()
 	//:: ExpectedOutput(type_error)
-	fold eq!<&x!>(&x)
+	fold eq{&x}(&x)
 	//:: ExpectedOutput(type_error)
-	fold eq!<&x, _!>()
+	fold eq{&x, _}()
 	//:: ExpectedOutput(type_error)
-	fold eq!<&x, _!>(&x, &y)
+	fold eq{&x, _}(&x, &y)
 }
 
 type Singleton struct {
@@ -59,9 +59,9 @@ pred (s *Singleton)isVal(val int) {
 
 func error4() {
 	s@ := Singleton{0}
-	fold (&s).isVal!<0!>()
+	fold (&s).isVal{0}()
 	e@ := Empty{}
 	// error: isVal expects a Singleton receiver
 	//:: ExpectedOutput(type_error)
-	fold (&e).isVal!<0!>()
+	fold (&e).isVal{0}()
 }
\ No newline at end of file
diff --git a/src/test/resources/regressions/features/defunc/defunc1.gobra b/src/test/resources/regressions/features/defunc/defunc1.gobra
index 98bc0ed6e..ee67ffe70 100644
--- a/src/test/resources/regressions/features/defunc/defunc1.gobra
+++ b/src/test/resources/regressions/features/defunc/defunc1.gobra
@@ -11,14 +11,14 @@ func foldTest() {
 	x@ := 1
 	y@ := 2
 	// partial application works as expected
-	fold eq!<&x, _!>(&x)
-	fold eq!<_, &y!>(&y)
-	fold eq!<_, _!>(&x, &x)
-	fold eq!<&x, &x!>()
+	fold eq{&x, _}(&x)
+	fold eq{_, &y}(&y)
+	fold eq{_, _}(&x, &x)
+	fold eq{&x, &x}()
 
 	// should fail because &x and &y are different 
 	//:: ExpectedOutput(fold_error)
-	fold eq!<&x, _!>(&y)
+	fold eq{&x, _}(&y)
 }
 
 type Pair struct {
@@ -33,12 +33,12 @@ pred (p *Pair) pairSum(sum int) {
 func foldPairSum() {
 	x@ := Pair{1, 1}
 	// predicate expression instances with mpredicate bases are also supported
-	fold (&x).pairSum!<3!>()
-	unfold (&x).pairSum!<3!>()
+	fold (&x).pairSum{3}()
+	unfold (&x).pairSum{3}()
 
 	// the following should fail because p.x + p.y == 2
 	//:: ExpectedOutput(fold_error)
-	fold (&x).pairSum!<2!>()
+	fold (&x).pairSum{2}()
 }
 
 type Singleton struct {
@@ -52,12 +52,12 @@ pred (s *Singleton) lessThan(bound int) {
 requires x >= 0
 func foldSingletonLessThan(x int) {
 	s@ := Singleton{}
-	fold (&s).lessThan!<x!>()
+	fold (&s).lessThan{x}()
 }
 
 // error: x may be less than the value of the singleton
 func foldSingletonLessThanError(x int) {
 	s@ := Singleton{0}
 	//:: ExpectedOutput(fold_error)
-	fold (&s).lessThan!<x!>()
+	fold (&s).lessThan{x}()
 }
\ No newline at end of file
diff --git a/src/test/resources/regressions/features/defunc/import-preds.gobra b/src/test/resources/regressions/features/defunc/import-preds.gobra
index 3da5ec326..5599b021e 100644
--- a/src/test/resources/regressions/features/defunc/import-preds.gobra
+++ b/src/test/resources/regressions/features/defunc/import-preds.gobra
@@ -7,7 +7,9 @@ package pkg
 import "preds"
 
 // tests importing predicates from other packages
-requires preds.PredExample!<1!>()
-requires preds.PredExample!<_!>(2)
+// Note: parenthesised base avoids the parser parsing `preds.PredExample{1}` as a
+// composite literal of an imported type. The blank-identifier form below is unambiguous.
+requires (preds.PredExample){1}()
+requires preds.PredExample{_}(2)
 requires preds.PredExample(3)
 func m()
\ No newline at end of file
diff --git a/src/test/resources/regressions/features/defunc/mutex1.gobra b/src/test/resources/regressions/features/defunc/mutex1.gobra
index 16cfa934b..cadee8dab 100644
--- a/src/test/resources/regressions/features/defunc/mutex1.gobra
+++ b/src/test/resources/regressions/features/defunc/mutex1.gobra
@@ -10,14 +10,14 @@ pred mutexInvariant(x *int) {
 	acc(x)
 }
 
-// For now, requires parentheses surrounding exp!<...!>
-requires acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant!<x!>
-ensures acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant!<x!>
+// For now, requires parentheses surrounding exp{...}
+requires acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant{x}
+ensures acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant{x}
 func foo(pmutex *sync.Mutex, x *int) {
 	pmutex.Lock()
-	unfold mutexInvariant!<x!>()
+	unfold mutexInvariant{x}()
 	*x = *x + 1
-	fold mutexInvariant!<x!>()
+	fold mutexInvariant{x}()
 	pmutex.Unlock()
 }
 
@@ -26,8 +26,8 @@ func ex1() {
 	var px *int = &x
 	var mutex@ = sync.Mutex{}
 	var pmutex *sync.Mutex = &mutex
-	fold mutexInvariant!<px!>()
-	pmutex.SetInv(mutexInvariant!<px!>)
+	fold mutexInvariant{px}()
+	pmutex.SetInv(mutexInvariant{px})
 	foo(pmutex, px)
 }
 
@@ -36,8 +36,8 @@ func ex2() {
 	var px *int = &x
 	var mutex@ = sync.Mutex{}
 	var pmutex *sync.Mutex = &mutex
-	fold mutexInvariant!<px!>()
-	pmutex.SetInv(mutexInvariant!<px!>)
+	fold mutexInvariant{px}()
+	pmutex.SetInv(mutexInvariant{px})
 	go foo(pmutex, px)
 	go foo(pmutex, px)
 	go foo(pmutex, px)
diff --git a/src/test/resources/regressions/features/defunc/pred-construct-fail1.gobra b/src/test/resources/regressions/features/defunc/pred-construct-fail1.gobra
index 82404636d..f74e66717 100644
--- a/src/test/resources/regressions/features/defunc/pred-construct-fail1.gobra
+++ b/src/test/resources/regressions/features/defunc/pred-construct-fail1.gobra
@@ -16,7 +16,7 @@ func f(ghost p pred())
 func error1() {
 	v := &T{}
 	fold v.AccInv()
-	f((*T).AccInv!<v!>)
+	f((*T).AccInv{v})
 }
 
 func g(x int)
@@ -26,5 +26,5 @@ func error2() {
 	// In previous versions of Gobra, we did not check for the pattern of the predicate constructor
 	// base, and examples like this would not throw a type error
 	//:: ExpectedOutput(type_error)
-	f(g!<x!>)
+	f(g{x})
 }
diff --git a/src/test/resources/regressions/features/defunc/pred-expr-base1.gobra b/src/test/resources/regressions/features/defunc/pred-expr-base1.gobra
index ce68d0691..f130a2449 100644
--- a/src/test/resources/regressions/features/defunc/pred-expr-base1.gobra
+++ b/src/test/resources/regressions/features/defunc/pred-expr-base1.gobra
@@ -19,15 +19,15 @@ pred (m Mutex) isValue(vState int32, vStema uint32) {
 func test1() {
 	m := Mutex{0, 0}
 	// predicate expressions are supported in predicate constructor
-	fold Mutex.isZero!<_!>(m)
-	fold Mutex.isZero!<m!>()
+	fold Mutex.isZero{_}(m)
+	fold Mutex.isZero{m}()
 }
 
 func test2() {
 	m := Mutex{1, 1}
 	// should fail, the predicate is not true for `m`
 	//:: ExpectedOutput(fold_error)
-	fold Mutex.isZero!<_!>(m)
+	fold Mutex.isZero{_}(m)
 }
 
 func test3() {
diff --git a/src/test/resources/regressions/features/defunc/waitgroup-fail1.gobra b/src/test/resources/regressions/features/defunc/waitgroup-fail1.gobra
index b7a696324..52371518c 100644
--- a/src/test/resources/regressions/features/defunc/waitgroup-fail1.gobra
+++ b/src/test/resources/regressions/features/defunc/waitgroup-fail1.gobra
@@ -6,10 +6,10 @@ package pkg
 import "sync"
 
 func problemWithCollect() {
-	fold acc(PredTrue!<!>(), 1/2)
-	fold sync.CollectFractions(seq[pred()]{ PredTrue!<!> }, seq[perm]{1/2})
-	assert sync.CollectFractions(seq[pred()]{ PredTrue!<!> }, seq[perm]{1/2})
-	assert sync.CollectFractions(seq[pred()]{ PredTrue!<!> }, seq[perm]{2/4})
+	fold acc(PredTrue{}(), 1/2)
+	fold sync.CollectFractions(seq[pred()]{ PredTrue{} }, seq[perm]{1/2})
+	assert sync.CollectFractions(seq[pred()]{ PredTrue{} }, seq[perm]{1/2})
+	assert sync.CollectFractions(seq[pred()]{ PredTrue{} }, seq[perm]{2/4})
 	//:: ExpectedOutput(assert_error:permission_error)
-	assert sync.CollectFractions(seq[pred()]{ PredTrue!<!> }, seq[perm]{3/4})
+	assert sync.CollectFractions(seq[pred()]{ PredTrue{} }, seq[perm]{3/4})
 }
\ No newline at end of file
diff --git a/src/test/resources/regressions/features/defunc/waitgroup-simple1.gobra b/src/test/resources/regressions/features/defunc/waitgroup-simple1.gobra
index f285e5558..abe285915 100644
--- a/src/test/resources/regressions/features/defunc/waitgroup-simple1.gobra
+++ b/src/test/resources/regressions/features/defunc/waitgroup-simple1.gobra
@@ -13,60 +13,60 @@ func spawnThreads(n int) {
 	// { acc(wg) && *wg == WaitGroup{} }
 	wg.Init()
 	// { wg.WaitGroupP() && !wg.WaitMode() }
-	wg.Add(1, 1/1, PredTrue!<!>)
-	// { wg.WaitGroupP() && !wg.WaitMode() && wg.UnitDebt(PredTrue!<!>) }
-	fold PredTrue!<!>()
-	// { wg.WaitGroupP() && !wg.WaitMode() && wg.UnitDebt(PredTrue!<!>) && PredTrue!<!>() }
-	wg.GenerateTokenAndDebt(PredTrue!<!>)
-	// { wg.WaitGroupP() && !wg.WaitMode() && wg.UnitDebt(PredTrue!<!>) && wg.Token(PredTrue!<!>) }
-	wg.Start(1/2, PredTrue!<!>)
-	// { acc(wg.WaitGroupP(), 1/2) && acc(wg.WaitGroupStarted(), 1/2) && !wg.WaitMode() && wg.UnitDebt(PredTrue!<!>) && wg.Token(PredTrue!<!>) }
-	fold PredTrue!<!>()
-	// { acc(wg.WaitGroupP(), 1/2) && acc(wg.WaitGroupStarted(), 1/2) && !wg.WaitMode() && wg.UnitDebt(PredTrue!<!>) && wg.Token(PredTrue!<!>) && PredTrue!<!>() }
-	go worker(-1, wg, PredTrue!<!>) // spawns first worker
-	// { acc(wg.WaitGroupP(), 1/2) && acc(wg.WaitGroupStarted(), 1/2) && !wg.WaitMode() && wg.Token(PredTrue!<!>) }
+	wg.Add(1, 1/1, PredTrue{})
+	// { wg.WaitGroupP() && !wg.WaitMode() && wg.UnitDebt(PredTrue{}) }
+	fold PredTrue{}()
+	// { wg.WaitGroupP() && !wg.WaitMode() && wg.UnitDebt(PredTrue{}) && PredTrue{}() }
+	wg.GenerateTokenAndDebt(PredTrue{})
+	// { wg.WaitGroupP() && !wg.WaitMode() && wg.UnitDebt(PredTrue{}) && wg.Token(PredTrue{}) }
+	wg.Start(1/2, PredTrue{})
+	// { acc(wg.WaitGroupP(), 1/2) && acc(wg.WaitGroupStarted(), 1/2) && !wg.WaitMode() && wg.UnitDebt(PredTrue{}) && wg.Token(PredTrue{}) }
+	fold PredTrue{}()
+	// { acc(wg.WaitGroupP(), 1/2) && acc(wg.WaitGroupStarted(), 1/2) && !wg.WaitMode() && wg.UnitDebt(PredTrue{}) && wg.Token(PredTrue{}) && PredTrue{}() }
+	go worker(-1, wg, PredTrue{}) // spawns first worker
+	// { acc(wg.WaitGroupP(), 1/2) && acc(wg.WaitGroupStarted(), 1/2) && !wg.WaitMode() && wg.Token(PredTrue{}) }
 
 	invariant 0 <= i && i <= n
 	invariant acc(wg.WaitGroupP(), 1/2)
 	invariant acc(wg.WaitGroupStarted(), 1/2)
 	invariant !wg.WaitMode()
-	invariant acc(wg.Token(PredTrue!<!>), (i + 1)/1)
+	invariant acc(wg.Token(PredTrue{}), (i + 1)/1)
 	for i := 0; i < n; i++ {
 		// {
 		//   acc(wg.WaitGroupP(), 1/2) &&
 		//   acc(wg.WaitGroupStarted(), 1/2) &&
 		//   !wg.WaitMode() &&
-		//   acc(wg.Token(PredTrue!<!>), i + 1) &&
+		//   acc(wg.Token(PredTrue{}), i + 1) &&
 		//   i < n
 		// }
-		wg.Add(1, 1/2, PredTrue!<!>)
+		wg.Add(1, 1/2, PredTrue{})
 		// {
 		//   acc(wg.WaitGroupP(), 1/2) &&
 		//   acc(wg.WaitGroupStarted(), 1/2) &&
 		//   !wg.WaitMode() &&
-		//   acc(wg.Token(PredTrue!<!>), i + 1) &&
+		//   acc(wg.Token(PredTrue{}), i + 1) &&
 		//   i < n &&
-		//   g.UnitDebt(PredTrue!<!>)
+		//   g.UnitDebt(PredTrue{})
 		// }
-		fold PredTrue!<!>()
-		// { same as above plus PredTrue!<!>() }
-		wg.GenerateTokenAndDebt(PredTrue!<!>)
+		fold PredTrue{}()
+		// { same as above plus PredTrue{}() }
+		wg.GenerateTokenAndDebt(PredTrue{})
 		// {
 		//   acc(wg.WaitGroupP(), 1/2) &&
 		//   acc(wg.WaitGroupStarted(), 1/2) &&
 		//   !wg.WaitMode() &&
-		//   acc(wg.Token(PredTrue!<!>), i + 2) && // permission increased by 1
+		//   acc(wg.Token(PredTrue{}), i + 2) && // permission increased by 1
 		//   i < n &&
-		//   wg.UnitDebt(PredTrue!<!>)
+		//   wg.UnitDebt(PredTrue{})
 		// }
-		fold PredTrue!<!>()
-		// { same as above plus PredTrue!<!>() }
-		go worker(i, wg, PredTrue!<!>)
+		fold PredTrue{}()
+		// { same as above plus PredTrue{}() }
+		go worker(i, wg, PredTrue{})
 		// {
 		//   acc(wg.WaitGroupP(), 1/2) &&
 		//   acc(wg.WaitGroupStarted(), 1/2) &&
 		//   !wg.WaitMode() &&
-		//   acc(wg.Token(PredTrue!<!>), i + 2) && // this reverts to i + 1 when i is incremented in the end of the iteration
+		//   acc(wg.Token(PredTrue{}), i + 2) && // this reverts to i + 1 when i is incremented in the end of the iteration
 		//   i < n
 		// }
 	}
@@ -75,13 +75,13 @@ func spawnThreads(n int) {
 	//   acc(wg.WaitGroupP(), 1/2) &&
 	//   acc(wg.WaitGroupStarted(), 1/2) &&
 	//   !wg.WaitMode() &&
-	//   acc(wg.Token(PredTrue!<!>), n + 1) // slightly simplified
+	//   acc(wg.Token(PredTrue{}), n + 1) // slightly simplified
 	// }
 	wg.SetWaitMode(1/2, 1/2)
 	// {
 	//   wg.WaitGroupP() &&
 	//   wg.WaitMode() &&
-	//   acc(wg.Token(PredTrue!<!>), n + 1)
+	//   acc(wg.Token(PredTrue{}), n + 1)
 	// }
 
 	// This example is simple and we do not need to perform any token redistribution before calling wait. This is not
@@ -89,7 +89,7 @@ func spawnThreads(n int) {
 	wg.Wait(1/1, seq[pred()]{ })
 	// {
 	//   wg.WaitGroupP() &&
-	//   PredTrue!<!>()
+	//   PredTrue{}()
 	// }
 }
 
@@ -97,7 +97,7 @@ requires P() && wg.UnitDebt(P)
 func worker(id int, wg *sync.WaitGroup, ghost P pred()) {
 	// { P() && wg.UnitDebt(P) }
 	wg.PayDebt(P)
-	// { wg.UnitDebt(PredTrue!<!>) }
+	// { wg.UnitDebt(PredTrue{}) }
 	wg.Done()
 	// { }
 }
\ No newline at end of file
diff --git a/src/test/resources/regressions/features/interfaces/predicateWithInterfaceParam.gobra b/src/test/resources/regressions/features/interfaces/predicateWithInterfaceParam.gobra
index b518a62c9..6fa7ecb65 100644
--- a/src/test/resources/regressions/features/interfaces/predicateWithInterfaceParam.gobra
+++ b/src/test/resources/regressions/features/interfaces/predicateWithInterfaceParam.gobra
@@ -22,8 +22,8 @@ func client() {
     fold somePredicate(impl)
     unfold somePredicate(impl)
     // this also works with first class predicates:
-    fold somePredicate!<_!>(impl)
-    unfold somePredicate!<_!>(impl)
-    fold somePredicate!<impl!>()
-    unfold somePredicate!<impl!>()
+    fold somePredicate{_}(impl)
+    unfold somePredicate{_}(impl)
+    fold somePredicate{impl}()
+    unfold somePredicate{impl}()
 }
diff --git a/src/test/resources/regressions/features/predicates/foldability.gobra b/src/test/resources/regressions/features/predicates/foldability.gobra
index d20a72079..d9440d037 100644
--- a/src/test/resources/regressions/features/predicates/foldability.gobra
+++ b/src/test/resources/regressions/features/predicates/foldability.gobra
@@ -43,7 +43,7 @@ func interfacePred(itf SomeInterface) bool {
 
 func predTrue() {
     // this should succeed
-    fold PredTrue!<!>()
+    fold PredTrue{}()
 }
 
 func isChannel(channel chan int) {
@@ -59,15 +59,15 @@ func predExprs() bool {
 	x@ := 1
 	y@ := 2
 	// having a predicate constructor as a base is supported:
-	fold eq!<&x, _!>(&x)
-	fold eq!<_, &y!>(&y)
-	fold eq!<_, _!>(&x, &x)
-	fold eq!<&x, &x!>()
+	fold eq{&x, _}(&x)
+	fold eq{_, &y}(&y)
+	fold eq{_, _}(&x, &x)
+	fold eq{&x, &x}()
 	// predicate constructors in unfolding expressions is not supported:
 	//:: ExpectedOutput(type_error)
-	b := unfolding eq!<&x, &x!>() in true
+	b := unfolding eq{&x, &x}() in true
 
-	predExpr := eq!<&x, &x!>;
+	predExpr := eq{&x, &x};
 	//:: ExpectedOutput(type_error)
     fold predExpr()
     //:: ExpectedOutput(type_error)
diff --git a/src/test/resources/regressions/issues/000164.gobra b/src/test/resources/regressions/issues/000164.gobra
index 08fa85fa7..ca196977f 100644
--- a/src/test/resources/regressions/issues/000164.gobra
+++ b/src/test/resources/regressions/issues/000164.gobra
@@ -14,12 +14,12 @@ pred (s *Singleton) lessThan(bound int) {
 requires x >= 0
 func foldSingletonLessThan(x int) {
 	s@ := Singleton{}
-	fold (&s).lessThan!<x!>()
+	fold (&s).lessThan{x}()
 }
 
 func foldSingletonLessThanError(x int) {
 	s@ := Singleton{}
 	// x may be less than the value of the singleton
 	//:: ExpectedOutput(fold_error)
-	fold (&s).lessThan!<x!>()
+	fold (&s).lessThan{x}()
 }
\ No newline at end of file
diff --git a/src/test/resources/regressions/issues/000176.gobra b/src/test/resources/regressions/issues/000176.gobra
index a57b4b42b..c02b5a45c 100644
--- a/src/test/resources/regressions/issues/000176.gobra
+++ b/src/test/resources/regressions/issues/000176.gobra
@@ -11,18 +11,18 @@ requires inv1(42)
 func test0()
 
 // Example provided by Linard
-requires inv1!<_!>(42)
+requires inv1{_}(42)
 func test1()
 
 // Gobra infers adequate type for each argument, despite being equal expressions
 pred inv2(a int, b uint32)
-requires inv2!<_, _!>(42, 42)
+requires inv2{_, _}(42, 42)
 func test2()
 
 // Gobra figures out the correct type of 42 here: int for the
 // first precondition and uint32 for the second
-requires inv2!<_, 42!>(42)
-requires inv2!<42, _!>(42)
+requires inv2{_, 42}(42)
+requires inv2{42, _}(42)
 func test3()
 
 type T struct {
@@ -32,13 +32,13 @@ type T struct {
 pred (r T) inv3()
 
 // used to crash in previous versions of Gobra
-requires (T{42}).inv3!<!>();
+requires (T{42}).inv3{}();
 func test4()
 
 // Gobra finds the cases where an overflow occurs in a predicate expression instance
 //:: ExpectedOutput(type_error)
-requires inv1!<_!>(213412341234124214231432142134123)
+requires inv1{_}(213412341234124214231432142134123)
 func test5()
 //:: ExpectedOutput(type_error)
-requires inv1!<213412341234124214231432142134123!>()
+requires inv1{213412341234124214231432142134123}()
 func test6()
\ No newline at end of file
diff --git a/src/test/resources/regressions/issues/000695.gobra b/src/test/resources/regressions/issues/000695.gobra
index f8832ac93..eb98b7e3c 100644
--- a/src/test/resources/regressions/issues/000695.gobra
+++ b/src/test/resources/regressions/issues/000695.gobra
@@ -13,23 +13,23 @@ pred sendInvariant(v ChannelMsgType) {
 }
 
 requires acc(channel.SendChannel(), 1/2)
-requires channel.SendGivenPerm() == sendInvariant!<_!>
-requires channel.SendGotPerm() == PredTrue!<!>
+requires channel.SendGivenPerm() == sendInvariant{_}
+requires channel.SendGotPerm() == PredTrue{}
 func sendMsg1(channel chan ChannelMsgType) {
-    fold sendInvariant!<_!>(ChannelMsg1)
-    fold PredTrue!<!>()
-    assert acc(channel.SendChannel(), _) && sendInvariant!<_!>(ChannelMsg1)
+    fold sendInvariant{_}(ChannelMsg1)
+    fold PredTrue{}()
+    assert acc(channel.SendChannel(), _) && sendInvariant{_}(ChannelMsg1)
     assert acc(channel.SendChannel(), _) && channel.SendGivenPerm()(ChannelMsg1)
     channel <- ChannelMsg1
 }
 
 requires acc(channel.SendChannel(), 1/2)
-requires channel.SendGivenPerm() == sendInvariant!<_!>
-requires channel.SendGotPerm() == PredTrue!<!>
+requires channel.SendGivenPerm() == sendInvariant{_}
+requires channel.SendGotPerm() == PredTrue{}
 func sendMsg2(channel chan ChannelMsgType) {
-    fold sendInvariant!<_!>(ChannelMsg2)
-    fold PredTrue!<!>()
-    assert acc(channel.SendChannel(), _) && sendInvariant!<_!>(ChannelMsg2)
+    fold sendInvariant{_}(ChannelMsg2)
+    fold PredTrue{}()
+    assert acc(channel.SendChannel(), _) && sendInvariant{_}(ChannelMsg2)
     assert acc(channel.SendChannel(), _) && channel.SendGivenPerm()(ChannelMsg2)
     channel <- ChannelMsg2
 }
diff --git a/src/test/resources/same_package/pkg_init/concfib/fib.go b/src/test/resources/same_package/pkg_init/concfib/fib.go
index fd3e9b70b..e2479b312 100644
--- a/src/test/resources/same_package/pkg_init/concfib/fib.go
+++ b/src/test/resources/same_package/pkg_init/concfib/fib.go
@@ -13,8 +13,8 @@ var lock *sync.Mutex = &sync.Mutex{}
 func init() {
 	cache[0] = 1
 	cache[1] = 1
-	// @ fold lockInv!<!>()
-	// @ lock.SetInv(lockInv!<!>)
+	// @ fold lockInv{}()
+	// @ lock.SetInv(lockInv{})
 	// @ fold acc(StaticInv(), _)
 }
 
@@ -25,19 +25,19 @@ func FibV1(n int) (res int) {
 	// @ openDupPkgInv
 	// @ unfold acc(StaticInv(), _)
 	lock.Lock()
-	// @ unfold lockInv!<!>()
+	// @ unfold lockInv{}()
 	if v, ok := cache[n]; ok {
-		// @ fold lockInv!<!>()
+		// @ fold lockInv{}()
 		lock.Unlock()
 		return v
 	}
-	// @ fold lockInv!<!>()
+	// @ fold lockInv{}()
 	lock.Unlock()
 	v := FibV1(n-1) + FibV1(n-2)
 	lock.Lock()
-	// @ unfold lockInv!<!>()
+	// @ unfold lockInv{}()
 	cache[n] = v
-	// @ fold lockInv!<!>()
+	// @ fold lockInv{}()
 	lock.Unlock()
 	return v
 }
@@ -55,18 +55,18 @@ func FibV2(n int) (res int) {
 }
 
 // @ requires  0 <= n
-// @ preserves lockInv!<!>()
+// @ preserves lockInv{}()
 // @ ensures   res == FibSpec(n)
 // @ decreases n
 func fibImpl(n int) (res int) {
-	// @ unfold lockInv!<!>()
-	// @ defer fold lockInv!<!>()
+	// @ unfold lockInv{}()
+	// @ defer fold lockInv{}()
 	if v, ok := cache[n]; ok {
 		return v
 	}
-	// @ fold lockInv!<!>()
+	// @ fold lockInv{}()
 	v := fibImpl(n-1) + fibImpl(n-2)
-	// @ unfold lockInv!<!>()
+	// @ unfold lockInv{}()
 	cache[n] = v
 	return v
 }
diff --git a/src/test/resources/same_package/pkg_init/concfib/fib_spec.gobra b/src/test/resources/same_package/pkg_init/concfib/fib_spec.gobra
index 8dab5f993..36ed9f5e2 100644
--- a/src/test/resources/same_package/pkg_init/concfib/fib_spec.gobra
+++ b/src/test/resources/same_package/pkg_init/concfib/fib_spec.gobra
@@ -22,7 +22,7 @@ pred lockInv() {
 
 pred StaticInv() {
 	acc(lock.LockP(), _) &&
-	lock.LockInv() == lockInv!<!>
+	lock.LockInv() == lockInv{}
 }
 
 // Given that we can always implement a ghost method like the one below to gain

From dc8722f96b1a0eb8885c5cdaf06ea1988145aa74 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Sat, 2 May 2026 23:06:53 +0000
Subject: [PATCH 02/11] Migrate parser unit tests to new predicate-constructor
 syntax

ParserUnitTests parse isolated expressions via parseExpr, which does
not run the package-level PredicateConstructorPostprocessor. Use the
parenthesised base form `(name){args}` so the parse goes through
`primaryExpr predConstructArgs` and produces a `PPredConstructor`
directly, matching the existing test patterns.

https://claude.ai/code/session_01DoEQdoLVWuLxD2mQUJDDRg
---
 src/test/scala/viper/gobra/parsing/ParserUnitTests.scala | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala b/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala
index 0ce28e67f..262d628eb 100644
--- a/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala
+++ b/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala
@@ -2494,19 +2494,19 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside {
   }
 
   test("Parser: should be able to parse a fpredicate constructor") {
-    frontend.parseExpOrFail("mutexInvariant!<x!>") should matchPattern {
+    frontend.parseExpOrFail("(mutexInvariant){x}") should matchPattern {
       case PPredConstructor(PFPredBase(PIdnUse("mutexInvariant")), Vector(Some(PNamedOperand(PIdnUse("x"))))) =>
     }
   }
 
   test("Parser: should be able to parse a mpredicate constructor") {
-    frontend.parseExpOrFail("p.mutexInvariant!<x!>") should matchPattern {
+    frontend.parseExpOrFail("(p.mutexInvariant){x}") should matchPattern {
       case PPredConstructor(PDottedBase(PDot( PNamedOperand(PIdnUse("p")), PIdnUse("mutexInvariant"))), Vector(Some(PNamedOperand(PIdnUse("x"))))) =>
     }
   }
 
   test("Parser: should be able to parse a fpredicate constructor with wildcard") {
-    frontend.parseExpOrFail("p!<x, _, y!>") should matchPattern {
+    frontend.parseExpOrFail("(p){x, _, y}") should matchPattern {
       case PPredConstructor(PFPredBase(PIdnUse("p")), Vector(Some(PNamedOperand(PIdnUse("x"))), None, Some(PNamedOperand(PIdnUse("y"))))) =>
     }
   }

From c2011b4a553de96463a859770fd98ddb707a0f6d Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Sun, 3 May 2026 08:17:17 +0000
Subject: [PATCH 03/11] Support cross-package predicate constructors
 `pkg.P{...}`

Adds a second-pass rewrite, driven by `Info.checkSources`, that uses the
freshly-available `dependentTypeInfo` to ask each imported package's
TypeInfo whether `pkg.id` resolves to a predicate. The rewrite logic is
factored out of `PredicateConstructorPostprocessor` into a shared
`PredicateConstructorRewriter` object so both passes (parse-time, local
predicates only; type-check-time, cross-package) share the same
`PCompositeLit` -> `PPredConstructor` machinery.

`import-preds.gobra` is restored to use direct `preds.PredExample{1}()`
syntax now that the cross-package case is handled.

https://claude.ai/code/session_01DoEQdoLVWuLxD2mQUJDDRg
---
 .../scala/viper/gobra/frontend/Parser.scala   | 62 +++++++++++++------
 .../viper/gobra/frontend/info/Info.scala      | 60 +++++++++++++++++-
 .../features/defunc/import-preds.gobra        |  4 +-
 3 files changed, 104 insertions(+), 22 deletions(-)

diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala
index fd370955d..1c2f72350 100644
--- a/src/main/scala/viper/gobra/frontend/Parser.scala
+++ b/src/main/scala/viper/gobra/frontend/Parser.scala
@@ -524,11 +524,10 @@ object Parser extends LazyLogging {
       * `PPredConstructor` when they are unambiguously predicate constructors:
       *   1. They contain at least one positional `_` element (illegal in composite literals), or
       *   2. The named/dotted base resolves syntactically to a top-level predicate declared in
-      *      the current package.
+      *      the current package or to a built-in predicate.
       *
-      * Cases that depend on cross-package resolution (e.g. `pkg.P{1}()` where `P` is a predicate
-      * declared in `pkg` and not shadowed locally) are left alone and must currently be written
-      * with an explicit parenthesised base, e.g. `(pkg.P){1}()`.
+      * Cross-package cases (e.g. `pkg.P{1}()`) are deferred to a second pass driven by the
+      * type checker -- see [[PredicateConstructorRewriter.rewriteCrossPackage]].
       */
     def postprocess(pkg: PPackage)(config: Config): Either[Vector[ParserError], PPackage] = {
       // collect names of all top-level (function and method) predicate declarations
@@ -536,29 +535,56 @@ object Parser extends LazyLogging {
         case d: PFPredicateDecl => d.id.name
         case d: PMPredicateDecl => d.id.name
       }).toSet
-      // also recognise built-in predicate identifiers (e.g. PredTrue, IsChannel, ...)
-      val builtInPredicateNames: Set[String] = viper.gobra.frontend.info.base.BuiltInMemberTag.builtInMembers().collect {
+      Right(PredicateConstructorRewriter.rewrite(pkg, localPredicateNames, _ => Set.empty)(positions))
+    }
+  }
+
+  /**
+    * Shared rewrite logic that turns `PCompositeLit` nodes whose name resolves (syntactically) to
+    * a predicate into the equivalent `PPredConstructor`. Used both by the parse-time
+    * [[PredicateConstructorPostprocessor]] (which only knows the current package's predicates)
+    * and by [[viper.gobra.frontend.info.Info]] (which additionally has access to imported
+    * packages' predicate names via `dependentTypeInfo`).
+    */
+  object PredicateConstructorRewriter {
+    private lazy val builtInPredicateNames: Set[String] =
+      viper.gobra.frontend.info.base.BuiltInMemberTag.builtInMembers().collect {
         case t: viper.gobra.frontend.info.base.BuiltInMemberTag.BuiltInPredicateTag => t.identifier
       }.toSet
-      val predicateNames: Set[String] = localPredicateNames ++ builtInPredicateNames
+
+    /** Runs the rewrite over `pkg`. `localPredicateNames` is the set of top-level predicate
+      * names (function and method) declared in `pkg`. `importedPredicateNames(qual)` returns the
+      * set of predicate names exposed by the package imported under qualifier `qual`, or an
+      * empty set if `qual` is not an import qualifier or its imports aren't yet known. */
+    def rewrite(
+      pkg: PPackage,
+      localPredicateNames: Set[String],
+      importedPredicateNames: String => Set[String],
+    )(positions: Positions): PPackage = {
+      val rewriter = new PRewriter(positions)
+      import rewriter._
 
       def hasKey(lit: PLiteralValue): Boolean = lit.elems.exists(_.key.isDefined)
       def hasBlank(lit: PLiteralValue): Boolean = lit.elems.exists {
         case PKeyedElement(None, PExpCompositeVal(_: PBlankIdentifier)) => true
         case _ => false
       }
-      def isPredName(id: PIdnUse): Boolean = predicateNames.contains(id.name)
+      def isLocalOrBuiltInPredName(name: String): Boolean =
+        localPredicateNames.contains(name) || builtInPredicateNames.contains(name)
 
       def shouldRewrite(typ: PLiteralType, lit: PLiteralValue): Boolean = {
-        // composite literals with keyed elements (e.g. `T{x: 1}`) cannot be predicate constructors
         if (hasKey(lit)) false
         else typ match {
-          case PNamedOperand(id) => hasBlank(lit) || isPredName(id)
-          case PDot(_, id) => hasBlank(lit) || isPredName(id)
+          case PNamedOperand(id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
+          case PDot(qual: PNamedOperand, id) =>
+            hasBlank(lit) || isLocalOrBuiltInPredName(id.name) || importedPredicateNames(qual.id.name).contains(id.name)
+          case PDot(_, id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
           case _ => false
         }
       }
 
+      def at[N <: AnyRef](node: N, source: PNode): N = { positions.dupPos(source, node); node }
+
       def convertArgs(lit: PLiteralValue): Vector[Option[PExpression]] = lit.elems.map {
         case PKeyedElement(None, PExpCompositeVal(_: PBlankIdentifier)) => None
         case PKeyedElement(None, PExpCompositeVal(e)) => Some(e)
@@ -566,23 +592,23 @@ object Parser extends LazyLogging {
       }
 
       def buildBase(typ: PLiteralType): PPredConstructorBase = typ match {
-        case op@PNamedOperand(id) => PFPredBase(id).at(op)
-        case d: PDot => PDottedBase(d).at(d)
+        case op@PNamedOperand(id) => at(PFPredBase(id), op)
+        case d: PDot => at(PDottedBase(d), d)
         case t => Violation.violation(s"unexpected base for predicate constructor: $t")
       }
 
       val rewritePredConstructors: Strategy =
         strategyWithName[Any]("rewritePredConstructors", {
           case n@PCompositeLit(typ, lit) if shouldRewrite(typ, lit) =>
-            Some(PPredConstructor(buildBase(typ), convertArgs(lit)).at(n))
+            Some(at(PPredConstructor(buildBase(typ), convertArgs(lit)), n))
           case n => Some(n)
         })
 
-      val updatedProgs = pkg.programs.map(prog => {
+      val updatedProgs = pkg.programs.map { prog =>
         val updatedDecls = rewrite(topdown(attempt(rewritePredConstructors)))(prog.declarations)
-        PProgram(prog.packageClause, prog.pkgInvariants, prog.imports, prog.friends, updatedDecls).at(prog)
-      })
-      Right(PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info).at(pkg))
+        at(PProgram(prog.packageClause, prog.pkgInvariants, prog.imports, prog.friends, updatedDecls), prog)
+      }
+      at(PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info), pkg)
     }
   }
 
diff --git a/src/main/scala/viper/gobra/frontend/info/Info.scala b/src/main/scala/viper/gobra/frontend/info/Info.scala
index 5b738cf2d..be7b6909f 100644
--- a/src/main/scala/viper/gobra/frontend/info/Info.scala
+++ b/src/main/scala/viper/gobra/frontend/info/Info.scala
@@ -221,6 +221,60 @@ object Info extends LazyLogging {
     } yield typeInfo
   }
 
+  /**
+    * Performs a second-pass rewrite of cross-package predicate constructors.
+    *
+    * The parse-time postprocessor only knows the current package's predicate names and so
+    * leaves expressions like `pkg.P{1}()` -- where `P` is a predicate declared in the imported
+    * package `pkg` -- as `PCompositeLit`. Once `dependentTypeInfo` is available, we know each
+    * import's qualifier name and can ask its `ExternalTypeInfo` whether a given identifier
+    * resolves to a predicate.
+    */
+  private def rewriteCrossPackagePredConstructors(
+    pkg: PPackage,
+    deps: Map[AbstractImport, ExternalTypeInfo],
+  ): PPackage = {
+    import viper.gobra.ast.frontend.PExplicitQualifiedImport
+
+    // Local predicate names (function and method): used to skip work for cases the parse-time
+    // postprocessor already handled.
+    val localPredicateNames: Set[String] = pkg.programs.flatMap(_.declarations.collect {
+      case d: viper.gobra.ast.frontend.PFPredicateDecl => d.id.name
+      case d: viper.gobra.ast.frontend.PMPredicateDecl => d.id.name
+    }).toSet
+
+    // Build a per-program function: qualifier-name -> set of predicate names exposed by the
+    // package imported under that qualifier.
+    val importedByQualifier: Map[String, Set[String]] = pkg.programs.flatMap { prog =>
+      prog.imports.collect {
+        case pi: PExplicitQualifiedImport =>
+          val abstractImport = RegularImport(pi.importPath)
+          deps.get(abstractImport).map { extInfo =>
+            // walk the imported package's declarations and collect top-level predicate names
+            val importedPkg = extInfo.getTypeInfo match {
+              case ti: TypeInfoImpl => Some(ti.tree.root)
+              case _ => None
+            }
+            val names: Set[String] = importedPkg.toVector.flatMap(_.programs.flatMap(_.declarations.collect {
+              case d: viper.gobra.ast.frontend.PFPredicateDecl => d.id.name
+              case d: viper.gobra.ast.frontend.PMPredicateDecl => d.id.name
+            })).toSet
+            pi.qualifier.name -> names
+          }
+      }.flatten
+    }.toMap
+
+    if (importedByQualifier.isEmpty) pkg
+    else {
+      val positions = pkg.positions.positions
+      viper.gobra.frontend.Parser.PredicateConstructorRewriter.rewrite(
+        pkg,
+        localPredicateNames,
+        q => importedByQualifier.getOrElse(q, Set.empty),
+      )(positions)
+    }
+  }
+
   type TypeInfoCacheKey = String
   private val typeInfoCache: ConcurrentMap[TypeInfoCacheKey, TypeInfoImpl] = new ConcurrentHashMap()
 
@@ -255,7 +309,11 @@ object Info extends LazyLogging {
     var cacheHit: Boolean = true
     def getTypeInfo(pkg: PPackage, dependentTypeInfo: Map[AbstractImport, ExternalTypeInfo], isMainContext: Boolean, config: Config): TypeInfoImpl = {
       cacheHit = false
-      val tree = new GoTree(pkg)
+      // Rewrite any remaining `pkg.P{...}` composite literals into predicate constructors when
+      // `P` is a top-level predicate of the imported package. This finishes the disambiguation
+      // started at parse time (see Parser.PredicateConstructorPostprocessor).
+      val rewrittenPkg = rewriteCrossPackagePredConstructors(pkg, dependentTypeInfo)
+      val tree = new GoTree(rewrittenPkg)
       new TypeInfoImpl(tree, dependentTypeInfo, isMainContext)(config: Config)
     }
 
diff --git a/src/test/resources/regressions/features/defunc/import-preds.gobra b/src/test/resources/regressions/features/defunc/import-preds.gobra
index 5599b021e..84e2c1b09 100644
--- a/src/test/resources/regressions/features/defunc/import-preds.gobra
+++ b/src/test/resources/regressions/features/defunc/import-preds.gobra
@@ -7,9 +7,7 @@ package pkg
 import "preds"
 
 // tests importing predicates from other packages
-// Note: parenthesised base avoids the parser parsing `preds.PredExample{1}` as a
-// composite literal of an imported type. The blank-identifier form below is unambiguous.
-requires (preds.PredExample){1}()
+requires preds.PredExample{1}()
 requires preds.PredExample{_}(2)
 requires preds.PredExample(3)
 func m()
\ No newline at end of file

From eda78b46e7313fc61d3be1aeeb341e677c91ec3f Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Sun, 3 May 2026 15:43:28 +0000
Subject: [PATCH 04/11] Fix ambiguous `positions`/`rewrite` references in
 predicate-constructor rewriter

Removing the `import rewriter._` and qualifying calls explicitly resolves
the name clash between the method-local `positions` parameter (and the
outer object's `rewrite` method) and the corresponding members imported
from the `PRewriter` instance.

https://claude.ai/code/session_01DoEQdoLVWuLxD2mQUJDDRg
---
 src/main/scala/viper/gobra/frontend/Parser.scala | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala
index 1c2f72350..2f6abbb2d 100644
--- a/src/main/scala/viper/gobra/frontend/Parser.scala
+++ b/src/main/scala/viper/gobra/frontend/Parser.scala
@@ -562,7 +562,6 @@ object Parser extends LazyLogging {
       importedPredicateNames: String => Set[String],
     )(positions: Positions): PPackage = {
       val rewriter = new PRewriter(positions)
-      import rewriter._
 
       def hasKey(lit: PLiteralValue): Boolean = lit.elems.exists(_.key.isDefined)
       def hasBlank(lit: PLiteralValue): Boolean = lit.elems.exists {
@@ -598,14 +597,14 @@ object Parser extends LazyLogging {
       }
 
       val rewritePredConstructors: Strategy =
-        strategyWithName[Any]("rewritePredConstructors", {
+        rewriter.strategyWithName[Any]("rewritePredConstructors", {
           case n@PCompositeLit(typ, lit) if shouldRewrite(typ, lit) =>
             Some(at(PPredConstructor(buildBase(typ), convertArgs(lit)), n))
           case n => Some(n)
         })
 
       val updatedProgs = pkg.programs.map { prog =>
-        val updatedDecls = rewrite(topdown(attempt(rewritePredConstructors)))(prog.declarations)
+        val updatedDecls = rewriter.rewrite(rewriter.topdown(rewriter.attempt(rewritePredConstructors)))(prog.declarations)
         at(PProgram(prog.packageClause, prog.pkgInvariants, prog.imports, prog.friends, updatedDecls), prog)
       }
       at(PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info), pkg)

From c3c890e425c5433cda5048e937ca579cb7a0cac7 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Sun, 3 May 2026 15:51:06 +0000
Subject: [PATCH 05/11] Move predicate-constructor rewrite into a
 PositionedRewriter subclass

`attempt`, `topdown`, etc. are inherited members of `PositionedRewriter`,
so the previous attempt to call them as `rewriter.attempt(...)` on a
`PRewriter` instance failed to resolve. Wrap the rewrite logic in a
`PositionedRewriter` subclass `Impl` so the strategy combinators are
available unqualified, mirroring the existing `Postprocessor` pattern.

https://claude.ai/code/session_01DoEQdoLVWuLxD2mQUJDDRg
---
 .../scala/viper/gobra/frontend/Parser.scala   | 103 ++++++++++--------
 1 file changed, 55 insertions(+), 48 deletions(-)

diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala
index 2f6abbb2d..f816d0256 100644
--- a/src/main/scala/viper/gobra/frontend/Parser.scala
+++ b/src/main/scala/viper/gobra/frontend/Parser.scala
@@ -552,63 +552,70 @@ object Parser extends LazyLogging {
         case t: viper.gobra.frontend.info.base.BuiltInMemberTag.BuiltInPredicateTag => t.identifier
       }.toSet
 
-    /** Runs the rewrite over `pkg`. `localPredicateNames` is the set of top-level predicate
-      * names (function and method) declared in `pkg`. `importedPredicateNames(qual)` returns the
-      * set of predicate names exposed by the package imported under qualifier `qual`, or an
-      * empty set if `qual` is not an import qualifier or its imports aren't yet known. */
-    def rewrite(
-      pkg: PPackage,
-      localPredicateNames: Set[String],
-      importedPredicateNames: String => Set[String],
-    )(positions: Positions): PPackage = {
-      val rewriter = new PRewriter(positions)
+    private class Impl(override val positions: Positions) extends PositionedRewriter {
+      def at[N <: AnyRef](node: N, source: PNode): N = { positions.dupPos(source, node); node }
 
-      def hasKey(lit: PLiteralValue): Boolean = lit.elems.exists(_.key.isDefined)
-      def hasBlank(lit: PLiteralValue): Boolean = lit.elems.exists {
-        case PKeyedElement(None, PExpCompositeVal(_: PBlankIdentifier)) => true
-        case _ => false
-      }
-      def isLocalOrBuiltInPredName(name: String): Boolean =
-        localPredicateNames.contains(name) || builtInPredicateNames.contains(name)
-
-      def shouldRewrite(typ: PLiteralType, lit: PLiteralValue): Boolean = {
-        if (hasKey(lit)) false
-        else typ match {
-          case PNamedOperand(id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
-          case PDot(qual: PNamedOperand, id) =>
-            hasBlank(lit) || isLocalOrBuiltInPredName(id.name) || importedPredicateNames(qual.id.name).contains(id.name)
-          case PDot(_, id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
+      def run(
+        pkg: PPackage,
+        localPredicateNames: Set[String],
+        importedPredicateNames: String => Set[String],
+      ): PPackage = {
+        def hasKey(lit: PLiteralValue): Boolean = lit.elems.exists(_.key.isDefined)
+        def hasBlank(lit: PLiteralValue): Boolean = lit.elems.exists {
+          case PKeyedElement(None, PExpCompositeVal(_: PBlankIdentifier)) => true
           case _ => false
         }
-      }
-
-      def at[N <: AnyRef](node: N, source: PNode): N = { positions.dupPos(source, node); node }
+        def isLocalOrBuiltInPredName(name: String): Boolean =
+          localPredicateNames.contains(name) || builtInPredicateNames.contains(name)
+
+        def shouldRewrite(typ: PLiteralType, lit: PLiteralValue): Boolean = {
+          if (hasKey(lit)) false
+          else typ match {
+            case PNamedOperand(id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
+            case PDot(qual: PNamedOperand, id) =>
+              hasBlank(lit) || isLocalOrBuiltInPredName(id.name) || importedPredicateNames(qual.id.name).contains(id.name)
+            case PDot(_, id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
+            case _ => false
+          }
+        }
 
-      def convertArgs(lit: PLiteralValue): Vector[Option[PExpression]] = lit.elems.map {
-        case PKeyedElement(None, PExpCompositeVal(_: PBlankIdentifier)) => None
-        case PKeyedElement(None, PExpCompositeVal(e)) => Some(e)
-        case e => Violation.violation(s"unexpected element form in predicate constructor candidate: $e")
-      }
+        def convertArgs(lit: PLiteralValue): Vector[Option[PExpression]] = lit.elems.map {
+          case PKeyedElement(None, PExpCompositeVal(_: PBlankIdentifier)) => None
+          case PKeyedElement(None, PExpCompositeVal(e)) => Some(e)
+          case e => Violation.violation(s"unexpected element form in predicate constructor candidate: $e")
+        }
 
-      def buildBase(typ: PLiteralType): PPredConstructorBase = typ match {
-        case op@PNamedOperand(id) => at(PFPredBase(id), op)
-        case d: PDot => at(PDottedBase(d), d)
-        case t => Violation.violation(s"unexpected base for predicate constructor: $t")
-      }
+        def buildBase(typ: PLiteralType): PPredConstructorBase = typ match {
+          case op@PNamedOperand(id) => at(PFPredBase(id), op)
+          case d: PDot => at(PDottedBase(d), d)
+          case t => Violation.violation(s"unexpected base for predicate constructor: $t")
+        }
 
-      val rewritePredConstructors: Strategy =
-        rewriter.strategyWithName[Any]("rewritePredConstructors", {
-          case n@PCompositeLit(typ, lit) if shouldRewrite(typ, lit) =>
-            Some(at(PPredConstructor(buildBase(typ), convertArgs(lit)), n))
-          case n => Some(n)
-        })
+        val rewritePredConstructors: Strategy =
+          strategyWithName[Any]("rewritePredConstructors", {
+            case n@PCompositeLit(typ, lit) if shouldRewrite(typ, lit) =>
+              Some(at(PPredConstructor(buildBase(typ), convertArgs(lit)), n))
+            case n => Some(n)
+          })
 
-      val updatedProgs = pkg.programs.map { prog =>
-        val updatedDecls = rewriter.rewrite(rewriter.topdown(rewriter.attempt(rewritePredConstructors)))(prog.declarations)
-        at(PProgram(prog.packageClause, prog.pkgInvariants, prog.imports, prog.friends, updatedDecls), prog)
+        val updatedProgs = pkg.programs.map { prog =>
+          val updatedDecls = rewrite(topdown(attempt(rewritePredConstructors)))(prog.declarations)
+          at(PProgram(prog.packageClause, prog.pkgInvariants, prog.imports, prog.friends, updatedDecls), prog)
+        }
+        at(PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info), pkg)
       }
-      at(PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info), pkg)
     }
+
+    /** Runs the rewrite over `pkg`. `localPredicateNames` is the set of top-level predicate
+      * names (function and method) declared in `pkg`. `importedPredicateNames(qual)` returns the
+      * set of predicate names exposed by the package imported under qualifier `qual`, or an
+      * empty set if `qual` is not an import qualifier or its imports aren't yet known. */
+    def rewrite(
+      pkg: PPackage,
+      localPredicateNames: Set[String],
+      importedPredicateNames: String => Set[String],
+    )(positions: Positions): PPackage =
+      new Impl(positions).run(pkg, localPredicateNames, importedPredicateNames)
   }
 
   private class SyntaxAnalyzer[Rule <: ParserRuleContext, Node <: AnyRef](tokens: CommonTokenStream, source: Source, errors: ListBuffer[ParserError], pom: PositionManager, specOnly: Boolean = false) extends GobraParser(tokens){

From 67615b3aa121a16b58c40523396bc8eaf94daf9c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Mon, 4 May 2026 22:04:03 +0200
Subject: [PATCH 06/11] Update
 src/test/resources/regressions/features/defunc/mutex1.gobra

---
 src/test/resources/regressions/features/defunc/mutex1.gobra | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/test/resources/regressions/features/defunc/mutex1.gobra b/src/test/resources/regressions/features/defunc/mutex1.gobra
index cadee8dab..874486850 100644
--- a/src/test/resources/regressions/features/defunc/mutex1.gobra
+++ b/src/test/resources/regressions/features/defunc/mutex1.gobra
@@ -10,7 +10,6 @@ pred mutexInvariant(x *int) {
 	acc(x)
 }
 
-// For now, requires parentheses surrounding exp{...}
 requires acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant{x}
 ensures acc(pmutex.LockP(), _) && pmutex.LockInv() == mutexInvariant{x}
 func foo(pmutex *sync.Mutex, x *int) {

From 36abfbac1aad74c654b85de1c8d8349cb05af10d Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 5 May 2026 10:36:18 +0000
Subject: [PATCH 07/11] Address PR review: drop two-pass design, remove dead
 `!<` tokens

- Collapse the predicate-constructor disambiguation into a single pass
  driven by `Info.checkSources`. The earlier parse-time postprocessor
  was redundant: the type-check-time pass already has full access to
  local predicate declarations and (via `dependentTypeInfo`) imported
  ones, so a separate parse-time rewrite added no information and made
  it unclear why both passes carried a `localPredicateNames` argument.
- Remove the now-unused `L_PRED` (`!<`) and `R_PRED` (`!>`) lexer tokens
  and the corresponding closing-bracket exception in `GobraParserBase`.
- Add comments in the rewriter clarifying that the `id.name` check on a
  `PDot` base catches local method-predicate references such as
  `recv.isZero{...}` and `Mutex.isZero{...}`.
- Document in `ParserUnitTests` why the existing predicate-constructor
  tests parenthesise the base, and add a parser-level test that pins
  down the `PCompositeLit` shape produced for an unparenthesised
  `name{...}` (the form that `Info.rewritePredConstructors` later
  converts into a `PPredConstructor`).

https://claude.ai/code/session_01DoEQdoLVWuLxD2mQUJDDRg
---
 src/main/antlr4/GobraLexer.g4                 |  2 -
 .../viper/gobra/frontend/GobraParserBase.java |  5 +-
 .../scala/viper/gobra/frontend/Parser.scala   | 47 ++++++--------
 .../viper/gobra/frontend/info/Info.scala      | 62 +++++++++----------
 .../viper/gobra/parsing/ParserUnitTests.scala | 18 ++++++
 5 files changed, 68 insertions(+), 66 deletions(-)

diff --git a/src/main/antlr4/GobraLexer.g4 b/src/main/antlr4/GobraLexer.g4
index ffeafe4d5..f56f91bbd 100644
--- a/src/main/antlr4/GobraLexer.g4
+++ b/src/main/antlr4/GobraLexer.g4
@@ -57,8 +57,6 @@ IMPLIES     : '==>';
 WAND        : '--*';
 APPLY       : 'apply';
 QMARK       : '?';
-L_PRED      : '!<';
-R_PRED      : '!>' -> mode(NLSEMI);
 SEQ         : 'seq'-> mode(NLSEMI);
 SET         : 'set'-> mode(NLSEMI);
 MSET        : 'mset'-> mode(NLSEMI);
diff --git a/src/main/java/viper/gobra/frontend/GobraParserBase.java b/src/main/java/viper/gobra/frontend/GobraParserBase.java
index 3d3ee41ab..993d59076 100644
--- a/src/main/java/viper/gobra/frontend/GobraParserBase.java
+++ b/src/main/java/viper/gobra/frontend/GobraParserBase.java
@@ -14,13 +14,12 @@ protected GobraParserBase(TokenStream input) {
     }
 
     /**
-     * Returns true if the current Token is a closing bracket (")", "}" or "!>")
+     * Returns true if the current Token is a closing bracket (")" or "}")
      */
     protected boolean closingBracket()
     {
         BufferedTokenStream stream = (BufferedTokenStream)_input;
         int prevTokenType = stream.LA(1);
-        // Gobra change: Also allow semicolons to be left out right before !>
-        return prevTokenType == GobraParser.R_CURLY || prevTokenType == GobraParser.R_PAREN || prevTokenType == GobraParser.R_PRED;
+        return prevTokenType == GobraParser.R_CURLY || prevTokenType == GobraParser.R_PAREN;
     }
 }
diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala
index f816d0256..c1b7bf9be 100644
--- a/src/main/scala/viper/gobra/frontend/Parser.scala
+++ b/src/main/scala/viper/gobra/frontend/Parser.scala
@@ -239,7 +239,6 @@ object Parser extends LazyLogging {
       postprocessors = Seq(
         new ImportPostprocessor(parseAst.positions.positions),
         new TerminationMeasurePostprocessor(parseAst.positions.positions, specOnly = specOnly),
-        new PredicateConstructorPostprocessor(parseAst.positions.positions),
       )
       postprocessedAst <- postprocessors.foldLeft[Either[Vector[ParserError], PPackage]](Right(parseAst)) {
         case (Right(ast), postprocessor) => postprocessor.postprocess(ast)(config)
@@ -516,35 +515,16 @@ object Parser extends LazyLogging {
     }
   }
 
-  private class PredicateConstructorPostprocessor(override val positions: Positions) extends Postprocessor {
-    /**
-      * Predicate constructors share their `name { args }` surface syntax with composite literals,
-      * so the parser conservatively builds a `PCompositeLit` for `IDENT { ... }` and
-      * `IDENT.IDENT { ... }` shapes. This postprocessor rewrites such literals into
-      * `PPredConstructor` when they are unambiguously predicate constructors:
-      *   1. They contain at least one positional `_` element (illegal in composite literals), or
-      *   2. The named/dotted base resolves syntactically to a top-level predicate declared in
-      *      the current package or to a built-in predicate.
-      *
-      * Cross-package cases (e.g. `pkg.P{1}()`) are deferred to a second pass driven by the
-      * type checker -- see [[PredicateConstructorRewriter.rewriteCrossPackage]].
-      */
-    def postprocess(pkg: PPackage)(config: Config): Either[Vector[ParserError], PPackage] = {
-      // collect names of all top-level (function and method) predicate declarations
-      val localPredicateNames: Set[String] = pkg.programs.flatMap(_.declarations.collect {
-        case d: PFPredicateDecl => d.id.name
-        case d: PMPredicateDecl => d.id.name
-      }).toSet
-      Right(PredicateConstructorRewriter.rewrite(pkg, localPredicateNames, _ => Set.empty)(positions))
-    }
-  }
-
   /**
-    * Shared rewrite logic that turns `PCompositeLit` nodes whose name resolves (syntactically) to
-    * a predicate into the equivalent `PPredConstructor`. Used both by the parse-time
-    * [[PredicateConstructorPostprocessor]] (which only knows the current package's predicates)
-    * and by [[viper.gobra.frontend.info.Info]] (which additionally has access to imported
-    * packages' predicate names via `dependentTypeInfo`).
+    * Rewrites `PCompositeLit` nodes whose name resolves (syntactically) to a predicate into the
+    * equivalent `PPredConstructor`. Predicate constructors (`P{x, _}`) and composite literals
+    * (`T{x, y}`) share the same surface syntax, so the parser uniformly builds `PCompositeLit`
+    * for `IDENT { ... }` and `IDENT.IDENT { ... }` shapes; we resolve the ambiguity here, once
+    * the type checker has enough information.
+    *
+    * Called from [[viper.gobra.frontend.info.Info]] just before constructing each
+    * `TypeInfoImpl`: at that point `dependentTypeInfo` is available, so we can ask each
+    * imported package whether `pkg.P` is a predicate.
     */
   object PredicateConstructorRewriter {
     private lazy val builtInPredicateNames: Set[String] =
@@ -571,9 +551,18 @@ object Parser extends LazyLogging {
         def shouldRewrite(typ: PLiteralType, lit: PLiteralValue): Boolean = {
           if (hasKey(lit)) false
           else typ match {
+            // Plain `P{...}`: a function predicate of the current package or a built-in fpredicate.
             case PNamedOperand(id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
+            // `qual.id{...}`: three flavours sharing this surface form. The `id.name` check
+            // catches local method-predicate references (`recv.isZero{...}` or
+            // `Mutex.isZero{...}`) where the qualifier names a value/type of the current
+            // package; the imported-names check catches imported function-predicate references
+            // (`pkg.P{...}`).
             case PDot(qual: PNamedOperand, id) =>
               hasBlank(lit) || isLocalOrBuiltInPredName(id.name) || importedPredicateNames(qual.id.name).contains(id.name)
+            // Other dotted bases shouldn't actually occur for `PCompositeLit` since the grammar
+            // restricts the type of a composite literal to a `typeName` (single ident or
+            // qualifiedIdent), but we keep this defensive branch for symmetry.
             case PDot(_, id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
             case _ => false
           }
diff --git a/src/main/scala/viper/gobra/frontend/info/Info.scala b/src/main/scala/viper/gobra/frontend/info/Info.scala
index be7b6909f..4ed099950 100644
--- a/src/main/scala/viper/gobra/frontend/info/Info.scala
+++ b/src/main/scala/viper/gobra/frontend/info/Info.scala
@@ -222,57 +222,55 @@ object Info extends LazyLogging {
   }
 
   /**
-    * Performs a second-pass rewrite of cross-package predicate constructors.
+    * Resolves the parser's deliberate ambiguity between composite literals and predicate
+    * constructors: rewrites `PCompositeLit` nodes whose name resolves to a predicate into the
+    * equivalent `PPredConstructor`.
     *
-    * The parse-time postprocessor only knows the current package's predicate names and so
-    * leaves expressions like `pkg.P{1}()` -- where `P` is a predicate declared in the imported
-    * package `pkg` -- as `PCompositeLit`. Once `dependentTypeInfo` is available, we know each
-    * import's qualifier name and can ask its `ExternalTypeInfo` whether a given identifier
-    * resolves to a predicate.
+    * Runs once per package, just before the package's `TypeInfoImpl` is constructed. By that
+    * point all imported packages have been type-checked (Gobra processes packages in
+    * dependency order), so we have access to:
+    *   - the current package's top-level `pred` declarations, and
+    *   - each imported package's exported predicate names via `dependentTypeInfo`.
+    *
+    * Both are passed to [[viper.gobra.frontend.Parser.PredicateConstructorRewriter.rewrite]]
+    * so the rewrite can distinguish predicate constructors from genuine struct/array/etc.
+    * composite literals.
     */
-  private def rewriteCrossPackagePredConstructors(
+  private def rewritePredConstructors(
     pkg: PPackage,
     deps: Map[AbstractImport, ExternalTypeInfo],
   ): PPackage = {
-    import viper.gobra.ast.frontend.PExplicitQualifiedImport
+    import viper.gobra.ast.frontend.{PExplicitQualifiedImport, PFPredicateDecl, PMPredicateDecl}
 
-    // Local predicate names (function and method): used to skip work for cases the parse-time
-    // postprocessor already handled.
+    // Names of all top-level (function and method) predicates declared in the current package.
     val localPredicateNames: Set[String] = pkg.programs.flatMap(_.declarations.collect {
-      case d: viper.gobra.ast.frontend.PFPredicateDecl => d.id.name
-      case d: viper.gobra.ast.frontend.PMPredicateDecl => d.id.name
+      case d: PFPredicateDecl => d.id.name
+      case d: PMPredicateDecl => d.id.name
     }).toSet
 
-    // Build a per-program function: qualifier-name -> set of predicate names exposed by the
-    // package imported under that qualifier.
+    // Map: import-qualifier -> set of predicate names declared in that imported package.
     val importedByQualifier: Map[String, Set[String]] = pkg.programs.flatMap { prog =>
       prog.imports.collect {
         case pi: PExplicitQualifiedImport =>
-          val abstractImport = RegularImport(pi.importPath)
-          deps.get(abstractImport).map { extInfo =>
-            // walk the imported package's declarations and collect top-level predicate names
+          deps.get(RegularImport(pi.importPath)).map { extInfo =>
             val importedPkg = extInfo.getTypeInfo match {
               case ti: TypeInfoImpl => Some(ti.tree.root)
               case _ => None
             }
             val names: Set[String] = importedPkg.toVector.flatMap(_.programs.flatMap(_.declarations.collect {
-              case d: viper.gobra.ast.frontend.PFPredicateDecl => d.id.name
-              case d: viper.gobra.ast.frontend.PMPredicateDecl => d.id.name
+              case d: PFPredicateDecl => d.id.name
+              case d: PMPredicateDecl => d.id.name
             })).toSet
             pi.qualifier.name -> names
           }
       }.flatten
     }.toMap
 
-    if (importedByQualifier.isEmpty) pkg
-    else {
-      val positions = pkg.positions.positions
-      viper.gobra.frontend.Parser.PredicateConstructorRewriter.rewrite(
-        pkg,
-        localPredicateNames,
-        q => importedByQualifier.getOrElse(q, Set.empty),
-      )(positions)
-    }
+    viper.gobra.frontend.Parser.PredicateConstructorRewriter.rewrite(
+      pkg,
+      localPredicateNames,
+      q => importedByQualifier.getOrElse(q, Set.empty),
+    )(pkg.positions.positions)
   }
 
   type TypeInfoCacheKey = String
@@ -309,10 +307,10 @@ object Info extends LazyLogging {
     var cacheHit: Boolean = true
     def getTypeInfo(pkg: PPackage, dependentTypeInfo: Map[AbstractImport, ExternalTypeInfo], isMainContext: Boolean, config: Config): TypeInfoImpl = {
       cacheHit = false
-      // Rewrite any remaining `pkg.P{...}` composite literals into predicate constructors when
-      // `P` is a top-level predicate of the imported package. This finishes the disambiguation
-      // started at parse time (see Parser.PredicateConstructorPostprocessor).
-      val rewrittenPkg = rewriteCrossPackagePredConstructors(pkg, dependentTypeInfo)
+      // Resolve `name { args }` composite-literal-vs-predicate-constructor ambiguity now that
+      // we know the current package's predicates and (from `dependentTypeInfo`) those of every
+      // imported package -- see [[rewritePredConstructors]].
+      val rewrittenPkg = rewritePredConstructors(pkg, dependentTypeInfo)
       val tree = new GoTree(rewrittenPkg)
       new TypeInfoImpl(tree, dependentTypeInfo, isMainContext)(config: Config)
     }
diff --git a/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala b/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala
index 262d628eb..a1e4af9c3 100644
--- a/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala
+++ b/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala
@@ -2493,6 +2493,12 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside {
     }
   }
 
+  // Predicate constructors share their `name { args }` surface syntax with composite literals.
+  // For an *isolated* expression the parser cannot tell the two apart on its own -- the
+  // disambiguation is performed by `Info.rewritePredConstructors` once the type checker knows
+  // whether `name` denotes a predicate. The `parseExp*` helpers below stop short of typing, so
+  // we wrap the base in parentheses to route through the `primaryExpr predConstructArgs`
+  // grammar rule, which produces a `PPredConstructor` directly without relying on the rewrite.
   test("Parser: should be able to parse a fpredicate constructor") {
     frontend.parseExpOrFail("(mutexInvariant){x}") should matchPattern {
       case PPredConstructor(PFPredBase(PIdnUse("mutexInvariant")), Vector(Some(PNamedOperand(PIdnUse("x"))))) =>
@@ -2511,6 +2517,18 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside {
     }
   }
 
+  // Without parentheses, `name { args }` parses as a `PCompositeLit`. The parse tree itself
+  // does not encode that this is a predicate constructor -- that decision is made later by
+  // `Info.rewritePredConstructors`, which has access to the surrounding declarations.
+  test("Parser: should parse `name{x}` as a composite literal at the syntax level") {
+    frontend.parseExpOrFail("mutexInvariant{x}") should matchPattern {
+      case PCompositeLit(
+        PNamedOperand(PIdnUse("mutexInvariant")),
+        PLiteralValue(Vector(PKeyedElement(None, PExpCompositeVal(PNamedOperand(PIdnUse("x")))))),
+      ) =>
+    }
+  }
+
 
   /* ** Parser tests related to explicit ghost statements */
 

From 11036d80b841065819bb0bbb5564f80f76c98355 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 5 May 2026 13:04:36 +0000
Subject: [PATCH 08/11] Address Linard's PDot ambiguity cases

Linard pointed out two false-positive scenarios for `qual.iden{...}`:
1. `iden` is an imported struct type *and* a local fpredicate or
   mpredicate -- the previous code rewrote based on the local match,
   silently turning a struct literal into a predicate constructor.
2. `iden` is an imported struct type *and* an imported mpredicate of
   the same package -- the previous code lumped imported mpredicates
   into the per-qualifier predicate-name set, again clobbering the
   struct literal interpretation.

Both stem from giving the local namespace and imported method
predicates a vote when the qualifier is an import. The qualifier
already determines whose namespace the second identifier lives in.
The new logic on `PDot(qual, id)`:

- If `qual` is a known import qualifier, only the imported package's
  *function*-predicate names are checked. Imported mpredicates aren't
  reachable as `qual.id` (they live on types, accessed via
  `qual.Type.id`), so they no longer compete with type names.
- Otherwise `qual` is a (local) value, type, or undeclared identifier.
  In Go, `qual.id` cannot be a type expression in any of those cases,
  so the composite-literal interpretation is structurally impossible
  and we rewrite unconditionally. The type checker will surface a
  precise error if `id` isn't actually a (method) predicate.

`Info.rewritePredConstructors` now passes the import qualifiers and the
imported fpredicate names separately, and only collects fpredicates
from imported packages.

https://claude.ai/code/session_01DoEQdoLVWuLxD2mQUJDDRg
---
 .../scala/viper/gobra/frontend/Parser.scala   | 70 ++++++++++++++-----
 .../viper/gobra/frontend/info/Info.scala      | 30 +++++---
 2 files changed, 74 insertions(+), 26 deletions(-)

diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala
index c1b7bf9be..80553a359 100644
--- a/src/main/scala/viper/gobra/frontend/Parser.scala
+++ b/src/main/scala/viper/gobra/frontend/Parser.scala
@@ -538,7 +538,8 @@ object Parser extends LazyLogging {
       def run(
         pkg: PPackage,
         localPredicateNames: Set[String],
-        importedPredicateNames: String => Set[String],
+        importQualifiers: Set[String],
+        importedFPredicateNames: String => Set[String],
       ): PPackage = {
         def hasKey(lit: PLiteralValue): Boolean = lit.elems.exists(_.key.isDefined)
         def hasBlank(lit: PLiteralValue): Boolean = lit.elems.exists {
@@ -548,21 +549,46 @@ object Parser extends LazyLogging {
         def isLocalOrBuiltInPredName(name: String): Boolean =
           localPredicateNames.contains(name) || builtInPredicateNames.contains(name)
 
+        // Determines whether a `PCompositeLit` should be reinterpreted as a `PPredConstructor`.
+        //
+        // The disambiguation hinges on what `typ` could mean. Go's package-level namespace is
+        // unique, so for a single name we have at most one declaration; for a dotted name
+        // `qual.id` the meaning of `id` is determined by what `qual` is.
         def shouldRewrite(typ: PLiteralType, lit: PLiteralValue): Boolean = {
+          // Composite literals with keyed elements (`T{x: 1}`) are never predicate constructors.
           if (hasKey(lit)) false
           else typ match {
-            // Plain `P{...}`: a function predicate of the current package or a built-in fpredicate.
+            // `IDENT{...}`: by Go's name uniqueness, IDENT is at most one of {fpredicate,
+            // type, ...}. If it's a (function or built-in) predicate name, rewrite.
             case PNamedOperand(id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
-            // `qual.id{...}`: three flavours sharing this surface form. The `id.name` check
-            // catches local method-predicate references (`recv.isZero{...}` or
-            // `Mutex.isZero{...}`) where the qualifier names a value/type of the current
-            // package; the imported-names check catches imported function-predicate references
-            // (`pkg.P{...}`).
+
+            // `qual.id{...}` with `qual` a single identifier. Two cases.
             case PDot(qual: PNamedOperand, id) =>
-              hasBlank(lit) || isLocalOrBuiltInPredName(id.name) || importedPredicateNames(qual.id.name).contains(id.name)
-            // Other dotted bases shouldn't actually occur for `PCompositeLit` since the grammar
-            // restricts the type of a composite literal to a `typeName` (single ident or
-            // qualifiedIdent), but we keep this defensive branch for symmetry.
+              if (importQualifiers.contains(qual.id.name)) {
+                // `qual` is an import alias. `qual.id` is therefore a top-level name in the
+                // imported package, which means it is *either* a type (struct literal) *or* a
+                // top-level function predicate (predicate constructor). Imported method
+                // predicates are not in scope as `qual.id` -- they are reached via
+                // `qual.Type.id`, which doesn't fit `qualifiedIdent`. So we look only at
+                // imported fpredicate names. Importantly, we do *not* fall back to local
+                // predicate names: the local namespace is irrelevant when the qualifier is an
+                // import.
+                hasBlank(lit) || importedFPredicateNames(qual.id.name).contains(id.name)
+              } else {
+                // `qual` is a (local) value, type, or undeclared identifier. Either way
+                // `qual.id` is not a Go type expression -- Go has no nested types, struct
+                // fields are not types, and method values aren't types either -- so the
+                // composite-literal interpretation is structurally impossible. The only valid
+                // reading is a method-predicate reference (`recv.isZero{...}` or the
+                // predicate-expression form `Mutex.isZero{...}`). Rewrite unconditionally and
+                // let the type checker emit a precise error if `id` isn't actually a predicate.
+                true
+              }
+
+            // Defensive: composite-literal `typ` is grammatically restricted to
+            // `typeName: IDENT | qualifiedIdent`, so a `PDot` whose base isn't a
+            // `PNamedOperand` shouldn't reach this point. Treat like the `PNamedOperand` case
+            // above.
             case PDot(_, id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
             case _ => false
           }
@@ -595,16 +621,26 @@ object Parser extends LazyLogging {
       }
     }
 
-    /** Runs the rewrite over `pkg`. `localPredicateNames` is the set of top-level predicate
-      * names (function and method) declared in `pkg`. `importedPredicateNames(qual)` returns the
-      * set of predicate names exposed by the package imported under qualifier `qual`, or an
-      * empty set if `qual` is not an import qualifier or its imports aren't yet known. */
+    /** Runs the rewrite over `pkg`.
+      *
+      * @param localPredicateNames     names of every top-level predicate (function or method)
+      *                                declared in `pkg`. Used to disambiguate the unqualified
+      *                                `IDENT{...}` form.
+      * @param importQualifiers        the set of import qualifier names visible in `pkg`. Used
+      *                                to decide whether the qualifier in `qual.id{...}` refers
+      *                                to an imported package or to a local value/type.
+      * @param importedFPredicateNames `importedFPredicateNames(q)` is the set of top-level
+      *                                function-predicate names in the package imported under
+      *                                qualifier `q`. Method predicates are intentionally
+      *                                omitted: they aren't reachable as `q.id`.
+      */
     def rewrite(
       pkg: PPackage,
       localPredicateNames: Set[String],
-      importedPredicateNames: String => Set[String],
+      importQualifiers: Set[String],
+      importedFPredicateNames: String => Set[String],
     )(positions: Positions): PPackage =
-      new Impl(positions).run(pkg, localPredicateNames, importedPredicateNames)
+      new Impl(positions).run(pkg, localPredicateNames, importQualifiers, importedFPredicateNames)
   }
 
   private class SyntaxAnalyzer[Rule <: ParserRuleContext, Node <: AnyRef](tokens: CommonTokenStream, source: Source, errors: ListBuffer[ParserError], pom: PositionManager, specOnly: Boolean = false) extends GobraParser(tokens){
diff --git a/src/main/scala/viper/gobra/frontend/info/Info.scala b/src/main/scala/viper/gobra/frontend/info/Info.scala
index 4ed099950..f7497818a 100644
--- a/src/main/scala/viper/gobra/frontend/info/Info.scala
+++ b/src/main/scala/viper/gobra/frontend/info/Info.scala
@@ -229,12 +229,14 @@ object Info extends LazyLogging {
     * Runs once per package, just before the package's `TypeInfoImpl` is constructed. By that
     * point all imported packages have been type-checked (Gobra processes packages in
     * dependency order), so we have access to:
-    *   - the current package's top-level `pred` declarations, and
-    *   - each imported package's exported predicate names via `dependentTypeInfo`.
+    *   - the current package's top-level `pred` declarations,
+    *   - the set of import qualifiers visible in the package, and
+    *   - each imported package's exported function-predicate names (via `dependentTypeInfo`).
     *
-    * Both are passed to [[viper.gobra.frontend.Parser.PredicateConstructorRewriter.rewrite]]
-    * so the rewrite can distinguish predicate constructors from genuine struct/array/etc.
-    * composite literals.
+    * The fpredicate-only restriction on the imported side avoids spurious rewrites of
+    * `pkg.T{...}` when `T` happens to share its name with a method predicate of some imported
+    * type: imported method predicates aren't reachable as `pkg.id`, so they don't compete with
+    * the type-name interpretation here.
     */
   private def rewritePredConstructors(
     pkg: PPackage,
@@ -243,13 +245,23 @@ object Info extends LazyLogging {
     import viper.gobra.ast.frontend.{PExplicitQualifiedImport, PFPredicateDecl, PMPredicateDecl}
 
     // Names of all top-level (function and method) predicates declared in the current package.
+    // Method predicates are included so that the unqualified `IDENT{...}` heuristic and the
+    // local method-predicate fallback see the same set of names; for the dotted import case
+    // they are deliberately *not* used (see Parser.PredicateConstructorRewriter).
     val localPredicateNames: Set[String] = pkg.programs.flatMap(_.declarations.collect {
       case d: PFPredicateDecl => d.id.name
       case d: PMPredicateDecl => d.id.name
     }).toSet
 
-    // Map: import-qualifier -> set of predicate names declared in that imported package.
-    val importedByQualifier: Map[String, Set[String]] = pkg.programs.flatMap { prog =>
+    // Set of import qualifiers visible in `pkg` (across all programs).
+    val importQualifiers: Set[String] = pkg.programs.flatMap(_.imports.collect {
+      case pi: PExplicitQualifiedImport => pi.qualifier.name
+    }).toSet
+
+    // Map: import-qualifier -> set of *function*-predicate names declared at the top level of
+    // the imported package. Method predicates are intentionally omitted: they are attached to
+    // types and so are not reachable as `qualifier.id`.
+    val importedFPredicatesByQualifier: Map[String, Set[String]] = pkg.programs.flatMap { prog =>
       prog.imports.collect {
         case pi: PExplicitQualifiedImport =>
           deps.get(RegularImport(pi.importPath)).map { extInfo =>
@@ -259,7 +271,6 @@ object Info extends LazyLogging {
             }
             val names: Set[String] = importedPkg.toVector.flatMap(_.programs.flatMap(_.declarations.collect {
               case d: PFPredicateDecl => d.id.name
-              case d: PMPredicateDecl => d.id.name
             })).toSet
             pi.qualifier.name -> names
           }
@@ -269,7 +280,8 @@ object Info extends LazyLogging {
     viper.gobra.frontend.Parser.PredicateConstructorRewriter.rewrite(
       pkg,
       localPredicateNames,
-      q => importedByQualifier.getOrElse(q, Set.empty),
+      importQualifiers,
+      q => importedFPredicatesByQualifier.getOrElse(q, Set.empty),
     )(pkg.positions.positions)
   }
 

From af082e0402a10266d29bf7c8079b383ea9b6da33 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 5 May 2026 13:08:04 +0000
Subject: [PATCH 09/11] Add regression test for shadowed-name
 predicate-constructor rewrite

Covers Linard's case 1: an importing package declares a local predicate
that shadows the name of a struct type exported by an imported package.
The new test (`import-preds-shadowed.gobra`) imports a `shadowed`
package whose `Foo` is a struct, and locally declares `pred Foo(...)`.
It exercises three forms in one file:

  - `shadowed.Foo{42}`  -- must stay a composite literal of the imported
                           struct, *despite* the local `pred Foo`.
  - `shadowed.Bar{1}`   -- imported fpredicate, must be rewritten.
  - `Foo{1}`            -- bare local fpredicate, must be rewritten.

If the rewriter fell back to local predicate names on the dotted import
form (the bug Linard pointed out), the first case would be incorrectly
rewritten to a `PPredConstructor` and type-checking would fail.

https://claude.ai/code/session_01DoEQdoLVWuLxD2mQUJDDRg
---
 .../defunc/import-preds-shadowed.gobra        | 32 +++++++++++++++++++
 .../defunc/includes/shadowed/shadowed.gobra   | 17 ++++++++++
 2 files changed, 49 insertions(+)
 create mode 100644 src/test/resources/regressions/features/defunc/import-preds-shadowed.gobra
 create mode 100644 src/test/resources/regressions/features/defunc/includes/shadowed/shadowed.gobra

diff --git a/src/test/resources/regressions/features/defunc/import-preds-shadowed.gobra b/src/test/resources/regressions/features/defunc/import-preds-shadowed.gobra
new file mode 100644
index 000000000..436478708
--- /dev/null
+++ b/src/test/resources/regressions/features/defunc/import-preds-shadowed.gobra
@@ -0,0 +1,32 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// ##(-I ./includes/)
+package pkg
+
+import "shadowed"
+
+// Local predicate that *intentionally* shares its name with the imported struct type
+// `shadowed.Foo`. The predicate-constructor rewrite must not be confused by this collision:
+// `shadowed.Foo{42}` is a composite literal of the imported struct, while bare `Foo{42}` is
+// a constructor of the local predicate.
+pred Foo(i int) {
+	i == i
+}
+
+// `shadowed.Foo{42}` is a struct literal of an imported type. Even though the current
+// package has a local predicate named `Foo`, `shadowed.Foo` lives entirely in the imported
+// package's namespace and is *not* a predicate, so the literal must remain a composite
+// literal.
+ensures res.x == 42
+func makeFoo() (res shadowed.Foo) {
+	return shadowed.Foo{42}
+}
+
+// `shadowed.Bar{1}` is an imported fpredicate constructor; it should be rewritten.
+requires shadowed.Bar{1}()
+func usesImportedPred()
+
+// `Foo{1}` references the *local* `Foo` predicate; it should also be rewritten.
+requires Foo{1}()
+func usesLocalPred()
diff --git a/src/test/resources/regressions/features/defunc/includes/shadowed/shadowed.gobra b/src/test/resources/regressions/features/defunc/includes/shadowed/shadowed.gobra
new file mode 100644
index 000000000..fb149e47b
--- /dev/null
+++ b/src/test/resources/regressions/features/defunc/includes/shadowed/shadowed.gobra
@@ -0,0 +1,17 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package shadowed
+
+// `Foo` is a struct type. Importantly, the importing package below also declares a local
+// predicate named `Foo`, so the predicate-constructor rewrite must not rely on the local
+// namespace when disambiguating `shadowed.Foo{...}`.
+type Foo struct {
+	x int
+}
+
+// `Bar` is a top-level function predicate, exposed under the same package. It shares its name
+// with no struct, so `shadowed.Bar{...}` is unambiguously a predicate constructor.
+pred Bar(i int) {
+	i == i
+}

From bff0e897a5dd2b8b634ce8e2ee03a28eceeeb780 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 5 May 2026 13:08:46 +0000
Subject: [PATCH 10/11] Add regression test for imported struct vs imported
 mpredicate name clash

Covers Linard's case 2: the imported package exports a struct `T` and
also has a method predicate `T` (on a different type). Imported method
predicates aren't reachable via the package qualifier, so
`shadowed_mpred.T{42}` should stay a composite literal of the struct
even though the predicate name `T` exists in the same imported package.

If `Info.rewritePredConstructors` collected imported `PMPredicateDecl`
names alongside `PFPredicateDecl` names (the bug Linard pointed out),
the rewrite would clobber the struct literal here.

https://claude.ai/code/session_01DoEQdoLVWuLxD2mQUJDDRg
---
 .../defunc/import-preds-shadowed-mpred.gobra   | 18 ++++++++++++++++++
 .../shadowed_mpred/shadowed_mpred.gobra        | 18 ++++++++++++++++++
 2 files changed, 36 insertions(+)
 create mode 100644 src/test/resources/regressions/features/defunc/import-preds-shadowed-mpred.gobra
 create mode 100644 src/test/resources/regressions/features/defunc/includes/shadowed_mpred/shadowed_mpred.gobra

diff --git a/src/test/resources/regressions/features/defunc/import-preds-shadowed-mpred.gobra b/src/test/resources/regressions/features/defunc/import-preds-shadowed-mpred.gobra
new file mode 100644
index 000000000..3e2a0e09f
--- /dev/null
+++ b/src/test/resources/regressions/features/defunc/import-preds-shadowed-mpred.gobra
@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// ##(-I ./includes/)
+package pkg
+
+import "shadowed_mpred"
+
+// `shadowed_mpred` exports both a struct `T` and a method predicate `T` (on `Holder`).
+// `shadowed_mpred.T{42}` is reachable as a *type name* (qualifiedIdent) and so must remain a
+// composite literal of the imported struct. The colliding mpredicate is not reachable as
+// `shadowed_mpred.T` -- it would be `shadowed_mpred.Holder.T`, which has three components and
+// doesn't fit the `qualifiedIdent` shape -- so the predicate-constructor rewrite must ignore
+// imported mpredicate names when disambiguating.
+ensures res.x == 42
+func makeT() (res shadowed_mpred.T) {
+	return shadowed_mpred.T{42}
+}
diff --git a/src/test/resources/regressions/features/defunc/includes/shadowed_mpred/shadowed_mpred.gobra b/src/test/resources/regressions/features/defunc/includes/shadowed_mpred/shadowed_mpred.gobra
new file mode 100644
index 000000000..a30ad6013
--- /dev/null
+++ b/src/test/resources/regressions/features/defunc/includes/shadowed_mpred/shadowed_mpred.gobra
@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package shadowed_mpred
+
+// Exposed struct type.
+type T struct {
+	x int
+}
+
+// `Holder` carries a method predicate that *also* happens to be named `T`. This is legal
+// Go-level naming: types and methods live in different namespaces, so `T` (the struct) and
+// `Holder.T` (the mpredicate) can coexist within the same package.
+type Holder struct{}
+
+pred (h Holder) T() {
+	true
+}

From cecf6c872454798519df8dc499e8a74854dd1e15 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 5 May 2026 17:13:46 +0000
Subject: [PATCH 11/11] Don't rewrite ADT constructor literals as predicate
 constructors

`X.A{}` where `X` is an ADT type and `A` is one of its constructors is
a legitimate composite-literal form that has nothing to do with
predicate constructors. The previous fix rewrote *every* `qual.id{...}`
whose qualifier wasn't an import qualifier under the (mistaken)
assumption that no other Go/Gobra construct used that shape. ADTs do.

Refine the disambiguation: in the dotted-non-import branch, only rewrite
when `id` actually matches a known method-predicate name (local or
built-in). The `IDENT{...}` branch is similarly tightened to consider
only function-predicate names, so an ADT whose bare clause name
(`B{}`) collides with a local *method*-predicate name still parses as
the ADT clause.

The rewriter API now takes `localFPredicateNames`,
`localMPredicateNames`, and the per-qualifier imported-fpredicate map
as separate arguments to keep the fpredicate-vs-mpredicate distinction
explicit at the call site. Restores `regressions/issues/000686-2.gobra`
without regressing any of the predicate-constructor regression suite.

https://claude.ai/code/session_01DoEQdoLVWuLxD2mQUJDDRg
---
 .../scala/viper/gobra/frontend/Parser.scala   | 84 +++++++++++--------
 .../viper/gobra/frontend/info/Info.scala      | 13 +--
 2 files changed, 56 insertions(+), 41 deletions(-)

diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala
index 80553a359..a03c42b3e 100644
--- a/src/main/scala/viper/gobra/frontend/Parser.scala
+++ b/src/main/scala/viper/gobra/frontend/Parser.scala
@@ -527,9 +527,13 @@ object Parser extends LazyLogging {
     * imported package whether `pkg.P` is a predicate.
     */
   object PredicateConstructorRewriter {
-    private lazy val builtInPredicateNames: Set[String] =
+    private lazy val builtInFPredicateNames: Set[String] =
       viper.gobra.frontend.info.base.BuiltInMemberTag.builtInMembers().collect {
-        case t: viper.gobra.frontend.info.base.BuiltInMemberTag.BuiltInPredicateTag => t.identifier
+        case t: viper.gobra.frontend.info.base.BuiltInMemberTag.BuiltInFPredicateTag => t.identifier
+      }.toSet
+    private lazy val builtInMPredicateNames: Set[String] =
+      viper.gobra.frontend.info.base.BuiltInMemberTag.builtInMembers().collect {
+        case t: viper.gobra.frontend.info.base.BuiltInMemberTag.BuiltInMPredicateTag => t.identifier
       }.toSet
 
     private class Impl(override val positions: Positions) extends PositionedRewriter {
@@ -537,7 +541,8 @@ object Parser extends LazyLogging {
 
       def run(
         pkg: PPackage,
-        localPredicateNames: Set[String],
+        localFPredicateNames: Set[String],
+        localMPredicateNames: Set[String],
         importQualifiers: Set[String],
         importedFPredicateNames: String => Set[String],
       ): PPackage = {
@@ -546,50 +551,56 @@ object Parser extends LazyLogging {
           case PKeyedElement(None, PExpCompositeVal(_: PBlankIdentifier)) => true
           case _ => false
         }
-        def isLocalOrBuiltInPredName(name: String): Boolean =
-          localPredicateNames.contains(name) || builtInPredicateNames.contains(name)
+        def isLocalOrBuiltInFPred(name: String): Boolean =
+          localFPredicateNames.contains(name) || builtInFPredicateNames.contains(name)
+        def isLocalOrBuiltInMPred(name: String): Boolean =
+          localMPredicateNames.contains(name) || builtInMPredicateNames.contains(name)
 
         // Determines whether a `PCompositeLit` should be reinterpreted as a `PPredConstructor`.
         //
-        // The disambiguation hinges on what `typ` could mean. Go's package-level namespace is
-        // unique, so for a single name we have at most one declaration; for a dotted name
-        // `qual.id` the meaning of `id` is determined by what `qual` is.
+        // We split the question by the syntactic shape of the literal's type: a single name
+        // (`IDENT{...}`), or a dotted name (`qual.id{...}`). For each shape we ask whether the
+        // identifier(s) could only sensibly denote a predicate.
         def shouldRewrite(typ: PLiteralType, lit: PLiteralValue): Boolean = {
           // Composite literals with keyed elements (`T{x: 1}`) are never predicate constructors.
           if (hasKey(lit)) false
           else typ match {
-            // `IDENT{...}`: by Go's name uniqueness, IDENT is at most one of {fpredicate,
-            // type, ...}. If it's a (function or built-in) predicate name, rewrite.
-            case PNamedOperand(id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
+            // `IDENT{...}`: bare names referring to a predicate must be top-level *function*
+            // predicates. Method-predicate references take the dotted form below; struct types,
+            // ADT clauses, and array/slice/map types share the package's name namespace with
+            // fpredicates and so cannot collide here (Go enforces uniqueness).
+            case PNamedOperand(id) => hasBlank(lit) || isLocalOrBuiltInFPred(id.name)
 
-            // `qual.id{...}` with `qual` a single identifier. Two cases.
+            // `qual.id{...}` with `qual` a single identifier. Two cases:
             case PDot(qual: PNamedOperand, id) =>
               if (importQualifiers.contains(qual.id.name)) {
                 // `qual` is an import alias. `qual.id` is therefore a top-level name in the
-                // imported package, which means it is *either* a type (struct literal) *or* a
-                // top-level function predicate (predicate constructor). Imported method
-                // predicates are not in scope as `qual.id` -- they are reached via
-                // `qual.Type.id`, which doesn't fit `qualifiedIdent`. So we look only at
-                // imported fpredicate names. Importantly, we do *not* fall back to local
-                // predicate names: the local namespace is irrelevant when the qualifier is an
-                // import.
+                // imported package -- either a type (struct literal) or a top-level function
+                // predicate (predicate constructor). Imported method predicates aren't
+                // reachable as `qual.id` (they live on types and need `qual.Type.id`), so we
+                // restrict the lookup to imported fpredicates and don't peek at the local
+                // namespace at all.
                 hasBlank(lit) || importedFPredicateNames(qual.id.name).contains(id.name)
               } else {
-                // `qual` is a (local) value, type, or undeclared identifier. Either way
-                // `qual.id` is not a Go type expression -- Go has no nested types, struct
-                // fields are not types, and method values aren't types either -- so the
-                // composite-literal interpretation is structurally impossible. The only valid
-                // reading is a method-predicate reference (`recv.isZero{...}` or the
-                // predicate-expression form `Mutex.isZero{...}`). Rewrite unconditionally and
-                // let the type checker emit a precise error if `id` isn't actually a predicate.
-                true
+                // `qual` is a (local) value, type, ADT, or undeclared identifier. The valid
+                // composite-literal forms in this branch are:
+                //   - ADT constructor literals: `X.A{...}` where X is an ADT type and A is a
+                //     constructor. These are *not* predicate constructors and must be left
+                //     alone.
+                // The valid predicate-constructor forms in this branch are:
+                //   - method-predicate references: `recv.isZero{...}` or the predicate-
+                //     expression form `Mutex.isZero{...}`.
+                // We disambiguate by checking whether `id` matches a known method-predicate
+                // name (local or built-in). The blank-identifier check still wins because `_`
+                // is illegal as a positional element in any composite literal.
+                hasBlank(lit) || isLocalOrBuiltInMPred(id.name)
               }
 
             // Defensive: composite-literal `typ` is grammatically restricted to
             // `typeName: IDENT | qualifiedIdent`, so a `PDot` whose base isn't a
-            // `PNamedOperand` shouldn't reach this point. Treat like the `PNamedOperand` case
-            // above.
-            case PDot(_, id) => hasBlank(lit) || isLocalOrBuiltInPredName(id.name)
+            // `PNamedOperand` shouldn't reach this point. Treat conservatively as the
+            // local-mpredicate case above.
+            case PDot(_, id) => hasBlank(lit) || isLocalOrBuiltInMPred(id.name)
             case _ => false
           }
         }
@@ -623,9 +634,11 @@ object Parser extends LazyLogging {
 
     /** Runs the rewrite over `pkg`.
       *
-      * @param localPredicateNames     names of every top-level predicate (function or method)
-      *                                declared in `pkg`. Used to disambiguate the unqualified
-      *                                `IDENT{...}` form.
+      * @param localFPredicateNames    names of every top-level function predicate declared in
+      *                                `pkg`. Used for the unqualified `IDENT{...}` form.
+      * @param localMPredicateNames    names of every top-level method predicate declared in
+      *                                `pkg`. Used for the dotted `qual.id{...}` form when
+      *                                `qual` is a local value/type (i.e. not an import alias).
       * @param importQualifiers        the set of import qualifier names visible in `pkg`. Used
       *                                to decide whether the qualifier in `qual.id{...}` refers
       *                                to an imported package or to a local value/type.
@@ -636,11 +649,12 @@ object Parser extends LazyLogging {
       */
     def rewrite(
       pkg: PPackage,
-      localPredicateNames: Set[String],
+      localFPredicateNames: Set[String],
+      localMPredicateNames: Set[String],
       importQualifiers: Set[String],
       importedFPredicateNames: String => Set[String],
     )(positions: Positions): PPackage =
-      new Impl(positions).run(pkg, localPredicateNames, importQualifiers, importedFPredicateNames)
+      new Impl(positions).run(pkg, localFPredicateNames, localMPredicateNames, importQualifiers, importedFPredicateNames)
   }
 
   private class SyntaxAnalyzer[Rule <: ParserRuleContext, Node <: AnyRef](tokens: CommonTokenStream, source: Source, errors: ListBuffer[ParserError], pom: PositionManager, specOnly: Boolean = false) extends GobraParser(tokens){
diff --git a/src/main/scala/viper/gobra/frontend/info/Info.scala b/src/main/scala/viper/gobra/frontend/info/Info.scala
index f7497818a..7c915b3aa 100644
--- a/src/main/scala/viper/gobra/frontend/info/Info.scala
+++ b/src/main/scala/viper/gobra/frontend/info/Info.scala
@@ -244,12 +244,12 @@ object Info extends LazyLogging {
   ): PPackage = {
     import viper.gobra.ast.frontend.{PExplicitQualifiedImport, PFPredicateDecl, PMPredicateDecl}
 
-    // Names of all top-level (function and method) predicates declared in the current package.
-    // Method predicates are included so that the unqualified `IDENT{...}` heuristic and the
-    // local method-predicate fallback see the same set of names; for the dotted import case
-    // they are deliberately *not* used (see Parser.PredicateConstructorRewriter).
-    val localPredicateNames: Set[String] = pkg.programs.flatMap(_.declarations.collect {
+    // Function vs method predicates are tracked separately: the rewriter needs to know which
+    // bucket to consult depending on the syntactic form (`IDENT{...}` vs `qual.id{...}`).
+    val localFPredicateNames: Set[String] = pkg.programs.flatMap(_.declarations.collect {
       case d: PFPredicateDecl => d.id.name
+    }).toSet
+    val localMPredicateNames: Set[String] = pkg.programs.flatMap(_.declarations.collect {
       case d: PMPredicateDecl => d.id.name
     }).toSet
 
@@ -279,7 +279,8 @@ object Info extends LazyLogging {
 
     viper.gobra.frontend.Parser.PredicateConstructorRewriter.rewrite(
       pkg,
-      localPredicateNames,
+      localFPredicateNames,
+      localMPredicateNames,
       importQualifiers,
       q => importedFPredicatesByQualifier.getOrElse(q, Set.empty),
     )(pkg.positions.positions)