Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005026OCamlOCaml generalpublic2010-04-16 15:272012-03-24 15:01
Reporteryziquel 
Assigned Togarrigue 
PrioritynormalSeveritycrashReproducibilityhave not tried
StatusclosedResolutionno change required 
PlatformOSOS Version
Product Version3.11.2 
Target VersionFixed in Version3.12.0+dev 
Summary0005026: Compiler in infinite loop or stack overflow.
DescriptionThe following code sends the compiler into an infinite loop and the toplevel in a stack overflow. Part of the infinite loop seems to be in the Ctype module, as far as I could debug the compiler.

yziquel@seldon:~$ ocaml
        Objective Caml version 3.11.2

# type untyped;;
type untyped
# type -'a typed = private untyped;;
type 'a typed = private untyped
# type -'typing wrapped = private sexp
  and +'a t = 'a typed wrapped
  and sexp = private untyped wrapped;;
type 'a wrapped = private sexp
and 'a t = 'a typed wrapped
and sexp = private untyped wrapped
# class type ['a] s3 = object
    val underlying : 'a t
  end;;
class type ['a] s3 = object val underlying : 'a t end
# class ['a] s3object r : ['a] s3 = object
    val underlying = r
  end;;
Fatal error: exception Stack_overflow
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005370)
garrigue (manager)
2010-04-26 10:57

Fixed for upcoming 3.12.

Ctype.non_recursive_abbrev and Ctype.cyclic_abbrev should use try_expand_once_opt
and expand_abbrev_opt, as later phases of the compiler may have to expand a type
using those operations.
(0005664)
yziquel (reporter)
2010-09-24 19:24

I noticed that this issue has been closed. Upgrading to 3.12, I understood that "closed" meant that this recursive subtyping is simply disallowed, and fails with "the type abbreviation tau is cyclic" error message.

I would dearly like to be able to do such a recursive subtyping. Is there any deep reason to disallow this? Could I expect to see such subtyping to be allowed in the future?

In my specific case, this is really useful, as it allows me to play very nicely with the possibly very horrible type systems of dynamically typed languages when binding interpreters of foreign languages. Just say "subtype to" is really cleaner than using Obj.magic or similar %identity functions when switching type systems...
(0005665)
garrigue (manager)
2010-09-29 15:19

> I noticed that this issue has been closed. Upgrading to 3.12, I understood that "closed" meant that this recursive subtyping is simply disallowed, and fails with "the type abbreviation tau is cyclic" error message.

> I would dearly like to be able to do such a recursive subtyping. Is there any deep reason to disallow this? Could I expect to see such subtyping to be allowed in the future?

Well, "simply disallowing" it required to track it down...

More seriously, the compiler is allowed internally to expand private
abbreviations (this is the whole of their being "private" rather than
"abstract"). Since your wrapped expands to sexp which expands to
wrapped, it is not well-founded, and this is not allowed (even if
you use the -rectypes option).

So, sorry, I don't see how we could allow that.
(0005669)
yziquel (reporter)
2010-10-03 21:15

This is perhaps too far fetched, but perhaps the issue is precisely that "private" means "expanding".

In a sense, if expanding simply means "rewrite", then yes, if you have recursive subtyping between a and b, they should naturally be identified (I guess), and there wouldn't be any need to do recursive subtyping.

However, it could perhaps be argued that "expanding" / "rewriting" is too strong. In the case of recursive subtyping, for instance of 'a t1 to t2 and of t2 to 'a t1, we could ask to allow only one subtyping, or both, depending on what we want to do. To do that, we should let the compiler know that there are two types and one-way subtyping, or equality. But it shouldn't be handled by syntactic rewriting but perhaps on a more logical level.

Perhaps I'm missing the whole point here, but I'd appreciate your view on that.

The whole point here is to be able to implement cleanly "type-inference barriers".
(0005735)
garrigue (manager)
2010-12-12 06:54

I agree with you that there are times when one would like to be able
to define completely opaque type abbreviations.
You can already to this by writing
  type -'a wrapped = private Wrap of sexp
Of course this means that the internal representation of sexp and
wrapped is going to differ, but I would say this is a compiler problem,
not a type system one.
Another appraoch might be to make private abbreviations completely
opaque (never expanded), but this goes against another of their goals,
which is to make them transparent enough to allow optimizations, which
in turn requires to be able to expand them.

- Issue History
Date Modified Username Field Change
2010-04-16 15:27 yziquel New Issue
2010-04-18 10:39 xleroy Status new => assigned
2010-04-18 10:39 xleroy Assigned To => garrigue
2010-04-26 10:57 garrigue Note Added: 0005370
2010-04-26 10:57 garrigue Status assigned => closed
2010-04-26 10:57 garrigue Resolution open => fixed
2010-04-26 10:57 garrigue Fixed in Version => 3.12.0+dev
2010-09-24 19:24 yziquel Note Added: 0005664
2010-09-24 19:24 yziquel Status closed => feedback
2010-09-24 19:24 yziquel Resolution fixed => reopened
2010-09-29 15:19 garrigue Note Added: 0005665
2010-10-03 21:15 yziquel Note Added: 0005669
2010-12-12 06:54 garrigue Note Added: 0005735
2010-12-12 06:54 garrigue Status feedback => resolved
2010-12-12 06:54 garrigue Resolution reopened => no change required
2012-03-24 15:01 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker