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/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/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/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/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..a03c42b3e 100644
--- a/src/main/scala/viper/gobra/frontend/Parser.scala
+++ b/src/main/scala/viper/gobra/frontend/Parser.scala
@@ -515,6 +515,148 @@ object Parser extends LazyLogging {
     }
   }
 
+  /**
+    * 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 builtInFPredicateNames: Set[String] =
+      viper.gobra.frontend.info.base.BuiltInMemberTag.builtInMembers().collect {
+        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 {
+      def at[N <: AnyRef](node: N, source: PNode): N = { positions.dupPos(source, node); node }
+
+      def run(
+        pkg: PPackage,
+        localFPredicateNames: Set[String],
+        localMPredicateNames: 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 {
+          case PKeyedElement(None, PExpCompositeVal(_: PBlankIdentifier)) => true
+          case _ => false
+        }
+        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`.
+        //
+        // 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{...}`: 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:
+            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 -- 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, 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 conservatively as the
+            // local-mpredicate case above.
+            case PDot(_, id) => hasBlank(lit) || isLocalOrBuiltInMPred(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 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 =
+          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)
+          at(PProgram(prog.packageClause, prog.pkgInvariants, prog.imports, prog.friends, updatedDecls), prog)
+        }
+        at(PPackage(pkg.packageClause, updatedProgs, pkg.positions, pkg.info), pkg)
+      }
+    }
+
+    /** Runs the rewrite over `pkg`.
+      *
+      * @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.
+      * @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,
+      localFPredicateNames: Set[String],
+      localMPredicateNames: Set[String],
+      importQualifiers: Set[String],
+      importedFPredicateNames: String => Set[String],
+    )(positions: Positions): PPackage =
+      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 5b738cf2d..7c915b3aa 100644
--- a/src/main/scala/viper/gobra/frontend/info/Info.scala
+++ b/src/main/scala/viper/gobra/frontend/info/Info.scala
@@ -221,6 +221,71 @@ object Info extends LazyLogging {
     } yield typeInfo
   }
 
+  /**
+    * 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`.
+    *
+    * 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,
+    *   - the set of import qualifiers visible in the package, and
+    *   - each imported package's exported function-predicate names (via `dependentTypeInfo`).
+    *
+    * 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,
+    deps: Map[AbstractImport, ExternalTypeInfo],
+  ): PPackage = {
+    import viper.gobra.ast.frontend.{PExplicitQualifiedImport, PFPredicateDecl, PMPredicateDecl}
+
+    // 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
+
+    // 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 =>
+            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: PFPredicateDecl => d.id.name
+            })).toSet
+            pi.qualifier.name -> names
+          }
+      }.flatten
+    }.toMap
+
+    viper.gobra.frontend.Parser.PredicateConstructorRewriter.rewrite(
+      pkg,
+      localFPredicateNames,
+      localMPredicateNames,
+      importQualifiers,
+      q => importedFPredicatesByQualifier.getOrElse(q, Set.empty),
+    )(pkg.positions.positions)
+  }
+
   type TypeInfoCacheKey = String
   private val typeInfoCache: ConcurrentMap[TypeInfoCacheKey, TypeInfoImpl] = new ConcurrentHashMap()
 
@@ -255,7 +320,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)
+      // 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/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-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/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/import-preds.gobra b/src/test/resources/regressions/features/defunc/import-preds.gobra
index 3da5ec326..84e2c1b09 100644
--- a/src/test/resources/regressions/features/defunc/import-preds.gobra
+++ b/src/test/resources/regressions/features/defunc/import-preds.gobra
@@ -7,7 +7,7 @@ package pkg
 import "preds"
 
 // tests importing predicates from other packages
-requires preds.PredExample!<1!>()
-requires preds.PredExample!<_!>(2)
+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/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
+}
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
+}
diff --git a/src/test/resources/regressions/features/defunc/mutex1.gobra b/src/test/resources/regressions/features/defunc/mutex1.gobra
index 16cfa934b..874486850 100644
--- a/src/test/resources/regressions/features/defunc/mutex1.gobra
+++ b/src/test/resources/regressions/features/defunc/mutex1.gobra
@@ -10,14 +10,13 @@ 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!>
+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 +25,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 +35,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
diff --git a/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala b/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala
index 0ce28e67f..a1e4af9c3 100644
--- a/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala
+++ b/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala
@@ -2493,24 +2493,42 @@ 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 {
+    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"))))) =>
     }
   }
 
+  // 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 */