Allow union types to pattern match type constraints

[SimonMeskens]

Not sure if this is a duplicate, I've searched, but couldn't find anything. Basically, allow union types to narrow types to fit constraints. I ran into this issue today, not allowing me to properly type a variable that I could clearly write the type for.

Would also negate the need for #12424 I think.

Specific case with fallbacks:

type A<T extends string> = { a: T };

type B<T> = A<T> | { b: number }

let x: B<string> // Should infer to type '{ a: string } | { b: number }'
let y: B<number> // Should infer to type '{ b: number }'

In this sample, we know there's an option that works regardless of T, so we only include the option with T if the constraint is met.

More general version allows pattern matching:

type A<T extends string> = { a: T };
type B<T extends number> = { b: T };

type C<T extends string | number> = A<T> | B<T>

let x: C<string> // Should infer to type '{ a: string }'

If the type system were able to solve this case, we'd basically get a really simple version of doing conditionals, type matching at a type level, etc.

Edge cases:
I would not make it order dependent because union types are not ordered. If multiple parts of the union check out, they should all be included. This is not an attempt at writing function overloads in types, though it could potentially be used as such for certain cases.

[olegdunkan]

Its looks like meta-programming, to force compiler to choose (evaluate) the type.

[SimonMeskens]

@olegdunkan

Its looks like meta-programming, to force compiler to choose (evaluate) the type.

Isn't that already what it does, all the time? The TypeScript compiler is constantly narrowing types, I'm just asking for another narrowing rule, namely that it eliminates impossible types from unions.

[olegdunkan]

type A<T extends string> = { a: T };
type B<T extends number> = { b: T };
type C<T extends string | number> = { c: T };

type D<T extends string | number> = A<T> | B<T> | C<T>

let x: D<string | number> ; //what to infer? {a:T} | {b:T} or {c:T}

And we break constraint rules.

[SimonMeskens]

What do you mean, what to infer? That example doesn't have a narrowing constraint, so no narrowing happens. Result is {a:T} | {b:T} | {c:T}

[SimonMeskens]

type A<T extends string> = { a: T };
type B<T extends number> = { b: T };
type C<T extends string | number> = { c: T };

type D<T extends string | number> = A<T> | B<T> | C<T>

let x: D<string | number> ; // x: {a:T} | {b:T} | {c:T}
let y: D<string> ; // x: {a:T} | {c:T}
let z: D<number> ; // x: {b:T} | {c:T}

[olegdunkan]

To understand each other. Do you suggest this form of discriminated unions

type T1<T extends U1> = ...;
type T2<T extends U2> = ...;
...
type Tn<T extends Un> = ...;

type U<T extends U1 | U2 | ... | Un> = T1<T> | T2<T> | ... | Tn<T>;

or

type T1<T extends ...> = U1;
type T2<T extends ...> = U2;
...
type Tn<T extends ...> = Un;

type U<T extends ...> = T1<T> | T2<T> | ... | Tn<T>;

where U1 | U2 | ... | Un are discriminated union?

[SimonMeskens]

Neither I think?

This first example wouldn't be allowed, because if U is a number, the result would be never.

type T1<T extends string> = Array<T>;
type U1<U extends string | number> = T1<U>; // error here, as it is now

This second example is allowed, because all possible values of U result in a valid type.

type T1<T extends string> = Array<T>;
type T2<T extends number> = Set<number>;
type U1<U extends string | number> = T1<U> | T2<U>; // no error

let x: U1<"foo"> // x: Array<"foo">
let y: U1<4> // x: Set<4>
let z: U1<"bar" | 2> // x: Array<"bar"> | Set<2>

The compiler doesn't "pick a type", all it does is narrow the type by eliminating cases from the discriminated union T1<U> | T2<U> once the generic type is known.

[olegdunkan]

))) I see, third case, discriminated union is T1<T> | T2<T> | ... | Tn<T>
But notion of the discriminated union supposes that resulting type of T1<T> | T2<T> | ... | Tn<T> will be some (only one) of them.
Conclude, for each Tn the compiler checks if type argument respects Tn's constraint then include Tn in the union.
But last question, how does the compiler understand that user wants to implement a discriminated union?
Because now it is not valid code:

type A<T extends string> = { a: T };
type B<T extends number> = { b: T };

type C<T extends string | number> = A<T> | B<T>; //error, C<T> constraint must be assignable to A<T> and B<T> constraints 

[SimonMeskens]

I think you're confused about what a discriminated union union type is. the "|" symbol in TypeScript denotes one basically. I'm not asking for a new feature, just some extra leniency on one end and a new type narrowing rule on the other.

[SimonMeskens]

I've replaced all instances of "discriminated union" with just "union type" to make it clearer. Not all union types are discriminated and I think that was causing some confusion. My mistake for not using the right words. Is it clearer now?

[olegdunkan]

Now, It is clear what you want. Thanks.

[gcnew]

Generally, I'm in two minds about type level pattern matching. On the one hand, it will allow interesting use cases to be properly typed, on the other, it'd add significant complexity. It's not clear how to do type inference, either.

type A<T extends string> = { a: T };
type B<T> = A<T> | { b: number }

Accepting definitions such as the above B worries me, because it breaks the intuition that T is valid for each of the constituents. A more straightforward approach has been proposed by @isiahmeadows in #13257, however its very very complicated. A less ambitions proposal might be a better start.

PS: Guards should be really simple, otherwise proving that moderately complex guards are total is far from trivial or even impossible - e.g. GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and laziness.

[dead-claudia]

Edit: Regarding my proposal in #13257.

@gcnew Yeah, and I should really re-work it enough to make the semantics a little clearer (it acts like it'll either match or error completely, when in reality, it should match or just fail, reusing that error if it's reasonably close).