[Caml-list] GADTs : a type variable cannot be deduced

[David RENAULT <renault@labri.fr>]

		Hi,

I was experimenting on GADTs and phantom types and was using the usual
encoding for naturals, as well as a classic implementation of the
associated singleton type :

type zero
type 'a succ
type _ nat =
  | Zero : zero nat
  | Succ : 'a nat -> ('a succ) nat

With ocamlc 4.01.0, this fails to compile with the following error
message :

Error: In this definition, a type variable cannot be deduced
       from the type parameters.

This is strange, because this code compiled pretty well with ocamlc
4.00.1. Of course, it is possible to modify the code to make it compile
by replacing the type variables by underscores, but the resulting type
is incorrect :

type _ nat =
  | Zero : zero nat
  | Succ : _ nat -> (_ succ) nat
(* type _ nat = Zero : zero nat | Succ : 'b nat -> 'a succ nat *)

Succ Zero;; (* 'a succ nat = Succ Zero, should be "zero succ nat" *)

I failed to find in the Changelog the modification that led to this
behavior, and nothing really simple about the error message showed up.
The following file seems to prove that the problem appears in various
other cases :

http://caml.inria.fr/svn/ocaml/trunk/testsuite/tests/typing-gadts/pr5985.ml

Is the code I am writing incorrect ? (for reference, the same code in
Haskell (with ghc) works as expected)

		RENAULT David