Allowing multiple "never" types to co-exist compromises type safety

[apendua]

Bug Report

🔎 Search Terms

never, property, extends, intersection

🕗 Version & Regression Information

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

⏯ Playground Link

Playground link with relevant code

💻 Code

type IsNever<T> = T extends never ? "YES" : "NO";
type NeverIsNever = IsNever<never>; // should be "YES" but is never, why?!
type ButNeverReallyIsNever = never extends never ? "YES" : "NO"; // this yields "YES" as expected
type ObjectWithNeverPropertyCannotExist = IsNever<{ value: never }> // should probably be "YES", but it is "NO"
type ArrayWithNeverItemsCannotExist = IsNever<never[]> // should probably be "YES", but it is "NO"

🙁 Actual behavior

None of the above types is recognized as never, even though they are all types that can have no legal values. The following comment from @RyanCavanaugh seems to confirm it:

#43954 (comment)

This leads to a conclusion that TS allows multiple "never" types to co-exist. In type theory, this shouldn't happen because the initial object (if it exists) must be necessarily unique. Unfortunately, not recognizing that those types are identical leads to type safety being compromised in certain situations, e.g.

#50559

🙂 Expected behavior

I think all these types should be recognized as equal to never. As such, no values of these types should be allowed to exist, as it the case of:

function modify<T extends { value: number }>(a: T): T {
    // type of "b" is T & { value: string } which is in fact "never"
    const b = {
        ...a,
        value: 'abc',
    };
    return b;
}

See: #50559

In particular a value of type never should not be considered a legal return value of any function unless the return type is explicitly declared as never.

[MartinJohns]

type NeverIsNever = IsNever<never>; // should be "YES" but is never, why?!

This is the expected behaviour of Distributive Conditional Types.

To prevent distributiveness you can wrap your types in brackets:

type IsNever<T> = [T] extends [never] ? "YES" : "NO";

In particular a value of type never should not be considered a legal return value of any function unless the return type is explicitly declared as never.

This is working by design. never is assignable to anything, but nothing is assignable to never. It's a bottom type. See also #28982.

// type of "b" is T & { value: string } which is in fact "never"

This is a duplicate of #50185.

type ArrayWithNeverItemsCannotExist = IsNever<never[]> // should probably be "YES", but it is "NO"

Such an array can absolutely exist. Here, an example: []

[apendua]

@MartinJohns Thank you for the hint regarding the brackets around T and for the example with an empty array. Somehow I missed that one, but let me fix it:

type NeverTupleShouldBeNever = IsNever<[never]> // should probably be "YES", but it is "NO"

I am also wondering what do you think about { value: never } being equivalent to never. Looks like you haven't addressed that one in your comment and at the same time it seems to be at the root of the problem that causes #50559.

[fatcerberus]

{ value: never } is equivalent to never in principle, as it is impossible to produce a legal value. However, they are still different types as far as the compiler is concerned:

let x: ObjWithNeverValue = { value: alwaysThrows() };  // ok
let y: never = { value: alwaysThrows() };  // not ok, error
let z: never = alwaysThrows();  // ok

The bottom type models the "return value" of functions that don't return normally. So you can treat it as anything you want, since the code that uses the value should always be unreachable. If you ever end up reading a value from something typed as never at runtime, type safety has already been violated.

This isn't just sleight of hand, either; it has mathematical and logical precedent. I wrote a more nerdy theoretical explanation in a different issue recently, see #49862 (comment)

[MartinJohns]

You can still construct objects with never properties using type assertions. These properties are sometimes used to model a "xor" union type. For example: { a: string; b: never } | { a: never; b: string }

[apendua]

@MartinJohns Well, I didn't know that type assertions would allow that. It doesn't sounds very type-safe. Digging a little bit deeper, it seems like the following is also possible:

function isNever(x: unknown): x is never {
    return true;
}
const a = 123;
let x: string;
if (isNever(a)) {
    x = a;
}

which really doesn't sounds valid to me.

These properties are sometimes used to model a "xor" union type. For example: { a: string; b: never } | { a: never; b: string }

Would you mind sharing a practical example which requires this kind of union type to be used? Shouldn't a union of two nevers also be never?

[apendua]

@fatcerberus

I wrote a more nerdy theoretical explanation in a different issue recently, see #49862 (comment)

Thank you for sharing the link. So yes, I am aware of all of that. And it only proves my point I guess. There shouldn't exist any values of type never or if we allow them to exist we pretty much loose type safety everywhere. A code that produces a value of type never is not valid in the sense of type checking.

[MartinJohns]

Well, I didn't know that type assertions would allow that.

The entire purpose of type assertions is to work around the type system. Nothing else. Just to clarify, in the example that follows you used a type guard, not a type assertion.

Digging a little bit deeper, it seems like the following is also possible:

The implementation of type guards is not checked against the return type annotation. This is whole different issue (too lazy to look it up), and completely unrelated to never. If you write a function that tells the compiler "this checks that the argument is a bool", and then your function does not check this, well... it's not the compilers fault that things get screwed up.

Would you mind sharing a practical example which requires this kind of union type to be used?

I would personally not do it like this, the better option is to use a discriminated union. But if you have a union of different cases, and you want to ensure that only one of it matches, you need to use these never properties. Otherwise trying to narrow the union type with the in-operator results in unsound behaviour, because object types are not sealed. If you simply omit the property b in my previous case, it might be that such a property exists. But having a property b typed never explicitly says that it must not be provided. Using undefined is also an option here.

Shouldn't a union of two nevers also be never?

A union of two never gets simplified to never. But this is not the case in my example.

There shouldn't exist any values of type never or if we allow them to exist we pretty much loose type safety everywhere. A code that produces a value of type never is not valid in the sense of type checking.

An object having a property typed never is not the same as never. The one case shouldn't happen, in the other case you do have an object, which explicitly mentions a property should not be set at all.

Another example, in this comment Ryan describes the type Record<string, never> as "a type, that if you accessed any of its properties, you'd get an exception."

[fatcerberus]

A code that produces a value of type never is not valid in the sense of type checking.

Correct. It working as a bottom type is contingent on the idea that you can’t legally produce a value of that type without subverting the type system (via a cast, e.g.). You can safely pretend it’s anything you want, so long as all the code that “holds” such a value remains unreachable.

[guillaumebrunerie]

Having studied type theory for many years, I would simply like to point out that this is incorrect:

In type theory, [multiple "never" types co-existing] shouldn't happen because the initial object (if it exists) must be necessarily unique.

The initial object is only required to be unique up to isomorphism, not up to equality. In type systems like Coq or Agda, which have a very strong (and sound) type theoretical basis, it is very easy to produce different empty types, for instance defining two different data types with no constructors (or the type of equalities between 0 and 1, or the type of functions from a non-empty type to an empty type, and so on). Elements of such types are not assignable to other empty types, it's only possible to construct functions between those types.

[apendua]

@MartinJohns

An object having a property typed never is not the same as never. The one case shouldn't happen, in the other case you do have an object, which explicitly mentions a property should not be set at all.

Well, the point is this doesn't seem the be the case:

const a: { value: never } = {};

actually gives an error:

Property 'value' is missing in type '{}' but required in type '{ value: never; }'.

which seems to be contradicting your statement. Please have a look at this tsplayground.

In fact "not having property" would be better represented by { value?: undefined }, but not quite. Actually, I don't think the concept of "not having property" can be accurately represented in any type system but I am not 100% sure. At least { value: never } does not seem to be the proper solution here.

The implementation of type guards is not checked against the return type annotation.

Of course it's not. I wasn't suggesting that this should be the case. What I meant was that type guards with return type x is never should probably be prohibited as they doesn't make any sense. Similarly, if you tried to use a conditional statement if (x === true) { ... } when x is of type number, TS would kindly notify you that the code will be unreachable.

[RyanCavanaugh]

I don't see any incorrect behavior here. See also https://twitter.com/SeaRyanC/status/1326575516250329088

[fatcerberus]

{ value?: never } is generally the way to write a type that you don't want to have a particular property. It's possible to work around because optional properties are unsound, but in practice it's usually enough to prevent the property from being created.

[RyanCavanaugh]

What I meant was that type guards with return type x is never should probably be prohibited as they doesn't make any sense.

There's an infinite amount of nonsensical code you can write and only a finite amount of time to check for all of those constructs before people get bored of waiting for the checker to finish and stop using static type checkers altogether. Unless people are frequently going around writing x is never either through mechanical error or common misconception, this isn't something we should spend a constrained resource on.

[apendua]

Lemme summarize the above discussion:

1. Even though a type like { value: never } is isomorphic with never it does not necessarily mean that it needs to be treated as the same type by the type system. In fact, it's a completely different type and it's completely fine. Because of that IsNever<{ value: never }> = "NO" and this is actually the expected behavior.
2. Values of type { value: never } cannot exist the same way values of type never cannot exist. The fact that the example code was able to produce such a value was due to another problem, basically TS making an oversimplification by assuming that the type of { ...a, value: 'abc' } is T & { value: string } = never but this is not really the case. In fact, the type should be evaluated as Omit<T, "value"> & { value: string } but this is already covered by Add spread/rest higher-order types operator #10727.
3. Finally, it does not make sense to expect TS to be able to verify if a given type is equivalent to never. In case of { value: never } this is actually simple but in general this is probably an "undecidable" problem as pointed out here https://twitter.com/SeaRyanC/status/1326575516250329088.