|Anonymous | Login | Signup for a new account||2018-08-16 04:14 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0007668||OCaml||typing||public||2017-11-05 13:45||2017-11-06 09:21|
|Target Version||Fixed in Version||4.07.0+dev/beta2/rc1/rc2|
|Summary||0007668: -principal is broken with polymorphic variants.|
|Description||The following code is wrongly type-checked by ocamlc -principal. I have checked it with 4.05.0 and 4.06.0. I guess something wrong with the polymorphic variant typing when -principal is given.|
let partition_map f xs =
let rec part left right = function
|  -> List.rev left, List.rev right
| x::xs ->
match f x with
| `Left v -> part (v::left) right xs
| `Right v -> part left (v::right) xs
part   xs
let f xs : (int list * int list) = partition_map (fun x -> if x then `Left () else `Right ()) xs
|Steps To Reproduce||$ ocamlc -c -i bug.ml|
File "/tmp/bug.ml", line 11, characters 35-96:
Error: This expression has type unit list * unit list
but an expression was expected of type int list * int list
Type unit is not compatible with type int
$ ocamlc -c -i -principal bug.ml
val partition_map :
('a -> [< `Left of 'b | `Right of 'c ]) -> 'a list -> 'b list * 'c list
val f : bool list -> int list * int list
|Tags||No tags attached.|
Apparently the problem is there since 4.00, so it was caused by the introduction of GADTs.
Still, the problem seems to be in f, which does not contain any pattern-matching. Strange.
edited on: 2017-11-06 07:24
BTW, what is the purpose of -principal in the OCaml compiler build? It bootstraps even without it.
I have added some code using polymorphic variants to the compiler and want to avoid this issue by removing -principal. Is it safe?
Fixed in trunk at commit 43d77ff6a.
The problem stems from the way -principal detects non-principal typing information when typing patterns.
Rather than tracking levels on the fly, like for expressions, it discards non-generic subparts of the propagated type. However, for some polymorphic variants this resulted in bad-formed types, that in turn could forget type information.
This is fixed by not keeping row field variables when the contents of the row field might be (partially) discarded.
As to whether -principal is needed to bootstrap the compiler, clearly no.
Code compiled with -principal is not safer (or less safe), it just detects some non-principalities, which can been seen as lack of robustness of typing for the future.
As this shows, one cannot exclude that -principal has some soundness bug that fortunately doesn't appear without it (or the other way round). For this reason it might be reasonable to compile with the two switches. This should probably be discussed at the developer meeting next week...
|Thank you for the fix! I turn off -principal for my compiler hacking for now.|
|2017-11-05 13:45||furuse||New Issue|
|2017-11-06 03:38||garrigue||Note Added: 0018640|
|2017-11-06 03:38||garrigue||Assigned To||=> garrigue|
|2017-11-06 03:38||garrigue||Status||new => confirmed|
|2017-11-06 07:23||furuse||Note Added: 0018641|
|2017-11-06 07:24||furuse||Note Edited: 0018641||View Revisions|
|2017-11-06 08:09||garrigue||Note Added: 0018642|
|2017-11-06 08:09||garrigue||Status||confirmed => resolved|
|2017-11-06 08:09||garrigue||Fixed in Version||=> 4.07.0+dev/beta2/rc1/rc2|
|2017-11-06 08:09||garrigue||Resolution||open => fixed|
|2017-11-06 08:10||garrigue||Category||middle end (typedtree to clambda) => typing|
|2017-11-06 09:21||furuse||Note Added: 0018643|
|Copyright © 2000 - 2011 MantisBT Group|