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

Seemingly unrelated and spurious error (unaliasable module) with value shadowing #7818

Closed
vicuna opened this Issue Jul 10, 2018 · 10 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

commented Jul 10, 2018

Original bug ID: 7818
Reporter: mandrykin
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2018-09-21T06:19:36Z)
Resolution: fixed
Priority: high
Severity: crash
Platform: x86_64 SMP
OS: Linux 4.4.0
OS Version: Ubuntu 16.04.4
Version: 4.06.1
Target version: 4.07.1+dev/rc1
Fixed in version: 4.07.1+dev/rc1
Category: typing
Monitored by: @nojb @Drup

Bug description

module Termsig = struct

module Term0 = struct
  module type S = sig
    module Id : sig end
  end
end
module Term = struct
  module type S = sig
    module Term0 : Term0.S
    module T = Term0
  end
end

end;;

module Make (T' : Termsig.Term.S) = struct

module T = struct
  include T'.T
  let u = 1
  let u = 1
end

end;;

Gives:
Error: Signature mismatch:
Modules do not match:
sig
module Id = T'.Term0.Id
module Id2 = Id
val u : int
val u : int
end
is not included in
sig module Id = T'.Term0.Id module Id2 = Id val u : int end
In module Id:
Module T'.Term0.Id cannot be aliased

While after removing the rebinding of u:

module Make (T' : Termsig.Term.S) = struct

module T = struct
  include T'.T
  let u = 1
end

end;;

is accepted as well as

module Make (T' : Termsig.Term.S) = struct

module T = struct
  include T'.T
  module Id2 = Id
  let u = 1
end

end;;

(so the module aliasing seems not to be related).

The real cause of the error is too confusing to me to try to explain it more clearly in the summary.

File attachments

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Jul 10, 2018

Comment author: mandrykin

Added another shorter reproduction case with another inconsistency: while the first functor is accepted, it's not possible to specify its (the same) output signature explicitly.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Jul 10, 2018

Comment author: @lpw25

This is a symptom of a bug that I already knew about but never got around to fixing (or reporting). Basically, the check that is supposed to stop you making aliases to functor parameters is very broken. IIRC there are at least 3 ways to work around it -- and you have stumbled onto one of them here.

I hadn't realised this could cause actual problems, but it seems that it can cause module inclusion checks to fail as in this case (although there is no explicit coercion the presence of repeated values causes an inclusion check between the module type with two us and the module type with one u).

I was already planning to try and remove the restriction on aliases to functor parameters for 4.08, which would fix this bug as a side-effect.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Jul 10, 2018

Comment author: mandrykin

So would you recommend currently to better avoid those aliases (to functor arguments) even when they are accepted e.g. by using

(* ... module Id : sig type t end ... *)

module Make3 (T' : Termsig.Term.S) = struct
module T = struct
include (T'.T : Termsig.Term0.S with module Id = T'.T.Id)
module Id2 = Id
let u = 1
let u = 1
end
end;; (* OK *)

(so that there are just type equalities instead of module aliases)? Module aliases are inferred by default even if the resulting signature doesn't contain them, so e.g.

module Make3 (T' : Termsig.Term.S) : sig end = struct
module T = struct
include T'.T
module Id2 = Id
let u = 1
let u = 1
end
end;;

also fails, but they can be avoided if prevented earlier (upon include).

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Jul 10, 2018

Comment author: @lpw25

Yeah, that's probably your best bet for now.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Jul 11, 2018

Comment author: @garrigue

Wouldn't it be reasonable to fix this bug (i.e. correctly detect non-aliasable modules)?
In this case, it looks like one should fix the ~aliasable argument to strengthen in env.ml, to reflect whether the path is alienable or not.
Even if you allow aliasing them at a later time, this cannot be a physical aliasing, so the distinction will still be relevant, isn't it?

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Jul 11, 2018

Comment author: @garrigue

Actually this doesn't seem to be the one. There are many calls to strengthen...

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Jul 11, 2018

Comment author: @garrigue

By the way, this is clearly a soundness bug. Using cannot_alias2.ml, we have:

module M = Make1 (struct module Term0 = struct module Id = struct let x = "a" end end module T = Term0 end);;

module M : sig module Id : sig val x : string end module Id2 = Id end

M.Id.x;;

Segmentation fault

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Jul 12, 2018

Comment author: @garrigue

I have opened #1898
It proposes a way to fix this problem, by checking the signature of functor argument types.
This is an incompatible change, prohibiting all the functors you proposed, but since this is a soundness bug, I prefer being on the safe side.

Leo, if you know other ways to break Env.is_functor_arg, please speak up because this is a bad problem.

Comment: I thought originally that Env.is_functor_arg was safe, because all accesses to the contents of the argument should use a path which starts from it. Unfortunately, copying components of a submodule of the argument seem to lose this connection, allowing to use aliases coming from inside the argument. Properly tracking this seems complex, hence this somehow radical approach.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Sep 18, 2018

Comment author: @garrigue

New alternative approach in #2051
The previous PR did break a lot of code, this one should be less intrusive.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Sep 21, 2018

Comment author: @garrigue

Solved in 4.07.1 and trunk by #2051, commits 457dcc5 and e8bb50e+f4274ed89.
All the examples of the original report are now accepted (but with a different type), and the related unsoundness is fixed. However another unsoundness has been found in the process :-(

@vicuna vicuna closed this Sep 21, 2018

@vicuna vicuna added this to the 4.07.1 milestone Mar 14, 2019

@vicuna vicuna added the bug label Mar 20, 2019

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.