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

PR#7511: Unboxed type with unboxed argument should not be accepted #1133

Merged
merged 3 commits into from Jun 20, 2017

Conversation

Projects
None yet
5 participants
@damiendoligez
Member

damiendoligez commented Apr 3, 2017

See MPR#7511 and the original implementation/discussion in GPR#606.

@garrigue, could you please review?

@damiendoligez damiendoligez added this to the 4.04.1 milestone Apr 3, 2017

@damiendoligez damiendoligez requested a review from garrigue Apr 3, 2017

@yallop

@damiendoligez, here's a slight variation of the example program that's not yet detected by this PR

type 'a s = S : 'a -> 'a option s [@@unboxed]
type t = T : _ s -> t [@@unboxed]
let _ = [| T (S 0.0); T (S 0) |]
@damiendoligez

This comment has been minimized.

Show comment
Hide comment
@damiendoligez

damiendoligez Apr 10, 2017

Member

This won't be fixed properly for 4.04.1. I've switched it to the 4.05 branch.

Member

damiendoligez commented Apr 10, 2017

This won't be fixed properly for 4.04.1. I've switched it to the 4.05 branch.

@damiendoligez damiendoligez modified the milestones: 4.05.0, 4.04.1 Apr 10, 2017

@damiendoligez damiendoligez changed the base branch from 4.04 to 4.05 Apr 10, 2017

@damiendoligez

This comment has been minimized.

Show comment
Hide comment
@damiendoligez

damiendoligez May 22, 2017

Member

@yallop, @garrigue, here is a version that is maybe a bit restrictive, but I believe sound.

Instead of checking that the representation is not an existential variable of the GADT, we now check that, if it is a type variable, it is one of the universal variables of the GADT.

Member

damiendoligez commented May 22, 2017

@yallop, @garrigue, here is a version that is maybe a bit restrictive, but I believe sound.

Instead of checking that the representation is not an existential variable of the GADT, we now check that, if it is a type variable, it is one of the universal variables of the GADT.

@lpw25

This comment has been minimized.

Show comment
Hide comment
@lpw25

lpw25 May 22, 2017

Contributor

I think you need to check parameters of abstract types more strictly than you check the GADT argument because you cannot ignore type variables underneath object types in parameters of abstract types.

For example, I think your check would not catch the following case:

module M : sig
    type 'a r constraint 'a = < foo : 'b >
    val inj : 'a -> < foo : 'a > r
  end = struct
    type 'a r = 'b constraint 'a = < foo : 'b >;;
    let inj x = x
  end

type 'a s = S : < foo : 'a> M.r -> 'a s [@@unboxed]

type t = T : _ s -> t [@@unboxed]

let _ = [| T (S (M.inj 0.0)); T (S (M.inj 0)) |]

This might be related to the contractiveness check for recursive types.

Contributor

lpw25 commented May 22, 2017

I think you need to check parameters of abstract types more strictly than you check the GADT argument because you cannot ignore type variables underneath object types in parameters of abstract types.

For example, I think your check would not catch the following case:

module M : sig
    type 'a r constraint 'a = < foo : 'b >
    val inj : 'a -> < foo : 'a > r
  end = struct
    type 'a r = 'b constraint 'a = < foo : 'b >;;
    let inj x = x
  end

type 'a s = S : < foo : 'a> M.r -> 'a s [@@unboxed]

type t = T : _ s -> t [@@unboxed]

let _ = [| T (S (M.inj 0.0)); T (S (M.inj 0)) |]

This might be related to the contractiveness check for recursive types.

@damiendoligez

This comment has been minimized.

Show comment
Hide comment
@damiendoligez

damiendoligez May 24, 2017

Member

@lpw25 in fact this is not specific to object types:

module M : sig
  type 'a r constraint 'a = unit -> 'b
  val inj : 'b -> (unit -> 'b) r
end = struct
  type 'a r = 'b constraint 'a = unit -> 'b
  let inj x = x
end

type t = T : (unit -> _) M.r -> t [@@unboxed]

;; [| T (M.inj 0.0); T (M.inj 0) |]
Member

damiendoligez commented May 24, 2017

@lpw25 in fact this is not specific to object types:

module M : sig
  type 'a r constraint 'a = unit -> 'b
  val inj : 'b -> (unit -> 'b) r
end = struct
  type 'a r = 'b constraint 'a = unit -> 'b
  let inj x = x
end

type t = T : (unit -> _) M.r -> t [@@unboxed]

;; [| T (M.inj 0.0); T (M.inj 0) |]
@damiendoligez

This comment has been minimized.

Show comment
Hide comment
@damiendoligez

damiendoligez May 24, 2017

Member

OK, I implemented the strict check for abstract types suggested by @lpw25.

Are there any more problems?

Member

damiendoligez commented May 24, 2017

OK, I implemented the strict check for abstract types suggested by @lpw25.

Are there any more problems?

@gasche

This comment has been minimized.

Show comment
Hide comment
@gasche

gasche May 29, 2017

Member

@lpw25 @yallop: If I understand correctly, this is the only major issue blocking the 4.05 release, so any concluding feedback would be much appreciated ;-)

Member

gasche commented May 29, 2017

@lpw25 @yallop: If I understand correctly, this is the only major issue blocking the 4.05 release, so any concluding feedback would be much appreciated ;-)

@yallop

This comment has been minimized.

Show comment
Hide comment
@yallop

yallop May 30, 2017

Member

The approach seems good to me, but I ran into a implementation problem when trying some things out. The following example

type _ s = S : 'a t -> _ s  [@@unboxed]
 and _ t = T : 'a -> 'a s t

leads to an assertion error:

Fatal error: exception File "typing/typedecl.ml", line 309, characters 16-22: Assertion failed
Member

yallop commented May 30, 2017

The approach seems good to me, but I ran into a implementation problem when trying some things out. The following example

type _ s = S : 'a t -> _ s  [@@unboxed]
 and _ t = T : 'a -> 'a s t

leads to an assertion error:

Fatal error: exception File "typing/typedecl.ml", line 309, characters 16-22: Assertion failed
@damiendoligez

This comment has been minimized.

Show comment
Hide comment
@damiendoligez

damiendoligez Jun 2, 2017

Member

@yallop fixed the problem

@garrigue I would really appreciate a review...

Member

damiendoligez commented Jun 2, 2017

@yallop fixed the problem

@garrigue I would really appreciate a review...

@garrigue

This comment has been minimized.

Show comment
Hide comment
@garrigue

garrigue Jun 5, 2017

Contributor

Actually, I was not involved in the discussion, and I have very little understanding of what the [@@unboxed] attribute does.
What is exactly the invariant you are trying to enforce?

Contributor

garrigue commented Jun 5, 2017

Actually, I was not involved in the discussion, and I have very little understanding of what the [@@unboxed] attribute does.
What is exactly the invariant you are trying to enforce?

@damiendoligez

This comment has been minimized.

Show comment
Hide comment
@damiendoligez

damiendoligez Jun 9, 2017

Member

The [@@unboxed] attribute changes the (run-time) representation of a type by removing one level of boxing.
The canonical example would be:

type t = A of int [@@unboxed]

instead of using the uniform representation for t (a block with tag 0 and one field that contains the int) we simply use the int itself to represent a value of type t.

Of course, this is not possible for arbitrary types: the type must have only one constructor with one field: either a concrete type with one constructor of one argument, or a record type with one field.

The trouble is with existential types and the float array hack: if the type of the field is existential, it becomes possible to mix floats and non-floats in the same type, which breaks the assumptions of ad-hoc polymorphic array primitives.

The invariant I am trying to enforce is the following: all values of the (field's) type are in one of the following categories:

  • float
  • non-float (int or pointer)
  • a single universal type variable

In the third case, we rely on the invariant itself to make sure that instances of the type will not mix floats and non-floats.

Member

damiendoligez commented Jun 9, 2017

The [@@unboxed] attribute changes the (run-time) representation of a type by removing one level of boxing.
The canonical example would be:

type t = A of int [@@unboxed]

instead of using the uniform representation for t (a block with tag 0 and one field that contains the int) we simply use the int itself to represent a value of type t.

Of course, this is not possible for arbitrary types: the type must have only one constructor with one field: either a concrete type with one constructor of one argument, or a record type with one field.

The trouble is with existential types and the float array hack: if the type of the field is existential, it becomes possible to mix floats and non-floats in the same type, which breaks the assumptions of ad-hoc polymorphic array primitives.

The invariant I am trying to enforce is the following: all values of the (field's) type are in one of the following categories:

  • float
  • non-float (int or pointer)
  • a single universal type variable

In the third case, we rely on the invariant itself to make sure that instances of the type will not mix floats and non-floats.

@gasche

This comment has been minimized.

Show comment
Hide comment
@gasche

gasche Jun 9, 2017

Member

The third case seems overly restrictive to me (so maybe I haven't understood things well enough); for example why would

 type 'a t (* abstract *)
 type 'a unboxed = Erased of 'a t [@@unboxed]

be incorrect?

Intuitively I would expect the following classification:

  • the argument is known to be all-float or non-float
  • or it does not use existential variables: if the constructor is named T, the function fun (T x) -> x is well-typed. (If I understand correctly, this is weaker than your restriction.)
Member

gasche commented Jun 9, 2017

The third case seems overly restrictive to me (so maybe I haven't understood things well enough); for example why would

 type 'a t (* abstract *)
 type 'a unboxed = Erased of 'a t [@@unboxed]

be incorrect?

Intuitively I would expect the following classification:

  • the argument is known to be all-float or non-float
  • or it does not use existential variables: if the constructor is named T, the function fun (T x) -> x is well-typed. (If I understand correctly, this is weaker than your restriction.)
@damiendoligez

This comment has been minimized.

Show comment
Hide comment
@damiendoligez

damiendoligez Jun 13, 2017

Member

I was probably not very clear, but your example is accepted because the representation of 'a t is either 'a or some regular (all-float or non-float) type.

Your "does not use existential variables" criterion is probably too restrictive:

type unboxed = Erased : _ option -> unboxed [@@unboxed];;

is accepted by the current proposal: the option type is already boxing the existential, so we can avoid a second level of boxing.

Member

damiendoligez commented Jun 13, 2017

I was probably not very clear, but your example is accepted because the representation of 'a t is either 'a or some regular (all-float or non-float) type.

Your "does not use existential variables" criterion is probably too restrictive:

type unboxed = Erased : _ option -> unboxed [@@unboxed];;

is accepted by the current proposal: the option type is already boxing the existential, so we can avoid a second level of boxing.

@gasche

This comment has been minimized.

Show comment
Hide comment
@gasche

gasche Jun 13, 2017

Member

My idea was that the two criterion above are "either or": _ option is never-a-float, so it passes the first test and is accepted.

Member

gasche commented Jun 13, 2017

My idea was that the two criterion above are "either or": _ option is never-a-float, so it passes the first test and is accepted.

@damiendoligez

This comment has been minimized.

Show comment
Hide comment
@damiendoligez

damiendoligez Jun 13, 2017

Member

It's not obvious how to define "uses an existential variable", and even less obvious to implement it, so I've implemented something more restrictive. See Jeremy's example at the top of the discussion: the existential variable is unified with 'a option and the resulting 'a is the field's type. This means that the field's type is not an existential introduced by the GADT, it's introduced by unification. A kind of derived existential variable if you want. Unification can also introduce derived universal variables and I'm not enough of a typechecker expert to tell the difference, so I just forbid them all and allow only variables that are both universal and directly introduced by the type declaration.

Maybe someday we'll have a finer criterion, but the most important now is to have something sound.

Member

damiendoligez commented Jun 13, 2017

It's not obvious how to define "uses an existential variable", and even less obvious to implement it, so I've implemented something more restrictive. See Jeremy's example at the top of the discussion: the existential variable is unified with 'a option and the resulting 'a is the field's type. This means that the field's type is not an existential introduced by the GADT, it's introduced by unification. A kind of derived existential variable if you want. Unification can also introduce derived universal variables and I'm not enough of a typechecker expert to tell the difference, so I just forbid them all and allow only variables that are both universal and directly introduced by the type declaration.

Maybe someday we'll have a finer criterion, but the most important now is to have something sound.

@yallop

yallop approved these changes Jun 15, 2017

@yallop

This comment has been minimized.

Show comment
Hide comment
@yallop

yallop Jun 15, 2017

Member

I've approved the changes, since the approach seems good to me, and it fixes the problem in the original report, but the PR might still benefit from a review by someone more familiar with that area of the code (e.g. @garrigue or @lpw25).

Member

yallop commented Jun 15, 2017

I've approved the changes, since the approach seems good to me, and it fixes the problem in the original report, but the PR might still benefit from a review by someone more familiar with that area of the code (e.g. @garrigue or @lpw25).

@damiendoligez damiendoligez merged commit b06e77f into ocaml:4.05 Jun 20, 2017

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details

@damiendoligez damiendoligez deleted the damiendoligez:m7511 branch Jun 20, 2017

@gasche

This comment has been minimized.

Show comment
Hide comment
@gasche

gasche Jul 12, 2017

Member

There is a Changes entry for this patch in the 4.04.1 category in the 4.05 branch. I believe that both the following are correct, @damiendoligez could you confirm?

  • the change was in 4.04.2 rather than 4.04.1 (the Changes entry is a bit wrong, but we can fix it only in trunk, we don't need to bother with the 4.05 branch as it touches an older release)
  • the change has not yet been merged into trunk (when do you plan to do this?)
Member

gasche commented Jul 12, 2017

There is a Changes entry for this patch in the 4.04.1 category in the 4.05 branch. I believe that both the following are correct, @damiendoligez could you confirm?

  • the change was in 4.04.2 rather than 4.04.1 (the Changes entry is a bit wrong, but we can fix it only in trunk, we don't need to bother with the 4.05 branch as it touches an older release)
  • the change has not yet been merged into trunk (when do you plan to do this?)
@damiendoligez

This comment has been minimized.

Show comment
Hide comment
@damiendoligez

damiendoligez Jul 13, 2017

Member

@gasche

  • No, this patch was never included in the 4.04 branch. The Changes entry is in the wrong place.
  • Yes I need to merge it into trunk. (today)
Member

damiendoligez commented Jul 13, 2017

@gasche

  • No, this patch was never included in the 4.04 branch. The Changes entry is in the wrong place.
  • Yes I need to merge it into trunk. (today)

damiendoligez added a commit that referenced this pull request Jul 13, 2017

@damiendoligez

This comment has been minimized.

Show comment
Hide comment
@damiendoligez

damiendoligez Jul 13, 2017

Member

Cherry-picked to trunk (ac4f3e6)

Member

damiendoligez commented Jul 13, 2017

Cherry-picked to trunk (ac4f3e6)

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