Flow: Exact type intersections are unsound

[jfirebaugh]

Flow v0.91.0 accepts the following (try):

function fn<T, U>(x: $ReadOnly<T & U>): T {
  return x;
}

const exact: {| a: any |} = fn<{| a: any |}, { b: any }>({ a: 1, b: 1 });

This potential for unsoundness with intersections of exact types was noted in this comment in the discussion about adding exact types to TypeScript.

The comment notes "it's really not OK to error on instantiation" -- is this a principle Flow adheres to as well? If so, it seems there is indeed no way to make this sound. But if not, this should be an error -- something like "Cannot call fn with object literal bound to x because object literal [1] is incompatible with empty [2]."

[dsainati1]

So this is actually sound as presented here because of the $ReadOnly in the type of x. We cannot modify any values in x, meaning that any values that are part of U but not of T are never accessible after fn returns. If you remove the $ReadOnly type then this will error as you expect.

[jfirebaugh]

@dsainati1 I'm not sure I understand.

const a: {| a: any |} = { a: 1, b: 1 };
const b: {| a: any |} = fn<{| a: any |}, { b: any }>({ a: 1, b: 1 });

Why is a an error, and b is ok, when the right-hand sides of the assignments produce identical values?

Are you saying that exact types don't actually aim to provide a runtime guarantee of the absence of certain properties? They're merely meant to constrain the set of accessible properties?

[jfirebaugh]

This yields coerce (thanks to @wchargin for the examples in other issues):

// @flow
function coerce<T, U>(t: T): U {
  function f<T, U>(x: $ReadOnly<T & U>): T {
    return x;
  }

  let r = f<{||}, { t: T }>({ t });
  let s: {||} | { t: empty } = r;
  if (s.t) {
    return s.t;
  }

  throw 'Unreachable';
}

const twelve: number = coerce("twelve"); // no type error!
twelve.toFixed(); // runtime error!

[wchargin]

Nice. That’s not quite coerce, because your coerce(false) hits the
“unreachable” branch, but that’s easily fixed:

let r = f<{||}, { b: true, t: T }>({ b: true, t });
let s: {||} | { b: true, t: empty } = r;
if (s.b) return s.t;