"β t is less general than ∀α. α t" with trunk #13176
Comments
|
another package |
|
The trunk behavior is correct: let ignore: _ -> unit = Obj.magic ignoredoesn't yield a polymorphic type in any version of OCaml. |
|
ok good to know. What would be the best way to fix those packages? |
Right, and the pre-trunk behaviour is unsound (and has been for a long time). Here's a program showing the issue: type t = {x : 'a. 'a list ref }
let {x} = {x = Obj.magic ref []}
let () = x := [0]; print_endline (List.hd !x)This example is rejected by |
|
Well, the best way would be that they stop using The hackish way is to embrace their brokenness and simply extrudes the type t = {x : 'a. 'a list ref }
let {x} = let x = Obj.magic ref [] in {x} |
|
Out of curiosity, do we know what change in the type-checker resulted in this change in behavior on user code? (Note: In some cases |
|
This is the consequence of #12932 which removed a special treatment for typing record label. type t = {f: 'a. ('a list -> int) Lazy.t}
let l : t = { f = lazy (raise Not_found)}and adapting it to take in account that let not_lazy x = lazy x
let l : t = { f = not_lazy (raise Not_found)}fails in trunk-only with
|
|
Hmm. Let me make sure I understand things correctly:
We should fire the reviewer of #12932 which did not catch any of this circus (let me explain the joke: I reviewed that PR), and maybe triple-check that the testsuite correctly covers both the desirable examples that we want to accept (from #4862) and the undesirable examples that we are now right to reject. |
We're right to reject them according to the generalization rules of the type checker, but those rules aren't doing anything valuable by rejecting the code in question. There's no additional safety gained by not generalizing the result of calls to In other words, while the following code is prohibited: let r : 'a. 'a list ref = Obj.magic (ref [])the following essentially equivalent code is permitted: type t = {x:'a.'a list ref}[@@unboxed]
let q = Obj.magic (ref [])
let r : 'a. 'a list ref = q.xand it's probably possible to fix up the newly-broken opam packages in the PR description with a similar change. |
|
In general I agree that it would soundness-preserving to treat In other words: I think that if the compiler had rejected this use-case in the first place, people would have written better code. So maybe it is not so bad to start rejecting it now, especially since people are already well aware that |
|
@gasche , my summary of the history would be more:
type t = {f: 'a. ('a list -> int) Lazy.t}
let not_found () = raise Not_found
let l = { f = lazy (not_found ())};;fails on trunk.
{ f = <body> }into let f = <body> in { f }Taking in account that:
I would be in favour to keep the simplification of #12932 . |
|
Yes, I am not in favor of removing #12932 either, just pointing out that its impact is larger than we had anticipated. |
|
My impression so far is that "deal with it" is a reasonable response to users whose code has been broken in trunk, at least in all the cases that have been brought to our attention so far. |
|
For now we decided to not change anything upstream. Feel free to add more information about existing breakages. |
A new error I'm seeing with trunk is this one:
I'm a bit surprised to see that
Obj.magicis no longer the catch-all of the type-system. Is that expected?The text was updated successfully, but these errors were encountered: