You seem to be implying these researchers are reinventing the wheel by making a syntax that isn't based on anything that's already implemented (like Haskell). That couldn't be further from it. The syntax is absolutely unimportant to a paper like this. Choosing to use curly braces is their version of naming a variable "foo". The goal is not to make a compiler that produces machine code or eventually gets a package manager, at all. They're not playing that game.
They are writing a type system, not a language. (Note the title.) They're attempting to write one that captures the very weak guarantees of concurrent systems, and this is actually really complicated, so research tends to start with a simple version of the new type system, and then steadily narrow the assumptions behind it over subsequent publications. The target is not machine code, but having a computer check your typing rules work and that you can write interesting proofs with it. The toy language only exists for this purpose. The same way a Haskell programmer might code until it compiles and then put it into production, a PL researcher codes until the Coq checker gets all the way through their proofs and then submits to the conference. And much the same way that you can implement a GHC extension to test an idea, Coq is an extremely feature-rich base to start building a type checker demo language and proof system. They are not wasting any time here.
The syntax they end up with is not meant to be used, it is meant to be the smallest possible language that demonstrates the theory in a machine-checkable way. If you want these features in a real language, take the OCaml type checker they wrote and go write it again for that new C++ frontend Circle or something, this time accounting for all the wild requirements that pop up in a real compiler.
They are writing a type system, not a language. (Note the title.) They're attempting to write one that captures the very weak guarantees of concurrent systems, and this is actually really complicated, so research tends to start with a simple version of the new type system, and then steadily narrow the assumptions behind it over subsequent publications. The target is not machine code, but having a computer check your typing rules work and that you can write interesting proofs with it. The toy language only exists for this purpose. The same way a Haskell programmer might code until it compiles and then put it into production, a PL researcher codes until the Coq checker gets all the way through their proofs and then submits to the conference. And much the same way that you can implement a GHC extension to test an idea, Coq is an extremely feature-rich base to start building a type checker demo language and proof system. They are not wasting any time here.
The syntax they end up with is not meant to be used, it is meant to be the smallest possible language that demonstrates the theory in a machine-checkable way. If you want these features in a real language, take the OCaml type checker they wrote and go write it again for that new C++ frontend Circle or something, this time accounting for all the wild requirements that pop up in a real compiler.