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
Compiler in infinite loop or stack overflow. #5026
Comments
Comment author: @garrigue Fixed for upcoming 3.12. Ctype.non_recursive_abbrev and Ctype.cyclic_abbrev should use try_expand_once_opt |
Comment author: yziquel 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... |
Comment author: @garrigue
Well, "simply disallowing" it required to track it down... More seriously, the compiler is allowed internally to expand private So, sorry, I don't see how we could allow that. |
Comment author: yziquel 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". |
Comment author: @garrigue I agree with you that there are times when one would like to be able |
Original bug ID: 5026
Reporter: yziquel
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2012-03-24T14:01:41Z)
Resolution: not a bug
Priority: normal
Severity: crash
Version: 3.11.2
Fixed in version: 3.12.0+dev
Category: ~DO NOT USE (was: OCaml general)
Monitored by: yziquel
Bug description
The 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
end;;
class type ['a] s3 = object val underlying : 'a t end
class ['a] s3object r : ['a] s3 = object
end;;
Fatal error: exception Stack_overflow
The text was updated successfully, but these errors were encountered: