It is possible to violate generic constraints when distributing union types

[aweebit]

🔎 Search Terms

constraint, conditional, distributive, distributed, distribution

🕗 Version & Regression Information

• This is the behavior in every version I tried, and I reviewed the FAQ for entries about "constraint"

⏯ Playground Link

https://www.typescriptlang.org/play/?#code/C4TwDgpgBAkgznArhAPAQQDRQEJQgD2AgDsATOKNAPigF5K9CTypFiBrYgewHdiAoKFAD8ORkTIU2nXgKFDRAZQAWvdFmxVB8gFxRiEAG4QATtr0HjJgNz9+oSFBVrMYghJbU6UANqvsALpQAGRQAN4Avrb24NAAGt7wSKgADFAAPlAAjFhpmVlUtkA

💻 Code

type Issue<A, B extends A> = A extends unknown
  ? B extends unknown
    ? Show<A, B>
    : never
  : never;

type Show<A, B extends A> = [A, B] & {};

type X = Issue<0 | 1, 0 | 1>;

🙁 Actual behavior

X is evaluated to [0, 0] | [0, 1] | [1, 0] | [1, 1].

No errors are reported despite the [0, 1] | [1, 0] part resulting from the evaluation of Show<0, 1> and Show<1, 0> which should not be allowed because of the B extends A constraint.

🙂 Expected behavior

An error is reported on line 3, saying the constraint might be violated.

Additional information about the issue

This is how the type should actually be implemented:

type Issue<A, B extends A> = A extends unknown
  ? B extends A
    ? Show<A, B> // only B members that extend the current A member reach this line
    : never
  : never;

[snarbles2]

Well, where is the distribution actually occurring? Is Issue distributing to Show<0, 0> | Show<0, 1> | Show<1, 0> | Show<1, 1>? That would violate the constraint, but that's not the only path to the result you're seeing.

If the distribution occurs inside Show, then you're simply constructing Show<0 | 1, 0 | 1>, which satisfies the constraint and produces [0 | 1, 0 | 1], which is equivalent to [0, 0] | [0, 1] | [1, 0] | [1, 1].

In other words, I don't think the constraint has been technically violated. There's a possibility that TS took a wrong turn and happened to end up at the right place anyways. Looking at those extends clauses, I wonder if this is an oversimplification of some genuinely problematic code.

[jcalz]

There's definitely an unsoundness here. The most obvious way I can think of to demonstrate it looks like

type Issue<A extends number, B extends A> = A extends B ? never : Show<A, B>
type Show<A extends number, B extends A> = `${B} extends ${A}`

type Hmm = Issue<0 | 1, 0>
//   ^? type Hmm = "0 extends 1" // <-- amazing!

Playground link

where TS is apparently happy to evaluate Show<1, 0> despite the generic constraints being violated.

Whether or not this unsoundness amounts to a bug remains to be seen here (kind of guessing it's more trouble than it's worth to deal with it).

[snarbles2]

So... is it validating the constraints to Show based on the original types specified for A and B, and then performing the actual substitution for the arguments to Show based on the distributed (narrower) constituents?

[ahejlsberg]

In a conditional type A extends B ? XXX : YYY we can (and do) accurately infer the constraint A extends B in type XXX, but we lack the ability to express and infer the opposite constraint in YYY. In theory, negated types would help here as we could infer the constraint A extends not B (which in the case of Show<A, B> would then cause B to fail its B extends A static constraint). However, lacking that ability, we can't (and don't) infer a constraint for A in YYY. That in turn is why the violation described in the issue isn't reported.

So, as things stand, this is a design limitation.

[aweebit]

Anders Hejlsberg (@ahejlsberg) your comment seems to be an answer to Joe Calzaretta (@jcalz)'s comment. In my original example, the YYY branches are completely irrelevant.

[aweebit]

But also in Joe Calzaretta (@jcalz)'s example, I think there should be an error. In my opinion, surprising constraint violation like this should never be possible. If TypeScript doesn't have enough information to decide if a constraint is satisfied, an error should be reported so that the developer is forced to check it first like this:

type Issue<A extends number, B extends A> = A extends B ? never : /* --> */ B extends A ? Show<A, B> : never

The issue is about TypeScript assuming that B still extends A even after A is distributed, and the examples show that this assumption can be wrong. The particular conditional type branch where that leads to problems doesn't really matter.

[ahejlsberg]

I agree that assumptions made involving A don't always hold when A is distributed. In the example

type Issue<A extends number, B extends A> = A extends B ? Show<A, B> : never

it would seem correct to report an error in Show<A, B> that B doesn't extend the distributed A. In a sense, the distributed A should really behave as a new type variable that extends the non-distributed A. Of course we haven't done ourselves any favors by using the same name for the distributed and non-distributed versions of A.

[ahejlsberg]

A fix is now available in #64237.