Undecidability of OCaml type checking

[Andreas Rossberg <rossberg@ps.uni-sb.de>]

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