From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p7UCNaIH022334
	for <caml-list@sympa-roc.inria.fr>; Tue, 30 Aug 2011 14:23:39 +0200
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AgkCAEfVXE6BryEpkWdsb2JhbABCmHaPHxQBAQEBCQsLBxQEIYFuE4EOMR6gOqBzhk0Ei2mYQg
X-IronPort-AV: E=Sophos;i="4.68,302,1312149600"; 
   d="scan'208";a="117689814"
Received: from smtp1.u-psud.fr ([129.175.33.41])
  by mail1-smtp-roc.national.inria.fr with ESMTP; 30 Aug 2011 14:23:39 +0200
Received: from smtp1.u-psud.fr (localhost [127.0.0.1])
	by localhost (MTA) with SMTP id 8B9492516F1
	for <caml-list@inria.fr>; Tue, 30 Aug 2011 14:23:39 +0200 (CEST)
Received: from ext.lri.fr (ext.lri.fr [129.175.15.4])
	by smtp1.u-psud.fr (MTA) with ESMTP id 656D62516EE
	for <caml-list@inria.fr>; Tue, 30 Aug 2011 14:23:39 +0200 (CEST)
Received: from localhost (localhost [127.0.0.1])
	by ext.lri.fr (Postfix) with ESMTP id 5AD0140708
	for <caml-list@inria.fr>; Tue, 30 Aug 2011 14:23:39 +0200 (CEST)
X-Virus-Scanned: Debian amavisd-new at lri.fr
Received: from ext.lri.fr ([127.0.0.1])
	by localhost (ext.lri.fr [127.0.0.1]) (amavisd-new, port 10024)
	with ESMTP id AHrPirbL8I0Z for <caml-list@inria.fr>;
	Tue, 30 Aug 2011 14:23:39 +0200 (CEST)
Received: from lri.fr (lri30-192 [129.175.30.192])
	(using TLSv1 with cipher DHE-RSA-AES128-SHA (128/128 bits))
	(No client certificate requested)
	by ext.lri.fr (Postfix) with ESMTPSA id 3A45740701
	for <caml-list@inria.fr>; Tue, 30 Aug 2011 14:23:39 +0200 (CEST)
Date: Tue, 30 Aug 2011 13:27:37 +0200
From: AUGER Cedric <Cedric.Auger@lri.fr>
To: caml-list@inria.fr
Message-ID: <20110830132737.78b7a08e@lri.fr>
X-Mailer: Claws Mail 3.7.9 (GTK+ 2.24.5; i386-portbld-freebsd8.1)
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
X-Validation-by: cedric.auger@lri.fr
Subject: [Caml-list]Warning 20: this argument will not be used by the
 function.

Hi all,
while playing with coq and extraction I did the following:

"
Fixpoint narity (n: nat) : Set :=
match n with
|  O  => nat
| S n => nat -> (narity n)
end.

Definition sum_aux : nat -> forall n, narity n :=
fix sum acc n :=
match n as n0 return narity n0 with
|  O  => acc
| S n => fun m => sum (m+acc) n
end.

Definition sum := sum_aux O.

Eval compute in sum 3 14 67 21.

Recursive Extraction sum.
"

I do not want to comment if this is or not meaningfull, but adapting
the code to caml ints (not doing so will do the same thing, but ints
are easier to play with), I got:

        Objective Caml version 3.12.0

# type __ = Obj.t
  ;;
type __ = Obj.t
# let rec sum_aux acc n = if n <= 0
  then Obj.magic acc
  else Obj.magic (fun m -> sum_aux (m+acc) (n-1));;
val sum_aux : int -> int -> 'a = <fun>
# let sum = sum_aux 0;;
val sum : int -> 'a = <fun>
# print_int (sum 3 14 67 21);;
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
102- : unit = ()

The result is correct, but the warning is quite unexpected!
(Changing the values of the arguments will of course change the result)

It is not important or armfull, but quite funny.