|Anonymous | Login | Signup for a new account||2018-10-22 09:15 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0007726||OCaml||typing||public||2018-02-16 17:23||2018-06-07 08:21|
|Priority||normal||Severity||minor||Reproducibility||have not tried|
|Target Version||Fixed in Version|
|Summary||0007726: Recursive modules, equi-recursive types and stack overflow|
|Description||Using recursive modules it's possible to build equi-recursive types, like this one|
type t = t option
even when -rectypes is not enabled:
module type T = sig type t end
module Fix(F:(T -> T)) = struct
module rec Fixed : T with type t = F(Fixed).t = F(Fixed)
module T = Fix(functor (X:sig type t end) -> struct type t = X.t option end)
(* T.Fixed.t = T.fixed.t option *)
Since the type recursion is not manifest, the checks associated with -rectypes don't kick in, and it's also possible to construct types that even -rectypes doesn't allow, such as
type t = t
as the following code does:
module T = Fix(functor (X:sig type t end) -> struct type t = X.t end)
leading to a compile-time error:
Fatal error: exception Stack overflow
|Tags||No tags attached.|
The problem was already there in 3.07, and probably since the introduction of recursive modules.
(Need to replace T -> T by struct module F : functor(X:T)->T end)
Supposedly check_recmod_typedecls should detect this, but it is only called on the recursive module in the body of Fix, which doesn't contain recursive definitions yet...
Producing recursive types is not too bad (GADT equations may already do that IIRC), but allowing type t = Fixed.t is a real problem.
A potential fix would be to require all definitions in a recursive module to be contractive when referring not only to itself, but also to a functor application taking a recursive module as argument. I wonder whether it would end up being too restrictive.
BTW, I wonder if you can exhibit an unsoundness. At this point the worse I see is a stack overflow.
Actually, Typedecl.check_recmod_typedecl already checks for recursive module ids in functor applications.
So I wonder what's going wrong here: it should already detect that F(Fixed).t might be Fixed.t itself.
I misunderstood: to_check indicates the paths for which recursion should be checked, not those requiring contractiveness.
So check_well_founded itself should be extended.
edited on: 2018-02-27 11:22
Thinking more of it, it seems that problematic paths (that could expand to any type from the recursive modules) are those containing both a recursive module and a "functor argument", i.e. some module that could be instanciated later. This might be specific enough not to get in the way.
There is a tentative fix at https://github.com/ocaml/ocaml/pull/1639 [^]
It is probably broken, but demonstrates the idea.
The previous attempt failed because it only prevented substitutions coming from functor applications, while one can also substitute in signatures using with.
There is a new attempt at https://github.com/ocaml/ocaml/pull/1676. [^]
Here is an example using a with constraint:
module type T = sig type t end
module type S =
module F : functor (X : T) -> T
module rec Fixed : sig type t = F(Fixed).t end
module Id (X : T) = X
module type Bad = S with module F = Id
It immediately causes a stack overflow before the fix.
|2018-02-16 17:23||yallop||New Issue|
|2018-02-27 09:59||garrigue||Note Added: 0018924|
|2018-02-27 09:59||garrigue||Assigned To||=> garrigue|
|2018-02-27 09:59||garrigue||Status||new => confirmed|
|2018-02-27 10:03||garrigue||Note Added: 0018925|
|2018-02-27 10:43||garrigue||Note Added: 0018926|
|2018-02-27 11:21||garrigue||Note Added: 0018928|
|2018-02-27 11:22||garrigue||Note Edited: 0018928||View Revisions|
|2018-02-27 14:41||garrigue||Note Added: 0018929|
|2018-03-23 04:45||garrigue||Note Added: 0018956|
|2018-06-01 15:51||garrigue||Relationship added||related to 0007611|
|2018-06-07 08:21||garrigue||Relationship added||related to 0003935|
|Copyright © 2000 - 2011 MantisBT Group|