Odd behaviour of refutation cases with polymorphic variants #7520
Description
Original bug ID: 7520
Reporter: @lpw25
Status: acknowledged (set by @xavierleroy on 2017-09-30T09:08:45Z)
Resolution: open
Priority: normal
Severity: minor
Version: 4.04.0
Target version: later
Category: typing
Monitored by: @gasche @yallop
Bug description
Refutation cases have some odd behaviour with polymorphic variants. Given an uninhabited type:
type ('a, 'b) eq = Refl : ('a, 'a) eq
type empty = (int, string) eqThe 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>