Skip to content

Track type of variables bound by as - #13763

Merged
lthls merged 4 commits into
ocaml:trunkfrom
lthls:lpw25-fix-bad-poly-variant-type
Feb 12, 2025
Merged

lthls merged 4 commits into
ocaml:trunkfrom
lthls:lpw25-fix-bad-poly-variant-type

Conversation

@lthls

@lthls lthls commented Jan 30, 2025 •

Copy link
Copy Markdown
Contributor

Port of oxcaml/oxcaml#3507.

Short description: when typing as patterns, we separate the type of the pattern from the type of the variable.
This can be seen on this example from the original PR:

let f x =
  match x with
  | Error ( `A as error )
  | Ok ( `B () as error ) -> use_error error
  | Ok `C -> ()

In the first pattern, `A as error has pattern type [< `A ], but since error also appears in other patterns it will end up having type [> `A | `B of unit] on the right-hand side.
The code in matching.ml generates a static handler for the shared right-hand side, which has error as parameter, and generates a value kind annotation on this parameter from the type of error in the pattern.
Before this PR, this would look up the type of the variable in the first case below the or-pattern, and would find the type of the pattern, [< `A ], which is always an integer so Pintval is generated.
After this PR, we still look only in the first case, but since we get the type of the variable instead of the pattern, we get the correct type (which produces Pgenval in this case).

Compared to the original PR, the only relevant difference is in the Ppat_constraint case: the flambda-backend version has removed the code for translating (var : t) as (_ as var : t), so I had to find what would be the correct type in this case.

I've chosen to add as a regression test for the native compiler the failing example from @lpw25's original PR, which fails both with Closure (since #8735) and Flambda (since #13758).

@gasche gasche self-assigned this Feb 5, 2025
@lthls lthls added the bug label Feb 6, 2025
@lthls lthls linked an issue Feb 6, 2025 that may be closed by this pull request

@gasche gasche left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is an annoying patch to read because of the amount of boilerplate, but I think that it is correct and I understand why it helps -- the problem is that the types of pattern variables returned by Typedtree.pat_bound_idents_full may be incorrect. I wish we had move Tpat_alias to an inline record in the process, but oh well, this is okay.

lpw25 and others added 4 commits February 12, 2025 09:47
Keep the types of variables bound by `as` because they may not equal the
types of the `as` patterns themselves. This fixes some incorrect value
kinds that can lead to miscompilation.
@lthls
lthls force-pushed the lpw25-fix-bad-poly-variant-type branch from 6df7974 to 9a67d5a Compare February 12, 2025 09:10
@lthls
lthls merged commit 9fb92d9 into ocaml:trunk Feb 12, 2025
tmcgilchrist pushed a commit to tmcgilchrist/ocaml that referenced this pull request Feb 17, 2025
Keep the types of variables bound by `as` because they may not equal the
types of the `as` patterns themselves. This fixes some incorrect value
kinds that can lead to miscompilation.

---------

Co-authored-by: Leo White <leo@lpw25.net>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Segfault due to incorrect value kinds

3 participants