Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007707OCamltypingpublic2018-01-12 12:432018-01-12 12:43
Assigned To 
PlatformOSOS Version
Product Version4.06.0 
Target VersionFixed in Version 
Summary0007707: mcomp on polymorphic variants is a little weak
DescriptionThe [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


  '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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2018-01-12 12:43 lpw25 New Issue

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker