Skip to content
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

Wrong error: "The type constructor X.t would escape its scope" #6150

Closed
vicuna opened this issue Aug 30, 2013 · 9 comments
Closed

Wrong error: "The type constructor X.t would escape its scope" #6150

vicuna opened this issue Aug 30, 2013 · 9 comments
Assignees
Milestone

Comments

@vicuna
Copy link

vicuna commented Aug 30, 2013

Original bug ID: 6150
Reporter: pw374
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2016-12-07T10:49:25Z)
Resolution: not a bug
Priority: normal
Severity: major
Version: 4.00.1
Target version: 4.01.1+dev
Category: typing
Has duplicate: #6264
Related to: #8391
Monitored by: pw374 @gasche

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

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 :(

@vicuna
Copy link
Author

vicuna commented Aug 30, 2013

Comment author: @damiendoligez

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.

@vicuna
Copy link
Author

vicuna commented Aug 30, 2013

Comment author: @damiendoligez

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.

@vicuna
Copy link
Author

vicuna commented Aug 30, 2013

Comment author: pw374

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.

@vicuna
Copy link
Author

vicuna commented Aug 31, 2013

Comment author: @garrigue

The standard way to write a skeleton is to use anonymous type variables _ .
Here you should just replace 'a -> 'b by _ -> _ .

@vicuna
Copy link
Author

vicuna commented Aug 31, 2013

Comment author: pw374

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?

@vicuna
Copy link
Author

vicuna commented Sep 1, 2013

Comment author: @garrigue

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]

@vicuna
Copy link
Author

vicuna commented Sep 1, 2013

Comment author: pw374

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

@vicuna
Copy link
Author

vicuna commented Sep 1, 2013

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented May 21, 2015

Comment author: @edwintorok

I just had one of those "head scratching" moments on the code below, and I only realized what is wrong when moving the 'type foo' above the 'global' fixed the compiler error (I encountered the error before but only with first class modules).

Would it be possible for the compiler to report the scope of the variable even if the cause of the escape is not easy to determine? For example add the info marked with ++:

File "x.ml", line 13, characters 26-31:
Error: This expression has type unit -> foo
but an expression was expected of type unit -> foo
The type constructor foo would escape its scope
++ type foo is not in scope between line 1, character 1 and line 10, character 6

This has the advantage that it tells you where the code you need to fix probably is (type annotations, or moving declarations), i.e. the negation of the scope (line 10, character 6 and EOF).

module M :sig
type 'a t
val v : unit -> 'a t
end = struct
type 'a t = unit
let v _ = ()
end

let global = M.v () (* line 9 )
type foo = {a: string list;} (
line 10 *)
let parse () : foo = failwith "TODO"
let make (_:'a M.t) ~(parse:unit -> 'a) : 'a = failwith "TODO"
let foo () = make global ~parse

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants