Wrong inference of cross product if component union types exceed (small) cardinality

[MMF2]

Bug Report

We have two union types A = A1 | ... | Am and B = B1 | ... | Bm and construct the cross product A x B as a mapped type C. If the cardinality of n x m exceeds a certain (low) limit, then the inferred cross product seems to miss some pairs. It worked fine for n = 4, m = 6 and already failed for n = 5, m = 6.

We compare the cross product type C with a coextensional expanded type D. We conclude in the failure case n = 5, m = 6 that C misses some pair members since D extends C ? true : false evaluates to false (while it evaluates to true for the n = 4, m = 6 case) what signals that C has less members than D.

🔎 Search Terms

cross product, union, inference

🕗 TypeScript versions 4.2.2, 4.1.5

Example code: The role of type A is played by type RowObject, the role of B by ColumnObject, the role of C by PositionAsCrossProduct and the role of D by Position or equivalently by SinglePosition<Row, Column>. Type EQ checks for coextensionality of types.

⏯

Playground Link working example, n = 4 (cardinality of type Row), m = 6 (cardinality of type Column)

💻 Code working example:

type EQ<A, B> =
    [A] extends [B]
        ? ([B] extends [A] ? true : false)
        : false;

type Row = 0 | 1 | 2 | 3;
type Column = 0 | 1 | 2 | 3 | 4 | 5;

type SinglePosition<R extends Row, C extends Column> = { r: R, c: C };
type Position = { r: Row, c: Column };

type RowObject = { r: 0 } | { r: 1 } | { r: 2 } | { r: 3 };
type ColumnObject = { c: 0 } | { c: 1 } | { c: 2 } | { c: 3 } | { c: 4 } | { c: 5 };

type PositionAsCrossProduct = RowObject & ColumnObject;

let testPosition1: EQ<SinglePosition<Row, Column>, Position>;  // true
let testPosition2: SinglePosition<Row, Column> extends PositionAsCrossProduct ? true : false;  // true
let testPosition3: Position extends PositionAsCrossProduct ? true : false;  // true
let testPosition4: EQ<Position, Position>;  // true

⏯

Playground Link failing example, n = 5, m = 6

💻 Code failing example:

type EQ<A, B> =
    [A] extends [B]
        ? ([B] extends [A] ? true : false)
        : false;

type Row = 0 | 1 | 2 | 3 | 4;
type Column = 0 | 1 | 2 | 3 | 4 | 5;

type SinglePosition<R extends Row, C extends Column> = { r: R, c: C };
type Position = { r: Row, c: Column };

type RowObject = { r: 0 } | { r: 1 } | { r: 2 } | { r: 3 } | { r: 4 };
type ColumnObject = { c: 0 } | { c: 1 } | { c: 2 } | { c: 3 } | { c: 4 } | { c: 5 };

type PositionAsCrossProduct = RowObject & ColumnObject;

let testPosition1: EQ<SinglePosition<Row, Column>, Position>;  // true
let testPosition2: SinglePosition<Row, Column> extends PositionAsCrossProduct ? true : false;  // !false
let testPosition3: Position extends PositionAsCrossProduct ? true : false;  // !false
let testPosition4: EQ<Position, Position>;  // true

🙁 Actual behavior

The types of variables testPosition2 and testPosition3 evaluate to false, respectively.

🙂 Expected behavior

The type of these two variables should evaluates to true since types SinglePosition<Row, Column>, Position and PositionAsCrossProduct are all coextensional, i.e. comprise the exact same values.

[IllusionMH]

Looks like related to #40803

[RyanCavanaugh]

Duplicate is correct. In general, T<U | V> is not the same as T<U> | T<V>, but there are places where the domain is small enough that we can iterate it quickly enough to determine that it actually is.

[MMF2]

Right, in general, T<U | V> is not the same as T<U> | T<V>. And, in general, it is OK, that the domain might be too big for the compiler to check. What is not OK but a real bug, imho, is that your compiler claims to know in such cases that the two types are not coextensional. As you say, it has not checked it, but it claims to know that the answer is false. This is plainly unacceptable to my mind. Your compiler should throw an error message in such a situation saying "I don't know, too complex for me", but instead it gives a wrong answer.
I have learned that soundness is a non-goal for TypeScript, but I nowhere saw documented this type of unsoundness, not to speak about a hardcoded number 24, as you said in #40803.
To my mind, you should either drop that "24" limitation (or make it at least configurable) or openly confess in your documentation at a prominent place that such hidden and surprising limitations exist.

[RyanCavanaugh]

This isn't unsoundness. Producing false from a type relational question with no provable outcome is always a sound answer because it prevents assignments that might be invalid from occurring; what you're seeing here is an incompleteness.

When comparing two types, there are several possible results:

• Provably, one has a subset of the of inhabitants of the other
• Provably, one does not have a subset of the of inhabitants as the other
• It's not immediately provable in either direction

There is an infinite class of pairs of types which might have the same inhabitants, but cannot be proven to in a reasonable period of time. What you're proposing is impossible per Gödel's incompleteness theorem.

[MMF2]

Sorry Ryan, I might not have expressed myself clearly. I do not propose that TypeScript overcomes the principled incompleteness that Gödel once had proved. I just tried to suggest the following: If I ask a question of the sort [T] extends [V] ? true : false, i.e. whether all values that comprise type T are compatible with type V, then I expect that in case TypeScript cannot answer this question it says so, instead of claiming "no", i,.e. evaluating to false. Why? Because the evaluation result false is indistinguishable for me from the case where TypeScript might have proved that not all values of T are compatible with V.

No Ryan, this behavior is not an instance of incompleteness, it is in fact one of unsoundness. If your compiler sometimes gives no answer (i.e. throws some kind of "too complex" or "unprovable" error), then it is incomplete. But if it gives wrong answers, as it is the case here, it is unsound. I don't want to rise an academic discussion about these two concepts. The point is rather that incompleteness is much more acceptable than unsoundness. And the kind of behavior under discussion here is definitely unacceptable to my mind.

And again, no, Ryan: "Producing false from a type relational question with no provable outcome is..." not "...always a sound answer", even though for the case that you have mentioned such an answer might be a defensible option. The point is that you cannot know what I use this answer for (e.g. nested in another conditional type). You do not seriously want to claim that, in general, substituting a false for a true definitely might not hurt, do you?

And by the way, the given code example above is not an example of a non-provable outcome. The opposite is true. Very elemental mathematics suffices to prove that the correct answer is true. It is just that your TypeScript compiler cannot prove this (probably due to this strange "24" limitation) and that is something very different. Gödel's incompleteness theorem is definitely not an appropriate excuse here.

[RyanCavanaugh]

If taking the false branch of a conditional type when it's too expensive to conclude that the types are compatible causes your program to become unsound, then you've written an incorrect conditional type. We can't stop you from making errors of that form.

[typescript-bot]

This issue has been marked as a 'Duplicate' and has seen no recent activity. It has been automatically closed for house-keeping purposes.