Revision - 96acd4d - Subtype: avoid false alarm caused by eager [...] - origin: https://github.com/JuliaLang/julia

visit type:

https://github.com/JuliaLang/julia

19 April 2024, 06:28:37 UTC

Revision 96acd4d4e90647caab17af0f689723f5a2594cfd authored by N5N3 on 02 February 2023, 03:41:26 UTC, committed by GitHub on 02 February 2023, 03:41:26 UTC

Subtype: avoid false alarm caused by eager `forall_exists_subtype`. (#48441)

* Avoid earsing `Runion` within nested `forall_exists_subtype`

If `Runion.more != 0` we‘d better not erase the local `Runion` as we need it if the subtyping fails after.

This commit replaces `forall_exists_subtype` with a local version.
It first tries `forall_exists_subtype` and estimates the "problem scale".
If subtyping fails and the scale looks small then it switches to the slow path.

TODO: At present, the "problem scale" only counts the number of checked `Lunion`s.
But perhaps we need a more accurate result (e.g. sum of `Runion.depth`)

* Change the reversed subtyping into a local check.

Make sure we don't forget the bound in `env`.
(And we can fuse `local_forall_exists_subtype`)

* Optimization for non-union invariant parameter.

1 parent d918576

Files
Changes

Permalinks

Tip revision: 96acd4d4e90647caab17af0f689723f5a2594cfd authored by N5N3 on 02 February 2023, 03:41:26 UTC
Subtype: avoid false alarm caused by eager `forall_exists_subtype`. (#48441)

Tip revision: 96acd4d

File	Mode	Size
.devcontainer
.github
base
cli
contrib
deps
doc
etc
src
stdlib
test
.buildkite-external-version	-rw-r--r--	5 bytes
.clang-format	-rw-r--r--	3.3 KB
.clangd	-rw-r--r--	114 bytes
.codecov.yml	-rw-r--r--	52 bytes
.git-blame-ignore-revs	-rw-r--r--	294 bytes
.gitattributes	-rw-r--r--	65 bytes
.gitignore	-rw-r--r--	514 bytes
.mailmap	-rw-r--r--	12.1 KB
CITATION.bib	-rw-r--r--	513 bytes
CITATION.cff	-rw-r--r--	940 bytes
CONTRIBUTING.md	-rw-r--r--	23.1 KB
HISTORY.md	-rw-r--r--	363.4 KB
LICENSE.md	-rw-r--r--	1.3 KB
Make.inc	-rw-r--r--	53.0 KB
Makefile	-rw-r--r--	30.1 KB
NEWS.md	-rw-r--r--	1.7 KB
README.md	-rw-r--r--	7.3 KB
THIRDPARTY.md	-rw-r--r--	3.7 KB
VERSION	-rw-r--r--	11 bytes
julia.spdx.json	-rw-r--r--	35.8 KB
sysimage.mk	-rw-r--r--	4.1 KB

Showing with 0 additions and 0 deletions (0 / 0 diffs computed)

Computing file changes ...

https://github.com/JuliaLang/julia

Subtype: avoid false alarm caused by eager `forall_exists_subtype`. (#48441)

README.md