Unsound handling of unions with multiple type variables (real this time)

Bug Report

Note: I previously opened a similar report, but made a mistake in the code example there #49186

🔎 Search Terms

unsound,union,generic

🕗 Version & Regression Information

This is a runtime error
This is the behavior in every version I tried, and I reviewed the FAQ for entries about: unions
- 4.7.0-beta, 4.6.4, 4.5.5, 4.4.4, 4.2.3, 4.1.5, 4.0.5, 3.9.7, 3.8.3, 3.7.5, 3.6.3, 3.5.1, 3.3.3

⏯ Playground Link

playground link

💻 Code

function extract<K>(x: Array<K> | Array<Array<K>>): K {
  const arr = x[0];
  if (Array.isArray(arr)) {
    return arr[0];
  }
  return arr;
}

function extract2<T>(x: Array<T>): T {
  return extract(x);
}

const x = extract2([[3]]); // hover to see type: `number[]`
console.log(x); // but value is `3`
x.map(x => x); // which leads to runtime error: 'x.map is not a function'

🙁 Actual behavior

Runtime error not caught by TypeScript, due to incorrect inference.

🙂 Expected behavior

Type error.

If this is the same bug, why didn’t you just post the corrected repro in the original issue?

edit: Disregard. Just noticed the original issue was closed as fixed so it's probably not an accurate description of the problem.

Looks like a duplicate of #45686. This sort of filtering is very useful but unsound, but without negated types there's not really much better we can do. If you care strictly about safety then the call signature <T>(x: T[] | T[][])=>T cannot be implemented, because nothing stops someone from writing both of these:

const num = extract<number>([[3]]); 
const arr = extract<number[]>([[3]]);

but of course at runtime those are the same call. If you want to work around it in your own code you can try to be more explicit like

function extract<T>(x: Exclude<T, readonly any[]>[] | T[][]): T { /* impl */ }

extract<number>([[3]]); // okay
extract<number[]>([[3]]); // error

function extract2<T>(x: T[]): T {
  return extract(x); // error
}

Playground link

Joe Calzaretta (@jcalz)

Joe Calzaretta (@jcalz) thanks for taking a look, but I think I disagree on the diagnosis and am more hopeful the problem is solvable

If you care strictly about safety then the call signature <T>(x: T[] | T[][])=>T cannot be implemented

I agree such signatures (where there are overlapping unions with type variables) are probably mistakes, but they do occur in the wild.

I think it's main the job of a type checker to error on unsound code, not to assume that what the user wrote is intentional.

... without negated types there's not really much better we can do

Here are some options:

Flow approach playground, where the implementation of such a whacky function is rejected. Imo, it would be even better if the signature could also be rejected, at least in the common cases.
Typed Racket, iuc, accepts the definition by doing multiple rounds of constraint solving gist. I wasn't able to trick it like TypeScript is tricked here.

Joe Calzaretta (@jcalz)

I see how the issue may have a common cause with #45686, but will leave this open for a bit because a different solution might be available. Thanks for the triage Joe Calzaretta (@jcalz)

Joe Calzaretta (@jcalz)

I think it's main the job of a type checker to error on unsound code, not to assume that what the user wrote is intentional.

Welcome to the TypeScript Unsoundness Support Group! I'm Joe Calzaretta (@jcalz) and I have been a member for four years. Please enjoy the complimentary coffee; the cups leak a little bit so don't hold them directly over your lap. Today we'll be discussing TypeScript Language Design Non-Goal #‍3 and how it can be used as a mantra to stay calm in the face of logical contradictions.

I don't consider Flow's handling of this to be sound either. Example that checks in both checkers:

type Cat<T> = { name: T, meow: string }
type Mortgage<T> = { length: T, amount: number };

declare function fn<T>(x: Cat<T> | Mortgage<T>): T;
// if isCat(x) return x.name else return x.amount

const m: Cat<"whiskers"> & Mortgage<30> = { amount: 0, length: 30, meow: "", name: "whiskers" };
const n: Mortgage<30> = m;
function fn(x: Mortgage<30>) {
  const o: number = fn(x); // allowed but is "whiskers"
}

There's not much we can do here that's useful. It's not plausible to warn on this kind of signature -- for one, it's effectively the same signature as Array#flat! Aliasing is always going to be capable of inducing incorrect inference results if the implementation isn't extremely watertight, but functions that are a tiny bit leaky are very common.

Switching to a sort of whole-program unification like Racket is clearly out of scope.

Switching to a sort of whole-program unification like Racket is clearly out of scope.

Typed Racket uses Local Type Inference, just like TypeScript
Section 4.3 of "Occurrence Typing Modulo Theories" https://arxiv.org/pdf/1511.07033.pdf. No whole-program inference.

I don't consider Flow's handling of this to be sound either. Example that checks in both checkers:

Flow's approach seems to be such that one can't define the "bad" functions. At least, I haven't managed to trick it yet:

function badUnion<K>(x: Array<K> | Array<Array<K>>): K {
  if (Array.isArray(x)) {
    return x[0]; // Error in the body of the function. Your example had no body
  }
  return x;
}

playground link

I don't understand the alternative example you provided, which omits the definition but has a comment that seems to refer to type predicates. Type predicates are a TypeScript feature that Flow doesn't have: facebook/flow#34.

There's not much we can do here that's useful.

Whether TS should provide a diagnostic for the body of extract/badUnion is independent of whether there should be a diagnostic at the use site.

Re providing a diagnostic on the signature vs. the body of the "bad" function: fwiw I would expect a diagnostic somewhere for the code in the original example (like Flow and Typed Racket do).

It's not plausible to warn on this kind of signature -- for one, it's effectively the same signature as Array#flat

Warning on the signature is not strictly necessary, if there is a diagnostic for the body.

But Array#flat may not be the best example, anyway, the signature doesn't use unions-with-type variables: https://github.com/microsoft/TypeScript/blob/35c1ba6/lib/lib.es2019.array.d.ts#L52. The issue I opened seems to be about unions-with-type-variables.

This issue has been marked 'Working as Intended' and has seen no recent activity. It has been automatically closed for house-keeping purposes.

Was this issue closed by mistake?
It was marked "working as intended", but the main reason given seems to be that it is impossible to handle the code soundly with local type inference, which does not seem to be correct.

I replied above with more information about how similar type checkers solve the problem.

If it's deemed not worth it to fix the problem, could we change to #wontfix?

Won't Fix would be that we identified it as a defect, but decided fixing it wasn't worth the cost. That isn't the case here.

Here, we think this is the "right" behavior. The actual prevalence of the sort of problematic aliasing is not common enough to justify issuing many false positive warnings.

The TS+Typed-Racket-inspired type checker I worked on at WhatsApp, eqWAlizer, was released this week. Thought it might be helpful to share the behavior, which was simple to implement safely but required fine-tuning for decent error messages:

Given input:

-module(sample).
-export([main/1]).

-spec extract([T] | [[T]]) -> T.
extract([[T]]) -> T;
extract([T]) -> T.

-spec extract2([T]) -> T.
extract2([T]) -> extract(T).

-spec main(any()) -> ok.
main(_) ->
    X = extract2([[3]]),
    %io:format("~s~n", [X]),
    lists:map(fun(Z) -> Z end, X),
    ok.

We report these errors:

error: expected_subtype
  ┌─ wa_util/src/sample.erl:5:19
  │
5 │ extract([[T]]) -> T;
  │                   ^ T.
Expected: T
Got     : any()

See https://fburl.com/eqwalizer_expected_subtype

error: expected_subtype
  ┌─ wa_util/src/sample.erl:6:17
  │
6 │ extract([T]) -> T.
  │                 ^
  │                 │
  │                 T.
Expected: T
Got     : T | [T]

See https://fburl.com/eqwalizer_expected_subtype
  │

  T | [T] is not a subtype of T
  because
  [T] is not a subtype of T

error: expected_subtype
  ┌─ wa_util/src/sample.erl:9:26
  │
9 │ extract2([T]) -> extract(T).
  │                          ^
  │                          │
  │                          T.
Expected: [T] | [[T]]
Got     : T

See https://fburl.com/eqwalizer_expected_subtype
  │

  T is not a subtype of [T] | [[T]]
  because
  T is not a subtype of [T]

3 ERRORS

eqWAlizer's handling is not perfect: error messages could pinpoint the problem more precisely, especially for easy cases. But at least it seems to be sound and the implementation of generics+unions is roughly 20 LOC.

A sound implementation of the check in < LOC, and the only cases that are rejected are cases where the user wrote something ambiguous: https://github.com/WhatsApp/eqwalizer/blob/1dbdbbd/eqwalizer/src/main/scala/com/whatsapp/eqwalizer/tc/generics/Constraints.scala#L163

Navigation Menu

Repository navigation

Unsound handling of unions with multiple type variables (real this time) #49432

Bug Report

🔎 Search Terms

🕗 Version & Regression Information

⏯ Playground Link

💻 Code

🙁 Actual behavior

🙂 Expected behavior

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Unsound handling of unions with multiple type variables (real this time) #49432

Description

Bug Report

🔎 Search Terms

🕗 Version & Regression Information

⏯ Playground Link

💻 Code

🙁 Actual behavior

🙂 Expected behavior

Activity

fatcerberus commented on Jun 8, 2022

jcalz commented on Jun 8, 2022

mheiber commented on Jun 9, 2022

mheiber commented on Jun 9, 2022

jcalz commented on Jun 9, 2022

RyanCavanaugh commented on Jun 9, 2022

mheiber commented on Jun 9, 2022

typescript-bot commented on Jun 11, 2022

mheiber commented on Jun 12, 2022

RyanCavanaugh commented on Jun 15, 2022

mheiber commented on Aug 2, 2022

mheiber commented on Jul 10, 2024

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions