Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007520OCamltypingpublic2017-04-21 14:552017-09-30 11:08
Assigned To 
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, [^] 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

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker