> Or go the opposite way: If you want a language that feels dynamic and leads to prototyping, well a type system that is total and complete might be too heavy. Instead of only allowing programs that are proven to be typed correctly you might want to allow all programs that you can not proved to be wrong. Lean into gradual typing. Everything goes at first and the typing becomes as strict as the programmer decides based on how much type information they add.

If you have generics and want type annotations to type check at compile time, you are going to need unification,

let l: List<Animal> = List(dog, cat)

At that point, you have written all the machinery to do inference anyway, so might as well use it.

I guess you could have a language where the above must be gradually typed like

let l: List<Animal> = List<Animal>(dog: Animal, cat: Animal)

but that doesn't seem particularly ergonomic.