Anonymous | Login | Signup for a new account | 2018-10-15 17:59 CEST |

Main | My View | View Issues | Change Log | Roadmap |

View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||

ID | Project | Category | View Status | Date Submitted | Last Update | ||||||

0007636 | OCaml | typing | public | 2017-09-23 19:39 | 2018-01-30 08:08 | ||||||

Reporter | ChriChri | ||||||||||

Assigned To | garrigue | ||||||||||

Priority | normal | Severity | minor | Reproducibility | have not tried | ||||||

Status | confirmed | Resolution | open | ||||||||

Platform | OS | OS Version | |||||||||

Product Version | |||||||||||

Target Version | 4.07.0+dev/beta2/rc1/rc2 | Fixed in Version | |||||||||

Summary | 0007636: Constant type can not be generalized ? | ||||||||||

Description | It looks like if variables were not values in Ocaml ? This is not accepted : type 'a iter = { f : 'b.'a -> unit } let promote f : 'a -> unit = { f } This works: let promote f = let f : 'b.'a -> unit = fun x -> f x in { f = fun x -> f x } | ||||||||||

Tags | No tags attached. | ||||||||||

Attached Files | |||||||||||

Notes | |

(0018313) ChriChri (reporter) 2017-09-23 19:43 |
Sory the previous example was too simple. My real problem is this : 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 } |

(0018314) ChriChri (reporter) 2017-09-23 19:44 |
Why can't I edit my original issue ? |

(0018315) gasche (administrator) 2017-09-23 20:04 |
Your code seems to be wrong: "let promote f : 'a -> unit" should, I suppose, be "let promote (f : 'a -> unit)". For your first code example, the following works: # type 'a iter = { f : 'b.'a -> unit };; # let promote (f : 'a -> unit) = { f = f };; val promote : ('a -> unit) -> 'a iter = <fun> 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, this works: # type ('a, 'b) elt = 'a * unit;; # type 'a iter = { f : 'b. ('a, 'b) elt -> unit };; # let promote (iter : 'a iter) : 'a iter = { f = iter.f };; val promote : 'a iter -> 'a iter = <fun> but this fails: # type ('a, 'b) elt = 'a;; # type 'a iter = { f : 'b. ('a, 'b) elt -> unit };; # let promote (iter : 'a iter) : 'a iter = { f = iter.f };; Error: This field value has type ('a, 'c) elt -> unit which is less general than 'b. ('a0, 'b) elt -> unit This may be a bug. |

(0018316) ChriChri (reporter) 2017-09-23 21:50 |
Thanks. This first example was indeed stupid, I wanted to simplify to much ... Thanks for the trick ... |

(0018317) gasche (administrator) 2017-09-23 21:54 edited on: 2017-09-23 21:55 |
Note that recent versions of OCaml (>= 4.04.0) can make the trick work without any change to the data representation: # type 'a id = Id of 'a [@@unboxed];; # type ('a, 'b) elt = 'a id;; # type 'a iter = { f : 'b. ('a, 'b) elt -> unit };; # let promote { f } = { f };; val promote : 'a iter -> 'a iter = <fun> |

(0018318) ChriChri (reporter) 2017-09-23 21:56 |
The following indeed works ! Very strange that 'a is not like 'a * unit in this case: # type ('a, 'b) elt = 'a * unit # type 'a iter = { f : 'b.'a -> unit } # let promote f = { f } type 'a iter = { f : 'a -> unit; } val promote : ('a -> unit) -> 'a iter = <fun> |

(0018319) ChriChri (reporter) 2017-09-23 21:58 |
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 } |

(0018320) lpw25 (developer) 2017-09-24 01:06 |
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. |

(0018404) xleroy (administrator) 2017-09-29 20:09 |
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. |

(0018454) lpw25 (developer) 2017-10-02 18:43 |
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. |

(0018463) garrigue (manager) 2017-10-03 09:53 |
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. But is it really what we want? In this case yes, as the expanded type is actually a parameter of the abbreviation. In general it is much harder to tell. 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. I don't think fixing this is urgent, we can first discuss what is the correct approach. |

(0018524) xleroy (administrator) 2017-10-09 20:18 |
Marking this for "later", as I'm not expecting a solution any time soon. |

(0018659) garrigue (manager) 2017-11-13 17:49 |
I intend to fix it for 4.07, but sill need to decide how to do it. Suggestion by Didier Rémy: do not lower levels on "absent" type variables, based on variance. This breaks the invariant that levels should decrease, but the variable doesn't matter anyway. Need to look into it. |

(0018858) victor-dumitrescu (reporter) 2018-01-29 11:53 |
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 Error: This definition has type 'a t -> 'a t which is less general than 'a0. 'a t -> 'a0 t 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 |

(0018860) garrigue (manager) 2018-01-30 08:08 |
Tentative fix: https://github.com/ocaml/ocaml/pull/1588 [^] |

Issue History | |||

Date Modified | Username | Field | Change |

2017-09-23 19:39 | ChriChri | New Issue | |

2017-09-23 19:43 | ChriChri | Note Added: 0018313 | |

2017-09-23 19:44 | ChriChri | Note Added: 0018314 | |

2017-09-23 20:04 | gasche | Note Added: 0018315 | |

2017-09-23 21:50 | ChriChri | Note Added: 0018316 | |

2017-09-23 21:54 | gasche | Note Added: 0018317 | |

2017-09-23 21:55 | gasche | Note Edited: 0018317 | View Revisions |

2017-09-23 21:56 | ChriChri | Note Added: 0018318 | |

2017-09-23 21:58 | ChriChri | Note Added: 0018319 | |

2017-09-24 01:06 | lpw25 | Note Added: 0018320 | |

2017-09-29 20:09 | xleroy | Note Added: 0018404 | |

2017-09-29 20:09 | xleroy | Status | new => acknowledged |

2017-10-02 18:40 | lpw25 | Assigned To | => lpw25 |

2017-10-02 18:40 | lpw25 | Status | acknowledged => confirmed |

2017-10-02 18:43 | lpw25 | Note Added: 0018454 | |

2017-10-03 09:53 | garrigue | Note Added: 0018463 | |

2017-10-09 20:18 | xleroy | Note Added: 0018524 | |

2017-10-09 20:18 | xleroy | Target Version | => later |

2017-11-13 17:49 | garrigue | Note Added: 0018659 | |

2017-11-13 17:49 | garrigue | Assigned To | lpw25 => garrigue |

2017-11-13 17:49 | garrigue | Target Version | later => 4.07.0+dev/beta2/rc1/rc2 |

2018-01-29 11:53 | victor-dumitrescu | Note Added: 0018858 | |

2018-01-30 08:08 | garrigue | Note Added: 0018860 |

Copyright © 2000 - 2011 MantisBT Group |