[Caml-list] Polymorphic variant subtyping riddle

[Christopher Zimmermann <madroach@gmerlin.de>]

[-- 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 --]