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=0.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 7166FBC6B for ; Fri, 21 Sep 2007 08:52:53 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAN4H80aCNhAB/2dsb2JhbAA X-IronPort-AV: E=Sophos;i="4.20,281,1186351200"; d="scan'208";a="1498623" Received: from kurims.kurims.kyoto-u.ac.jp ([130.54.16.1]) by mail2-smtp-roc.national.inria.fr with ESMTP; 21 Sep 2007 08:54:21 +0200 Received: from localhost (orion [130.54.16.5]) by kurims.kurims.kyoto-u.ac.jp (8.13.8/8.13.8) with ESMTP id l8L6sCfg027232; Fri, 21 Sep 2007 15:54:12 +0900 (JST) Date: Fri, 21 Sep 2007 15:54:02 +0900 (JST) Message-Id: <20070921.155402.213471450.garrigue@math.nagoya-u.ac.jp> To: Christophe.Raffalli@univ-savoie.fr Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] polymorphic variant From: Jacques Garrigue In-Reply-To: <46F35FB3.6060304@univ-savoie.fr> References: <46F28C38.2080801@univ-savoie.fr> <20070921.091337.134531783.garrigue@math.nagoya-u.ac.jp> <46F35FB3.6060304@univ-savoie.fr> X-Mailer: Mew version 4.2 on Emacs 22.1 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; christophe:01 raffalli:01 christophe:01 raffalli:01 univ-savoie:01 unifications:01 inference:01 val:01 syntax:01 val:01 polymorphic:01 typing:01 caml-list:01 jambon:01 jambon:01 From: Christophe Raffalli > > The above behaviour was correctly explained by Martin Jambon, but I'll > > add some detail: > > The type of f is actually an instance of the type of g, where the > > first and second columns of the pattern were unified. The reason for > > that is that in f the 1st line returns the 2nd column, and the 2nd > > line the first column. Since the return type has to be unique, this > > unifies x and y, i.e. the 1st and 2nd columns. > > > > I hope this clarifies the situation. > > > > Jacques Garrigue > > > OK, I understand. But I would prefer if the decision to close or not the > pattern (and therefore > make the last case useless) did not depend upon the right members ... So actually you didn't understand :-) The point here is that the typing for the pattern matching is determined completely independently of the right members. This is only afterwards that some extra unifications may happen, as is always the case with type inference. This is not a "decision", but a natural consequence of the type system. The warning about the useless case is actually a clever trick: rather than immediately checking for useless cases after checking the pattern matching, it waits for the whole expression to be typed, in order to be more accurate. In some way what you are saying is a bit like: # let f (x : [> `A]) (y : [> `B]) = ignore [x;y] ;; val f : ([> `A | `B ] as 'a) -> 'a -> unit = Why are the types for x and y unified, I'd much prefere them to be independent... By the way, as Martin Jambon explained, you can protect you variables against type propagation with the "as" syntax. # let f (`A as x) (`B as y) = [x;y];; val f : [< `A ] -> [< `B ] -> [> `A | `B ] list = Jacques Garrigue