Intersection of conditional types, acting on a generic type, with another type doesn't narrow the generic type

[aaditmshah]

🔎 Search Terms

• intersect
• conditional
• generic
• narrow
• typeof
• function
• callable
• ts2349

🕗 Version & Regression Information

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

⏯ Playground Link

https://www.typescriptlang.org/play?target=99&jsx=0#code/C4TwDgpgBAKgFgVwHYGsA8BBAfFAvFACgEo8cMBuAKEtEigDkB7JAMWQGNgBLZzHfDFAgAPYBCQATAM5Q2STjyRQA-FCQQAbhABOUAFxQK1WtACiwsNr55YiVNYA+DZnIW9sVSu2ZTgQjQCGADYIAWI2fAQilgbmlnxEBoK4WJRQUCaMAGZCFrq4BVAARFkc3MxFKrmWxPrV2lTpAPRN6W3tHZ1dAHq93WlQLVAAtKNj4xOTU9Mzs3PzUwND8Fwy0doQUlKKUKtqjH7swUEBAEZBEAB0S63pTH7HUN5IvlzACOLAMtkZ4NAA5PBkOhsFAnAQmKwyoprAAyWTQ5hEf5QAIbJ7HM4Xa7NW5tGB-KD-SGucpIOEI+RklFwAIyJCMDFBIJQbYAcyQYQQGykl0IACYAMwAFgAnEQbiMFtKZbK5TNJQQwGiAgBbCBibQkdYGIH2UHgkmI8mg+GkxQS3FS+U2212iaUIA

💻 Code

type Thunk<A> = () => A;

type NonFunction<A> = A extends Function ? never : A;

type Expr<A> = Thunk<A> | NonFunction<A>;

const evaluate = <A>(expr: Expr<A>): A =>
  typeof expr === "function" ? expr() : expr;
  //                           ^^^^
  // -------------------------------------------------------------------------------------
  // This expression is not callable.
  //   Not all constituents of type 'Thunk<A> | (NonFunction<A> & Function)' are callable.
  //     Type 'NonFunction<A> & Function' has no call signatures. (2349)
  // -------------------------------------------------------------------------------------
  // (parameter) expr: Thunk<A> | (NonFunction<A> & Function)
  // -------------------------------------------------------------------------------------

🙁 Actual behavior

The parameter expr, which has the type Expr<A>, is being narrowed by the typeof expr === "function" condition. When the condition is true, the type of expr is narrowed to Thunk<A> | (NonFunction<A> & Function). When the condition is false, the type of expr is narrowed to NonFunction<A>.

🙂 Expected behavior

When the condition is true, the type of expr should be simplified to just Thunk<A>.

  Thunk<A> | (NonFunction<A> & Function)
= Thunk<A> | ((A extends Function ? never : A) & Function)          // (1) by definition
= Thunk<A> | (A extends Function ? never & Function : A & Function) // (2) distributivity
= Thunk<A> | (A extends Function ? never : A & Function)            // (3) annihilation
= Thunk<A> | (A extends Function ? never : never)                   // (4) law of non-contradiction
= Thunk<A> | never                                                  // (5) simplification
= Thunk<A>                                                          // (6) identity

The challenging step to understand is step number 4 where we invoke the law of non-contradiction to simplify the type A & Function to never. The law of non-contradiction states that some proposition P and its negation can't both be true. In our case, the proposition is Function. Since A & Function is in the else branch of the conditional A extends Function, it implies that A is not a function. Hence, A and Function are contradictory. Thus, by the law of non-contradiction we should be able to simplify it to never.

In plain English, NonFunction<A> & Function is a contradiction. A type can't both be a Function and a NonFunction<A> at the same time. Hence, the type checker should simplify NonFunction<A> & Function to never.

At the very least, NonFunction<A> & Function should be callable. We shouldn't get a ts2349 error.

Additional information about the issue

I understand that as TypeScript is currently implemented, NonFunction<A> & Function doesn't simplify to never for all possible types A. For example, consider the scenario when A is unknown.

  NonFunction<unknown> & Function
= (unknown extends Function ? never : unknown) & Function // (1) by definition
= unknown & Function                                      // (2) simplification
= Function                                                // (3) identity

This seems to be because in step number 2 we're simplifying unknown extends Function ? never : unknown to just unknown. Instead, we should simplify it to unknown & !Function where the ! denotes negation, i.e. an unknown value which is not a function. Then we can apply the law of non-contradiction to get the correct type.

  NonFunction<unknown> & Function
= (unknown extends Function ? never : unknown) & Function // (1) by definition
= (unknown & !Function) & Function                        // (2) simplification
= unknown & (!Function & Function)                        // (3) associativity
= unknown & never                                         // (4) law of non-contradiction
= never                                                   // (5) annihilation

At the very least, this seems to suggest the need for some sort of negation type.

[MartinJohns]

At the very least, this seems to suggest the need for some sort of negation type.

#4196

[fatcerberus]

It's actually not true that NonFunction<A> & Function is a contradiction in TypeScript. Because object types are not sealed¹, intersecting objects with disjoint sets of properties merges them, and function types have a special pseudo-property called a "call signature". So:

type NonFunction<A> = A extends Function ? never : A;
type Fun = () => void;
type Obj = { foo: string };
type MoreFun = NonFunction<Obj> & Fun;
declare const foo: MoreFun;
foo.foo;  // ok
foo();    // also ok

Footnotes

1. Which, for those keeping score, also implies that a NonFunction<A> may be a function in reality, and you've just forgotten its call signature. The call signature can be reintroduced via type intersection. ↩

[aaditmshah]

@fatcerberus Can you give me a real life example of how you would construct a value of type MoreFun in JavaScript?

[fatcerberus]

function foo() {
    console.log("you fooey bard!")
}
foo.foo = "foo";

All functions are objects in JavaScript.

[aaditmshah]

@fatcerberus I understand that. In fact, I wrote about this very issue in the Additional information about the issue section.

I understand that as TypeScript is currently implemented, NonFunction<A> & Function doesn't simplify to never for all possible types A.

However, that's what I think is wrong. I think that in your example MoreFun should simplify to never. In fact, I think that NonFunction<T> & F, for all types T and for all types F which extend Function, should simplify to never.

Note that I have no issue with the type Obj & Fun. I only have an issue with the type NonFunction<Obj> & Fun. I think it's a mistake for NonFunction<Obj> to simplify to Obj. I think it should simplify to Obj & !Function. Hence, NonFunction<Obj> & Fun should simplify to never as follows.

  NonFunction<Obj> & Fun
= (Obj & !Function) & Fun // by definition
= Obj & (!Function & Fun) // associativity
= Obj & never             // law of non-contradiction
= never                   // annihilation

[RyanCavanaugh]

It's not practical for every possible non-inhabitable type to be simplified to never -- this requires a potentially unbounded amount of work. Because it can't be done, it's not an invariant you should be trying to take a dependency on.

[fatcerberus]

Note that I have no issue with the type Obj & Fun. I only have an issue with the type NonFunction<Obj> & Fun

But that's the thing - those are the same type. Type aliases are just type-functions - NonFunction<Obj> "returns" Obj, so in the end you are just doing Obj & Fun. TS doesn't go back and reevaluate the conditional type every time you manipulate it - that's not how they work.

[fatcerberus]

I think [NonFunction<Obj>] should simplify to Obj & !Function.

If we had negated types, you could just write the latter directly, but I disagree that that's what the conditional type you wrote should simplify to. Ternary expressions aren't retroactive at runtime, so I wouldn't expect the typespace equivalent to be either.

[aaditmshah]

Note that I have no issue with the type Obj & Fun. I only have an issue with the type NonFunction<Obj> & Fun

But that's the thing - those are the same type. Type aliases are just type-functions - NonFunction<Obj> "returns" Obj, so in the end you are just doing Obj & Fun. TS doesn't go back and reevaluate the conditional type every time you manipulate it - that's not how they work.

Yes, NonFunction<Obj> "returns" Obj currently but that's a defect of the type system, which is why I created this issue.

The type NonFunction<Obj> should return Obj & !Function. You don't need to go back and re-evaluate the conditional type. Just make the conditional type return Obj & !Function.

By simplifying NonFunction<Obj> to just Obj, we're losing type information. In particular, we're losing the information that we checked whether Obj is a function and we found out that it isn't a function. The check is the important part here.

I think [NonFunction<Obj>] should simplify to Obj & !Function.

If we had negated types, you could just write the latter directly, but I disagree that that's what the conditional type you wrote should simplify to. Ternary expressions aren't retroactive at runtime, so I wouldn't expect the typespace equivalent to be either.

True, if we had negated types then I could define NonFunction as follows, which by the way is oh so perfect.

type NonFunction<A> = A & !Function;

However, I disagree with the second part of your statement. A conditional type of the form A extends B ? never : A should simplify to A & !B for all types A and B. And, here's the proof.

First, we need to understand what A extends B denotes. Turns out, extends denotes material implication. If A extends B then we should be able to substitute a value of type A everywhere a value of type B is expected. That is, A should be "assignable" to B. In propositional logic, we would write this as $A \to B$.

Next, the never type denotes falsehood and is represented as $\bot$ in propositional logic. Finally, any conditional type P ? Q : R can be represented as the conjunction of two conditionals $(P \to Q) \land (\neg P \to R)$ in propositional logic.

Putting it all together, the conditional type A extends B ? never : A would be represented in propositional logic as $((A \to B) \to \bot) \land (\neg (A \to B) \to A)$. However, $P \to \bot$ is the same as $\neg P$. Hence, the proposition can be simplified to $\neg (A \to B) \land (\neg (A \to B) \to A)$.

At this point, we can use the modus ponens rule to infer that $A$ is a true proposition. However, inference is not the same as simplification. Yes, $(\neg (A \to B) \land (\neg (A \to B) \to A)) \to A$ is a true proposition. However, $\neg (A \to B) \land (\neg (A \to B) \to A) \neq A$. Since, $P \land (P \to Q)$ simplifies to $P \land Q$, we can simplify $\neg (A \to B) \land (\neg (A \to B) \to A)$ to $\neg (A \to B) \land A$.

Finally, $\neg (A \to B) \land A$ can be simplified to $\neg (\neg A \lor B) \land A$ because $P \to Q$ is equivalent to $\neg P \lor Q$. Next, by De Morgan's law we can further simplify $\neg (\neg A \lor B) \land A$ to $(A \land \neg B) \land A$. And, now we can trivially see that $(A \land \neg B) \land A$ is just $A \land \neg B$.

Now, you might be think that there's some flaw in my argument because I'm treating types as propositions. After all, types are not the same as propositions. But, the Curry—Howard isomorhpism is proof that types and propositions are indeed equivalent. It's one of the seminal theorems of computer science.

In conclusion, A extends B ? never : A should simplify to A & !B. Inference is not the same as simplification. Yes, A extends B ? never : A implies A. However, it also implies !B.

[aaditmshah]

It's not practical for every possible non-inhabitable type to be simplified to never -- this requires a potentially unbounded amount of work. Because it can't be done, it's not an invariant you should be trying to take a dependency on.

I understand that the solution this for this problem might take a lot of work to implement, and therefore it's not something that you want to solve. However, this is indeed a defect of the type system as I demonstrated using propositional logic above. Hence, I don't think the "Not a Defect" label is justified here.

To be fair, I can easily solve this problem using type guards.

type Thunk<A> = () => A;

type NonFunction<A> = A extends Function ? never : A;

type Expr<A> = Thunk<A> | NonFunction<A>;

const isThunk = <A>(expr: Expr<A>): expr is Thunk<A> =>
  typeof expr === "function";

const evaluate = <A>(expr: Expr<A>): A =>
  isThunk(expr) ? expr() : expr;

However, I expected TypeScript to correctly narrow the type of expr to Thunk<A> even without type guards. It's quite obvious that an inhabitant of Expr<A> can only be a function if it's an inhabitant of Thunk<A>.

[fatcerberus]

The type NonFunction<Obj> should return Obj & !Function. You don't need to go back and re-evaluate the conditional type. Just make the conditional type return Obj & !Function.

That would make the conditional type retroactive, which, again, is not how they work. That would be like writing a function:

function nonString(x) {
    // let's assume throw expressions are available for brevity
    return typeof x !== 'string' ? x : throw Error("no strings allowed!");
}

and then expecting it to throw if, at any point, x is transformed into a string, such as by calling String(x). In other words NonFunction<Obj> & Fun is completely analogous to calling String(nonString(x)) at runtime.

A conditional type is a computation done on a type at compile time, not a new kind of "dynamic type".

[RyanCavanaugh]

I understand that the solution this for this problem might take a lot of work to implement, and therefore it's not something that you want to solve

The problem literally isn't computable. It's not for lack of desire to compute BB(12) that I haven't.

[aaditmshah]

That would make the conditional type retroactive, which, again, is not how they work.

I don't understand what you mean by "retroactive". Could you please provide a definition for this term? This is the second time you've used this term and I'm honestly confused as to what you're trying to convey.

Also, could you please elucidate the following statement?

Ternary expressions aren't retroactive at runtime, so I wouldn't expect the typespace equivalent to be either.

Again, I don't understand what you mean by "retroactive" and hence I don't understand what "typespace equivalent" means in this sentence either.

---

That would be like writing a function:

function nonString(x) {
    // let's assume throw expressions are available for brevity
    return typeof x !== 'string' ? x : throw Error("no strings allowed!");
}

and then expecting it to throw if, at any point, x is transformed into a string, such as by calling String(x). In other words NonFunction<Obj> & Fun is completely analogous to calling String(nonString(x)) at runtime.

Your analogy is wrong. If you want to view types as values then you should reify them as predicates. The predicate takes any value, and returns true if and only if that value satisfies the type that the predicate reifies.

// Analogous to the type `unknown`.
const unknown = () => true;

// Analogous to the type `Function`.
const func = (x) => typeof x === "function";

// Analogous to the type `NonFunction<A> = A & !Function`.
const nonFunc = (t) => (x) => t(x) && !func(x);

// Analogous to the type `A & B`.
const intersect = (t1, t2) => (x) => t1(x) && t2(x);

// Analogous to the type `NonFunction<A> & Function`.
const nonFuncAndFunc = (t) => intersect(nonFunc(t), func);

// Analogous to the type `never`.
const absurd = nonFuncAndFunc(unknown);

console.log(absurd(42));       // false
console.log(absurd(() => 42)); // false

As you can see, the absurd type always returns false no matter what its input is. This is because a value can't both be a non-function and a function at the same time.

Also note that the intersect type constructor requires that the same value satisfy both the types provided. I mention this to refute your statement about x somehow transforming into String(x). x doesn't transform into String(x). They are two separate values. Hence, your analogy fails there.

Anyway, you might have noticed that I defined NonFunction<A> as A & !Function instead of A extends Function ? never : A. This was on purpose because I want to pose two questions two you.

1. If TypeScript supported negated types and NonFunction<A> was defined as A & !Function, would you agree then that NonFunction<A> & Function should simplify to never? If not, why?
2. If I showed you a step-by-step mechanical way to simplify A extends Function ? never : A to A & !Function, would you agree that they are indeed equivalent? By mechanical, I mean that I'll provide a computer algorithm which will reduce A extends Function ? never : A to A & !Function in a finite number of steps regardless of the type A. This means that we'll literally be able to implement said algorithm in the TypeScript type system.

A conditional type is a computation done on a type at compile time, not a new kind of "dynamic type".

So is the algorithm I have in mind to simplify A extends Function ? never : A to A & !Function.

[aaditmshah]

The problem literally isn't computable.

Interesting, so you're telling me that this particular problem is undecidable? I would love to understand why. Would you explain it to me?

It's not for lack of desire to compute BB(12) that I haven't.

What is "BB(12)"?

[fatcerberus]

I don't understand what you mean by "retroactive". Could you please provide a definition for this term?

Retroactive is probably the wrong term. But basically you wrote a ternary expression (a conditional type) and now expect it to remain live after it's already been computed, i.e. you expect the type-level equivalent of String(nonString(x)) to throw.

Your analogy is wrong. If you want to view types as values then you should reify them as predicates. The predicate takes any value, and returns true if and only if that value satisfies the type that the predicate reifies.

NonFunction<T> is not a type, or even a type constructor. It is a function on types. It takes a type T, does a (very simple) computation based on what's assignable to it, and returns a (potentially different) type. It so happens that NonFunction<Obj> is an identity transformation. You're operating on the premise that a conditional type is a new kind of type, a sort of live predicate, but this is not true--it's simply a kind of computation you do within the type system, using types instead of values. Types and values are exactly analogous in this situation. Which is why we have #14833.

[aaditmshah]

Retroactive is probably the wrong term. But basically you wrote a ternary expression (a conditional type) and now expect it to remain live after it's already been computed, i.e. you expect the type-level equivalent of String(nonString(x)) to throw.

I don't understand what you mean by "remain live". Could you please elucidate?

Also, your String(nonString(x)) analogy is wrong as I demonstrated in my previous comment.

NonFunction<T> is not a type, or even a type constructor. It is a function on types.

I agree. In fact, in my previous comment I indeed reified NonFunction<A> as a function on types.

// Analogous to the type `NonFunction<A> = A & !Function`.
const nonFunc = (t) => (x) => t(x) && !func(x);
//              ^^^    ^^^^^^^^^^^^^^^^^^^^^^^
//               |                |
//           input type      output type

It takes a type T, does a (very simple) computation based on what's assignable to it, and returns a (potentially different) type.

The algorithm I have in mind also does a very simple computation. In fact, let me demonstrate what I have in mind.

type Example<A> = A extends string ? { foo: A } | { bar: A; baz: A };

type Foo = Example<"a" | "b" | "c">; // Simplifies to { foo: "a" } | { foo: "b" } | { foo: "c" }

type Bar = Example<"bar" | number>; // Simplifies to { foo: "bar" } | { bar: number & !string; baz: number & !string }

type Baz = Example<unknown>; // Simplifies to { bar: unknown & !string; baz: unknown & !string  }

Here are the key points of this algorithm.

1. This algorithm only works on conditional types which act on a generic type. This is exactly how distributive conditional types work too. Hence, there's prior art for such algorithms.
2. The true branch of the conditional type evaluates exactly the same way as it does right now.
3. The false branch of the conditional type evaluates almost exactly the same way as it does right now.
4. The only difference is that references to the generic type in the false branch of the conditional, such as the generic type A in the above example, are narrowed down to A & !B for whatever the type B is in the condition A extends B.

In the above example, A is used twice in the false branch of the conditional. Hence, each reference of A in the false branch is narrowed down to A & !string. If there was only one reference to A in the false branch, then only that one reference would be narrowed down. And, if there are zero references to A in the false branch then nothing would be narrowed down.

As you can see, this is a purely compile-time computation and it works exactly like you would expect a function on types to work.

It so happens that NonFunction<Obj> is an identity transformation.

That's what is wrong, and that's what I want to change. NonFunction<Obj> should not behave like an identity transformation. It should instead map Obj to Obj & !Function statically at compile time. No "retroactive", "dynamic", "live predicate" magic involved. NonFunction should algorithmically map Obj to Obj & !Function. And, the algorithm as I described above is very simple.

You're operating on the premise that a conditional type is a new kind of type, a sort of live predicate

I think I've sufficiently demonstrated that I'm not operating under such a premise.

[MartinJohns]

Hence, each reference of A in the false branch is narrowed down to A & !string.

It can't be narrowed down to this type, because types like !string don't exist. This would require negated types to be supported first (issue linked earlier).

Based on the types support currently existing this is working as intended / not a defect. Undesirable? Sure. But not a bug.

[aaditmshah]

It can't be narrowed down to this type, because types like !string don't exist. This would require negated types to be supported first (issue linked earlier).

This is precisely what I wrote in my original post.

At the very least, this seems to suggest the need for some sort of negation type.

In fact, if we had negation types then as you pointed out we could simply define NonFunction<A> as A & !Function. Hence, we should have a discussion about negation types. To that end, I'll close this issue and mark it as a duplicate of #4196.

Anyway, now that we agree on something, could you at least tell me what are your thoughts on narrowing in the false branch of conditional types if negated types were added to TypeScript?

Based on the types support currently existing this is working as intended / not a defect. Undesirable? Sure. But not a bug.

Logically, it is a defect. You wouldn't expect the true branch of the following if statement to be evaluated right?

const conditionA = true;
const conditionB = true;

if (conditionA && !conditionB) {
  console.log(`
    You wouldn't expect this log to be printed
    because conditionB is not false. Hence, if
    this log's printed that means that there's
    a defect in the JavaScript runtime. In the
    same way NonFunction<A> should evaluate to
    A & !Function. If it evaluated to simply A
    then it should be regarded a major defect.
  `);
}

After this discussion, I'm convinced that not having negation types in TypeScript is indeed a defect. It's like a baby born without hearing. Deafness is certainly a defect. Similarly, not having negation types in TypeScript is also a defect.

Anyway, I'm closing this issue as a duplicate of #4196.

[aaditmshah]

@MartinJohns Sorry, I mistook you for @fatcerberus. Anyway, it seems like I'm not the first person to face this exact issue. See #29317. In particular, the following paragraph sums up my experience perfectly.

Negated types, as the name may imply, are the negation of another type. Conceptually, this means that if string covers all values which are strings at runtime, a "not string" covers all values which are... not. We had hoped that conditional types would by and large subsume any use negated types would have... and they mostly do, except in many cases we need to apply the constraint implied by the conditional's check to it's result. In the true branch, we can just intersect the extends clause type, however in the false branch we've thus far been discarding the information. This means unions may not be filtered as they should (especially when conditionals nest) and information can be lost. So that ended up being the primary driver for this primitive - it's taking what a conditional type false branch implies, and allowing it to stand alone as a type.

Emphasis mine.

[fatcerberus]

That's what is wrong, and that's what I want to change.

I'm really not sure how you can see

type NonFunction<T> = T extends Function ? never : T;

and interpret that as anything other than

typefun NonFunction(T: Type) {
    if (T assignsto Function)
        return never;
    else
        return T;
}

because that's exactly what that type means. It's literally an identity function if you pass it anything that's not currently assignable to Function. The fact that you intersect the resulting type with Function afterwards is irrelevant.

[aaditmshah]

@fatcerberus I'm really not sure how you can see

typefun NonFunction(T: Type) {
    if (T assignsto Function)
        return never;
    else
        return T;
}

and not realize that T assignsto Function narrows the type T to T & !Function in the else branch.

It's literally an identity function if you pass it anything that's not currently assignable to Function.

I lot of people besides myself would disagree with you on that. Just look at the number of 👍🏼, 🎉, ❤️, and 🚀 emojis on #29317. And, not to mention when you view types as propositions, which is a fundamental theorem of computer science, it becomes obvious that T should be narrowed in the else branch.

The fact that you intersect the resulting type with Function afterwards is irrelevant.

I concur. The type returned by NonFunction<T> should not depend upon its context, i.e. it should be context free. That being said, I stand by my words that the type returned by NonFunction<T> should be T & !Function. And, when T & !Function is intersected with Function the result is simplified to never.

This is the kind of simplification that TypeScript does often. For example, T & unknown is simplified to T, T | unknown is simplified to unknown, T & never is simplified to never, and T | never is simplified to T. Similarly, T & !T is simplified to never and T | !T is simplified to unknown. Hence, (T & !Function) & Function is simplified to never.

[fatcerberus]

I think I might see where you're coming from here; you envision the A as being narrowed in the false branch due to the extends check, making it not an identity in that context. Even so, what you propose is still incorrect: T = A & !Function implies that F extends T is false for all types F extends Function, which is something that was not checked in the conditional type. So the proposed narrowing is still wrong, even if negated types existed.

tl;dr is that, in general, T extends U being true or false only tells you whether T is assignable to U but says nothing about whether U is assignable to T. So it doesn't make sense to set T = T & !U in the false branch of said check.

[somebody1234]

Hi, just wanted to point out that negated types are absent in virtually all other languages as well, making all other languages defective as well - if not more defective than TS.

[aaditmshah]

@somebody1234 Other languages don't have conditional types like TypeScript does. So, no that analogy doesn't apply.

[fatcerberus]

More concretely:

type NonDog<T> = T extends Dog ? never : T;
type Test = NonDog<Animal>;

You asked whether Animal was assignable to Dog. It's true that it isn't. If you then narrow T to T & !Dog in the false branch, you're asserting that Dog is not assignable to the original T, which is false.

[aaditmshah]

I think I might see where you're coming from here; you envision the A as being narrowed in the false branch due to the extends check, making it not an identity in that context. Even so, what you propose is still incorrect: T = A & !Function implies that F extends T is false for all types F extends Function, which is something that was not checked in the conditional type. So the proposed narrowing is still wrong, even if negated types existed.

@fatcerberus Let me formalize what you're saying so that I understand it.

• Let's represent the type Function as the proposition $F$.
• T = A & !Function can be represented as the proposition $T = \neg (A \to F)$.
• F extends Function can be represented as the proposition $G \to F$.
• I used $G$ to represent F because $F$ represents Function.
• F extends T can be represented as $G \to T$ which is $G \to \neg (A \to F)$.
• So, what you're saying is that $\forall A. \neg (A \to F)$ implies $\forall G. (G \to F) \to \neg (G \to \neg (A \to F))$.
• In plains words, if A is not a function and G is a function then G can't be assigned to A.

That makes sense to me. I don't see any problem here. $\forall A. \neg (A \to F) \to \forall G. (G \to F) \to \neg (G \to \neg (A \to F))$ is indeed true.

I certainly don't see how the proposed narrowing is wrong.

tl;dr is that, in general, T extends U being true or false only tells you whether T is assignable to U but says nothing about whether U is assignable to T. So it doesn't make sense to set T = T & !U in the false branch of said check.

Why would you even care if U is assignable to T? The proposition T extends U is just material implication. It's equivalent to $T \to U$. The negation of $T \to U$ is not $U \to T$. The negation of $T \to U$ is material nonimplication, i.e. $\neg (T \to U)$.

• $T \to U$ is equal to $\neg T \lor U$.
• $\neg (T \to U)$ is equal to $\neg (\neg T \lor U)$ which is $T \land \neg U$.

So, it makes perfect sense to set T = T & !U in the false branch.

More concretely:

type NonDog<T> = T extends Dog ? never : T;
type Test = NonDog<Animal>;

You asked whether Animal was assignable to Dog. It's true that it isn't. If you then narrow T to T & !Dog in the false branch, you're asserting that Dog is not assignable to the original T, which is false.

You don't make any sense. If T is Animal, then T & !Dog is Animal & !Dog. It represents the values which are assignable to Animal but not assignable to Dog, which makes perfect sense. Nowhere are we asserting that Dog is not assignable to Animal.

Animal & !Dog is not the same as !(Dog extends Animal) because !(Dog extends Animal) simplifies to Dog & !Animal.

[fatcerberus]

Nowhere are we asserting that Dog is not assignable to Animal.

In fact you are. Animal & !Dog means, as you say, "value which is assignable to Animal but not assignable to Dog", i.e. it's a set which contains no dogs. It is not valid to conclude that, just because T is not a subset of Dog, that T contains no dogs. The conditional type expression operates on the entire type, not individual members of it, or even individual subtypes (modulo distribution over union types)

[aaditmshah]

I literally don't see the check for Dog extends T anywhere in your example. And, Animal & !Dog is literally assignable to Animal.

type Animal = Cat | Dog | Horse;

type NotDog = Animal & !Dog; // equivalent to Cat | Horse

declare const cat: Cat;

const notDog: NotDog = cat;

const animal: Animal = notDog;

[aaditmshah]

It is not valid to conclude that, just because T is not a subset of Dog, that T contains no dogs.

We're not concluding that Animal contains no dogs. We're concluding that Animal & !Dog contains no dogs. There's a very big difference.

[fatcerberus]

You're arguing that !(T extends Dog) always implies T & !Dog, which is not true, because T might be (and is, in my example) Animal. Dog | Cat | Horse is not a subset of Dog, but it still contains dogs. Cat | Horse contains no dogs, so you've changed the meaning of the original type by narrowing it.

[aaditmshah]

You're arguing that !(T extends Dog) always implies T & !Dog, which is not true, because T might be (and is, in my example) Animal.

Yes, !(T extends Dog) always implies T & !Dog, even if T is Animal. It's impossible to assign a Dog to NonDog<Animal>.

type Cat = "cat";
type Dog = "dog";
type Horse = "horse";

type Animal = Cat | Dog | Horse;

type NonDog<T> = T extends Dog ? never : T;

const dog: Dog = "dog";

const nonDog: NonDog<Animal> = dog;
//    ^^^^^^
// Type '"dog"' is not assignable to type '"cat" | "horse"'. (2322)

Playground Link

Dog | Cat | Horse is not a subset of Dog, but it still contains dogs.

What does that have to do with anything?

Cat | Horse contains no dogs, so you've changed the meaning of the original type by narrowing it.

I haven't. You literally can't assign a Dog to NonDog<Animal>.

[somebody1234]

@aaditmshah counterexample:
Open in Playground

type Cat = { cat: true };
type Dog = { dog: true };
type Horse = { horse: true };

type Animal = Cat | Dog | Horse;

type NonDog<T> = T extends Dog ? never : T;

const dog = { dog: true, horse: true } satisfies Animal & Dog;

const nonDog: NonDog<Animal> = dog;

[aaditmshah]

@somebody1234 Your counterexample has errors.

type Cat = { cat: true };
type Dog = { dog: true };
type Horse = { horse: true };

type Animal = Cat | Dog | Horse;

type NonDog<T> = T extends Dog ? never : T;

const dog: Dog = { dog: true, horse: true };
//                            ^^^^^
// Object literal may only specify known properties, and 'horse' does not exist in type 'Dog'. (2353)

const nonDog: NonDog<Animal> = dog;
//    ^^^^^^
// Type 'Dog' is not assignable to type 'Cat | Horse'.(2322)

Playground link

[aaditmshah]

Listen, as much as I love to argue with random strangers on the internet, I'm going to have to withdraw from this conversation now. It's pointless and unhealthy. Feel free to keep commenting, but I'm not going to reply. In fact, I'm unsubscribing from this thread. I already closed this issue because it's a duplicate of #4196. Have a great day folks.

[somebody1234]

@aaditmshah it doesn't have errors, you modified the code so that it produced an error

[somebody1234]

hmm... i guess the idea doesn't quite check out
my bad.

[somebody1234]

@aaditmshah Here is a proper incorrect case:
Open in Playground

type Cat = { animal: true; cat: true };
type Dog = { animal: true; dog: true };
type Horse = { animal: true; horse: true };

type Animal = { animal: true };

type NonDog<T> = T extends Dog ? never : T;

const dog: Dog = { animal: true, dog: true };
const animal: Animal = dog;
const nonDog: NonDog<Animal> = animal;

[fatcerberus]

For arbitrary T and U, "T is not a subset of U" does not imply "T is a set which contains no elements fromU". T & !U means the latter.