Skip to content
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

-principal is broken with polymorphic variants. #7668

Closed
vicuna opened this issue Nov 5, 2017 · 4 comments
Closed

-principal is broken with polymorphic variants. #7668

vicuna opened this issue Nov 5, 2017 · 4 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Nov 5, 2017

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

@vicuna
Copy link
Author

vicuna commented Nov 6, 2017

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Nov 6, 2017

Comment author: furuse

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?

@vicuna
Copy link
Author

vicuna commented Nov 6, 2017

Comment author: @garrigue

Fixed in trunk at commit 43d77ff.

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...

@vicuna vicuna closed this as completed Nov 6, 2017
@vicuna
Copy link
Author

vicuna commented Nov 6, 2017

Comment author: furuse

Thank you for the fix! I turn off -principal for my compiler hacking for now.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants