|Anonymous | Login | Signup for a new account||2013-12-09 16:13 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006150||OCaml||OCaml typing||public||2013-08-30 18:20||2013-09-03 19:55|
|Status||resolved||Resolution||no change required|
|Target Version||4.01.1+dev||Fixed in Version|
|Summary||0006150: Wrong error: "The type constructor X.t would escape its scope"|
|Description||"The type constructor X.t would escape its scope" while it wouldn't.|
This error is likely caused by the use of a simple (potentially polymorphic) type annotation, such as in (foo:'a).
Proving why it actually is a bug:
- Removing the type annotation ('a) removes the error.
- Replacing ('a) by (X.t) removes the error.
|Steps To Reproduce||let f () =|
let module X = struct type t = O end in
let open X in
let g : 'a -> 'b = function O -> () in
|Additional Information||In "let g : 'a -> 'b = function O -> () in", the type constraint "'a -> 'b" is the only way that I can think of to constrain g to be an arrow (without having to precisely specify the left and right parts of the arrow).|
I met this bug by accident in a small piece of software (4 kloc), I didn't mean to find it, and it was pretty annoying :(
|Tags||No tags attached.|
I'm lowering the severity from "block" to "major" because, unless I'm mistaken, you can work around the bug by specifying a more precise type instead of 'a -> 'b.
Also, I'll let the typing specialists give a better answer, but it seems to me that the error message is correct. The problem is in the binding of the type variables ('a and 'b): they have no syntactic binder, so in OCaml they are implicitly bound at the top-level let (in this case, your "let f () =..."). Hence, the X.t does escape its scope, even if in this case you don't use it ouside its scope.
Now I agree this is annoying and maybe there is something that can be done about it.
Sorry I didn't quite know what "block" meant, I picked it while I was actually searching for one *less* severe than "major" but more severe than "minor".
(I did work around the bug by removing the type constraint but it made me lose quite some time while I was trying to figure out whether I was insane or if the compiler was "probably wrong", since I almost never find bugs.)
I don't (want to) see why an 'a would be bound to the top-level let, since at the end g is monomorphic (hence 'a should "disappear"), and even f is monomorphic as well.
The standard way to write a skeleton is to use anonymous type variables _ .
Here you should just replace 'a -> 'b by _ -> _ .
Thanks for the _ -> _.
However it doesn't convince me at all that this issue is not a bug.
In the following example, you might not want to write _ -> _ but 'a -> 'a to ensure that both left and right parts of the arrow are the same.
let f () =
let module X = struct type t = O end in
let open X in
let g : 'a -> 'a = function O -> O in
If there are special cases where it would be wrong to accept such a program, then I'd be ok with it, as for the value restriction. But I really don't see any. Can't we remove binding at the top-level LET for types that actually bind nothing?
There is a confusion here.
The specification of ocaml is that the syntactic scope of type variables is the whole toplevel phrase.
I.e. two different occurrences of the same type variables occurring in different parts of the phrase must be shared.
Changing this behavior would change the specification, and break lots of code.
This behavior is ensured in a simple way, by only allowing to generalize a named type variable at toplevel.
No bug here, since this is the specification.
There are some ways around this limitation, such as anonymous type variables, or explicit polymorphism
(if you want the function to be really polymorphic).
Now you could discuss whether this is expressive enough.
As discussed in some other bug report (reference missing...),
Standard ML uses another approach, of computing the smallest scope including all occurrences of a type variable. This is complicated, and in SML this would still not allow your example, as named typed variables cannot be instantiated. However, in ocaml this could be used to give a smaller scope to named type variables. This is under consideration.
Yet, this is not the only problem type definition scope.
For instance, the following program is not valid, and many people will scratch their heads on that:
let r = ref 
type t = O
let () = r := [O]
Ok, thanks. So the problem is that by writing that 'a, the type X.t is "seen" *above its definition*, hence the escaping error.
In your example, in my opinion, the error message given by the compiler is a bug (not that there's not an error, but the formulation of the message is very wrong).
$ ocamlc -i o.ml
File "o.ml", line 3, characters 15-16:
Error: This expression has type t but an expression was expected of type t
The type constructor t would escape its scope
In the following example, the error message is also very disturbing. I get the error message with 4.01.0+dev or 4.02.0+dev, with previous versions it asserts false.
# class type t = t;;
Error: The class type t is not yet completely defined
Sometimes, it would be better for the message to be something like "Error: sorry I can't (yet) explain." or just "Error." instead of some insane phrases.
Would it be worth proposing patches for such things? (or should I wait until it gets better, or abandon?)
Ah, error messages!
I try to fix them when I can, but the problem is that an error message which makes sense in one context doesn't make sense in another, and it is very hard to see all the cases in advance (and to avoid making the core overly complicated).
> # class type t = t;;
> Error: The class type t is not yet completely defined
Here, this is a special case of recursive definition.
In some situation this is allowed, but in others not.
class type t = object method m : int end and u = t
class type t = u and object method m : int end
So maybe we should add a special error message when there is only one class.
For the scoping messages, this is even harder, as the cause is hard to track.
Proposing patches is not going to help much, except if you also provide a big test suite to ensure that all cases were taken into account. Otherwise the situation might be worse than before.
|2013-08-30 18:20||pw374||New Issue|
|2013-08-30 21:48||doligez||Note Added: 0010272|
|2013-08-30 21:48||doligez||Severity||block => major|
|2013-08-30 21:48||doligez||Target Version||=> 4.01.1+dev|
|2013-08-30 21:52||doligez||Note Added: 0010273|
|2013-08-30 21:52||doligez||Status||new => feedback|
|2013-08-30 22:45||pw374||Note Added: 0010275|
|2013-08-30 22:45||pw374||Status||feedback => new|
|2013-08-30 23:11||doligez||Relationship added||related to 0001952|
|2013-08-31 09:27||garrigue||Note Added: 0010281|
|2013-08-31 09:27||garrigue||Status||new => resolved|
|2013-08-31 09:27||garrigue||Resolution||open => no change required|
|2013-08-31 09:27||garrigue||Assigned To||=> garrigue|
|2013-08-31 14:36||pw374||Note Added: 0010283|
|2013-09-01 02:24||garrigue||Note Added: 0010287|
|2013-09-01 02:57||pw374||Note Added: 0010288|
|2013-09-01 04:29||garrigue||Note Added: 0010289|
|2013-12-07 23:20||gasche||Relationship added||has duplicate 0006264|
|Copyright © 2000 - 2011 MantisBT Group|