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
Constant type can not be generalized ? #7636
Comments
Comment author: ChriChri Sory the previous example was too simple. type ('a, 'b) elt = 'a
type 'a iter = { f : 'b.('a, 'b) elt -> unit }
let promote f : 'a -> unit =
let f : 'b.('a, 'b) elt -> unit = fun x -> f x in
{ f } |
This comment has been minimized.
This comment has been minimized.
Comment author: @gasche Your code seems to be wrong: For your first code example, the following works:
For you second example, this seems related to the fact that ('a, 'b) elt is a type synonym, which confuses the type-checking of polymorphic methods. Indeed,
but this fails:
This may be a bug. |
Comment author: ChriChri Thanks. This first example was indeed stupid, I wanted to simplify to much ... |
Comment author: @gasche Note that recent versions of OCaml (>= 4.04.0) can make the trick work without any change to the data representation:
|
Comment author: ChriChri The following indeed works ! Very strange that 'a is not like 'a * unit
|
Comment author: ChriChri And this works too: type 'a t = U of 'a [@@unboxed]
type ('a, 'b) elt = 'a t
type 'a iter = { f : 'b.'a -> unit }
let promote (f : 'a t -> unit) = { f } |
Comment author: @lpw25 This is an interesting one. If you have a type: type ('a, 'b) t = 'a and you unify ('p, 'q) t with ('r, 's) t then it will essentially unify ('p, 'q) t with 'r. That means that if the level of 'r is lower than the level of 'q then the level of 'q will be lowered. (I'm glossing over some slight details of how the levels are handled here, but this is the basic idea). In your example the 'r is 'a and the 'q is 'b. The level from 'a is too low to be generalized, and thus 'b cannot be generalised either, which causes the error. I'm not sure what the best thing to do here is. In this case we would essentially like 'r to unify with 'p and thus leave the level of 'q untouched, but I'm not sure that is the right thing to do in general. |
Comment author: @xavierleroy Reading this discussion I can't see whether (1) everything works as intended even though the behavior is surprising in the end, or (2) something might possibly need to be changed. Please classify this PR according to the answer to this question. |
Comment author: @lpw25 I think it is worth trying to do better here, so I'm marking as confirmed. In particular, this seems like a potential problem for principality or at least a case where we are not really inferring the most general type possible. |
Comment author: @garrigue Unfortunately, I don't think that we can really do better, short of changing to some extent our approach to abbreviations. Namely, if your analysis is correct (and I think it is), the problem comes from the way abbreviations types are unified; i.e. both sides are first expanded, and the expanded type is redirected to point to (one of) the abbreviations. In doing that, the levels of type variables in that abbreviation are lowered to that of the root of the expanded type. This is fine if the type variables actually occur in the expanded type, but this may lower them more than needed if they don't. Yet not lowering them would break the invariant that levels in types go down towards the leaves. A fix would be to only redirect to abbreviations if their variables all appear in the expanded type. First option, fix just this example: if the expansion of an abbreviation is in one of its parameters, then do not redirect to it. I'm not sure what the cost would be; probably not that high. Second option, consider abbreviations less important than principality: as soon as one of the parameters of an abbreviation does not appear in its (fully expanded) body, do not redirect to it. In theory, this could be very easy to check: this amounts to empty variance information for this parameter. In practice, there are many corner cases where this information is not accurate, and I'm not sure how far we want to go. Anyway, this is good to understand what is happening, as this can help working around the problem. |
Comment author: @xavierleroy Marking this for "later", as I'm not expecting a solution any time soon. |
Comment author: @garrigue I intend to fix it for 4.07, but sill need to decide how to do it. |
Comment author: victor-dumitrescu We've encountered an instance of this issue in F* extraction to OCaml (4.02.3 and 4.05.0). Currently we are extracting polymorphic functions in this form: type 'a t = int
let test : 'a. int -> 'a t = fun i -> i This fails with
However, it does go through when using the -principal flag. It doesn't seem to be an issue when writing this function slightly differently. All of the following are accepted: let test2 : int -> 'a t = fun i -> i
let test3 : type a. int -> a t = fun i -> i
let test4 : 'a. int -> 'a t = fun i -> let i: int = i in i |
Original bug ID: 7636
Reporter: ChriChri
Assigned to: @garrigue
Status: confirmed (set by @lpw25 on 2017-10-02T16:40:50Z)
Resolution: open
Priority: normal
Severity: minor
Target version: 4.07.0+dev/beta2/rc1/rc2
Category: typing
Monitored by: ChriChri
Bug description
It looks like if variables were not values in Ocaml ?
This is not accepted :
This works:
The text was updated successfully, but these errors were encountered: