Problems with TypeIs

[Liz (Elizabeth King)]

@carljm

So if we want to make TypeIs safe in this respect, there’s no need to change the general rules around variance and subtyping in super-disruptive ways, there’s only a need for more correct handling of intersection simplification.

This is true for TypeIs, but not for higher kinded types more generally. It would be a good thing if we could get consensus on if higher kinded types are ever going to be fully supported or not, I’ve had some discussions with @mikeshardmind on this, and while I was against this at first, I think fully ruling them out would be more beneficial to the type system as we can stop needing to consider them, and can start using things that only work on rank 1 types.

@carljm

The theoretical reason it is incorrect is because MySequence is invariant in its type parameter, therefore there is no subtype relationship between MySequence[object] & Sequence[int], therefore the intersection can’t be simplified.

The problem with this is the indirection possible that allows assigning MySequence to something that expects a Sequence then has the visible intersections be Sequence[object] & Sequence[int], when the actual type is invariant. There are major issues around writing a safe TypeIs function. You can’t write it assuming only the input type, but any possible subtype of of that input type with unknown attributes, properties, methods, and variance. I agree with:

@mikeshardmind

It’s not possible to narrow a generic type safely if you have a subtype of that generic type. You no longer have all of the relevant information and cannot know if you have checked all places the subtype uses a type variable

Not even only from a place of variance, it could be an unsafe narrowing even entirely within covariance, as @ImogenBits showed Revisiting variance - #43 by ImogenBits (after modifications to use a tuple where a list was used)

I think some of these cases are detectable and type checkers should warn about those, but not all of them will be, and some need to be documented cases only. This means that this feature cannot be considered safe within the current type system, as it is possible to construct a TypeIs function that would be impossible to determine if the function and use of the function was safe or not statically.