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

program (mistakenly?) rejected due to nongeneralizable type variable that appears nowhere #5663

Closed
vicuna opened this issue Jun 26, 2012 · 6 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link

commented Jun 26, 2012

Original bug ID: 5663
Reporter: sweeks
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-09-24T15:33:15Z)
Resolution: fixed
Priority: normal
Severity: minor
Target version: 4.02.3+dev
Fixed in version: 4.03.0+dev / +beta1
Category: typing

Bug description

The program below is rejected by the type checker.

module F (M : sig
type 'a v = string
include sig
type 'a t
type 'a u
val f : unit -> _ t
val g : 'a t -> 'a u -> unit
end with type 'a u := 'a v
end) = struct
open M

 let t = (f () (*: unit v t*))  (* uncomment here to make it type check *)
 let () = g t "foo"

end

The error message is:

Error: The type of this module,
functor
(M : sig
type 'a v = string
type 'a t
val f : unit -> 'a t
val g : 'a t -> 'a v -> unit
end) ->
sig val t : '_a M.t end,
contains type variables that cannot be generalized

I think this program should be accepted. The type variable that OCaml
is complaining about is unused, if one expands out the types.

File attachments

@vicuna

This comment has been minimized.

Copy link
Author

commented Jun 26, 2012

Comment author: @garrigue

I'm not sure I understand your point here.
It seems that M.t is abstract in this program, so you cannot expand it.
So the type variable is really there, even if you didn't name it.
Writing "type +'a t" would probably solve the problem, if this is acceptable.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jul 24, 2012

Comment author: sweeks

Sorry, my example had a mistake. Here is a much simpler example:

module F (M : sig
type 'a t
type 'a u = string
val f : unit -> _ u t
end) = struct
let t = M.f ()
end

This causes the following error message:

Error: The type of this module,
functor
(M : sig type 'a t type 'a u = string val f : unit -> 'a u t end) ->
sig val t : '_a M.u M.t end,
contains type variables that cannot be generalized

The type variable that OCaml is complaining about, ['_a], is in the
expression ['_a M.u], which OCaml knows is equivalent to [string]. I
don't see why OCaml should be complaining about ['_a], since it need
not appear in the type of [t], which has type [string M.t].

Adding a type constraint to [t] of the form [string M.t] isn't
sufficient to make the error go away. However, adding a type
constraint [unit M.u M.t] does make the error go away.

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 18, 2014

Comment author: @yallop

With -short-paths the type variable doesn't even appear in the error message:

$ ocamlc -short-paths pr5663.ml
File "pr5663.ml", line 1, characters 9-109:
Error: The type of this module,
functor
(M : sig type 'a t type 'a u = bytes val f : unit -> bytes t end) ->
sig val t : bytes M.t end,
contains type variables that cannot be generalized

@vicuna

This comment has been minimized.

Copy link
Author

commented Apr 21, 2015

Comment author: @garrigue

Added a patch which expands constructors while checking for non-generalizable variables.
This is disabled during class definitions, as it broke typing-poly/poly.ml.

@vicuna

This comment has been minimized.

Copy link
Author

commented Apr 22, 2015

Comment author: @garrigue

Fixed in trunk, at revision 16030, by expanding type abbreviations while checking for nongeneralizable type variables.
Note that we only do it for compilation units.
For classes, this is not done, because typing-poly/poly.ml would fail.

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 1, 2016

Comment author: @lpw25

This change seems to cause #7305

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.