From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id AE6A05D5 for ; Thu, 5 Dec 2019 10:47:09 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.69,281,1571695200"; d="asc'?scan'208,217";a="417854380" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 05 Dec 2019 11:47:08 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 8EC3B7F3A9; Thu, 5 Dec 2019 11:47:08 +0100 (CET) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 396797F332 for ; Tue, 3 Dec 2019 22:50:51 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=madroach@gmerlin.de; spf=Pass smtp.mailfrom=madroach@gmerlin.de; spf=None smtp.helo=postmaster@mout.kundenserver.de IronPort-PHdr: =?us-ascii?q?9a23=3AspwyyBzT7Y5me2TXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?1OMUIJqq85mqBkHD//Il1AaPAdyArasb1KGP7vuocFdDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZr?= =?us-ascii?q?KeTpAI7SiNm82/yv95HJbAhEmTSwbalvIBi0rwjdudQajItsJ60s1hbHv3xEdv?= =?us-ascii?q?hMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTD?= =?us-ascii?q?QhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlS?= =?us-ascii?q?EKPCM7/m7KkMx9lKxVrhK/qRJiwIDbb52aO+dlc6PSYd8WWXBMUtpNWyFDBI63?= =?us-ascii?q?cosBD/AGPeZdt4TwuVsOrQG/BQm3GOPvzSdIhn/o0q0gzu8uEgDG3AklH90Qqn?= =?us-ascii?q?TUqc/6NKEUUeuoy6TIyC/MYO5M2Tf68ofHbhAhrOqDXbJ1b8XR000vFwLDjlmK?= =?us-ascii?q?tIPqISqY2+IQuGaV6OpgUPigi28hqwxprTivw9kjipPNhoIUzFDI7zh2z5gzKN?= =?us-ascii?q?alS0B7ecapHIVNuy2ELYd6XN0uTmNytConyLAKo4O3cSYSxJkkxxPTceKLf5WW?= =?us-ascii?q?7h75UOucLy10iG9ldb+5mh2861KvyvfmWcmxyFtKrjRKkt3Ltn0V0hzT7dWHSu?= =?us-ascii?q?dn8keixDaP0R3c5f9CIUAvi6XbMYAhzaAqlpYJrEvMADf6mETwjKCIakUp4vak?= =?us-ascii?q?5/n5brn8uJOQKY15hhvjPqksgMCzHOo1PhALX2eB+OS80LPj/Vf+QLVPlvA2l7?= =?us-ascii?q?PWv43AJcQcvKG2Hw9V350s6xa6ETimytAYnXgBLF5fZR2IkZDlO0vSL/DgEfe/?= =?us-ascii?q?n1OsnS93yP/cO73hBozBLnzCkLf6YbZw8FVcyQo2zdBH/Z1YELABIPTpWk/wrt?= =?us-ascii?q?PUFBE5Mxbni9rgXd5004dbXWOUHoeYNrnTuBmG/LEBOe6JMaQVojfmN/895/P0?= =?us-ascii?q?xU04nFoQZ6yg251fPHWxEu5hKk6ZSXXpj80FEGFMsgdoH7+is0GLTTMGPyX6ZK?= =?us-ascii?q?k7/DxuUNv7X7eGfZikhfm65An+HpBSYTocWFWLDGuudJiCV/oKcy+IPMJ71DAJ?= =?us-ascii?q?B+D4Gt0RkCq2vQq/8IJJa+/d+ykWr5XmjYIn6OjejxUz83p4ApbEij3ffyRPhm?= =?us-ascii?q?oNAgQO8uVnu0UkkAWM1KVih/1eU9BetatE?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BrFABh2OZdhw0R49RlHgELHIIAgRqBc?= =?us-ascii?q?FUyKpM6VAaBRmeCFoZdkUQJAQMBBwUfDQECAQGGTxwHAQQ0EwIQAQEEAQEBAgE?= =?us-ascii?q?CAwQBEwEBAQgNCQgphT4MQgEQAYFnIoMjgQ4TIYQDAYJSKQEKsnYzijMQgTYBg?= =?us-ascii?q?VKKQxp5gQeBR4IwAYNnhQ6CLASfMI8TgUttA4cbji8ngzSLDotilwiSB4FpTIE?= =?us-ascii?q?ucRQ7gmwJRxEUjQCEDIohQDOBBQEBiRqHXgEB?= X-IPAS-Result: =?us-ascii?q?A0BrFABh2OZdhw0R49RlHgELHIIAgRqBcFUyKpM6VAaBRme?= =?us-ascii?q?CFoZdkUQJAQMBBwUfDQECAQGGTxwHAQQ0EwIQAQEEAQEBAgECAwQBEwEBAQgNC?= =?us-ascii?q?QgphT4MQgEQAYFnIoMjgQ4TIYQDAYJSKQEKsnYzijMQgTYBgVKKQxp5gQeBR4I?= =?us-ascii?q?wAYNnhQ6CLASfMI8TgUttA4cbji8ngzSLDotilwiSB4FpTIEucRQ7gmwJRxEUj?= =?us-ascii?q?QCEDIohQDOBBQEBiRqHXgEB?= X-IronPort-AV: E=Sophos;i="5.69,275,1571695200"; d="asc'?scan'208,217";a="331243646" X-MGA-submission: =?us-ascii?q?MDEmdlXHRgk0m+INtc+6UHCykql+HuYK7vambo?= =?us-ascii?q?wTKuwrhlR424EObaa6fY5FwfVAqGL9Gp83fQNYiu3zNW+9x0Ej+1np41?= =?us-ascii?q?rVcajOG2AHQkslEre/z6WkuMEuDjdg/0H4MVwpBYHmhjwT8npE0H9Has?= =?us-ascii?q?FlPaUndOdCm9fu89TQH1Xoig=3D=3D?= Received: from mout.kundenserver.de ([212.227.17.13]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-GCM-SHA256; 03 Dec 2019 22:50:49 +0100 Received: from mortimer.gmerlin.de ([85.212.93.15]) by mrelayeu.kundenserver.de (mreue108 [212.227.15.183]) with ESMTPSA (Nemesis) id 1M5wY1-1iiYmx39bP-007Vbe for ; Tue, 03 Dec 2019 22:50:48 +0100 Received: from localhost (mortimer.gmerlin.de [local]) by mortimer.gmerlin.de (OpenSMTPD) with ESMTPA id 1851de3a for ; Tue, 3 Dec 2019 22:50:48 +0100 (CET) Date: Tue, 3 Dec 2019 22:50:48 +0100 From: Christopher Zimmermann To: caml-list@inria.fr Message-ID: <20191203215048.GA80518@mortimer.gmerlin.de> Mail-Followup-To: caml-list@inria.fr MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="ucex7ukGtmF7A+6a" Content-Disposition: inline X-Provags-ID: V03:K1:NvjzANiTnAW/+l9Bk2A+yEGKDFJN1xWC+iQQEMf334HgigxkudQ gXxi/nuLxUKR0nmgnfqdIUfXQIlJOpwct2Z1WPBvhAV82i2hfonw8c4ZWm9AcXJ3JxR/si2 XBa9bsgweX7aeB4ZhZwbJQxwLUYAy0xsG0hYMzkEhmA4hEZ4xXa2sUBcXxDtR9qh+VZ+vHo xapEQAUV67GMWMgejX1LQ== X-Spam-Flag: NO X-UI-Out-Filterresults: notjunk:1;V03:K0:XFTxuRgGByM=:e/GrRAbI6QXSnpkM3hlGAR +/hmUbK+V+O/SBOqouIuJpuSm3jxwgUocSEBpiEKI4pjNAg2MMBrEY2wTq6Wt3CoeqyVseU2Y cHVDlj1HC60iZBqneauw4s1AjX0ph4A187Y3rnqRcydNEZYbcHuyW/24whZDLxB+A/GxLNdLI UGrng177T3NhnrsXvXeuBtu8tHN8UhPYc2NPSBe57D6YzJeDkNM4ybbqEdvAPZiAjui0zCu2K 1PIe2zGynl4Mc7GJmf/9io95lYhMgrDDhABwEwa20Z4ziyYxEeGE1t4NWp4ZehJgJNSUfohkV hvED/11WyRk8iNIAmo4SBc4tAV0EHT6i8uflXKVGk4fYGmdqo/MSmDGIpNGBfetkI27TTYeMR SasQhmS0yrBjDyJBtN6fcG6TxczN0Wn+7jEreT5NPWdJ3FGzU9iYe7g/nSEM8yTCWb64xsIHH Ylg7m7zkiLmXnBxYMQRO1Uz9q4WGkFA2L/hbobEJ6l1wsvo8PU2B0SdHgM54ipiYSNprLncbz i5aTttbBogE4N2uLu4EPcigxNkpU26hoh3/uWIHqgctWeUTVxwP1OCdKKIUxeDVXUqP8tlRaS 1cZ9VfRTlRGSIPC6LwyqnRAXC7H7NO4FTIMsFiUtvb4XzgTBayCbs1NESsMbvYMYpVPkCqg1N TRpDu16MdZjkaXTilY1cHYmwrYn34BOp+qZkjQ3F9Eo13fvP5vQkLlpguTESA5Jh1jsD/W+f2 DwBIUs0G0oYGz0wofEj6ff8tmNKldE74Yi7cKYXbiPbdNppvFoes+CqJGJDSo1UHpxGzqrkM6 aDc2+RAvD7a2XlAwBr0CELc+r29prZ3NKXartqF5b3FkcSX4jVoWCtEWP8OMd3vT7sOUrZ35n 8esnGcfb20ZASch9o/xg== X-Validation-by: christopher@gmerlin.de Subject: [Caml-list] Polymorphic variant subtyping riddle Reply-To: Christopher Zimmermann X-Loop: caml-list@inria.fr X-Sequence: 17895 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --ucex7ukGtmF7A+6a Content-Type: multipart/alternative; boundary="OrwSqpoKXVrHuQkB" Content-Disposition: inline --OrwSqpoKXVrHuQkB Content-Type: text/plain; charset=us-ascii; format=flowed Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Hi, I've just encountered a type failure which I can easily solve by adding=20 a subtyping constraint, but fail to see why it is necesarry. The following example code types just fine: ``` type safe =3D [ `A | `B ] type basic =3D [ `A ] let basic :basic =3D `A let of_safe :safe -> char =3D function | `A -> 'a' | `B -> 'b' let relaxed =3D (of_safe : safe -> char :> [< safe ] -> char) let x =3D relaxed basic ``` note that there is no subtyping constraint used in the application of=20 ``relaxed`` function to ``basic``. But an analogous piece of code with more complex polymorphic variant=20 types fails to type: ``` let relaxed =3D (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 =3D [ `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 ] =3D [< `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 =3D [ `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 =3D [ `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 ]=20 The first variant type does not allow tag(s) `Intlit, `Tuple, `Vari= ant ``` The typechecker can be persuaded to let this pass by adding a subtyping=20 constraint: ``` let relaxed =3D (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=20 more complex polymorphic variant type and can be avoided in the=20 simplified experiment. Any insight is appreciated Christopher --=20 http://gmerlin.de OpenPGP: http://gmerlin.de/christopher.pub CB07 DA40 B0B6 571D 35E2 0DEF 87E2 92A7 13E5 DEE1 --OrwSqpoKXVrHuQkB Content-Type: text/html; charset=us-ascii Content-Disposition: inline Content-Transfer-Encoding: quoted-printable HTML E-Mail

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 =3D [ `A | `B ]

type basic =3D [ `A ]

let basic :basic =3D `A

let of_safe :safe -> char =3D function
   | `A -> 'a'
   | `B -> 'b'

let relaxed =3D
   (of_safe
    : safe -> char
    :> [< safe ] -> char)

let x =3D 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 =3D
   (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 =3D
            [ `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 ] =3D
            [< `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 =3D
            [ `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 =3D
            [ `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 ]=20
        The first variant type does not allow tag(s) `Intlit, `Tuple, `Vari=
ant

The typechecker can be persuaded to let this pass by adding a subtyping constraint:

let relaxed =3D
   (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

--OrwSqpoKXVrHuQkB-- --ucex7ukGtmF7A+6a Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEE+CT73l6XX3KFKq8nJS8PWAcyqzQFAl3m2LQACgkQJS8PWAcy qzSSDxAAtl0dssQC9L53KBE2izpfDm1XnwGx+hZdIgvqUSFnBuGKik4AA24PmC0m inF43WS4hjwmIxjIV0tuBFDo1ZPl922xLQP0hbOJoKyFu9mppD2r53x7jCFRr1xg FB/1CREa1vNwByzCeH7jp+ssDb1BBSHSykCu5Vb+Q1ST1+Sxoj2Lm12rYdvyGQwE PBVUTNJEGQo7MlFI7Fxu+dsvV5UNF+kN3zidK6Rotcl/kMVa6fXm8z6OI0X6afdM yZhd4+u09y/ByWsezhAdlvzbJH/AqN/kA63dI3UXpWrWmEpzbyB2w/aORJE/4PRB Kn6uCt2YIvckJBYHznQnuQ4oAlCyti5wKQKtwaXGwuYpskVCchTyeIayhr5yllap i+C9uOYb8kQwG9Gy/r/D278bHselhFZj1d2IBES2Q547nBwwfm5Wjx4G0Q9RMwq6 1ncnR9nTYE9n4N+bp/rDsy+zIa9HMbSlbHr0P/CUhg5mbFJCPtol66HFZUYOJW6N Yjv48AUnzc3k6kXO4Fj4GxxjFXnYR2UhC7Ue5cw20iBN6Bzp+UHQe+cilBHb2Nq5 zZiA4AwDix5F0SfB2W1Lt4+Ovo495spiS+/oMXI0cniqAVh4Yh/1DAK6X7av1jiB NYPFnnN4FfI5ataq4YJYg7Zqbvsk5s7vwA3CGA952i2f4Dy0jhY= =Bpdj -----END PGP SIGNATURE----- --ucex7ukGtmF7A+6a--