Anonymous | Login | Signup for a new account 2018-06-18 08:14 CEST
 Main | My View | View Issues | Change Log | Roadmap

View Issue Details  Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007520OCamltypingpublic2017-04-21 14:552017-09-30 11:08
Reporterlpw25
Assigned To
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen
PlatformOSOS Version
Product Version4.04.0
Target VersionlaterFixed 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 lpw25 (developer) 2017-04-21 15:10 This seems to be a regression between 4.03.0 and 4.04.0. garrigue (manager) 2017-09-13 03:20 OK, the situation is rather complicated. The problem here is that, when checking inhabitedness, the type annotation on _ is no longer available. It disappears when we move from parse tree to typed tree and back. The type of the whole pattern is available, and correctly pushed in, but when checking inhabitedness, unification ignores the "second true" in Reither (the one that force the unification of the argument) for soundness reasons. So in the end, the type "empty" is not propagated to the wild card argument to `Foo, no splitting is done. The natural fix here would be to reconstruct the type annotation to the wild card, which is available in the typed tree but discarded in the translation (it cannot occur for generated patterns). But this requires writing a new translation to parsetree types. It might be possible to use Untypeast.typ, but I'm concerned that the scoping might be wrong... or is it really ok? By the way, the behavior when adding an extra refutation is strange. The type inferred seems wrong anyway. garrigue (manager) 2017-09-13 03:26 Actually, I understand what's happening in the last case: pressure_variants is called with all the cases (including the refutations), and assumes that this is an open variant type, which later by unification makes it a fixed one. Not sure what the correct behavior should be. Probably remove all the refutation cases when calling pressure_variants. BTW, in what kind of code does this pattern arise? garrigue (manager) 2017-09-13 04:18 Tentative fix at https://github.com/ocaml/ocaml/pull/1328, [^] using Untypeast. Note that I didn't fix the second problem (with an extra refutation case), because removing refutation cases breaks the logic of pressure_variants. It seems better to assume that adding an extra refutation cases implies a real intent wrt. the inferred type. xleroy (administrator) 2017-09-30 11:08 Tentative fix didn't work. Pushing this for after 4.06.

 Issue History Date Modified Username Field Change 2017-04-21 14:55 lpw25 New Issue 2017-04-21 15:10 lpw25 Note Added: 0017751 2017-09-13 03:20 garrigue Note Added: 0018245 2017-09-13 03:26 garrigue Note Added: 0018246 2017-09-13 04:18 garrigue Note Added: 0018247 2017-09-30 11:08 xleroy Note Added: 0018416 2017-09-30 11:08 xleroy Status new => acknowledged 2017-09-30 11:08 xleroy Target Version => later