[bug] Type Exclusion Should be Consistent

[erikerikson]

🔎 Search Terms

"Exclude" "exclusion" "general" "concrete" "type"

🕗 Version & Regression Information

• This is a crash
• This changed between versions ______ and _______
• This changed in commit or PR _______
• This is the behavior in every version I tried, and I reviewed the FAQ for entries about anything
• I was unable to test this on prior versions because _______

⏯ Playground Link

Playground Link

💻 Code

type T1 = {
  type: 1
  f1: 1
}
type T2 = {
  type: number
  f2: 2
}
type TA = T1 | T2

type T3 = {
  type: 3
  f3: 3
}
type TB = T1 | T3

const t1 = (t: T1) => {}
const t2 = (t: T2) => {}
const t3 = (t: T3) => {}

const fA = (t: TA) => {
  if (t.type === 1) {
    // These errors are correct since t can be either T1 or T2
    t.f1 // Property 'f1' does not exist on type 'TA'.\nProperty 'f1' does not exist on type 'T2'.(2339)
    t1(t) // Argument of type 'TA' is not assignable to parameter of type 'T1'.\nProperty 'f1' is missing in type 'T2' but required in type 'T1'.(2345)
  } else {
    // t must be of type T2 as T1 has been excluded
    t.f2 // Property 'f2' does not exist on type 'TA'.\nProperty 'f2' does not exist on type 'T1'.(2339)
    t2(t) // Argument of type 'TA' is not assignable to parameter of type 'T2'.\nProperty 'f2' is missing in type 'T1' but required in type 'T2'.(2345)
  }
}

const fB = (t: TB) => {
  if (t.type === 1) {
    t.f1
    t1(t)
  } else {
    t.f3
    t3(t)
  }
}

type T4 = 4
type T5 = number
type TC = T4 | T5
const t4 = (t: T4) => {}
const t5 = (t: T5) => {}

type T6 = 6
type TD = T4 | T6
const t6 = (t: T6) => {}

const fC = (t: TC) => {
  if (t === 4) {
    t4(t)
  } else {
    t5(t)
  }
}

const fD = (t: TD) => {
  if (t === 4) {
    t4(t)
  } else {
    t6(t)
  }
}

🙁 Actual behavior

The type system does not exclude type T1 from TA (via if (t.type === 1) where t: TA) when TA.type is 1 | number but excludes T1 from TB when TB.type is 1 | 3.

ALSO

The type system excludes type T4 from TC (via if (t === 4) where t: TC) when TC is 1 | number and excludes T5 from TD when TD is 4 | 5.

🙂 Expected behavior

Frankly I'm confused but I am attempting to share that to identify the problem or at least a clear model of how to understand this.

The narrowing behavior should be consistent whether the type excluded is part of a structure or not.

In more words: the else clause of fA should be able to determine that t is of type T2 (since type T1 is excluded) even though the type remains ambiguous in the if block OR the if and else clause of fc should be unable to determine the type of t.

My intuition is that the more useful choice would be for T1 to be excluded from TA determining that t is of type T2 in the else clause.

Additional information about the issue

A little history: I originally confused myself by trying to declare an unknown type Exclude<string, 'concrete'> and looking into it came to understand that Exclude works by removing types from a union. This broke my intuitive understanding of the class of strings and a concrete strings membership therein but was a coherent and consistent way for it to work.

However, as I discovered I was wrong but also tried to simplify the situation, I discovered that Exclude was a distraction and that I could reproduce the behavior using conditionals but not in the way I expected. On the back of my union-type-removal model of understanding exclude I expected fB to also not work but found the opposite. Trying to scratch further, i removed the object structure and to my surprise found that the exclusion worked fine if the narrowing was not on an attribute of an object type.

To my ignorant eyes, it seems that a corner case may have been missed. I expect it is more likely that my model is too simple.

[erikerikson]

related: #55095

[fatcerberus]

Another person throwing yet more evidence on the pile that TypeScript is either 1) a gateway drug to type theory or 2) just tends to attract mathematically-inclined thinkers in general...

As fun as it is at times to think about (and things like union types do have very interesting type thoery implications), it's been my experience that trying to construct a consistent mathematical model of the TypeScript type system is more or less a fool's errand. The type system is built on years of pragmatic case-by-case decisions guided by what people are actually doing with JS/TS code in the wild, so any model you come up with to describe things is inevitably going to run into inconsistencies like this. Trying to model it mathematically is a fun diversion, but has little real-world application, IMO.

[RyanCavanaugh]

a clear model of how to understand this.

I guess the overarching principle to keep in mind is that TypeScript is not a constraint solver.

Anyway, given how narrowing works, we'd need negated types to represent what's happening here. See #42876 (comment)

[fatcerberus]

More practically speaking, I don't think discriminated-union narrowing works by elimination, e.g. even if you invert the condition so that

  if (t.type !== 1) {
    t.f2
    t2(t)
  } else {
    t.f1
    t1(t)
  }

It still doesn't rule out T1 in the true branch, even though it would be sound to do so.

[erikerikson]

Thank you both very much. For these comments and for Typescript.

A number of responses, the important two at the end

@fatcerberus I don't mean anything as responsible as a mathematical model so much as just a mental one. I am Mort and mere mortal here.

@RyanCavanaugh Regarding #42876 (comment), I had attempted, with my discussion of escaping my confusion about Exclude (and a few other details), to communicate I had removed that mental trap from my thinking.

@fatcerberus > I don't think discriminated-union narrowing works by elimination

Practically, it clearly doesn't in the object attribute case (fA where TA = { type: 1 | number } and the conditional is if (t.type === 1)), while does appear to work that way in the primitive case (fC where TC = 1 | number and the conditional is if (t === 1)). The inconsistency between those cases is the only reason I thought this issue might be worth the team's time. FWIW, adopting your negative case approach gives the same result.

@RyanCavanaugh I don't understand what "we'd need negated types to represent what's happening here" means. Can we get a pointer to the current implementation so that I could at least attempt to understand the meaning of the code?

TypeScript is not a constraint solver.

Apologies that I missed the significance of this principle. Typescript is a useful tool and I'm happy to accept its behavior in this case. I'm happy to close this issue but thought that the inconsistency might be worth review. Again, thank you both and the entire team very much.

[erikerikson]

fatcerberus: here is a simpler formulation that uses the negative conditional and works as expected in the primitive case but not in the object attribute case:

type T1 = {
  type: 1
  f1: 1
}
type T2 = {
  type: number
  f2: 2
}
type T3 = 3
type T4 = number

type TA = T1 | T2
type TB = T3 | T4

const t1 = (t: T1) => {}
const t2 = (t: T2) => {}
const t3 = (t: T3) => {}
const t4 = (t: T4) => {}

const fA = (t: TA) => {
  if (t.type !== 1) {
    t2(t) // Argument of type 'TA' is not assignable to parameter of type 'T2'.\nProperty 'f2' is missing in type 'T1' but required in type 'T2'.(2345)
  } else {
    t1(t) // Argument of type 'TA' is not assignable to parameter of type 'T1'.\nProperty 'f1' is missing in type 'T2' but required in type 'T1'.(2345)
  }
}

const fB = (t: TB) => {
  if (t !== 3) {
    t4(t)
  } else {
    t3(t)
  }
}

[RyanCavanaugh]

@erikerikson see the function narrowTypeByBinaryExpression in src/compiler/checker.ts

[erikerikson]

Thanks so much. I am going to close this but feel welcome to reopen if it will provide the team with value.

[fatcerberus]

I don't mean anything as responsible as a mathematical model so much as just a mental one. I am Mort and mere mortal here.

That’s what you say, but I remember thinking the same thing when I was first trying to internalize the complexities of TS once upon a time, and it ultimately got me interested in category theory. So just watch out for that in the future… 😉

@erikerikson If it helps at all, there is no meaningful distinction between 1 | number and number - afaik, in any situation where the former type is constructed, it immediately collapses to the latter. That’s why Ryan says you need negated types for this in general - so the type system can understand the concept of “any number except 1” at all levels of abstraction.

[RyanCavanaugh]

It isn't exactly what happens, but you can form a good-enough mental model by thinking of narrowing as intersection:

type X1 = { x: 1, y: "one" };
type XN = { x: number, y: "other" };
let obj: X1 | XN;

if (obj.x === 1) {
 // Intersect (X1 | XN) with { x: 1 }
 // X1 & { x: 1 } === X1
 // XN & { x: 1 } === well, just that
 // Neither are never
 // the result is obj: X1 | XN
}

if (obj.x === 2) {
 // Intersect (X1 | XN) with { x: 2 } 
 // X1 & { x: 2 } === never (1 & 2 is never)
 // XN & { x: 2 } === well, just that
 // result: obj is XN, the union is filtered
}

if (obj.x !== 2) {
 // Intersect (X1 | XN) with OH NO...
 // There's no type of "not 2"
 // Nothing can be done
}

[erikerikson]

it immediately collapses to the latter

This is the case. I have confirmed using ~/tests/cases/compiler/narrowByEquality.ts. Interestingly, trying to pin this down better, I put Ryan's code in there and then simplified it as follows to no difference in the type outputs for the relevant types (and fixing the last conditional to what I presume was intended):

type X1 = { x: 1 };
type XN = { x: number };
declare let x1N: X1 | XN;
if (x1N.x === 1) {
    x1N;
}
if (x1N.x === 2) {
    x1N;
}
if (x1N.x !== 1) {
    x1N;
}

The corresponding output in tests/baselines/local/narrowByEquality.types does show the narrowing (>x1N : XN) in the never intersection case (if (x1N.x === 2)):

type X1 = { x: 1 };
  >X1 : { x: 1; }
  >x : 1

type XN = { x: number };
  >XN : { x: number; }
  >x : number

declare let x1N: X1 | XN;
  >x1N : X1 | XN

if (x1N.x === 1) {
  >x1N.x === 1 : boolean
  >x1N.x : number
  >x1N : X1 | XN
  >x : number
  >1 : 1

    x1N;
    >x1N : X1 | XN
}
if (x1N.x === 2) {
  >x1N.x === 2 : boolean
  >x1N.x : number
  >x1N : X1 | XN
  >x : number
  >2 : 2

    x1N;
    >x1N : XN
}
if (x1N.x !== 1) {
  >x1N.x !== 1 : boolean
  >x1N.x : number
  >x1N : X1 | XN
  >x : number
  >1 : 1

    x1N;
    >x1N : X1 | XN
}

Thank you very much for helping me identify this and decompose it into a more tangible and detailed model! The implicitly negative case's narrowing carries a lot of explanatory power - great example to share and make it more concrete. Hope this extended documentation provides a lot of help to the community.