Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006150OCamlOCaml typingpublic2013-08-30 18:202013-09-03 19:55
Reporterpw374 
Assigned Togarrigue 
PrioritynormalSeveritymajorReproducibilityalways
StatusresolvedResolutionno change required 
PlatformOSOS Version
Product Version4.00.1 
Target Version4.01.1+devFixed in Version 
Summary0006150: 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 Reproducelet f () =
  let module X = struct type t = O end in
  let open X in
  let g : 'a -> 'b = function O -> () in
  g(O)
Additional InformationIn "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 :(
TagsNo tags attached.
Attached Files

- Relationships
related to 0001952resolved référence et polymorphisme 
has duplicate 0006264resolvedgasche Strange restriction on unification between rigid and flexible variables 

-  Notes
(0010272)
doligez (administrator)
2013-08-30 21:48

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.
(0010273)
doligez (administrator)
2013-08-30 21:52

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.
(0010275)
pw374 (reporter)
2013-08-30 22:45

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.
(0010281)
garrigue (manager)
2013-08-31 09:27

The standard way to write a skeleton is to use anonymous type variables _ .
Here you should just replace 'a -> 'b by _ -> _ .
(0010283)
pw374 (reporter)
2013-08-31 14:36

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
  ignore(g(O))

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?
(0010287)
garrigue (manager)
2013-09-01 02:24

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]
(0010288)
pw374 (reporter)
2013-09-01 02:57

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?)
(0010289)
garrigue (manager)
2013-09-01 04:29

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

For instance,
> # 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
but not
  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.

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