Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007726OCamltypingpublic2018-02-16 17:232018-06-07 08:21
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityhave not tried
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0007726: Recursive modules, equi-recursive types and stack overflow
DescriptionUsing 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
TagsNo tags attached.
Attached Files

- Relationships
related to 0007611resolvedgarrigue Generative functors are allowed to be applicative ! 
related to 0003935acknowledged Structural types forming non-regular trees can be defined through recursive modules. 

-  Notes
garrigue (manager)
2018-02-27 09:59

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.
garrigue (manager)
2018-02-27 10:03

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.
garrigue (manager)
2018-02-27 10:43

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.
garrigue (manager)
2018-02-27 11:21
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.

garrigue (manager)
2018-02-27 14:41

There is a tentative fix at [^]
It is probably broken, but demonstrates the idea.
garrigue (manager)
2018-03-23 04:45

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 [^]

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.

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker