I only glanced over the paper but its novelty seems to lie in the turnstile language itself, i.e. the design of a metalanguage to define EDSLs that have a types

I only glanced over the paper but its novelty seems to lie in the turnstile language itself, i.e. the design of a metalanguage to define EDSLs that have a typesystem. Yes, it is built using macros and I assume cleverly uses whatever macro system features Racket provides so there is possibly something novel there as well. However, the fact that it can be done or has been done on its own is not quite so surprising to me. If you have the ability to inspect syntax you can obviously do something like that.