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?