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

nondep_type_decl: expand to private abbrev instead of abstracting #1826

Merged
merged 7 commits into from Jun 14, 2018

Conversation

Projects
None yet
2 participants
@trefis
Copy link
Contributor

commented Jun 8, 2018

Given:

# module F(_ : sig end) = struct type t = private int end
  module G(X : sig end) : sig type t = F(X).t end = F(X);;
module F : sig  end -> sig type t = private int end
module G : functor (X : sig  end) -> sig type t = F(X).t end

Before this PR:

# module M = G(struct end);;
module M : sig type t end

After:

# module M = G(struct end);;
module M : sig type t = private int end
[%%expect{|
module IndirectPriv : sig type t = private [ `Foo of 'a ] as 'a end
|}]

This comment has been minimized.

Copy link
@garrigue

garrigue Jun 11, 2018

Contributor

The code looks fine, but I'm concerned by IndirectPriv.
What would happen if the original type definition in Priv were

type t = private [`Foo of t -> int | `Bar of int]

Private abbreviations can be soundly expanded by subtyping, but only in covariant positions.

This comment has been minimized.

Copy link
@garrigue

garrigue Jun 11, 2018

Contributor

I think that you need to track variance in nondep_type_rec, and only call expand_abbrev_opt at covariant positions.

This comment has been minimized.

Copy link
@trefis

trefis Jun 11, 2018

Author Contributor

Good catch. I do check is_covariant before calling nondep_type_rec with ~expand_private:true, but I am indeed recursing without being careful about this.

I'll push a fix.

@garrigue

This comment has been minimized.

Copy link
Contributor

commented Jun 11, 2018

Thinking more, I'm not even 100% sure that this is sound when restricted to covariant positions.
It certainly looks OK, but I would like to see a formal argument.

@trefis

This comment has been minimized.

Copy link
Contributor Author

commented Jun 11, 2018

I pushed a fix for the issue you pointed to above.

As for restricting to covariant positions: the restriction which is now implemented is stronger than this: we call expand_abbrev_opt only at the toplevel, not when recursing.
Doing so we match what the user can already do manually in other parts of the system, e.g. below s is in a covariant position, but the user is not allowed to use its expansion:

# type s = private int;;                                                           
type s = private int
# module M : sig type t = private int list end = struct type t = s list end;;
Characters 47-73:
  module M : sig type t = private int list end = struct type t = s list end;;
                                                 ^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Signature mismatch:
       Modules do not match:
         sig type t = s list end
       is not included in
         sig type t = private int list end
       Type declarations do not match:
         type t = s list
       is not included in
         type t = private int list
# module M : sig type t end = struct type t = s list end;;                   
module M : sig type t end
# 

Likewise:

# module F(_ : sig end) = struct type t = private int end;;
module F : sig  end -> sig type t = private int end
# module G(X : sig end) = struct type t = F(X).t list end;;
module G : functor (X : sig  end) -> sig type t = F(X).t list end
# module M = G(struct end);;
module M : sig type t end
# 
@trefis

This comment has been minimized.

Copy link
Contributor Author

commented Jun 11, 2018

And to be somewhat more explicit: we allow ourselves the expansion at the toplevel for nondep_type_rec, as it is already allowed here:

# type s = private int;;
type s = private int
# module M : sig type t = private int end = struct type t = s end;;
module M : sig type t = private int end

Which is similar to the example in my initial message:

# module F(_ : sig end) = struct type t = private int end
  module G(X : sig end) = F(X);;
module F : sig  end -> sig type t = private int end
module G : functor (X : sig  end) -> sig type t = F(X).t end
# module M = G(struct end);;
module M : sig type t = private int end
@garrigue

This comment has been minimized.

Copy link
Contributor

commented Jun 13, 2018

Indeed in Includecore.type_manifest we allow expanding ty1 with try_expand_opt when priv2 = Private.
So morally what you do looks correct.
However, one might be even more careful, and add an assertion checking the subtyping between the original module type and the result of Mtype.nondep_supertype. This would have caught the variance problem. The cost is not significant, so maybe it's time to be more defensive when possible (unfortunately this is not often the case...)

@trefis trefis force-pushed the trefis:nondep-private branch from 04a8e04 to b6e2ec9 Jun 13, 2018

@trefis

This comment has been minimized.

Copy link
Contributor Author

commented Jun 13, 2018

I added the check you suggested (in commit b5d4f87), it indeed would have caught the variance issue.

I also rebased and updated the changes entry; so it's ready to merge if you're happy with it.

@garrigue
Copy link
Contributor

left a comment

Now it's 100% safe.

@trefis trefis merged commit 9702af7 into ocaml:trunk Jun 14, 2018

2 checks passed

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

@trefis trefis deleted the trefis:nondep-private branch Jun 14, 2018

@trefis

This comment has been minimized.

Copy link
Contributor Author

commented Jun 14, 2018

Thank you!

@trefis trefis referenced this pull request Jul 9, 2018

Merged

Ctype.unroll_abbrev bug #1890

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.