From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 7A8E57ED25 for ; Fri, 19 Jul 2013 12:29:42 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of ivg@ieee.org) identity=pra; client-ip=209.85.215.43; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of ivg@ieee.org designates 209.85.215.43 as permitted sender) identity=mailfrom; client-ip=209.85.215.43; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-la0-f43.google.com) identity=helo; client-ip=209.85.215.43; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="postmaster@mail-la0-f43.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApgCAEQU6VHRVdcrk2dsb2JhbABasloBkwYWDgEBAQEHCwsJFAQkglITezQBJAEFAYhFBJV2gn6dTZAsg2YDiSKOO49oP4Q9 X-IPAS-Result: ApgCAEQU6VHRVdcrk2dsb2JhbABasloBkwYWDgEBAQEHCwsJFAQkglITezQBJAEFAYhFBJV2gn6dTZAsg2YDiSKOO49oP4Q9 X-IronPort-AV: E=Sophos;i="4.89,700,1367964000"; d="scan'208";a="26606702" Received: from mail-la0-f43.google.com ([209.85.215.43]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 19 Jul 2013 12:29:41 +0200 Received: by mail-la0-f43.google.com with SMTP id fh20so1570535lab.30 for ; Fri, 19 Jul 2013 03:29:41 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=20120113; h=from:to:subject:date:message-id:mime-version:content-type :x-gm-message-state; bh=PkPH88IfJlcNgMbzGZcedeEbnIpXXAzrObK01oLKzjc=; b=k89X88HC+7NSaZNL+khuYlL/swCO+SlNGL3N4GpbuLdbzeuyIO2rzdSFzTVKER2zKf BEK/psLEVAIBtm/+QrHXCXouZmtjU6naYeYsG78PJoXbrYmaeKY4wP/M7ItYjPzJip80 uxnty80kYvpuT3LKigSISo3vSAlmaE7+PELM+skqRh/gXfZ+FajStW4XIK4A20hZAJ1g XeG7f6BaFkBaZ5LBTwJ9RHe7XhalXFAGoJt4KdU6zwUDLjkQPkqmxj4dq8aQyWT9h7aS /+uxbEWRYaroHEZ4SLYDgvnfNTX16WN2NtTggsCspPjEpZD1Uo6Yb00kGXrBNwaPppEt YOSA== X-Received: by 10.152.121.73 with SMTP id li9mr7211099lab.42.1374229780797; Fri, 19 Jul 2013 03:29:40 -0700 (PDT) Received: from golf.niidar.ru.niidar.ru ([109.188.124.235]) by mx.google.com with ESMTPSA id m1sm5682426lag.3.2013.07.19.03.29.39 for (version=TLSv1.1 cipher=RC4-SHA bits=128/128); Fri, 19 Jul 2013 03:29:40 -0700 (PDT) From: Ivan Gotovchits To: caml-list@inria.fr Date: Fri, 19 Jul 2013 14:29:35 +0400 Message-ID: <877ggmx2pc.fsf@golf.niidar.ru> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Gm-Message-State: ALoCoQlz5eKBz6HWjR2Fo/ym4ZYHjP/edoG3EQJdSJI6mgCSquIsb2XXVJuk2hL7Klwq6M9cZZLj Subject: [Caml-list] GADT: equal functions typechecks differently I've found a case when two function, that differs very slightly (almost identical), causes different reactions of a typechecker. For me, this looks like a bug, but may be there is something (well of course there is) that I do not understand: I have two types, an id and a pool of id. Both are protected with phantom type. The definitions is very small, so I will provide them: module Set = Set.Make(struct type t = int let compare = compare end) type 'a pool = { set : Set.t; min : int; max : int; } type 'a id = int type our type ads type ows type ext I define two GADT's and two injections: type _ sys = | Our : our sys | Ows : ows sys | Ads : ads sys | Ext : ext sys type tid = Id : 'a sys * 'a id -> tid type tpool = Pool : 'a sys * 'a pool -> tpool let to_tid sys id = Id (sys,id) let to_tpool sys pool = Pool (sys,pool) Using common idiom (it is common, isn't?) I can typesafely compare my systems. type (_,_) eq = Eq : ('a,'a) eq let try_sys_equal: type a b. (a sys * b sys) -> (a,b) eq option = function | Our,Our -> Some Eq | Ows,Ows -> Some Eq | Ads,Ads -> Some Eq | Ext,Ext -> Some Eq | _ -> None Next, I provide two injections: # let of_tid: type t1. t1 sys -> tid -> t1 id option = fun sys1 (Id (sys2,id)) -> match try_sys_equal (sys1,sys2) with | Some Eq -> Some id | None -> None;; val of_tid : 't1 sys -> tid -> 't1 id option = # let of_tpool: type t1. t1 sys -> tpool -> t1 pool option = fun sys1 (Pool (sys2,pool)) -> match try_sys_equal (sys1,sys2) with | Some Eq -> Some pool | None -> None;; val of_tpool : 't1 sys -> tpool -> 't1 pool option = As you can see, they typechecks. But here is the strange behavior - if I write the first function in a slightly different manner, it typechecks: # let of_tid: type t1 t2. t1 sys -> tid -> t2 id option = fun sys1 (Id (sys2,id)) -> match try_sys_equal (sys1,sys2) with | Some Eq -> Some id | None -> None;; val of_tid : 't1 sys -> tid -> 't2 id option = But if I add the same t2 type to the second function it fails: let of_tpool: type t1 t2. t1 sys -> tpool -> t2 pool option = fun sys1 (Pool (sys2,pool)) -> match try_sys_equal (sys1,sys2) with | Some Eq -> Some pool | None -> None;; Characters 158-162: | Some Eq -> Some pool ^^^^ Error: This expression has type ex#7 pool but an expression was expected of type t2 pool Type ex#7 = t1 is not compatible with type t2 Thank in advance for any clues Ivan