Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005981OCamlOCaml typingpublic2013-04-12 00:262013-04-23 02:07
Reporteryallop 
Assigned Togarrigue 
PrioritynormalSeveritymajorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.00.1 
Target VersionFixed in Version4.01.0+dev 
Summary0005981: Incompatibility check assumes abstracted type constructors are injective
Description$ cat incompat.ml
module F(S : sig type 'a t end) =
struct

  type _ ab =
      A : int S.t ab
    | B : float S.t ab

  let f : int S.t ab -> float S.t ab -> string =
    fun (l : int S.t ab) (r : float S.t ab) -> match l, r with
      | A, B -> "f A B"
end

module M = F(struct type 'a t = unit end)

let () = print_endline M.(f A A)

$ ocaml incompat.ml
f A B
Additional InformationPerhaps related to 5785.
TagsNo tags attached.
Attached Files

- Relationships
related to 0005989resolvedgarrigue Assumed inequalities involving private rows 
child of 0005998assignedgarrigue GADT typing and exhaustiveness bugs 

-  Notes
(0009084)
garrigue (manager)
2013-04-12 12:22

Thanks for this report.
Indeed, while the handling of abstracted constructors was correct in mcomp, the code in unify3 was wrong.

Committed a preliminary fix in trunk. Will merge into 4.00 branch after more tests.

- Issue History
Date Modified Username Field Change
2013-04-12 00:26 yallop New Issue
2013-04-12 12:22 garrigue Note Added: 0009084
2013-04-12 12:22 garrigue Status new => resolved
2013-04-12 12:22 garrigue Fixed in Version => 4.01.0+dev
2013-04-12 12:22 garrigue Resolution open => fixed
2013-04-12 12:22 garrigue Assigned To => garrigue
2013-04-18 14:20 garrigue Relationship added related to 0005989
2013-04-23 02:07 garrigue Relationship added child of 0005998


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker