I do not have much personal experience, but SBCL's type inference is supposed to be decent/comparable to the Franz/Allegro/Lisp Works commercial options. I'm n

I do not have much personal experience, but SBCL's type inference is supposed to be decent/comparable to the Franz/Allegro/Lisp Works commercial options. I'm not sure if anyone has done "declare-density needed to achieve xyz perf" cross comparisons or the like. There is also https://en.wikipedia.org/wiki/Stalin_(Scheme_implementation) https://en.wikipedia.org/wiki/Stalin_(Scheme_implementation) which was doing lifetime analysis waaay back in the mid 90s, but I don't think Suskind had a declare system at all in Stalin. So, places where inference did not work were probably just "slow to be fixed by users tweaking code" to make inference better. I think he was mostly his own main user. Both Coalton & Carp do look interesting. There can be complaints with how "prefix notation" scales to large expressions. Cython is a gradually typed Python, but late noughties ideas in metaprogramming/macros/etc. never quite took off. There can be an undesirable effect of gradual/optional static types that code starts off "lazy" and then can require surprisingly large efforts to tighten down, especially in team settings. Even with profiling/90-10 heuristic rules, a later dev trying to optimize earlier lazy work can still be 10X, especially if type dynamism was really leaned upon. So, at least having an easy switch to force early/in-development static typing on original authors is likely a good thing (or at least strongly encourage with warnings...).