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
Comments
Comment author: @lpw25
I'm pretty sure you meant: (x :> ('a, abc) result);; do you still get an error with |
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:
Characters 1-2: 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 |
Comment author: @ivg OK, it looks like that my attempt to limit the issue to minimal example failed. The following program typechecks:
But, if I will use core_kernel 113.33.01, then the program doesn't typecheck:
With the following error: ocamlfind c -package core_kernel abc.ml Compilation exited abnormally with code 2 at Fri Apr 15 10:20:18 So, I will try to pinpoint the issue. |
Comment author: @ivg Ok, I've managed to reproduce it. So the core_kernel library uses So, if I understood everything correctly this is a bug on core_kernel side. Thanks everyone! |
Comment author: @garrigue Bug was not in ocaml itself. |
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
andabc
, 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 'bEven 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 typesub = < a : unit; b : unit >
Additional information
It still works for row-types, for example, if we define types
sub
andsup
: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);;
The text was updated successfully, but these errors were encountered: