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

mcomp on polymorphic variants is a little weak #7707

Open
vicuna opened this Issue Jan 12, 2018 · 0 comments

Comments

Projects
None yet
1 participant
@vicuna
Copy link
Collaborator

vicuna commented Jan 12, 2018

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.