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
Recursive modules, equi-recursive types and stack overflow #7726
Comments
Comment author: @garrigue The problem was already there in 3.07, and probably since the introduction of recursive modules. 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. BTW, I wonder if you can exhibit an unsoundness. At this point the worse I see is a stack overflow. |
Comment author: @garrigue Actually, Typedecl.check_recmod_typedecl already checks for recursive module ids in functor applications. |
Comment author: @garrigue I misunderstood: to_check indicates the paths for which recursion should be checked, not those requiring contractiveness. |
Comment author: @garrigue 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. |
Comment author: @garrigue The previous attempt failed because it only prevented substitutions coming from functor applications, while one can also substitute in signatures using with. Here is an example using a with constraint: module type T = sig type t end It immediately causes a stack overflow before the fix. |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
Original bug ID: 7726
Reporter: @yallop
Assigned to: @garrigue
Status: confirmed (set by @garrigue on 2018-02-27T08:59:23Z)
Resolution: open
Priority: normal
Severity: minor
Category: typing
Related to: #3935 #7611
Monitored by: @gasche
Bug 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)
end
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
The text was updated successfully, but these errors were encountered: