From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q1AACRMP029996
	for <caml-list@sympa-roc.inria.fr>; Fri, 10 Feb 2012 11:12:28 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AlIBAE3tNE9KfVI0imdsb2JhbABDDoUFqlsIIgEBAQoJDQcSBiOCCwIPBBkBGx4DEgMNDwImAiQBEQEFASIBGhqlHgqLJkuCcIUWP4ELAgULgSSKAwgsBQoGBQIEAwQKAQIHBQYBAwgBASWGZoEWBJUwjiM9g0s4
X-IronPort-AV: E=Sophos;i="4.73,395,1325458800"; 
   d="scan'208";a="130846668"
Received: from mail-ww0-f52.google.com ([74.125.82.52])
  by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 10 Feb 2012 11:12:09 +0100
Received: by wgbds10 with SMTP id ds10so2903428wgb.9
        for <caml-list@inria.fr>; Fri, 10 Feb 2012 02:12:09 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=gamma;
        h=mime-version:from:date:message-id:subject:to:content-type
         :content-transfer-encoding;
        bh=ccsd6G+/U9Dq1bBP19Lhp2YkPjeludaftnS+BuC5ueE=;
        b=a/i+QpNia5XK221Lw6DgCLSQG6jFBx9q9kaUe1lVpqpdwI6dao2NwfMGS5Z9FbXKgC
         j4JK+dlM0KVQeGeZM+Z/MAsfNzP0D+S3fidgZ8fTGFci588uaXJlhkhkGWsUiynA28PK
         7x68qhpwaKR+/GBQfvZaM6h6M3H5nNt86oLck=
Received: by 10.180.87.8 with SMTP id t8mr2144077wiz.15.1328868729219; Fri, 10
 Feb 2012 02:12:09 -0800 (PST)
MIME-Version: 1.0
Received: by 10.227.42.208 with HTTP; Fri, 10 Feb 2012 02:11:27 -0800 (PST)
From: Gabriel Scherer <gabriel.scherer@gmail.com>
Date: Fri, 10 Feb 2012 11:11:27 +0100
Message-ID: <CAPFanBHvSWRTbgR-bb5q2DHZtN5Gfa__cVxUhqG_Zx2tm1V4nw@mail.gmail.com>
To: caml users <caml-list@inria.fr>,
        Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q1AACRMP029996
Subject: [Caml-list] Variance of GADT parameters

I've been playing with GADTs and noticed that the condition on
parameter variance is very restrictive.

The two following examples fail:

  type +_ const =
  | Const : int -> int expr

  type +_ expr =
  | Const : 'a -> 'a expr
  | Prod : 'a expr * 'b expr -> ('a * 'b) expr

  Error: In this GADT definition, the variance of some parameter
  cannot be checked

I looked at the source, and this is what I could infer of the current
typer behavior: parameter variance check will fail (on non-invariant
parameters) as soon as they appear *instantiated* (not just
a variable) in one of the GADT branch return type. The two examples
above fail for this reason: `const` parameter is instantiated with int
and `expr` with ('a * 'b).

Would it be possible to relax this condition a bit? Intuitively, I
would say that:
1. variables that do not appear in the instantiations of the return
   type always satisfy their variance constraint (for the branch)
2. variables that appear covariantly in the instantiations of the
   return type should satisfy their constraints on the argument types
3. variables that appaear contravariantly should satisfy the
   *reversed* constraints on the argument type

For example, with a GADT having some argument type σ('a) using
a variable instantiated in its return type :

  type +_ t = | C : σ('a) -> ('a -> unit) t

If α ≤ β, then α t ≤ β t only if α, β are of the form α' → unit, β' →
unit, so α' *≥* β' and α t ≤ β t only if σ(α') ≤ σ(β'), that is 'a
appears *contravariantly* in σ.

Is the above condition sound? It would allow my two examples above. If
not, or if it's not reasonable to implement, is there a weaker
condition that would make those example work?

Having a powerful enough variance inference is important if we want to
use GADTs to implement abstract data types – that's how I ran into
this problem.