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

Fix MPR#7818 by removing aliases in functor argument types #2051

Merged
merged 6 commits into from Sep 20, 2018

Conversation

Projects
None yet
5 participants
@garrigue
Copy link
Contributor

commented Sep 18, 2018

This is an alternative fix to MPR#7818, which uncovered some situations where a non-aliasable module (coming from a functor argument) can be aliased in the return type of a functor.

The first approach in #1898 was to prohibit those types, but this seems to break lots of code at Jane Street.
Here is a milder approach, by remove aliases in the types of arguments, through a reuse of the approach for module type of.

Not 100% compatible, due to the same module type of, but this should break less stuff hopefully.

It doesn't try to be 100% safe, since this is a stop-gap (i.e. there are probably ways to put an alias in a place where it will not be removed, but this is going to be much more verbose).

| mty ->
mty
let rec remove_aliases_mty env r excl mty =
let r' = ref false in

This comment has been minimized.

Copy link
@Drup

Drup Sep 18, 2018

Contributor

Is that just an optim to try to preserve sharing ? If yes ... can we use a more understandable name, like was_expanded ?

@lpw25

This comment has been minimized.

Copy link
Contributor

commented Sep 18, 2018

This looks more promising that the approach in the other PR. I'll give it a go on our code base.

@lpw25

This comment has been minimized.

Copy link
Contributor

commented Sep 18, 2018

This is definitely an improvement, but it still produces a couple of tricky errors. Both of these errors is caused by an alias in the functor argument type to something outside of the argument. What about something half-way between this PR and the last one -- so only inner module aliases are removed? It looks like that would catch the cases we're worried about and be able to compile our entire code base without any errors.

@lpw25

This comment has been minimized.

Copy link
Contributor

commented Sep 18, 2018

(Sorry to keep nitpicking on this. Normally I'm happy to just fix backward compatibility problems in our code base -- but the errors here are genuinely hard to diagnose and fix. I can fix the ones we have now, but if anyone else creates a similar situation they are going to have a really hard time working out what's going on, so I'd like to avoid that if possible. If we can get to the point where there are no cases in our 8 million lines of code then I think the chances are pretty good that no-one will come up against this)

@garrigue

This comment has been minimized.

Copy link
Contributor Author

commented Sep 18, 2018

I'm trying to do that, but then I have a regression on PR#6307, since we end up keeping too many aliases...
I suppose that I need to refine the behavior. Not clean at all.

@garrigue

This comment has been minimized.

Copy link
Contributor Author

commented Sep 18, 2018

OK, the new version is more conservative, and keeps aliases to outside modules, but only in functor arguments (not with [@remove_aliases]). It still should be sufficient to avoid the unsoundness.

@garrigue

This comment has been minimized.

Copy link
Contributor Author

commented Sep 18, 2018

I had a hard time recalling what collect_arg_paths was about, but now I can see it shouldn't apply in the Functor case: it avoids the expansions of aliases that are used as functor arguments, but here it could be unsound. I think it's fine, but it's worth testing, If it doesn't work, I can revert to the previous commit, which is still an improvement.

@garrigue

This comment has been minimized.

Copy link
Contributor Author

commented Sep 19, 2018

To clarify: commit 81a760e expands all internal alias definitions, whether they are used as functor arguments inside the signature or not. Of course this can break code, but then it can break too if not used inside the signature, so I believe this should not have a big impact, and it's clearly safer.
In some hard to create cases, this may leave us with an unusable signature, or even a contradictory one, so there could be strange error messages, but I don't think this can be used to break soundness.
If you find some case triggering such an error message, I'm willing either to provide a proper error message, or at worse revert to commit 94bb40c.

BTW, the AppVeyor failure seems unrelated.

@garrigue

This comment has been minimized.

Copy link
Contributor Author

commented Sep 20, 2018

I did a small cleanup, using a separate function for Mtype.scrape_for_functor_arg.
The behavior for Mtype.scrape_for_type_of is now that of 4.07.
If this works on the Jane Street, then I think it is ready for merging.

@garrigue

This comment has been minimized.

Copy link
Contributor Author

commented Sep 20, 2018

Not everything is rosy though.
I could write an example showing that losing aliases in this way can break abstraction, i.e. for instance allow to equate types of sets using different orders.
However, I have a strong suspicion that you can also do that with Mtype.nondep_supertype too, so this is probably something that should have a separate solution (i.e., check that types are well formed when we lose equations, and there are other places where this happens).
Fortunately, this is not the kind of things that happens by chance: you have to repeatedly use module type of, recursive modules, and with constraints to do that.
There is still the concern of what happens if you lose equations between concrete types; if you can then instantiate with types with different concrete representations, then you would break soundness. I've not yet found an example of that.

@garrigue

This comment has been minimized.

Copy link
Contributor Author

commented Sep 20, 2018

Actually, it is possible to break soundness using plain applicative functors and GADTs, using the same idea.
So the problem is not specific to this PR, but seems rather related to the fact module type of returning a non-strengthened type, it becomes possible to instantiate it in a dangerous way.
We should have a generic check for wellformedness somewhere.
I submitted MPR#7851
Here is the example, unrelated to this PR.

type (_,_) eq = Eq : ('a,'a) eq
module F(X : Set.OrderedType) = struct
  type x = Set.Make(X).t and y = Set.Make(X).t
  type t = E of (x,x) eq
  type u = t = E of (x,y) eq
end;;
module M = F(struct type t let compare = compare end);;
module type S = module type of M;;
module rec M1 : S with type x = int and type y = bool = M1;;
let (E eq : M1.u) = (E Eq : M1.t);;
let cast : type a b. (a,b) eq -> a -> b = fun Eq x -> x;;
cast eq 3;;
- : M1.y = <unknown constructor>
@garrigue

This comment has been minimized.

Copy link
Contributor Author

commented Sep 20, 2018

@lpw25 Still grateful if you could test this PR at Jane Street. It solves a problem that could bite somebody by inadvertance. Basically, it's as simple as:

module type S = sig module Id : sig end module T = Id end
module F(X : S) = struct module Id = X.T end
module M = F(struct module Id = struct let x = 3 end module T = Id end)

which one could end up writing when trying to work around the module alias restriction, not understanding that the internal representation is wrong.

@lpw25

This comment has been minimized.

Copy link
Contributor

commented Sep 20, 2018

I tested the version before your cleanup commit overnight. There was one error, but it was pretty easy to debug, so I think this approach is good for 4.07.1. I'll give the code itself a review this afternoon.

@lpw25

lpw25 approved these changes Sep 20, 2018

Copy link
Contributor

left a comment

Ok. Code looks good to me.

@garrigue garrigue merged commit 457dcc5 into ocaml:4.07 Sep 20, 2018

0 of 2 checks passed

continuous-integration/appveyor/pr Waiting for AppVeyor build to complete
Details
continuous-integration/travis-ci/pr The Travis CI build is in progress
Details
@damiendoligez

This comment has been minimized.

Copy link
Member

commented Sep 24, 2018

FTR, AFAICT, this PR breaks aync-kernel.v0.11.1 (I guess this is the error that @lpw25 mentioned) and zipperposition.1.5 (cc @c-cube), and no other OPAM package.

See https://damiendoligez.github.io/opamcheck-results/2018-09-18/index.html for details. There are other failures, but I think they are all noise, mostly due to buggy dependencies in OPAM package definitions.

@c-cube

This comment has been minimized.

Copy link
Contributor

commented Sep 24, 2018

Hum, what am I supposed to do? Do you have the failing output? Zipperposition contains a lot of module type of but they're usually pretty tame since I'm not fond of complicated module abstractions…

damiendoligez added a commit to damiendoligez/ocaml that referenced this pull request Nov 5, 2018

@damiendoligez

This comment has been minimized.

Copy link
Member

commented Nov 23, 2018

I'm not sure why but this is not triggered by 4.07.1, so the problem fixed itself magically.

If you're still interested in the details:

The OPAM log is here: https://damiendoligez.github.io/opamcheck-results/2018-09-18/data/zipperposition.1.5-st_952c9cf85bb9927c5f38c4d3033f2698.txt
and the error message is buried in the middle of it. Here's a copy:

- File "src/prover_calculi/avatar.mli", line 29, characters 4-56:
- Error: In this `with' constraint, the new definition of Solver
-        does not match its original definition in the constrained signature:
-        ...
-        In module Lit:
-        Modules do not match:
-          sig
-            type t = Libzipperposition.BBox.Lit.t
-            type payload = Libzipperposition.BBox.payload
-            val compare : t -> t -> int
-            val equal : t -> t -> bool
-            val hash : t -> int
-            val dummy : t
-            val neg : t -> t
-            val sign : t -> bool
-            val abs : t -> t
-            val norm : t -> t * bool
-            val set_sign : bool -> t -> t
-            val apply_sign : bool -> t -> t
-            val make : payload -> t
-            val payload : t -> payload
-            val to_int : t -> int
-            val fresh_id : unit -> int
-            val pp : t CCFormat.printer
-            module Set = Lit.Set
-            module Tbl = Lit.Tbl
-          end
-        is not included in
-          (module Libzipperposition.BBox.Lit)
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.