Hello,

In the article "Many Holes in Hindley-Milner" [1], Sam Lindley claims
that the type of x is ('a * 'a s, int) NList.t in the following ocaml
program because of Garrigue's relaxed value restriction [2].
==========
type 'a s

module NList : sig
  type (+'length, +'elem_type) t
  val nil : ('m*'m, 'a) t
  val cons: 'a * ('m*'n, 'a) t -> ('m*'n s,'a) t
end = struct
  type ('i,'a) t = 'a list
  let nil = []
  let cons (x, l) = x :: l
end

let x = NList.cons (1, NList.nil)
==========

But, both with ocaml v3.10.2 and ocaml v3.12.0+dev1 (2008-12-03) (that
is the current cvs version), the infered type of [x] only contains a
weak type variable: ('_a * '_a s, int) NList.t.

I quickly look at the typing rules introduced by Jacques Garrigue in [2]
and it seems to me that Sam Lindley is right: [x] is generalisable in
the above program.

So, what's wrong here?

[1] Many Holes in Hindley-Milner.
    Sam Lindley. In ACM Sigplan Workshop of ML 2008, Victoria, British
    Columbia, Canada, September 2008.
[2] Relaxing the value restriction.
        Jacques Garrigue. In International Symposium on Functional and
        Logic Programming, Nara, April 2004. Springer-Verlag LNCS 2998.

Best regards,
Julien Signoles
-- 
Researcher-engineer
CEA LIST, Software Reliability Lab
91191 Gif-Sur-Yvette Cedex
tel:(+33)1.69.08.71.83  fax:(+33)1.69.08.83.95  Julien.Signoles@cea.fr