|Anonymous | Login | Signup for a new account||2019-02-23 07:20 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0007707||OCaml||typing||public||2018-01-12 12:43||2018-01-12 12:43|
|Target Version||Fixed in Version|
|Summary||0007707: mcomp on polymorphic variants is a little weak|
|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 _ -> .;;
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
'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.
|Tags||No tags attached.|
|2018-01-12 12:43||lpw25||New Issue|
|Copyright © 2000 - 2011 MantisBT Group|