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

Recursive modules, equi-recursive types and stack overflow #7726

Open
vicuna opened this issue Feb 16, 2018 · 6 comments

Comments

Projects
None yet
3 participants
@vicuna
Copy link

commented Feb 16, 2018

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

@vicuna

This comment has been minimized.

Copy link
Author

commented Feb 27, 2018

Comment author: @garrigue

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Feb 27, 2018

Comment author: @garrigue

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Feb 27, 2018

Comment author: @garrigue

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Feb 27, 2018

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.

@vicuna

This comment has been minimized.

Copy link
Author

commented Feb 27, 2018

Comment author: @garrigue

There is a tentative fix at #1639
It is probably broken, but demonstrates the idea.

@vicuna

This comment has been minimized.

Copy link
Author

commented Mar 23, 2018

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.
There is a new attempt at #1676.

Here is an example using a with constraint:

module type T = sig type t end
module type S =
sig
module F : functor (X : T) -> T
module rec Fixed : sig type t = F(Fixed).t end
end
module Id (X : T) = X
module type Bad = S with module F = Id

It immediately causes a stack overflow before the fix.

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.