[-- Attachment #1.1: Type: text/plain, Size: 2989 bytes --] Hi, I've just encountered a type failure which I can easily solve by adding a subtyping constraint, but fail to see why it is necesarry. The following example code types just fine: ``` type safe = [ `A | `B ] type basic = [ `A ] let basic :basic = `A let of_safe :safe -> char = function | `A -> 'a' | `B -> 'b' let relaxed = (of_safe : safe -> char :> [< safe ] -> char) let x = relaxed basic ``` note that there is no subtyping constraint used in the application of ``relaxed`` function to ``basic``. But an analogous piece of code with more complex polymorphic variant types fails to type: ``` let relaxed = (conv : Yojson.Safe.t -> ('a, string) Result.t :> [< Yojson.Safe.t] -> ('a, string) Result.t) in relaxed (Basic.from_string s) ``` this is the explanation of the compiler: ``` 477 | (Basic.from_string s) ^^^^^^^^^^^^^^^^^^^^^ Error: This expression has type Basic.t = [ `Assoc of (string * Basic.t) list | `Bool of bool | `Float of float | `Int of int | `List of Basic.t list | `Null | `String of string ] but an expression was expected of type [< Safe.t > `Null `String ] = [< `Assoc of (string * Safe.t) list | `Bool of bool | `Float of float | `Int of int | `List of Safe.t list | `Null | `String of string > `Null `String ] Type Basic.t = [ `Assoc of (string * Basic.t) list | `Bool of bool | `Float of float | `Int of int | `List of Basic.t list | `Null | `String of string ] is not compatible with type Safe.t = [ `Assoc of (string * Safe.t) list | `Bool of bool | `Float of float | `Int of int | `Intlit of string | `List of Safe.t list | `Null | `String of string | `Tuple of Safe.t list | `Variant of string * Safe.t option ] The first variant type does not allow tag(s) `Intlit, `Tuple, `Variant ``` The typechecker can be persuaded to let this pass by adding a subtyping constraint: ``` let relaxed = (conv : Yojson.Safe.t -> ('a, string) Result.t :> [< Yojson.Safe.t] -> ('a, string) Result.t) in relaxed (Basic.from_string s : Yojson.Basic.t :> Yojson.Safe.t) ``` will type just fine. Now I'm confused why the subtyping constraint is only needed for the more complex polymorphic variant type and can be avoided in the simplified experiment. Any insight is appreciated Christopher -- http://gmerlin.de OpenPGP: http://gmerlin.de/christopher.pub CB07 DA40 B0B6 571D 35E2 0DEF 87E2 92A7 13E5 DEE1 [-- Attachment #1.2: Type: text/html, Size: 4313 bytes --] [-- Attachment #2: signature.asc --] [-- Type: application/pgp-signature, Size: 833 bytes --]

Hi, The meaningful difference here is that the type `safe` and `base` are recursive. It is not particularly clear, but the second part of the error message is complaining about the difference of type in the argument of `List. Typically, if your example is extended to: type safe = [ `A of safe | `B | `C ] type basic = [ `A of basic | `B ] let basic :basic = `A `B let of_safe :safe -> char = function | `A _ -> 'a' | `B -> 'b' | `C -> 'c' let relaxed = (of_safe : safe -> char :> [< safe ] -> char) let x = relaxed (basic :> safe) Then the coercion becomes necessary too. — octachron.