I think I got that in the form of type-aware auto completion in Atom with Haskell. It might be partially limited, but I'm not sure. It was rather flaky due to version missmatch between GHC and the language server.

It's pretty awesome.

Ah I have just realized it might be "just a classic typed language IDE" experience and Dependent Types seems just way above.

Am I missing something?

Yes. Dependent typed tell you that the vector you pass along the matrix to a matrix-vector-multiply has to be one with not just the right datatype, but also the right size. It could also suggest (postfix w.r.t. the container type) operators with better performance for the container's known size (range). Or, depending on previous conditionals, filter postfix operators you apply to a field of a datastructure, if that field is constrained by the condition branching on another field in the datastructure. I.e., applying a specific operator to a conditional sum type that's no longer a sum type if another variable / field is restricted beyond it's datatype (a range of integers, an enum value, a theoretical utf-8 string previously restricted to ASCII, etc.).