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

Soundness issue with class generalization #8550

Closed
yallop opened this issue Mar 27, 2019 · 3 comments

Comments

Projects
None yet
2 participants
@yallop
Copy link
Member

commented Mar 27, 2019

There's a soundness issue with generalization of type variables in class definitions:

    # class ['a] r = let r : 'a = ref [] in object method get = r end;;
    class ['a] r : object constraint 'a = 'b list ref method get : 'a end
    # (new r)#get := [3];;
    - : unit = ()
    # List.hd !((new r)#get) ^ "two";;
    Segmentation fault

Bisecting shows that this has been around for a while: it was introduced in OCaml 4.00.0 along with GADTs (6c78f42) for programs checked with -principal and more recently spread to programs without -principal, too (8029450). Before these commits the program was rejected:

    Characters 0-63:
      class ['a] r = let r : 'a = ref [] in object method get = r end;;
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    Error: The type of this class,
           class ['a] r : object constraint 'a = '_b list ref method get : 'a end,
           contains type variables that cannot be generalized
@yallop

This comment has been minimized.

Copy link
Member Author

commented Mar 27, 2019

@garrigue, you may like to take a look at this.

@garrigue

This comment has been minimized.

Copy link
Contributor

commented Mar 28, 2019

I see. This code is utterly wrong: variables are only lowered if they are first reached through a contra variant branch! I don't know what I was drinking on that day.

@garrigue

This comment has been minimized.

Copy link
Contributor

commented Mar 28, 2019

Actually the original code was not as absurd as I first thought, but partial generalization was probably a bad idea anyway. See #8552 for a proper solution.

@garrigue garrigue self-assigned this Mar 28, 2019

garrigue added a commit that referenced this issue Apr 9, 2019

Fix #8550: Soundness issue with class generalization (#8552)
* also rename generalize_expansive -> lower_contravariant

garrigue added a commit that referenced this issue Apr 9, 2019

Fix #8550: Soundness issue with class generalization (#8552)
* also rename generalize_expansive -> lower_contravariant
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.