From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p3S46SLu021093
	for <caml-list@sympa-roc.inria.fr>; Thu, 28 Apr 2011 06:06:28 +0200
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Ar4DANDmuE3UGyoFkWdsb2JhbACYUY0uFAEBAQEJCwsHFAMiw3yFdgSSeg+KAQ
X-IronPort-AV: E=Sophos;i="4.64,278,1301868000"; 
   d="scan'208";a="98211879"
Received: from smtp5-g21.free.fr ([212.27.42.5])
  by mail2-smtp-roc.national.inria.fr with ESMTP; 28 Apr 2011 06:06:23 +0200
Received: from yeeloong (unknown [82.67.194.89])
	by smtp5-g21.free.fr (Postfix) with SMTP id A1295D4801A
	for <caml-list@inria.fr>; Thu, 28 Apr 2011 06:06:15 +0200 (CEST)
Received: by yeeloong (sSMTP sendmail emulation); Thu, 28 Apr 2011 06:05:51 +0200
Date: Thu, 28 Apr 2011 06:05:51 +0200
From: rixed@happyleptic.org
To: caml-list@inria.fr
Message-ID: <20110428040550.GB9733@yeeloong.happyleptic.org>
References: <20110427204629.GA8872@yeeloong.happyleptic.org>
 <20110427205416.GL4023@localhost>
 <20110427212852.GC8872@yeeloong.happyleptic.org>
 <20110427215146.GD4023@localhost>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <20110427215146.GD4023@localhost>
User-Agent: Mutt/1.5.21 (2010-09-15)
Subject: Re: [Caml-list] Strange behavior of mutualy recursive definitions

-[ Wed, Apr 27, 2011 at 11:51:46PM +0200, Guillaume Yziquel ]----
> able to evaluate toto. [rec] keyword: much the same behaviour as
> 'let rec f x = f x'; no need to have f evaluated in order to evaluate f.
>
> However, 'let rec f = f' will fail for the exact same reason as before:
> To evaluate f, you need to have evaluated f beforehand.
>
> Just focus on the difference between:
> 
>       let rec f x = f x
>       let rec f = f

Very good idea let's focus on this example.
Why 'let rec f = f' is rejected is clear: you cannot type f.  In my
original example, however, the point was precisely that both toto and
titi types were known to be 'a -> int beforehand (because of the type of
inc and dec).

So, an equivalent and simpler question would be:

Although "let rec f = f" is unsound and rejected as expected,
why is "let rec f : unit -> unit = f" also rejected, since it seams
trivially equivalent to "let rec f () : unit = f ()" (which is
accepted) ?


Now that I think about it, another equivalent question would be:
Why is "let rec f = f" rejected with the error "This kind of expression
is not allowed" instead of being rejected by the type system ?
I'm under the impression that the mutual recursion rules stated in
manual section 7.3 are checked somewhat too early, and that the typer
could resolve some practical cases that are ruled out by mutual
recursion acceptability checks.

Either that, or there is something fundamentally simple in ocaml that I
still failed to grasp despite your patient explanations :-)