You're preaching to the choir about the superiority of static type systems, but your argument was about imperative vs/ functional, not dynamic vs/ strong.

GADT's and composition are trivial to achieve with imperative languages.

There's a reason not a single production imperative language supports GADTs. Imperative sequencing and mutability semantics, as done in practice, are inimical to rigorous formalization. When imperative language designers try to make a nice consistent type system, they hit road blocks early on and give up. Rust doesn't even support HKTs. GADTs are just an example of something that you rarely see in imperative languages because they almost never even make it that far.

One of the other nice things you get with languages with good functional/pure/immutable(/lazy) semantics are free theorems, where you can actually make strong useful statements about the nature of your program like "this will not crash", "this is memory safe", "this will terminate", "this follows the functor laws", etc. whereas it's effectively impossible to make such claims in a language with messier abstractions like loops and mutable variables.

Basically, the reason functional languages have better type systems is that their underlying untyped semantics are more sensible and simpler than the untyped semantics of mutable imperative (strict) languages, and this is reflected in the safety records of languages through mechanisms other than type safety.

> There's a reason not a single production imperative language supports GADTs.

Scala?

OCaml would also qualify as a counter example, although you cheated a bit by adding all these adjectives and you could argue that OCaml is not "production".

Haskell can easily do imperative as well.

I agree with you overall but I think you're drawing too strict a line between these concepts. Most of the guarantees you obtain from these languages do not even come close to "this will not crash" (this is very hard to guarantee in languages with no totality guarantee, i.e... most of them), let alone "this will terminate" (since most of these are Turing complete).

> Scala?

Well, I'd say Scala is definitely a functional language, but even then its GADT (and even plain old ADT) support is pretty limited and uncomfortable. "Case classes" are one of those things in Scala where it's obvious they're running into the limits of the JVM.

> OCaml would also qualify as a counter example

Again, I'd say OCaml is absolutely a functional language. It's also definitely a production language; I know of a number of firms that use it.

I should have said "Imperative and not Functional languages", a la C, C++, Java, Javascript, etc.

> Most of the guarantees you obtain from these languages

You're right, most of the guarantees you get from e.g. Haskell rely on people following the typeclass laws for whatever you're doing, which isn't necessarily the case. It's not a guarantee in the sense that e.g. Coq or Agda give you a guarantee; it's just a guarantee in the sense that if you follow some simple rules, you get good behavior.

As for totality and termination, it's true that you can't guarantee either in plain old Haskell, but Haskell (and some others) do support checking for pattern match completeness, and then it's not very hard to (informally) guarantee totality by sticking to certain pre-defined operations that operate on data (as opposed to codata) and have good decreasing/tightening rules. For example, if I saw some code composed entirely of functor/foldable/traversable operations over well-behaved data structures, I could be quite confident in correctness and termination.