Assignability rule for conditional types needs to require check types and distributivity to be identical

[mattmccutchen]

TypeScript Version: master (e471856)

Search Terms: assignable assignability conditional type check type checkType distributive distributivity identical unsound

Code

type MyElement<A> = [A] extends [[infer E]] ? E : never;
function oops<A, B extends A>(arg: MyElement<A>): MyElement<B> { 
    return arg;  // compiles OK, expected compile error
}
oops<[number | string], [string]>(42).slice();  // runtime error

type MyAcceptor<A> = [A] extends [[infer E]] ? (arg: E) => void : never;
function oops2<A, B extends A>(arg: MyAcceptor<B>): MyAcceptor<A> { 
    return arg;  // compiles OK, expected compile error
}
oops2<[number | string], [string]>((arg) => arg.slice())(42);  // runtime error

type Dist<T> = T extends number ? number : string; 
type Aux<A extends { a: unknown }> = A["a"] extends number ? number : string;
type Nondist<T> = Aux<{a: T}>;
function oops3<T>(arg: Dist<T>): Nondist<T> {
    return arg;  // compiles OK, expected compile error
}
oops3<number | string>(42).slice();  // runtime error

Expected behavior: Compile errors as marked.

Actual behavior: Compiles OK, runtime errors as marked.

Playground Link: link

Related Issues: None found

[weswigham]

This is less about conditional type check types and more about how tuple members/array indexes should be invariant instead of covariant. This is a known tradeoff we make to make passing around arrays of things in a (mostly) readonly fashion easier.

[mattmccutchen]

@weswigham I don't understand: no tuples or arrays are mutated in the example. In fact, since the example works even with distributive conditional types in this case, it can be rewritten without any tuples. I hope you agree that Wrapped should be covariant because it's read-only.

type Wrapped<T> = {readonly value: T};
type MyElement<A> = A extends Wrapped<infer E> ? E : never;
function oops<A, B extends A>(arg: MyElement<A>): MyElement<B> { 
    return arg;  // compiles OK, expected compile error
}
oops<Wrapped<number | string>, Wrapped<string>>(42).slice();  // runtime error

type MyAcceptor<A> = A extends Wrapped<infer E> ? (arg: E) => void : never;
function oops2<A, B extends A>(arg: MyAcceptor<B>): MyAcceptor<A> { 
    return arg;  // compiles OK, expected compile error
}
oops2<Wrapped<number | string>, Wrapped<string>>((arg) => arg.slice())(42);  // runtime error

Or were you saying that the assignability rule for conditional types contributes in some way to the goal of most generic types being covariant by default? How that would be is not clear to me yet.

[weswigham]

Or were you saying that the assignability rule for conditional types contributes in some way to the goal of most generic types being covariant by default? How that would be is not clear to me yet.

Eyyyea. We're (probably) comparing the check type of a conditional type as unconditionally covariant, when an infer type can implicitly make them invariant by extracting a covariant position and using it in the output (which would usually be a contravariant) position. Just like with arrays, we're not correctly measuring the variance of a conditional type. It's probably not desirable.

Or it could be another bug, I'm just speculating since I haven't actually looked into it yet.

[mattmccutchen]

I guess I should have stated in the initial comment, currently the check type of a conditional type is treated as unconditionally bivariant. I'll copy and paste the code from the checker since the file is too big to link to:

// Two conditional types 'T1 extends U1 ? X1 : Y1' and 'T2 extends U2 ? X2 : Y2' are related if
// one of T1 and T2 is related to the other, U1 and U2 are identical types, X1 is related to X2,
// and Y1 is related to Y2.
if (isTypeIdenticalTo((<ConditionalType>source).extendsType, (<ConditionalType>target).extendsType) &&
    (isRelatedTo((<ConditionalType>source).checkType, (<ConditionalType>target).checkType) || isRelatedTo((<ConditionalType>target).checkType, (<ConditionalType>source).checkType))) {
    if (result = isRelatedTo(getTrueTypeFromConditionalType(<ConditionalType>source), getTrueTypeFromConditionalType(<ConditionalType>target), reportErrors)) {
        result &= isRelatedTo(getFalseTypeFromConditionalType(<ConditionalType>source), getFalseTypeFromConditionalType(<ConditionalType>target), reportErrors);
    }
    if (result) {
        errorInfo = saveErrorInfo;
        return result;
    }
}

For arrays and objects, covariance is defensible as a useful behavior on the grounds that read-only use of arrays and objects is very common. For conditional types, do we know anything about (1) how often they are genuinely covariant or contravariant and (2) how often banning one or the other form of variance would produce undesired errors compared to desired ones? Measuring the variance would be ideal, but I don't know if it's feasible given all the weird things that TypeScript type inference does.

[jack-williams]

EDIT: removing some things that are patently wrong.

Currently it seems to be considering the two occurrences of Wrapped<infer E> in the following types as identical:

• A extends Wrapped<infer E> ? E : never;
• B extends Wrapped<infer E> ? E : never;

which feels very wrong. I don't think infer E should be identical to infer E when appearing in the extends clause of conditional types where the check types are not identical. Though that point could be obsolete if the rules are changed to only consider identical check types, rather than the current bivariant.

As a random aside, would these rules work:

T1 extends U1 ? X1 : Y1 < T2 extends U2 ? X2 : Y2

if

INV-RULE : if T1 === T2 and U1 === U2 then X1 < X2 and Y1 < Y2

else if < is a transitive relation then the following rules also apply

  CO-RULE     : if T1 < T2   and U1 === U2 then X1 < X2 and X1 < Y2 and Y1 < Y2
  CONTRA-RULE : if T2 < T1   and U1 === U2 then X1 < X2 and Y1 < X2 and Y1 < Y2

taking === to be identical, and < to be the relation

[mattmccutchen]

@jack-williams Assuming the conditional types are non-distributive (sigh), you are close. We may want to account for nontransitivity of assignability. For example, consider:

function foo<A, B extends A>(arg: A extends number ? {} : never):
    B extends number ? {} : never {
    return arg;
}
let n: never = foo<any, string>({});

I suspect the concept we would need may be similar to the "definitely assignable" relation that is used to evaluate conditional types. Or we could just say that anyone who writes the above code deserves what they get.

[jack-williams]

@mattmccutchen Yes, nontransitivity is definititely going to break things! Additional example:

function anotherOne<A, B extends A>(arg: A extends object ? {} : never):
    B extends object ? {} : never {
    return arg;
}
let n: never = anotherOne<Object, string>({});

[jack-williams]

Assuming the conditional types are non-distributive (sigh)

Have you looked into the distributive case much? I think the covariant case might be ok, but the contravariant case seems unresolvable.

type X<A> = A extends object ? true : false;

function distr<A, B extends A>(arg: X<A>): X<B> {
    return arg;
}

let n: never = distr<Function, never>(true);

[RyanCavanaugh]

We'll see what happens - might be too large of a break, but the theoretical justification is strong

[mattmccutchen]

Re #27619 (comment):

Has the team looked at the impact of switching from bivariance to invariance? I don't really have an intuition for what is used in RWC, but I could imagine something like Exclude<A, null> <: Exclude<B, null> if A <: B being useful.

I may as well just prepare a pull request and let the TypeScript team run it on the RWC suite.

[mattmccutchen]

PR is #27697. When I ran the test suite, I found the the previous issue in which the bivariance was introduced: #22860. This is basically the example with Exclude that @jack-williams was talking about. A workaround would be to effectively hide the problematic partition2 signature from the variance measurement by overriding the this type:

export class Option<T> {
    toVector(): Vector<T> {
        return <any>undefined;
    }
}

interface Seq<T> {
    tail(): Option<Seq<T>>;
}

class Vector<T> implements Seq<T> {

    tail(): Option<Vector<T>> {
        return <any>undefined;
    }

    partition2<T, U extends T>(this: Vector<T>, predicate:(v:T)=>v is U): [Vector<U>,Vector<Exclude<T,U>>];
    partition2(predicate:(x:T)=>boolean): [Vector<T>,Vector<T>];
    partition2<U extends T>(predicate:(v:T)=>boolean): [Vector<U>,Vector<any>] {
        return <any>undefined;
    }
}

[jcalz]

Is this the same issue or a different one:

interface Foo { a: string; }

interface Bar extends Foo { a: "literal"; }

type Cond<T extends Foo> = string extends T['a'] ? true : false;

type True = Cond<Foo>; // okay
type ShouldBeFalse = Cond<Bar> // true?! 😮
type ShouldBeFalseInlined = string extends Bar['a'] ? true : false; // false

[mattmccutchen]

@jcalz Looks unrelated. That's caused by the following rule in isStructuredTypeRelatedTo in the checker:

                    // A type S is related to a type T[K], where T and K aren't both type variables, if S is related to C,
                    // where C is the base constraint of T[K]
                    if (relation !== identityRelation && !(isGenericObjectType((<IndexedAccessType>target).objectType) && isGenericIndexType((<IndexedAccessType>target).indexType))) {
                        const constraint = getBaseConstraintOfType(target);
                        if (constraint && constraint !== target) {
                            if (result = isRelatedTo(source, constraint, reportErrors)) {
                                return result;
                            }
                        }
                    }

This rule has caused me grief on my project and I am happy to have another reason that might help justify getting rid of it. (Did your example originate in real code?) Feel free to file a separate issue; I didn't see an existing one.

[jack-williams]

@jcalz @mattmccutchen Related to that issue: #27470. (I'll leave the discussing of this issue at that as I don't want to go off topic).