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 CA0C981799 for ; Fri, 26 Jul 2013 22:28:01 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.54; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.54 as permitted sender) identity=mailfrom; client-ip=209.85.214.54; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; 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-bk0-f54.google.com) identity=helo; client-ip=209.85.214.54; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f54.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgICAGLb8lHRVdY2k2dsb2JhbABbgztQvV6BEQgWDgEBAQEHCwsJFAQkgiQBAQQBJxkBGx0BAwELBgULDS4hAQERAQUBHAYTCId1AQMJBgybNYxPgn+EOgoZJw1kh3QBBQyNCYJoB4QFA5V2gWmBKYp9g0EWKYQ8Og X-IPAS-Result: AgICAGLb8lHRVdY2k2dsb2JhbABbgztQvV6BEQgWDgEBAQEHCwsJFAQkgiQBAQQBJxkBGx0BAwELBgULDS4hAQERAQUBHAYTCId1AQMJBgybNYxPgn+EOgoZJw1kh3QBBQyNCYJoB4QFA5V2gWmBKYp9g0EWKYQ8Og X-IronPort-AV: E=Sophos;i="4.89,753,1367964000"; d="scan'208";a="27462206" Received: from mail-bk0-f54.google.com ([209.85.214.54]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 26 Jul 2013 22:28:01 +0200 Received: by mail-bk0-f54.google.com with SMTP id it19so1292761bkc.27 for ; Fri, 26 Jul 2013 13:28:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=8dnjXaVbjIrBHSRV3+nndmdwtmWx0vVyivSHcu7FVEg=; b=u745R0ujd46uvDDda0nOJoewIbIPg/iHvrI7lT0Bsw/1iXn3l6OzW1m2by5hZFFLfK WVYPBcfyPqFrKtsEnAaN/pAWFs4cUKrau45xNfo7yfWNgo9xVAPcyO7j7S/7IMYhl8l7 Z2nOSgkVS7/hSd96Cn1Kx0voHghy27jxqVOPNfDKSC7y8Iz4wdc075ITd6WTst2bDj0n l7DGaor9hsVwPWaM0GstDhKeW6seOdfZpaWLY2DULUDjT+GCoRDRdFvcq5OtKo5mglN4 /Y+mE6swlb9FYNH7XTkRd7qcFJ9kbp0v2rA+u89luQVwE72AOQGypuuuK//bCs/6fBQW Pinw== X-Received: by 10.204.241.75 with SMTP id ld11mr2762048bkb.35.1374870480575; Fri, 26 Jul 2013 13:28:00 -0700 (PDT) MIME-Version: 1.0 Received: by 10.204.20.131 with HTTP; Fri, 26 Jul 2013 13:27:20 -0700 (PDT) In-Reply-To: References: From: Gabriel Scherer Date: Fri, 26 Jul 2013 22:27:20 +0200 Message-ID: To: Mathieu Barbin Cc: caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] GADT: question about inference This is explained in the manual (emphasis mine) http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc85 > The constraints associated to each constructor can be recovered through pattern-matching. > Namely, **if the type of the scrutinee of a pattern-matching contains a locally abstract type**, > this type can be refined according to the constructor used. The only types that can be refined by the type equalities introduced by GADT are locally abstract types, the variable-like constructor "a" introduced by the "(type a)" and "foo : type a . bar" syntaxes. Your first two examples have no locally abstract type, only type members of modules, so there was no GADT refinement happening. On Fri, Jul 26, 2013 at 7:15 PM, Mathieu Barbin wrote: > Hello, > > Playing around with a reduced version of a dynamic types, I ran into some > type errors, and I feel that I'd love to understand more about the way the > inference work: > > type _ ty = Int : int ty | String : string ty > > module H : sig > type t > val ty : t ty > end = struct > type t = int > let ty = Int > end > > (* from now, trying various implementation for [f] *) > > let f : H.t -> int = > match H.ty with > | Int -> (fun (a : H.t) -> (a : int)) > | _ -> assert false > ;; > Error: This expression has type H.t but an expression was expected of type > int > > let f : H.t -> int = fun (a : H.t) -> > match H.ty with > | Int -> (a : int) > | _ -> assert false > ;; > Error: This expression has type H.t but an expression was expected of type > int > > let f : H.t -> int = > let aux : type a. a ty -> a -> int = function > | Int -> (fun a -> a) > | _ -> assert false > in > aux H.ty > ;; > > (* val f : H.t -> int = *) > > I can't quite come up with a clear mental model of why in-lining the pattern > matching in the first versions of [f]t would not type check. I tried adding > some more type coercions without great success. I'd be very grateful to get > some feed back about this restriction. > > Thanks, > Mathieu >