IDEs should suggest adding explicit type annotations when you get compiler errors related to type checking, maybe with a cute GUI so you can just click the places where type inference is happening to fill them in with what was inferred. that way the process of narrowing down the cause of a type error can be less tedious.

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.