Repository navigation
Enhance user experience in face of false-positive type errors and type loss #53977
Description
Activity
There's really only a tiny handful of such limits, e.g. 24 for expanding literal unions. I find it really unlikely that those represent the majority of cases where you're getting false positives unless it's something super domain-specific.
I do not believe it is that complex.
This example has nothing to do with the linked tweet thread, which I think you've overinterpreted beyond its original intention.
This is complex. It requires an entirely new way of tracking types to see that
fieldis the same variable with the same value in both locations. For example, from an analysis perspective, the code you have there is the same asfunction foo(currentUser: CreateUserDto,user: CreateUserDto) { const field1 = allowedPatchFields[Math.floor(Math.random() * 3)]; const field2 = allowedPatchFields[Math.floor(Math.random() * 3)]; currentUser[field1] = user[field2]; }
which is clearly unsafe.
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.
I think you've misapprehended how this works. One way to think of it is that when TS sees a
Strying to be used as aT, it "tries to construct a proof" (*) that all validSare validTs. If it can't do that, it might be because there truly areSs that aren'tTs. It might also be that it's just not clever enough to construct such a proof. But, by definition, we don't know which of those is happening.The same result is seen in other domains: We don't know if the Collatz conjecture is true or not. The lack of a counterexample doesn't mean that it is true, and it's not correct to say "The Collatz conjecture is true because we can't construct a counterexample". The only thing we can say is "We don't know how to construct a proof for this [yet]".
*It is not literally a proof solver and please don't overindex on this use of the phraseReacted by Bruce PascoeDevil’s advocate: We can (in theory, at least) tell the difference between “this is provably not assignable” vs. “we don’t have the tools to say whether it’s assignable or not”. Whether making this distinction in the compiler would be useful in practice is another matter (my money’s on probably not)
Reacted by Árpád MagosányiThere's really only a tiny handful of such limits, e.g. 24 for expanding literal unions.
In limits I also mean the cases when the algorithm does not look into something as it is deemed to explode the search space.
The only thing we can say is "We don't know how to construct a proof for this [yet]".
My understanding that there is the above case, and the "this is clearly wrong" case. Distinguishing between them would be helpful.
For example, from an analysis perspective, the code you have there is the same as
Until the "completely new way of tracking fields" is implemented. (You can take this as an example of a constraint of the nature I was talking about above.) Which obviously a programming effort. Which you understandably do not put into it if you suspect that the use cases of the new algorithm will be prohibitively resource intensive.
And it may wery well turn out that in most cases it is just a waste of effort.
But in this particular case I believe it would not be prohibitive. If you look at the problem from the perspective I offered, it is easier to implement such things, as it is sure that they won't be a complete waste of effort. Even if they have to be turned off by default, they can be turned on for the particular case they are needed.
Or alternatively you can probably shortcut it by allowing something along the lines offunction foo(currentUser: CreateUserDto,user: CreateUserDto) { for (const field of allowedPatchFields) { if (field in user) { const value = user[field]; currentUser[field as FieldOf<CreateUserDTO,for(typeof value)>] = value; // I do not intend to make a statement here about how the syntax should look like } } }Which i suspect that falls into the category of "driving the algorithm" I mentioned.
My last false positive when Gödel got blamed. I do not believe it is that complex.
tsplay.dev/WJV6rWSee @jcalz's answer to "Assert a value type is the same at both sides of the assignment" on StackOverflow for an explanation of why this code is invalid.
Relevant parts copied below for ease of reference and searchability:
Question (extract)
interface InterfaceA { transfer?: string[]; deposit?: number[]; test?: boolean[]; } interface InterfaceB extends InterfaceA { moretest?: boolean[]; } type Label = ("transfer" | "deposit" | "test") const a: InterfaceA = {} const b: InterfaceB = {} const labels: Label[] = ["transfer" , "deposit" , "test"]; for (const label of labels){ a[label] = b[label] }
Type 'string' is not assignable to type 'number'.
It fails to compile because
a[label](left side of the assignment) can be one ofstring[],number[]ortest[]whileb[label](right side of the assignment) can also be one ofstring[],number[]ortest[].It kinds of make sense, except that Typescript should know that if the left side is
string[], the right side will bestring[]too, same applies for the other types.This is why replacing the assignment with
a[label as "transfer"] = b[label as "transfer"]works.Answer (extract)
TypeScript can't handle "correlated union" types in which a single block of code is checked multiple types for each member of a union. This issue is described in detail in microsoft/TypeScript#30581.
From a pure type system perspective, it's unsafe, because the type of
b[label]is theInterfaceB[Label]union, and the compiler is worried that when you try to assign it toa[label]of union typeInterfaceA[Label], maybe the two keys are actually different? That is, it's ignoring the identity oflabeland just looking at the type. Put another way: imagine you hadlabel1andlabel2both of typeLabel. Thena[label1] = b[label2]would clearly be unsafe. (See microsoft/TypeScript#30769 for the pull request implementing this safety check.) Of course you're not doing this, but the compiler is unable to see the difference because the types are the same for both situations.~ jcalz
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:
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:
⭐ Suggestion
📃 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
thisidiocy of JS) with type loss:https://tsplay.dev/NrQZ2w