Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Odd behaviour of refutation cases with polymorphic variants #7520

Closed
vicuna opened this issue Apr 21, 2017 · 11 comments · Fixed by #9547
Closed

Odd behaviour of refutation cases with polymorphic variants #7520

vicuna opened this issue Apr 21, 2017 · 11 comments · Fixed by #9547

Comments

@vicuna
Copy link

vicuna commented Apr 21, 2017

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) 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>
@vicuna
Copy link
Author

vicuna commented Apr 21, 2017

Comment author: @lpw25

This seems to be a regression between 4.03.0 and 4.04.0.

@vicuna
Copy link
Author

vicuna commented Sep 13, 2017

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Sep 13, 2017

Comment author: @garrigue

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?

@vicuna
Copy link
Author

vicuna commented Sep 13, 2017

Comment author: @garrigue

Tentative fix at #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.

@vicuna
Copy link
Author

vicuna commented Sep 30, 2017

Comment author: @xavierleroy

Tentative fix didn't work. Pushing this for after 4.06.

@github-actions
Copy link

github-actions bot commented May 8, 2020

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label May 8, 2020
@lpw25
Copy link
Contributor

lpw25 commented May 8, 2020

Is this issue made any easier to fix by the various changes to typing pattern matching?

Personally, I still think that the general approach of generating actual Parsetree fragments and re-typechecking them is a mistake that is destined to always cause issues like this one. Is there a particular reason that we don't have a separate data type to represent the candidate patterns (with things like type annotations and constructor identifiers already resolved) and a separate function for check that these candidate patterns are well typed?

@garrigue
Copy link
Contributor

garrigue commented May 9, 2020

For me this rather falls in the category: combination of GADT and polymorphic variant is unsupported.
And no, the changes to type_pat do not help, they have just made the code more complicated.

@garrigue
Copy link
Contributor

garrigue commented May 9, 2020

Looking back at #7269, which is the source of the passive_variants mode, it seems that always setting passive_variants changes nothing in the test suite. This probably related to the fact type checking of counter-examples is now more relaxed.

If I remove passive_variants, this solves this problem, so I'm tempted to do that. It was just a hack anyway.

@gasche
Copy link
Member

gasche commented May 9, 2020

And no, the changes to type_pat do not help, they have just made the code more complicated.

@garrigue
Copy link
Contributor

garrigue commented May 9, 2020

I should have add: for me.
Since I understood well the code from the beginning, all your "improvement" do not help me.
But I understand that they can help others.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants