From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: *** X-Spam-Status: No, score=3.1 required=5.0 tests=AWL,DNS_FROM_RFC_POST, SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id B6AEBBBAF for ; Wed, 25 Mar 2009 22:39:32 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: At8BABdByknRVcbqk2dsb2JhbACVPz8BAQEBCQkKCREDrDKBB49HAQMBA4NyBg X-IronPort-AV: E=Sophos;i="4.38,421,1233529200"; d="scan'208";a="37210815" Received: from rv-out-0506.google.com ([209.85.198.234]) by mail4-smtp-sop.national.inria.fr with ESMTP; 25 Mar 2009 22:39:31 +0100 Received: by rv-out-0506.google.com with SMTP id f6so1621740rvb.57 for ; Wed, 25 Mar 2009 14:39:30 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:from:to :content-type:content-transfer-encoding:mime-version:subject:date :x-mailer; bh=UqdSblkRRCOSXYKKw4b+nYAICt/aWG3iEopfKiiOsOU=; b=ResBfnc/7XqMWBF7224I30PkFkPfBRsaOVlXPplomstiRogowbktjphTAe0Pcu/21Y zUhHL5m+O39yL1EWgRD5r5Ha779DZVe9eLME4Xmy+89ekTk0oBifC+MozLq5Nw77Brv3 EB3JqK93ramBDRvLCpgea3mCaaY3CnSd/30+g= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:from:to:content-type:content-transfer-encoding :mime-version:subject:date:x-mailer; b=SECTkERdIU8z+k8/s9ivlJNyXyO1m6JnDDGNnCGEAM9WoR8lyDFPcAC3LzHSVpxK4l BSBvh36MwHXvdGBy4oKDHkdLgrYFLOhbHd3rhev+d1B52ifXstI0ObGYtTpskmp2Wb2P b1VU9dusZy5XnFi1BT9pn+EBq9RV55e6veY/A= Received: by 10.114.240.13 with SMTP id n13mr57065wah.41.1238017170449; Wed, 25 Mar 2009 14:39:30 -0700 (PDT) Received: from timesink.corp.631h.metaweb.com (nat08.sjc1.metaweb.com [208.68.111.103]) by mx.google.com with ESMTPS id l28sm8232252waf.30.2009.03.25.14.39.29 (version=TLSv1/SSLv3 cipher=RC4-MD5); Wed, 25 Mar 2009 14:39:29 -0700 (PDT) Message-Id: From: Warren Harris To: OCaml Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v930.3) Subject: polymorphic variants and recursive functions Date: Wed, 25 Mar 2009 14:39:28 -0700 X-Mailer: Apple Mail (2.930.3) X-Spam: no; 0.00; variants:01 recursive:01 variants:01 compiler:01 recursive:01 satisfiable:01 overlooking:01 constructors:01 higher-order:01 constructors:01 coercions:01 coercions:01 val:01 val:01 warren:98 I stumbled upon a little puzzle that I can't quite work out. I'm trying to use polymorphic variants as phantom types and in one particular situation involving a polymorphic type with an invariant type parameter (Lwt.t) the compiler is unhappy with a set of mutually recursive functions. I can appreciate at some level that an invariant type parameter will cause the phantom types to become unsatisfied, but in this particular case my sense is that they should be satisfiable, and feel that I might be overlooking an appropriate coercion. Perhaps someone here can lend a hand... Here's the best I can do at creating a simple example: First, here's the case the works... I would like a family of constructors, including two higher-order ones, 'arr' and 'obj', such that 'arr' can only be constructed from 'obj' instances: let obj (v:[> `V]) : [`O|`V] = `V let arr (v:[> `O]) : [`V] = `V let v0 : [`V] = `V This works as expected: let ok1 = obj v0 let ok2 = arr (obj v0) let ok3 = obj (arr (obj v0)) and fails as expected: let fail1 = arr v0 ^^ This expression has type [ `V ] but is here used with type [> `O ] The first variant type does not allow tag(s) `O I can now use these constructors in conjunction with some mutually- recursive functions (coercions are needed): let rec eval = function | `Arr v -> (eval_arr v : [`V] :> [> `V]) | `Obj v -> (eval_obj v : [`V|`O] :> [> `V]) and eval_arr v = arr (eval_obj v) and eval_obj v = obj (eval v) although oddly, the coercions don't seem to affect the final type of eval: val eval : ([< `Arr of 'a | `Obj of 'a ] as 'a) -> [ `O | `V ] = val eval_arr : ([< `Arr of 'a | `Obj of 'a ] as 'a) -> [ `V ] = val eval_obj : ([< `Arr of 'a | `Obj of 'a ] as 'a) -> [ `O | `V ] = Now the case that doesn't work: Introducing 'a Lwt.t into the above: open Lwt let obj (v:[> `V]) : [`O|`V] Lwt.t = return `V let arr (v:[> `O]) : [`V] Lwt.t = return `V let v0 : [`V] Lwt.t = return `V let ok1 = v0 >>= obj let ok2 = v0 >>= obj >>= arr let ok3 = v0 >>= obj >>= arr >>= obj (*let fail1 = v0 >>= arr*) let rec eval = function | `Arr v -> (eval_arr v : [`V] Lwt.t :> [> `V] Lwt.t) | `Obj v -> (eval_obj v : [`V|`O] Lwt.t :> [> `V] Lwt.t) and eval_arr v = eval_obj v >>= arr and eval_obj v = eval v >>= obj | `Obj v -> (eval_obj v : [`V|`O] Lwt.t :> [> `V] Lwt.t) ^^^^^^^^^^ This expression has type [ `O | `V ] Lwt.t but is here used with type [ `V ] Lwt.t The second variant type does not allow tag(s) `O Any suggestions would be much appreciated, Warren