Re: [Caml-list] Type generalization confusion

[Jeremy Yallop <yallop@gmail.com>]

On 9 May 2017 at 20:56, Reed Wilson <cedilla@gmail.com> wrote:
>   type (_,_) field =
>   | Int8 : ('a,'b) field -> ((int -> 'a),'b) field
>   | String : (int * ('a,'b) field) -> ((string -> 'a),'b) field
>   | End : ('b,'b) field
[...]
> No number of "+" or "-" in my type parameters fix the issue as they did with
> the example in my previous e-mail. Everything returns:
>   Error: In this GADT definition, the variance of some parameter cannot be
> checked

Indeed, soundness requires the parameters of 'field' to be invariant,
so there's no possibility of adding variance annotations here.

For example, the type of the End constructor makes the following
definition well typed:

  let x : (< m : int >, < m : int >) field = End

If one of the parameters (the first, say) were covariant, then that
parameter could be coerced to a supertype of < m:int >, like this

  let y = (x :> ( < >, < m : int >) field)

and then matching against y would introduce an invalid equality
between < > and < m: int >:

  match y with
    End ->
      (* Here the type checker knows by the type of End that the
         two type parameters are equal, i.e. that < > is equal to < m : int > *)
    let x = (object end) in x#m + 1

A similar argument can be made against making either parameter
contravariant.  The parameters of 'field' are therefore invariant, and
so the relaxed value restriction doesn't apply.

> The current issue I'm actually facing is trying to create a lookup table for
> these templates, which only differ by the length of some of the fields. For
> example:
>
>   let lookup_array = [| String (0, End); String (1, End) |]

The value restriction prevents generalization here, since arrays are
mutable.  If bindings of array expressions were generalized then the
following program, which writes to the array at one type (int option)
and reads from the array at a different type (string option), would be
allowed.

   let array = [| None |] in                   (* val array : 'a option array *)
   let () = array.(0) <- Some 3 in
   let Some x = array.(0) in                (* val x : 'a *)
   "abc" ^ x

So it's essential for soundness that the types of array values are not
generalized.