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

type equation conceals polymorphic variants subtyping #7229

Closed
vicuna opened this issue Apr 15, 2016 · 5 comments
Closed

type equation conceals polymorphic variants subtyping #7229

vicuna opened this issue Apr 15, 2016 · 5 comments
Assignees
Milestone

Comments

@vicuna
Copy link

vicuna commented Apr 15, 2016

Original bug ID: 7229
Reporter: @ivg
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-09-24T15:32:20Z)
Resolution: not a bug
Priority: normal
Severity: minor
Version: 4.02.3
Target version: 4.03.1+dev
Category: typing
Monitored by: @ivg @gasche @yallop

Bug description

A behavior of polymorphic sum type is changed with respect to the polymorphic variant subtyping, when it is reintroduced via type equation.

Steps to reproduce

Given two types ab and abc, where the former is the subtype of the latter:

type ab = [a | b]
type abc = [ab| `c]

The following program (that uses result library from opam) typechecks:

let a : ab = `a
let x = Result.Error a;;
(x :> ('a,abc) Result.result);;

However, if we reintroduce it with a type equation:

type ('a,'b) result = ('a,'b) Result.result = Ok of 'a | Error of 'b

Then the following program doesn't typecheck:

let a : ab = a let x = Error a;; (x :> ('a, sup) result);; ^ Error: This expression cannot be coerced to type ('a, sup) result = ('a, sup) Result.result; it has type ('a, ab) result = ('a, ab) Result.result but is here used with type ('a, < a : unit; .. > as 'b) Result.result Type ab = [ a | `b ] is not compatible with type 'b

Even we try a full coercion:

(x : ('a,sub) result :> ('a, sup) result);;
^
Error: This expression has type ('a, ab) result = ('a, ab) Result.result
but an expression was expected of type
('a, sub) result = ('a, sub) Result.result
Type ab = [ a | b ] is not compatible with type
sub = < a : unit; b : unit >

Additional information

It still works for row-types, for example, if we define types sub and sup:

type sub = <a : unit; b : unit>
type sup =

The following program will typecheck:

let sub : sub = object method a = () method b = () end
let x = Error sub
(x :> ('a, sup) result);;

@vicuna
Copy link
Author

vicuna commented Apr 15, 2016

Comment author: @lpw25

(x :> ('a, sup) result);;
^
Error: This expression cannot be coerced to type
('a, sup) result = ('a, sup) Result.result;
it has type ('a, ab) result = ('a, ab) Result.result
but is here used with type ('a, < a : unit; .. > as 'b) Result.result
Type ab = [ a | b ] is not compatible with type 'b

I'm pretty sure you meant:

(x :> ('a, abc) result);;

do you still get an error with abc instead of sup?

@vicuna
Copy link
Author

vicuna commented Apr 15, 2016

Comment author: @ivg

Update: Damn, looks like that I confused myself in the toplevel. So it was an error in my attempt to pinpoint the issue. The issue still exists. This note can be skipped.

This was the original interaction:

# type ('a,'b) result = ('a,'b) Result.result = Ok of 'a | Error of 'b;;
type ('a, 'b) result = ('a, 'b) Result.result = Ok of 'a | Error of 'b
# let x = Error x;;
val x : ('a, ('b, ab) Result.result) result = Error (Result.Error `a)

# (x :> ('a, abc) result);;
Characters 1-2:
(x :> ('a, abc) result);;
 ^
Error: This expression cannot be coerced to type
     ('a, abc) result = ('a, abc) Result.result;
   it has type
     ('a, ('b, ('c, ab) Result.result) result) result =
       ('a, ('b, ('c, ab) Result.result) result) Result.result
   but is here used with type ('a, [< abc ] as 'd) Result.result
   Type
     ('b, ('c, ab) Result.result) result =
       ('b, ('c, ab) Result.result) Result.result
   is not compatible with type 'd = [< `a | `b | `c ] 
# (x : ('a,ab) result :> ('a, abc) result);;

Characters 1-2:
(x : ('a,ab) result :> ('a, abc) result);;
^
Error: This expression has type
('a, ('b, ('c, ab) Result.result) result) result =
('a, ('b, ('c, ab) Result.result) result) Result.result
but an expression was expected of type
('a, ab) result = ('a, ab) Result.result
Type
('b, ('c, ab) Result.result) result =
('b, ('c, ab) Result.result) Result.result
is not compatible with type ab = [ a | b ]

Tried to make it nice and failed :) If you need I can just upload a test ml files.

Btw, this issue breaks my programs, after core suite in version 113.33 switched from their own result type, to the Result.result and introduced it with the type equation.

@vicuna
Copy link
Author

vicuna commented Apr 15, 2016

Comment author: @ivg

OK, it looks like that my attempt to limit the issue to minimal example failed. The following program typechecks:

type ('a,'b) result = ('a,'b) Result.result = Ok of 'a | Error of 'b
type ab = [`a | `b]
type abc = [ab| `c]
let a : ab = `a
let x = Error a
let _ = (x :> ('a,abc) result)

But, if I will use core_kernel 113.33.01, then the program doesn't typecheck:

open Core_kernel.Std

type ab = [`a | `b]
type abc = [ab| `c]

let a : ab = `a

let x = Error a

let _ = (x :> ('a,abc) Result.t)

With the following error:

ocamlfind c -package core_kernel abc.ml
File "abc.ml", line 10, characters 9-10:
Error: This expression cannot be coerced to type
('a, abc) Core_kernel.Std.Result.t =
('a, abc) Result_lib.Result.result;
it has type
('a, ab) Core_kernel.Std._result = ('a, ab) Result_lib.Result.result
but is here used with type
('a, abc) Core_kernel.Std.Result.t =
('a, abc) Result_lib.Result.result
Type ab = [ a | b ] is not compatible with type
abc = [ a | b | c ] The first variant type does not allow tag(s) c

Compilation exited abnormally with code 2 at Fri Apr 15 10:20:18

So, I will try to pinpoint the issue.

@vicuna
Copy link
Author

vicuna commented Apr 15, 2016

Comment author: @ivg

Ok, I've managed to reproduce it. So the core_kernel library uses Result_lib.mli that has the following contents: module Result = Result. Unfortunately they do not install result_lib.cmi, so the compiler cannot establish that result is actually an algebraic type and injective and so on.

So, if I understood everything correctly this is a bug on core_kernel side.

Thanks everyone!

@vicuna
Copy link
Author

vicuna commented Apr 15, 2016

Comment author: @garrigue

Bug was not in ocaml itself.

@vicuna vicuna closed this as completed Sep 24, 2017
@vicuna vicuna added the typing label Mar 14, 2019
@vicuna vicuna added this to the 4.03.1 milestone Mar 14, 2019
@vicuna vicuna added the bug label Mar 20, 2019
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