Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007520OCamltypingpublic2017-04-21 14:552017-04-21 15:10
Reporterlpw25 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusnewResolutionopen 
PlatformOSOS Version
Product Version4.04.0 
Target VersionFixed in Version 
Summary0007520: Odd behaviour of refutation cases with polymorphic variants
DescriptionRefutation cases have some odd behaviour with polymorphic variants. Given an uninhabited type:

  type ('a, 'b) eq = Refl : ('a, 'a) eq
  type empty = (int, string) eq

The following fails:

  # let f = function `Foo (_ : empty) -> .;;
  Characters 17-33:
    let f = function `Foo (_ : empty) -> .;;
                     ^^^^^^^^^^^^^^^^
  Error: This match case could not be refuted.
         Here is an example of a value that would reach it: `Foo _

It continues to fail if the variant type is constrained:

  # let f : [< `Foo of empty] -> int = function `Foo (_ : empty) -> .;;
  Characters 44-60:
    let f : [< `Foo of empty] -> int = function `Foo (_ : empty) -> .;;
                                                ^^^^^^^^^^^^^^^^
  Error: This match case could not be refuted.
         Here is an example of a value that would reach it: `Foo _

But it works of the type is fixed:

  # let f : [`Foo of empty] -> int = function `Foo (_ : empty) -> .;;
  val f : [ `Foo of empty ] -> int = <fun>

Or if we add a second empty refutation case:

  # let f : [< `Foo of empty] -> int = function `Foo _ -> . | _ -> .;;
  val f : [ `Foo of empty ] -> int = <fun>
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0017751)
lpw25 (developer)
2017-04-21 15:10

This seems to be a regression between 4.03.0 and 4.04.0.

- Issue History
Date Modified Username Field Change
2017-04-21 14:55 lpw25 New Issue
2017-04-21 15:10 lpw25 Note Added: 0017751


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker