Indeed. A type means assigning a rigid category to something.

There is not a single taxonomy that is universal, it ends up like the Celestial Emporium of Benevolent Knowledge that decides animals into:

    those belonging to the Emperor,

    those that are embalmed,

    those that are tame,

    pigs,

    sirens,

    imaginary animals,

    wild dogs,

    those included in this classification,

    those that are crazy-acting,

    those that are uncountable,

    those painted with the finest brush made of camel hair,

    miscellaneous,

    those which have just broken a vase, and

    those which, from a distance, look like flies.

Then you have a new use case.

What, to you, is an ultra strong type system? Both OCaml and Haskell are used in plenty of non academic contexts. Do you mean something like Coq or F*?

"plenty" is relative.

You don't see many GAFAM products created in either, and that's because of the trade off OP talks about.

I don't see many GAFAM products created in any functional language, even those with primitive type systems. Are you sure it is the type system that is scaring people away?

I was thinking of Haskell and F#. Neither one is completely unused outside of academic contexts but it is rare.

Rust is an example where a stronger type system has an associated payoff and it's being used all over.

In Idris you get to choose how strict you want to make your types. E.g. you can choose to use "Vect n a" if you want a vector a's where the size is tracked by the type system. Or you can use e.g. "List a" if you want a list of a's where the size is not tracked by the type system.

Of course the problem comes when you have to interface some code which expects a "Vect n a" and you have a "List a", but that's solvable by simply checking the size (dynamically) and deciding what to do if your "List a" isn't of size exactly n. (Fail, or whatever.). Going from "Vect n a" to a "List a" is trivial, of course.

... but really, that's where most of the friction is: Boundaries between APIs where the types don't quite line up. (Which is often the case for other languages, tbf. We tend to just notice less at compile time since most languages are so bad at expressing constraints.)