Any statically typed language allows one to use dynamic types when it is necessary. I don't see the problem. If you need a map of string keys to variants, this can be done. At least one can still put some static constraints on the types when necessary.
Untyped languages make it very easy to write programs while the stronger the type system, the harder it gets to write the program in the first place.
I think balance is in order and this is one reason why we haven’t seen fancy type systems become mainstream except for niche domains. If I’m writing a program in F#, I have a balance between a type system constraining me but a language that allows me, the programmer, to do what I want to do for the most part. The stronger and fancier type systems means I now have to somehow teach the type system things that I already now how to do and are safe.
Fancy type systems simply try to say that you should write down a specification of your program. But in the real world, this is an enormously difficult if not impossible task. It makes the programming process and program rigid and brittle and not robust, which is not necessarily properties of software you want.
There’s a reason why certain language ecosystems like Erlang/Elixir say errors, unexpected input, and more pathological events will happen (i.e., they can’t be reasoned out of the system) and so you need a way to explicitly deal with them. This is also a big theme in the recent book Software Design for Flexibility in terms of expanding programs, getting them to handle things they couldn’t before.
While fancy type systems are neat, like those in Idris, I think the most useful idea is to have mixed type systems and programming paradigms in a program, which seems to be relatively unexplored right now.