Enhance user experience in face of false-positive type errors and type loss

Suggestion

A common source of frustration is false-positive type errors and cases when typing is lost. There are understandable reasons for limitations of the inference algorithm, but the sheer number of closed bug reports, features and stack overflow questions show that there is a big frustration around it.

I am referring to this: https://twitter.com/SeaRyanC/status/1544414378383925250

As a coder,

• I would like to be able to figure out whether I ran into a limitation in the inference algorithm or a real type bug. That could be facilitated by including the complexity limits the algorithm ran into while coming up with the type error. As a bonus, the compiler could suggest to use typings if we are sure that it is a false positive.

• I would like to be able to balance between the use of my brainpower spent on chasing false positives and the computing power spent on inference. That could be facilitated by making complexity limits configureable.

• I would like to be able to provide utility functions to make life easier, to be able to express things more succintly, which requires complex typing. Loosing typing in those situations means that the resulting usage will be more verbose (like because type templates should be filled in by hand) than the expressions those functions meant to replace, making the effort useless. I see two kinds of helps in those cases:

  • increase complexity limits for specific type functions
  • make it possible to drive the inference algorithm for a type function in much the same way we drive the solver when doing formal verification.

I do understand that it is a lot of features, some of them might be insanely complicated to implement. I am more of talking about a change of approach than about features implemented right now. I believe that the current status where coders are frustrated, and the whole thing is blamed on Gödel is unsustainable.

🔍 Search Terms

a lot of closed issues and feature request, and also a lot of Stack Overflow questions show that this topic does create a lot of frustration.

I searched for "inference" in feature requests

✅ Viability Checklist

My suggestion meets these guidelines:

• [ ✅ ] This wouldn't be a breaking change in existing TypeScript/JavaScript code
• [ ✅] This wouldn't change the runtime behavior of existing JavaScript code
• [ ✅ ] This could be implemented without emitting different JS based on the types of the expressions
• [ ✅ ] This isn't a runtime feature (e.g. library functionality, non-ECMAScript syntax with JavaScript output, new syntax sugar for JS, etc.)
• [ ✅ ] This feature would agree with the rest of TypeScript's Design Goals.

⭐ Suggestion

• configureable complexity of the inference algorithm
• errors stating which inference limits they have ran into
• ways to drive the inference algorithm exposed for type functions

📃 Motivating Example

When you run into a type error, the error message tells you what limitations the inference engine ran into, so it is easier to figure out whether it was a false positive or a real error.

You can set the limits of the inference engine in tsconfig.json, which you can increase to get rid of a false positive, and then it is your choice whether you wait more for the compiler to finish or use force-typing.

When you really need a type to be correct, you can drive the inference engine to achieve that without explosion of the decision space.

💻 Use Cases

My last false positive when Gödel got blamed. I do not believe it is that complex.
https://tsplay.dev/WJV6rW

A utility function (to work around the this idiocy of JS) with type loss:
https://tsplay.dev/NrQZ2w

Start with the two linked TypeScript playground examples, WJV6rW and NrQZ2w, and read the discussion comments for the reported false-positive and type-loss cases. Then investigate how TypeScript's inference limits and type functions are handled; the issue proposes several possible directions, so a concrete completion criterion is not defined.