On Wed, Jan 14, 2009 at 04:31:24PM +0100, Julien SIGNOLES wrote:
> 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?

You need to say "type +'a s", otherwise the compiler (since "s" is an
abstract type) cannot know the variance of that type parameter inside a
value of type 'a s.  That information is needed to determine how to
generalize the type of x.

Mark