From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: weis
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id DAA30896 for caml-redistribution; Tue, 13 Jul 1999 03:08:41 +0200 (MET DST)
Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id TAA27543 for <caml-list@pauillac.inria.fr>; Mon, 12 Jul 1999 19:20:39 +0200 (MET DST)
Received: from emerald.ps.uni-sb.de (emerald.ps.uni-sb.de [134.96.186.105])
	by nez-perce.inria.fr (8.8.7/8.8.7) with ESMTP id TAA04207
	for <caml-list@inria.fr>; Mon, 12 Jul 1999 19:20:38 +0200 (MET DST)
Received: from ps.uni-sb.de (IDENT:rossberg@localhost [127.0.0.1])
	by emerald.ps.uni-sb.de (8.9.1a/8.9.1) with ESMTP id TAA03522;
	Mon, 12 Jul 1999 19:20:36 +0200
Sender: weis
Message-ID: <378A23E4.ECEDD6DB@ps.uni-sb.de>
Date: Mon, 12 Jul 1999 19:20:36 +0200
From: Andreas Rossberg <rossberg@ps.uni-sb.de>
Organization: =?iso-8859-1?Q?Universit=E4t?= des Saarlandes
X-Mailer: Mozilla 4.6 [en] (X11; I; Linux 2.2.9 i686)
X-Accept-Language: German, de, en
MIME-Version: 1.0
To: caml-list@inria.fr
Subject: Undecidability of OCaml type checking
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit

I have been working through Mark Lillibridge's thesis on
translucent sums [1] recently. One main result of his work is
the undecidability (semi-decidability) of subtyping in his
system. Since the module system in OCaml is in many aspects
very similar to his system, I tried to code one of his
undecidable examples in OCaml. And it was indeed possible, the
following input will send the type checker into an infinite
loop:

     module type I =
     sig
       module type A
       module F :
	 functor(X :
	 sig
	   module type A = A
	   module F : functor(X : A) -> sig end
	 end) -> sig end
     end

     module type J =
     sig
       module type A = I
       module F : functor(X : I) -> sig end
     end

     (* Try to check J <= I *)

     module Loop(X : J) = (X : I)

I am sure that Xavier and the other Caml developers are aware of
this. I do not think this behaviour is really a problem, as the
example is really contrived -- nobody would write such code.
Thus I find this property of the language perfectly
acceptable. However, IMHO you should at least document the
fact that type checking is incomplete and compilation may not
terminate due to this.

Best regards,

	- Andreas
	

[1] Mark Lillibridge
    "Translucent Sums: A Foundation for Higher-Order Modules",
    PhD Thesis, CMU, 1997