From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <nicolas@incubaid.com>
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 042F87F986
	for <caml-list@sympa.inria.fr>; Sun, 29 Jun 2014 00:55:36 +0200 (CEST)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  nicolas@incubaid.com) identity=pra; client-ip=74.125.82.45;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="nicolas@incubaid.com";
  x-sender="nicolas@incubaid.com";
  x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  nicolas@incubaid.com) identity=mailfrom;
  client-ip=74.125.82.45;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="nicolas@incubaid.com";
  x-sender="nicolas@incubaid.com";
  x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@mail-wg0-f45.google.com) identity=helo;
  client-ip=74.125.82.45;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="nicolas@incubaid.com";
  x-sender="postmaster@mail-wg0-f45.google.com";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AkwBAJZHr1NKfVItlGdsb2JhbABag1+DSMNkFg8BAQEBBwsLCRIqhBwRgQsCJgI2AQUBIjWIIAQBCJlCgxJqiyedHRMECoEhkFqBTAWhZIsGQYMwgUSBbiQ
X-IPAS-Result: AkwBAJZHr1NKfVItlGdsb2JhbABag1+DSMNkFg8BAQEBBwsLCRIqhBwRgQsCJgI2AQUBIjWIIAQBCJlCgxJqiyedHRMECoEhkFqBTAWhZIsGQYMwgUSBbiQ
X-IronPort-AV: E=Sophos;i="5.01,568,1400018400"; 
   d="scan'208";a="82715507"
Received: from mail-wg0-f45.google.com ([74.125.82.45])
  by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 29 Jun 2014 00:55:35 +0200
Received: by mail-wg0-f45.google.com with SMTP id l18so6552146wgh.4
        for <caml-list@inria.fr>; Sat, 28 Jun 2014 15:55:35 -0700 (PDT)
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=1e100.net; s=20130820;
        h=x-gm-message-state:message-id:subject:from:to:date:content-type
         :mime-version:content-transfer-encoding;
        bh=SUfxnnIRBlY7ujel9dtfTi362wWt8eD+g+iCmjxi9K8=;
        b=mkmP7/AptjUWbEZ63PXHgIsbcVCe05f7IJOVlroFUMJeSDrZ+biBVQ8Yb3KYkFiUGU
         dCZ3/hzRV5mzyA2qnprOskoUqPzEfdCX8P5IzPKAGI8Z0gGko0YZmEG5c1UatgSYfWp9
         6rfut+7P4714KJ0pbj7IBchIXnkuEnyT3LkSU7PdFNcLz6uDix1ADVKypgBBWMZ9jjfc
         tmnx6ce0JhgxOoYVeqt1RfjcHtAjNX23oLZY0vZs6n5nbELCpwh9NFFsQp9K000QAhV3
         lNtxyYj1j4+v0sXuwA26DdwnG1+JZKlqd0uZKQXk4lgydC6wws9772Ok6naYZA4uE+3L
         NLYg==
X-Gm-Message-State: ALoCoQlRVBeYAkVcneE91zXbnC3qVLiA14thoLPY3eI+kAkmJ9pHQL85et9W1sE3yVrK3pTPZmEc
X-Received: by 10.194.174.35 with SMTP id bp3mr25778506wjc.33.1403996135017;
        Sat, 28 Jun 2014 15:55:35 -0700 (PDT)
Received: from [192.168.123.173] (78-20-0-121.access.telenet.be. [78.20.0.121])
        by mx.google.com with ESMTPSA id gc5sm12738937wic.6.2014.06.28.15.55.33
        for <caml-list@inria.fr>
        (version=TLSv1 cipher=RC4-SHA bits=128/128);
        Sat, 28 Jun 2014 15:55:34 -0700 (PDT)
Message-ID: <1403996132.26873.18.camel@chi.nicolast.be>
From: Nicolas Trangez <nicolas@incubaid.com>
To: Caml-list <caml-list@inria.fr>
Date: Sun, 29 Jun 2014 00:55:32 +0200
Content-Type: text/plain; charset="UTF-8"
X-Mailer: Evolution 3.10.4 (3.10.4-2.fc20) 
Mime-Version: 1.0
Content-Transfer-Encoding: 7bit
Subject: [Caml-list] Strange interaction between recursive modules, GADT
 exhaustiveness checking and type-checking?

All,

I was working on some code lately (admittedly, pushing some boundaries
w.r.t. recursive modules & GADTs), and got some confusing results.

All of this using OCaml 4.01.0, using `-w +A -warn-error +A`.

I tried to break it down to a small test-case, which you can find at
https://gist.github.com/NicolasT/3a6ef50d5607b744206b

The first case, implemented in module `W`, works as expected. No
warnings about a pattern match for `W (BB, _)` missing in `W.f`. Jay!

When doing something fairly similar in a couple of recursive modules
below, things become confusing. The compiler warns about a missing case
for `W (T.BB, _)` in `S.f`, as noted above it, whilst I think that
pattern shouldn't even type-check... I validated this by adding some
code at the end (in the `demo` function), trying to call `S.f` with a
`B.b S.w` argument, and this fails (as expected & desired). So why would
I be forced, or even allowed, to match on this case in `S.f` at all?

Nicolas