Fix #31833 Relate two indexed access types covariantly

[jack-williams]

Fixes #31833

I think the predicate I've added it probably too permissive, but it works as a short-fix if that is what is needed. I would be curious to explore trying to apply the write simplification during expression checking rather that type relating.

[fatcerberus]

Hmm, I'm not sure this is 100% sound. Intuitively it sounds right at first--but, hypothetically, if we have two unknown keys both of type K can we guarantee that T[K] is safely assignable to T[K]?

If K represents the same key on both sides it's okay, but if there are two keys...

[jack-williams]

I'm not sure this is 100% sound.

It's not - but it wasn't before.

To get this right I think you really need to drive the simplifications by the expression forms, not by the relation. The biggest give-away here is that you can construct cases where it is unsound for T[K] to be assignable to itself, meaning the type relation is not reflexive.

[fatcerberus]

Thinking about it some more, I’m not sure it’s a decidable problem. We have an unknown key on both sides of the relation, so the question then becomes analogous to my favorite variance conundrum: given we have an animal of type Carnivore | Herbivore and food of type Meat | Plant, can we feed the animal—yes or no? This question is impossible to answer because we simply don’t have enough information. Asking if T[K] is assignable to itself is essentially the same question, so I guess in the end it comes down to whether we be optimistic or pessimistic about it.

Interesting thing to think about.

[jack-williams]

Whether T[K] is assignable to itself should be an easily decidable question, but the issue is whether it is the right question. When you have mutable references and sub-typing you really need to assign two types to a reference: a read type and a write type.

So when we have something like:

interface Carnivore { food: "meat"; }
interface Herbivore { food: "plants"; }
type Ref = Carnivore | Herbivore;

declare const x: Ref;
declare const y: Ref;
x.food = y.food;

We need to use the write type of x which is Carnivore & Herbivore, and the read type of y which is Carnivore | Herbivore.

But the import thing is that the selection of types is driven by the expression, not the typing relation. So we never actually ask whether (Carnivore | Herbivore)['food'] is related to itself, we ask whether READ(Carnivore | Herbivore)['food'] is related to WRITE(Carnivore | Herbivore)['food'] - these are two distinct types.

The read/write distinction does not show up in the typing relation here. When you want to relate functions that accept indexed accesses, such as in the original issue, the types are just related like normal because there is no assignment going on.

[jack-williams]

And FWIW my PR is a hack - I'm really throwing it out there as a quick fix if lots of people are hitting the issue.

[fatcerberus]

Whether T[K] is assignable to itself should be an easily decidable question

You would think so, right? But AFAICT the only way you can make this decision with certainty is if you can prove K represents the same key on both sides (we don’t have to know what the key is, just that the relationship is symmetrical). Given only the type T[K] we have no way to prove K will access the same property on both sides and therefore the question at the type level is circular: “Will the animal eat the food? Yes, if the animal eats the food.” And that’s a question we can’t answer.

So I guess this is part of what you meant about looking at the expressions instead of the types: If we know something about the origin of K other than just its type, then the circularity above can be broken.

[fatcerberus]

When you want to relate functions that accept indexed accesses, such as in the original issue, the types are just related like normal because there is no assignment going on.

(Sorry if I’m a being a pest - the implications of #30769 have been really thought-provoking.)

function foo<T, K extends keyof T>(arg: T[K]): void;
function bar<T, K extends keyof T>(arg: T[K]): void;
foo = bar;
bar = foo;

In type theory terms, would I be correct to assume the reason the above is sound is that K is in a contravariant position of a type which is also in a contravariant position and therefore the whole relation becomes covariant again?

[jack-williams]

The problem is that T[K] isn't really a type, if it were then it would simply be denoted by a set and therefore assignability to itself follows from reflexivity of subset inclusion. In reality T[K] has been overloaded to represent two types: the type of reading T[K] and the type of writing T:=K.

So in the cases you highlight where there is trickiness you aren't truly relating T[K] to itself; when you are doing an assignment you are actually relating the distinct types T[K] to T:=K.

Once you have the distinction then both T[K] and T:=K are trivially related to themselves, but not necessarily each-other. So in the function case (#31833) we actually have a true read type T[K] as an argument which should be related to itself. This makes sense because the two things you are relating are really just the same function argument looked up using the same key.

So I guess this is part of what you meant about looking at the expressions instead of the types: If we know something about the origin of K other than just its type, then the circularity above can be broken.

Yep, though it's not so much about the origin as opposed to the use (I guese the same thing?). Given:

l.x = r.y

The type of the LHS should be the write type T:=K, and the type on the RHS should be the read type T[K], if both l and r have type T, and both x and y have type K.

The uncertainty you refer to is encoded in the type constructors [] and =: that are fundamentally different operations/types that have different sets of values in their domain.

EDIT: Just saw your edit.

Sorry if I’m a being a pest

Not at all! This is all super interesting.

Regarding your question. I believe that is sound because there is no mutation of the object T at key K. When you call the function you are simply being passed a value that satisfies the read type of T at K - with either alias it will be the same types, keys, and values. Co/Contra-variance in function types, and read/write co/contra-variance of mutable references is very similar, but not exactly overlapping.

[fatcerberus]

I guess I just subconsciously split it into two types in my head without realizing it, so thanks for highlighting that and making it explicit.

What’s really interesting about T:=K as a type is that, to use my animal analogy again, if we have the union Herbivore | Carnivore, we don’t necessarily have to feed it type Rocks = Meat & Plant - it’s merely that that’s the only thing it’s guaranteed to eat without further investigation—which is what discriminated unions are about. So with that in mind, I can now understand how resolving T:=K to an intersection is going to be very restrictive to actual real-world scenarios. Maybe it’s worth rethinking that change.

[jack-williams]

without further investigation

Yep I believe that observation is correct. Everything I've said has been ignoring narrowing of the object type. If you can narrow the object prior to narrowing you can effectively prove that everyone else must have a pointer to the object at that that narrowed type, therefore allowing you to write at the more specific type.

In your analogy. If I can narrow my reference of Herbivore | Carnivore to Herbivore then it is not possible for someone else to have a pointer to the same reference at type Carnivore (as this would break soundness). So I should be able to pass in (or update) using plants only.

[fatcerberus]

It’s particularly problematic in the case of functions too:

type Carnivore = (food: Meat) => void;
type Herbivore = (food: Plant) => void;

function feedMe(eater: Carnivore | Herbivore, food: Meat | Plant) {
    // let’s assume we can discriminate between Meat and Plant.
    // how do we know what 'eater' is?  there’s no way to tell.
    eater(food);  // type error
}

Which means in most cases if you have a union of functions with differing disjoint parameter types, you’ll never be able to do anything with it. And the current behavior of T[K] in contravariant positions just makes that worse. Hmm.

[fatcerberus]

Anyway if it wasn’t clear: 👍 to making (arg: T[K]) => void be assignable to itself.

[fatcerberus]

Having done some experiments, I'm more and more convinced this is a good change. The #30769 behavior breaks this perfectly reasonable code:

• Playground link

declare function frob<T>(value: T): T;

interface Thing
{
    pig: string;
    cow: number;
    ape: boolean;
}

const t: Thing = { pig: "it's fat", cow: 1208, ape: true };
const ks = Object.keys(t) as (keyof Thing)[];
for (const k of ks) {
    t[k] = frob(t[k]);  // what do you mean, "error"?!
}

The compiler knows exactly what T is here: it's Thing. What it doesn't know (based on type information alone) is what K is.

As discussed above it's not possible to prove this is sound in general without:

1. Narrowing K to a single possibility on each side before each assignment, or alternatively
2. Proving that K represents the same key on both sides of the relation

Generics rule out the former path almost entirely: We have no way to narrow a type parameter (cf. #31672), so K extends keyof T can only reasonably be treated as its upper bound for this purpose. Case 2 is probably decidable in some cases if we examine the expression, but TypeScript doesn't currently do that kind of thing (see e.g. #31445), so that's out too.

So what the compiler now basically does is, as it can't prove this is safe, takes the lazy way out with an existential quantification: there exists some subset of A | B whose values are always safe to assign to either A or B, even if you don't know which one it is. It just so happens this type is exactly the intersection A & B. But since that's not exhaustive--there's about 50% probability the assignment is still safe anyway--the restriction ends up getting in the way. Basically we're being forced to feed the animal dirt because the compiler can't figure out whether it's a carnivore or herbivore

But I digress. Given the inherent design limitations, I'm not thinking it makes much sense in general to be pessimistic about T:=K, soundness be damned. So this is a step back in the right direction, methinks.