Conditions for conditional types of function parameters don't propagate into function bodies

[bb010g]

Bug Report

Even when TypeScript proves that conditional type conditions hold, these proofs aren't fully propagated into the function body.

🔎 Search Terms

conditional type propagation witness entails function parameter

🕗 Version & Regression Information

• This is the behavior in every version I tried since v3.3.3, and I reviewed the FAQ for entries about conditional type condition propagation

⏯ Playground Link

Playground Link

💻 Code

interface IData<T> {
    data: T
};
function getData<T extends IData<U>, U>(x: T): U {
    return x.data;
}

class A implements IData<boolean> {
    constructor(public data: boolean) {};
};
class B {
    constructor() {};
}

type MyMap = {
    "a": A,
    "b": B,
}
const myMap: MyMap = {
    "a": new A(true),
    "b": new B,
};

function myConsumer<K extends keyof MyMap, T extends IData<U>, U>(key: MyMap[K] extends T ? K : never): U {
    const _: K = key; // valid iff `MyMap[K] extends T`
    const value: T = myMap[key];
    return getData(value);
}

🙁 Actual behavior

TypeScript fails to type check this code, with the following error:

Type 'MyMap[MyMap[K] extends T ? K : never]' is not assignable to type 'T'.
  'T' could be instantiated with an arbitrary type which could be unrelated to 'MyMap[MyMap[K] extends T ? K : never]'.

🙂 Expected behavior

TypeScript successfully type checks this code. It can already prove that MyMap[K] extends T in order to bind key with type K.

[MartinJohns]

Resolving of conditional types is deferred when they involve unbound type argumente. This is a design limitation.

[bb010g]

Is there a way to explicitly carry the resolution that occurs in const _: K = key; out & into const value: T = myMap[key];? Haskell would allow (roughly) case key of (_ :: K) -> (myMap[key] :: T) to work here, and I was hoping that const _: K = key; would work similarly (like how narrowing works). I should add that const key2: K = key; const value: T = myMap[key2]; also fails to type check.

[RyanCavanaugh]

There's not really a great way to describe the sorts of behavior where functions want to talk about "keys K of type T where T[K] is assignable to U". You can perform the filtering operation and you can perform the lookup operation but TS doesn't carry over the higher-order information that K' from keyof K in T where T[K] extends U means the T[K'] should behave as an arbitrary subtype of U.

See #48992

[DetachHead]

assuming this is a simpler example of the same issue

type Foo<T extends string> = T extends string ? T : never

const makeFoo = <T extends string>(value: T): Foo<T> => value // error

[mengdu]

Got a similar error

function foo<T extends true | false>(arg: T): T extends true ? string : number {
  return arg === true ? 'yes' : 0 // Type 'number' cannot be assigned to type 'T extends true? String: number'. ts(2322)
}

How to implement the function of Conditional Types? No example is found in the document.

[DetachHead]

@mengdu i believe that's a different issue. it's caused by the fact that narrowing a value with a generic type doesn't necessarily mean it's safe to narrow the generic itself. this can be demonstrated by adding a second argument to your function:

type Foo<T extends string> = T extends string ? T : never

const makeFoo = <T extends string>(value: T): Foo<T> => value // error

function foo<T extends true | false>(arg: T, arg2: T): T extends true ? string : number {
    if (arg === true) {
        // these two lines have errors, because narrowing arg can't narrow T because it would be unsafe to do so
        const foo: true = arg2 //arg2 can be false
        return 'yes'
    } else {
        return 0
    }
}

foo<boolean>(true, false)

see #21732 (comment) for another example

[bb010g]

@RyanCavanaugh The initial test case still fails type check on 5.5.0-dev.20240324. Why was this closed as completed?