caml-list - the Caml user's mailing list
 help / color / Atom feed
* [Caml-list] Polymorphic variant subtyping riddle
@ 2019-12-03 21:50 Christopher Zimmermann
  2019-12-05 11:04 ` Florian Angeletti
  0 siblings, 1 reply; 2+ messages in thread
From: Christopher Zimmermann @ 2019-12-03 21:50 UTC (permalink / raw)
  To: caml-list

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

^ permalink raw reply	[flat|nested] 2+ messages in thread

* Re: [Caml-list] Polymorphic variant subtyping riddle
  2019-12-03 21:50 [Caml-list] Polymorphic variant subtyping riddle Christopher Zimmermann
@ 2019-12-05 11:04 ` Florian Angeletti
  0 siblings, 0 replies; 2+ messages in thread
From: Florian Angeletti @ 2019-12-05 11:04 UTC (permalink / raw)
  To: caml-list

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.



^ permalink raw reply	[flat|nested] 2+ messages in thread

end of thread, back to index

Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-12-03 21:50 [Caml-list] Polymorphic variant subtyping riddle Christopher Zimmermann
2019-12-05 11:04 ` Florian Angeletti

caml-list - the Caml user's mailing list

Archives are clonable:
	git clone --mirror http://inbox.vuxu.org/caml-list
	git clone --mirror https://inbox.ocaml.org/caml-list

Example config snippet for mirrors

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.caml-list


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git