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.5 required=5.0 tests=AWL,DNS_FROM_RFC_POST, DNS_FROM_SECURITYSAGE,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 D5D6DBB84 for ; Sat, 1 Nov 2008 20:41:27 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjMBAKtNDElKfVwblGdsb2JhbACTVj4BAQEBCQkKCQ+oaYEAijIBAwEDg0+DLg X-IronPort-AV: E=Sophos;i="4.33,527,1220220000"; d="scan'208";a="31015091" Received: from qw-out-2122.google.com ([74.125.92.27]) by mail4-smtp-sop.national.inria.fr with ESMTP; 01 Nov 2008 20:41:27 +0100 Received: by qw-out-2122.google.com with SMTP id 9so1569331qwb.15 for ; Sat, 01 Nov 2008 12:41:26 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from :user-agent:mime-version:to:cc:subject:references:in-reply-to :content-type:content-transfer-encoding; bh=f+bpHR5TBLKuye7Mj1q1bSiyD97O2vQSAQen2loaGow=; b=d36JVhKRzaIiw+AsqWW1vtj/QBoq/q6xfK6b9gq3xTYWjt5kfI7+/J53zkgM/UAX2B TekkjSH9g0IgmV6O0QXDbUyoy4xqmsh7u6ZQK1QCntdWb/+iWjDakOe9rCjr173XjF14 /TG+8/gfL3IwThbpfXq3l0Sl8/xqix7PIRPbU= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:user-agent:mime-version:to:cc:subject :references:in-reply-to:content-type:content-transfer-encoding; b=rWtBW36MhBT+5tLiFKMBP93TRso4ZasoKRXyl6Zh92HkGmdvGnE85+xQ3zetcb7M1t a2scYMfL8h8APYGQb5CZJ+PjImtOR4/5iuoZyGPlkh6seMNr4ujlKa/FeW25AN5SOmJX 79ReRrWtI6CaoqjQbSsw5CvCmTHuIoUPqUs8g= Received: by 10.215.41.10 with SMTP id t10mr10358614qaj.62.1225568486048; Sat, 01 Nov 2008 12:41:26 -0700 (PDT) Received: from ?192.168.0.11? (ppp-70-242-67-240.dsl.stlsmo.swbell.net [70.242.67.240]) by mx.google.com with ESMTPS id 30sm6555540yxk.4.2008.11.01.12.41.24 (version=TLSv1/SSLv3 cipher=RC4-MD5); Sat, 01 Nov 2008 12:41:25 -0700 (PDT) Message-ID: <490CB0E3.5030602@gmail.com> Date: Sat, 01 Nov 2008 14:41:23 -0500 From: Edgar Friendly User-Agent: Thunderbird 2.0.0.17 (X11/20080925) MIME-Version: 1.0 To: Jacques Garrigue Cc: dra-news@metastack.com, caml-list@yquem.inria.fr Subject: Re: [Caml-list] Private types References: <5687D906367C49F981398A97A5966E09@countertenor> <20081031.090842.254669920.garrigue@math.nagoya-u.ac.jp> <490BB657.5050301@gmail.com> <20081101.190036.135520839.garrigue@math.nagoya-u.ac.jp> In-Reply-To: <20081101.190036.135520839.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; inference:01 subtyping:01 casts:01 edgar:98 wrote:01 typing:01 caml-list:01 algorithm:01 variables:02 variables:02 garrigue:03 garrigue:03 seems:03 jacques:03 jacques:03 Jacques Garrigue wrote: > If we limit ourselves to the case where both [x] and [y] contrain no > type variables, this si not particularly difficult. However whether > they will contain type variables or not depends heavily on how the > type inference algorithm proceeds. > > If they contain type variables, then the situation becomes much more > muddled, as these type variables may get instantiated by the subtyping > check, and not necessarily as expected. So typing becomes rather > unpredictable... > > Jacques Garrigue We've reached the end of my intuition - I admit I get stuck thinking about automatic casts with type variables. I can only point out that for an appropriate definition of "expected" (as in "found type x but expected type y"), one will always get the expected type. :) If the line in the sand has to be drawn somewhere (between auto-subtyping and not), this seems a simple and effective place to do so. E.