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

Incorrect rejection of program due to faux scope escape #7519

Closed
vicuna opened this issue Apr 20, 2017 · 3 comments
Closed

Incorrect rejection of program due to faux scope escape #7519

vicuna opened this issue Apr 20, 2017 · 3 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Apr 20, 2017

Original bug ID: 7519
Reporter: @mmottl
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2017-08-29T07:34:22Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.04.1
Fixed in version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing
Monitored by: @gasche @yallop @mmottl

Bug description

The following program is rejected by the compiler:


module Gen_spec = struct type 't extra = unit end

module type S = sig
module Spec : sig type 't extra = unit end

type t
val make : unit -> t Spec.extra
end (* S *)

module Make () : S with module Spec := Gen_spec = struct
type t = int
let make () = ()
end (* Make *)

let () =
let module M = Make () in
M.make ()
(* (M.make () : unit) *)

The error is:


File "./foo.ml", line 17, characters 2-11:
Error: This expression has type M.t Gen_spec.extra = unit
but an expression was expected of type unit
The type constructor M.t would escape its scope

The error shows that the compiler already knows that M.t Gen_spec.extra is equivalent to the unit type. Therefore, there should not be any type escaping the scope of the local module. Using the commented out last line instead of the preceding one also shows that the compiler will happily unify the type with "unit" and then accept the program.

I suppose that there is a missing conversion somewhere in the type checker that should attempt to eliminate all local types before complaining about scope violations.

@vicuna
Copy link
Author

vicuna commented Aug 2, 2017

Comment author: @garrigue

The interesting phenomenon here is that one needs to expand extra, not t, to avoid the escape.
This is nowhere in the logic of the compiler at this point.
This can be done, but the runtime cost could be significant (should check).

@vicuna
Copy link
Author

vicuna commented Aug 2, 2017

Comment author: @garrigue

Tentative fix: #1273

@vicuna
Copy link
Author

vicuna commented Aug 29, 2017

Comment author: @garrigue

Fixed by #1273.

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