Thanks for the info! I didn't think about just telling the type system about the variance, and this kind of fix is exactly what I was (eventually) getting at. Unfortunately, this solution doesn't seem to work in my actual code.

I wrote a module to read and write binary data with fixed layouts, and I'm using a GADT to enforce typing. A simplification of my actual code:

type (_,_) field =

| Int8 : ('a,'b) field -> ((int -> 'a),'b) field

| String : (int * ('a,'b) field) -> ((string -> 'a),'b) field

| End : ('b,'b) field

let intstring = Int8 (String (3, End))

In this case, intstring would be used as a template for reading/writing an 8-bit integer, followed by a 3-byte long string. The type would be:

val intstring : (int -> string -> 'a, 'a) field

My reading/writing functions are of the type:

val to_chan : ('a, unit) field -> out_channel -> 'a

val of_chan : ('a, 'b) field -> 'a -> in_channel -> 'b

This ensures that the arguments I pass are of the correct type for the field. Passing intstring to the field parameter of the functions results in a type:

val intstring_to_chan : out_channel -> int -> string -> unit

val intstring_of_chan : (int -> string -> '_a) -> in_channel -> '_a

(Note that the non-generalization of intstring_of_chan is not a problem since I would always pass the reading function at the same time as the field value.)

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) |]

let lookup_fun i = String (i, End)

These end up being the following types:

val lookup_array : (string -> '_a, '_a) field array

val lookup_fun : int -> (string -> 'a, 'a) field

The lookup array is nongeneralized. The function works, but I'll be using this in a very tight loop which is extremely resource-intensive. I wanted to use a lookup table to see if that runs any faster, but I can't get it to compile. (Even using Obj.magic didn't work)

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

Thanks again for your help! I think I'm a bit over my head with all this, but I'd like to figure out as much as I can.

On May 9, 2017 01:55, "Leo White" <leo@lpw25.net> wrote:

> But this similar type has no problem:

> type 'a field = Int of int

> let a = Int 3

> let b = Int (1 + 2)

This is the relaxed value restriction: `field` is covariant in it's parameter which means that the type variable is only used in covariant positions and so can be generalized even though the expression is not a value.

> Both a and b receive the same generalized type. Why does the GADT style prevent this from occuring?

OCaml currently just assumes that types defined with GADT syntax are invariant because checking of variance with GADTs is more difficult. If you annotate your type as covariant then it behaves the same:

type +_ field = Int : int -> 'a field

let a = Int 3

let b = Int (1 + 2)

gives:

type +_ field = Int : int -> 'a field

val a : 'a field = Int 3

val b : 'a field = Int 3

Regards,

Leo