Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007668OCamltypingpublic2017-11-05 13:452017-11-06 09:21
Reporterfuruse 
Assigned Togarrigue 
PrioritynormalSeveritymajorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.06.0 
Target VersionFixed in Version4.07.0+dev 
Summary0007668: -principal is broken with polymorphic variants.
DescriptionThe 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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0018640)
garrigue (manager)
2017-11-06 03:38

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.
(0018641)
furuse (reporter)
2017-11-06 07:23
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?

(0018642)
garrigue (manager)
2017-11-06 08:09

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...
(0018643)
furuse (reporter)
2017-11-06 09:21

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

- Issue History
Date Modified Username Field Change
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
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
Powered by Mantis Bugtracker