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

Assumed inequalities involving private rows #5989

Closed
vicuna opened this issue Apr 18, 2013 · 3 comments
Closed

Assumed inequalities involving private rows #5989

vicuna opened this issue Apr 18, 2013 · 3 comments
Assignees
Labels
bug typing typing-GADTS GADT typing and exhaustiveness bugs

Comments

@vicuna
Copy link

vicuna commented Apr 18, 2013

Original bug ID: 5989
Reporter: @yallop
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:18:39Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.00.1
Fixed in version: 4.00.2+dev
Category: typing
Related to: #5981 #5997
Child of: #5998
Monitored by: @gasche

Bug description

$ cat private_row_inequality.ml
type (_, _) t =
Any : ('a, 'b) t
| Eq : ('a, 'a) t

module M :
sig
type s = private [> A] val eq : (s, [A | B]) t end = struct type s = [A | `B]
let eq = Eq
end

let f : (M.s, [A | B]) t -> string = function
| Any -> "Any"

let () = print_endline (f M.eq)
$ ocaml private_row_inequality.ml
Any

@vicuna
Copy link
Author

vicuna commented Apr 18, 2013

Comment author: @garrigue

Indeed, this is the same problem as 5989: it seems that I misunderstood the relation between unify and mcomp.
In this case again, mcomp is correct, but unify3 itself needs to implement the same behavior.
While we're at that, we should also check object rows...

@vicuna
Copy link
Author

vicuna commented Apr 18, 2013

Comment author: @garrigue

Fixed in trunk and 4.00, revisions 13578 and 13581.

@vicuna
Copy link
Author

vicuna commented Apr 18, 2013

Comment author: @yallop

Excellent; thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug typing typing-GADTS GADT typing and exhaustiveness bugs
Projects
None yet
Development

No branches or pull requests

3 participants