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

Closed
vicuna opened this issue Feb 16, 2018 · 8 comments
Closed

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

vicuna opened this issue Feb 16, 2018 · 8 comments

Comments

@vicuna
Copy link

vicuna 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
Copy link
Author

vicuna 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
Copy link
Author

vicuna 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
Copy link
Author

vicuna 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
Copy link
Author

vicuna 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
Copy link
Author

vicuna commented Feb 27, 2018

Comment author: @garrigue

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

@vicuna
Copy link
Author

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

@github-actions
Copy link

github-actions bot commented May 7, 2020

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.

@github-actions github-actions bot added the Stale label May 7, 2020
@yallop
Copy link
Member

yallop commented May 7, 2020

This has been fixed by @garrigue in #1676.

@yallop yallop closed this as completed May 7, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

4 participants