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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 99E0C7EF38 for ; Fri, 31 Jul 2015 16:32:06 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lukstafi@gmail.com) identity=pra; client-ip=209.85.214.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of lukstafi@gmail.com designates 209.85.214.179 as permitted sender) identity=mailfrom; client-ip=209.85.214.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ob0-f179.google.com) identity=helo; client-ip=209.85.214.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lukstafi@gmail.com"; x-sender="postmaster@mail-ob0-f179.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0C0AQAEhrtVm7PWVdFbhFcGgx2lfgabEgKBKgdMAQEBAQEBEgEBAQEBBgsLCSEuhCQBAQQSEQQZARsdAQMMBgULDQICJgICIQEBEQEFARwGEyKHdgEDEqNTgSw+MYs/gWyCeYsiChknDVeEWAEBAQEGAgEZAQUOgRSEfYUvgk6COQeCaYFDAQSUeIpegWuSD4VkEiOBFxeEDjwxgkwBAQE X-IPAS-Result: A0C0AQAEhrtVm7PWVdFbhFcGgx2lfgabEgKBKgdMAQEBAQEBEgEBAQEBBgsLCSEuhCQBAQQSEQQZARsdAQMMBgULDQICJgICIQEBEQEFARwGEyKHdgEDEqNTgSw+MYs/gWyCeYsiChknDVeEWAEBAQEGAgEZAQUOgRSEfYUvgk6COQeCaYFDAQSUeIpegWuSD4VkEiOBFxeEDjwxgkwBAQE X-IronPort-AV: E=Sophos;i="5.15,584,1432591200"; d="scan'208";a="141708794" Received: from mail-ob0-f179.google.com ([209.85.214.179]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 31 Jul 2015 16:32:05 +0200 Received: by obbop1 with SMTP id op1so55161207obb.2 for ; Fri, 31 Jul 2015 07:32:04 -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=GwGnSGl+sDCR5noehfFn5dkKiLHCadL58pGq+lgg0JE=; b=HUH2ccg0tPINQePFps9Jcedbyu3BFlJMgbpMib0My4LYC4zT0kcXfmXSyIcmGB+Vu5 qHL45yyHe2dfz4/2E7/ePwDy0UdorrifOFTq5G9jz2FzvJOkDXgUS55RYe23u2tC/TfI h6mRaFCX1B9Blnd+eePZBwydPmxZqkUiQWIsI8wSsTJAZU/C9qscoUrSh5YnwiURGvOS nh2yCQOw7ZEmazcOnYOYP+dOwMb+UUaE7IwiQtQmCd+ro/FbjnpgymWin9ukv88jzaTZ G4gnPql+Zo4ftYp0XEnnBasy+m59zRHjiz+a9YRP/Lv/OHaGVklSI0/rfJtbBHYAoHOC OQXA== X-Received: by 10.182.252.66 with SMTP id zq2mr3410096obc.84.1438353124387; Fri, 31 Jul 2015 07:32:04 -0700 (PDT) MIME-Version: 1.0 Received: by 10.202.95.131 with HTTP; Fri, 31 Jul 2015 07:31:45 -0700 (PDT) In-Reply-To: References: From: Lukasz Stafiniak Date: Fri, 31 Jul 2015 16:31:45 +0200 Message-ID: To: Ashish Agarwal Cc: Carl Eastlund , Caml List Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] selecting GADT parameter On the face of it, this is not possible. There must be as many pattern matching branches as there are reachable conditions in the formulation of the type, because only a pattern matching branch introduces a conditional (an implication) into reasoning about types. In particular, you need to pattern match against Tag1 and Tag2 if you don't want to treat the parameter of the type "t" as an abstract type. On Fri, Jul 31, 2015 at 4:18 PM, Ashish Agarwal wrote: > You essentially still have 2 constructors, so this isn't quite what I'm > aiming for. > > > On Fri, Jul 31, 2015 at 9:57 AM, Carl Eastlund > wrote: >> >> Perhaps like this? (Caveat: I typed this straight into gmail, I haven't >> tried to compile or run this code at all.) >> >> type ('a, 'b, 'c) tag = >> | Tag1 : ('a, int, int) tag >> | Tag2 : ('a, string, 'a) tag >> >> type 'a t = >> | Foo : ('a, 'b, 'c) tag * 'a * 'b -> 'c t