You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Original bug ID: 7668 Reporter: furuse Assigned to:@garrigue Status: resolved (set by @garrigue on 2017-11-06T07:09:49Z) Resolution: fixed Priority: normal Severity: major Version: 4.06.0 Fixed in version: 4.07.0+dev/beta2/rc1/rc2 Category: typing Monitored by:@gasche
Bug 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
in
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
The text was updated successfully, but these errors were encountered:
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.
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...
Original bug ID: 7668
Reporter: furuse
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2017-11-06T07:09:49Z)
Resolution: fixed
Priority: normal
Severity: major
Version: 4.06.0
Fixed in version: 4.07.0+dev/beta2/rc1/rc2
Category: typing
Monitored by: @gasche
Bug 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) xsin
part [] [] xs
let f xs : (int list * int list) = partition_map (fun x -> if x then
Left () else
Right ()) xsSteps 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 listval f : bool list -> int list * int list
The text was updated successfully, but these errors were encountered: