Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

mcomp on polymorphic variants is a little weak #7707

Closed
vicuna opened this issue Jan 12, 2018 · 4 comments
Closed

mcomp on polymorphic variants is a little weak #7707

vicuna opened this issue Jan 12, 2018 · 4 comments
Assignees
@lpw25
Labels
Stale typing

Comments

@vicuna
Copy link

vicuna commented Jan 12, 2018 •
edited by yallop

Original bug ID: 7707
Reporter: @lpw25
Status: new
Resolution: open
Priority: normal
Severity: minor
Version: 4.06.0
Category: typing

Bug description

The [mcomp] function doesn't really consider the row variable in polymorphic variants. For example, the following doesn't type check:

  # type ('a, 'b) eq = Refl : ('a, 'a) eq;;
  type ('a, 'b) eq = Refl : ('a, 'a) eq

  # let f : (< foo : 'a . [> `Foo] as 'a >, < foo : 'b . [> `Bar ] as 'b >) eq -> 'a = function _ -> .;;
  Characters 92-93:
    let f : (< foo : 'a . [> `Foo] as 'a >, < foo : 'b . [> `Bar ] as 'b >) eq -> 'a = function _ -> .;;
                                                                                              
  ^
  Error: This match case could not be refuted.
         Here is an example of a value that would reach it: Refl

because [mcomp] does not notice the incompatibility between:

  'a. [> `Foo] as 'a

and

  'b. [> `Bar] as 'b

This is of course safe, since it is conservative to assume that all types are compatible. Still it would be nice if it handled these types more accurately.

At the moment [mcomp] will only consider two polymorphic variants incompatible if one of them is closed and does not contain a tag from the other. This doesn't take account of cases where the row variable is a non-aliasable constructor or a universal variable. Ideally [mcomp] would construct the rows necessary to make the variants compatible and would then compare those rows with the actual rows for compatibility.
@vicuna vicuna added the typing label Mar 14, 2019
@github-actions
Copy link

github-actions bot commented May 7, 2020

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label May 7, 2020
@lpw25 lpw25 self-assigned this May 7, 2020
@lpw25 lpw25 removed the Stale label May 7, 2020
@garrigue
Copy link
Contributor

garrigue commented May 9, 2020

How did you stumble into this example?
I agree that fixing it should not be difficult (basically, one can take the minimal instance of each polymorphic variant type, which amount to closing, and they should be compatible), but is the extra work justified.

@lpw25
Copy link
Contributor

lpw25 commented May 10, 2020

I don't really remember, but probably by reading the code and being surprised that it didn't try comparing the row_more parts of the types at all.

@github-actions
Copy link

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label May 12, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@lpw25 lpw25

Labels
Stale typing
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@garrigue @lpw25 @vicuna