> Typed Racket stems from a research interest and a bunch of great minds, not a need for ML and certainly not the need to be "mainstream".
You could argue the same point about language "becoming more than Lisp" though, they add features because they are good features, not to be "mainstream". That doesn't change the fact that Lisp is far from a pioneer in static typing compared to other languages.
Typed Racket has been at the bleeding edge of gradual typing research since a long time now, and the 'types as macros' papers made quite a splash, I think. Idris is also built on scheme. This fits the 'pioneering' aspect, I think. The point being that making new things, including new type systems, is much easier in lisp.
Much easier compared to what though? Agda is made in Haskell which recently got linear types. If you mean much easier than mainstream languages like JS, Python or Java you're right. If you mean much easier than everything, I think you're wrong.
You could argue the same point about language "becoming more than Lisp" though, they add features because they are good features, not to be "mainstream". That doesn't change the fact that Lisp is far from a pioneer in static typing compared to other languages.