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.

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.

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).

Comment author: @lpw25

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

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?

Comment author: @garrigue

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

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

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.

Comment author: @garrigue

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

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 :-(