Do not treat all type constructors as injective
commit858374a88650dcbbe218005cc735c785bb4e5cd2
authorFrank Emrich <frankemrich@fb.com>
Mon, 23 May 2022 14:35:14 +0000 (23 07:35 -0700)
committerFacebook GitHub Bot <facebook-github-bot@users.noreply.github.com>
Mon, 23 May 2022 14:35:14 +0000 (23 07:35 -0700)
tree4ecf68a330d33a33dbb65dc224f4fe3d9d5eaa01
parent142a8a651b904057d5872badbf683780990242cc
Do not treat all type constructors as injective

Summary:
The type-checker currently treats all type constructors as if they were injective. For example, given
```
newtype N<+T> = int
```
it treats the constraints `N<T1> <: N<T2>` and `T1 <: T2` as equivalent, even though they are not. Simplifying the former to the latter is sound, but not complete.

However, we observe that when type-checking for example a call site, we can rely on such sound-but-incomplete simplifications. Otherwise, we wouldn't be able to type-check even simple examples like the following:
```

function foo<T>(N<T> $x) : void {}

function bar(N<string> $y) : void {
  foo($y);
}
```
that require `T` to be instantiated with `string`.

Therefore, we continue treating all type constructors as injective if completeness is not required, as indicated by the value of `require_completeness` in `Typing_subtype.subtype_env`.

Reviewed By: andrewjkennedy

Differential Revision: D36444677

fbshipit-source-id: ca743055835687feff68b1fe7d2c15c5d38ba3d4
hphp/hack/src/typing/typing_subtype.ml
hphp/hack/test/typecheck/newtype11.php [new file with mode: 0644]
hphp/hack/test/typecheck/newtype11.php.exp [new file with mode: 0644]