Generic parameter does not satisfy the constraint

Question

The following code gives the expected error Type 'Type[T][1]' does not satisfy the constraint 'Type[T][0]'.

declare type Type = {
  0: [B, A],
  1: [0, 0],
}

type A = { A: number }
type B = { B: number }

type FirstExtendsSecond<First extends Second, Second> = void;
type Test<T extends 0 | 1> = FirstExtendsSecond<Type[T][1], Type[T][0]>;

However, when we replace [0, 0] on line three with [A, A], the error disappears. This is very unexpected. Is the compiler unable to see that this is not allowed?

Answer 1

Unfortunately, TypeScript is indeed unable to see that what you are doing should be prohibited. The type checker takes shortcuts to check constraints, as described in GitHub issues such as microsoft/TypeScript#46076, and sometimes these shortcuts fail to catch errors.

This is one of the ways in which TypeScript's type system is intentionally unsound in order to keep TypeScript usable. The alternative would either be to: trade false negatives for false positives, breaking lots of real-world code; or try to make the compiler checks more accurate by doing more work, which would almost certainly degrade performance to an unacceptable level.

(For more information about TypeScript's complicated relationship with soundness, see microsoft/TypeScript#9825, as well as Why are TypeScript arrays covariant? and TypeScript type narrowing seems to make incorrect assumption where I've gone into this.)

---

Here's a slightly more explicit version of your code that explains why there should be an error somewhere:

type FirstExtendsSecond<X extends Y, Y> =
    [X] extends [Y] ? true : false; // should always be true

Since FirstExtendsSecond<X, Y> has a constraint on X, it should be impossible to write FirstExtendsSecond<X, Y> unless X extends Y is true. And it evaluates to a (non-distributive) conditional type where X extends Y is checked, so it should always return true, no matter what, right?

Nope! As you showed, we can do this:

declare type Type = {
    0: [string, number],
    1: [number, string],
}        
type Test<T extends 0 | 1> =
    FirstExtendsSecond<Type[T][1], Type[T][0]>; // no error

type Test0 = Test<0> // false 
type Test1 = Test<1> // false 

There's no error in the definition of Test, but both Test<0> and Test<1> evaluate to false! After all, neither string extends number nor number extends string are true. So why didn't Test's definition fail?

---

The answer is described in this comment in microsoft/TypeScript#46076. In order to evaluate whether types are compatible with other types, the following intentionally unsound rule is employed:

A type S is related to a type T[K] if S is related to C, where C is the base constraint of T[K]

In the above example that translates to

The type Type[T][1] is related to the type Type[T][0], since Type[T][1] is related to the base constraint of Type[T][0], which is Type[0 | 1][0], which is string | number.

Or, in other words, there is no error because when T is substituted with its constraint 0 | 1, it type checks:

type Test01 = Test<0 | 1> // true

The rule is unsound for the reason we showed. But it's useful. According to a comment on the related issue microsoft/TypeScript#27470:

We do this for reasons of backwards compatibility and also to avoid drowning in generic types.

There have been some soundness improvements over the history of the language, so I suppose there is a possibility that if someone filed an issue about this example, it could be fixed. But my strong suspicion is that such a report would be closed as a design limitation, since it's hard to make such changes without breaking real-world code.

Playground link to code