> Compiler would infer the types, and the programmer would read it and say, oh, I agree with this type, but I disagree with this type, that's perhaps wrong, this should be rather that type. Then the compiler would infer types again, based on programmer's incremental input.

This is possible today, at least in Haskell. (and I'd guess in OCaml too ... surely also Scala?)

Your proposal for adaptive data structure selection based on benchmarking is intriguing!