I don’t understand why the following program is ill-typed:
type _ foo = B : int list -> [> `B ] foo
module M : sig
val bar : [> `B ] foo
end = struct
let bar = B (Seq.ints 0 |> Seq.take 5 |> List.of_seq)
end
The error is
File "test.ml", lines 5-7, characters 6-3:
5 | ......struct
6 | let bar = B (Seq.ints 0 |> Seq.take 5 |> List.of_seq)
7 | end
Error: Signature mismatch:
Modules do not match:
sig val bar : ([> `B ] as '_weak1) foo end
is not included in
sig val bar : [> `B ] foo end
Values do not match:
val bar : ([> `B ] as '_weak1) foo
is not included in
val bar : [> `B ] foo
The type ([> `B ] as '_weak1) foo is not compatible with the type
[> `B ] foo
Type [> `B ] as '_weak1 is not compatible with type [> `B ]
File "test.ml", line 4, characters 2-23: Expected declaration
File "test.ml", line 6, characters 6-9: Actual declaration
Which makes me believe it is related to the value restriction. And indeed, if I guard the function bar with unit, it works. However, as far as I know, the bar definition should already be considered a value because it begins with a constructor. So, I’m curious why it is necessary to convert it into a function to meet the criteria of the value restriction.
This seems related to the use of Seq.
Notice that if I rewrite my program this way, it seems well-typed though .
type _ foo = B : int list -> [> `B ] foo
module M : sig
val bar : [> `B ] foo
end = struct
let l = Seq.ints 0 |> Seq.take 5 |> List.of_seq
let bar = B l
end
Have you tried asking GitHub Copilot? It gives this explanation, but unfortunately the suggested fix doesn’t work But maybe it will lead you in the right direction.
The error message you’re seeing is due to a mismatch between the type of bar in the module M’s signature and its implementation.
In OCaml, the type [> B]is a polymorphic variant type that can be extended with additional constructors. The[> B] type is an “open” variant type, meaning it can include the B variant but also any other variants.
However, the type ([> B] as '_weak123)is a slightly different type. It's also an open variant type that includesB, but the '_weak123` part means that the type is weakly polymorphic within a certain scope. This is usually inferred by the OCaml type system when a type variable is used in a limited scope and doesn’t escape that scope.
In your case, the type of bar in the module implementation is ([> B] as '_weak123) foo, but in the module signature, it's [> B] foo. These types are not the same, hence the error.
To fix this, you can change the module signature to match the implementation:
module M : sig
val bar : ([> `B] as 'a) foo
end = struct
let bar = B (Seq.ints 0 |> Seq.take 5 |> List.of_seq)
end
This tells OCaml that bar has the type ([> B] as 'a) foofor some’a`, which matches the type inferred in the module implementation.
Unfortunately, it is not enough for the head of the expression to be a constructor to be considered a syntactic value for the purposes of the value restriction, as you could be storing hidden state in the argument of the constructor:
type 'a t = A of ('a -> 'a)
Clearly, A does not add anything here and this type is equivalent to 'a -> 'a. So if one generalized the type of A e for any expression e it would be equivalent to saying that one should generalize the type of e for any e, which is unsound and the whole point of the value restriction.
The actual value restriction requires that the argument of the constructor also be a syntactic value in order for its type to be generalized.
Thank you for your explanation. Now that I understand why value restriction applies, I still wonder why the typer rejects my program since there it seems there is no polymorphism in the type. I do not understand very well the typing of polymorphic variant and considering the error message of the typer some polymorphism is involved. But isn’t it weird to reject this program ? Since I can give a name to the payload and just used this name instead as shown in my initial post. Isn’t something the typer could figure out?
IIRC there is an implicit type variable in [> `B ], since it means any type that contains at least `B but also other constructors. And because of the value restriction, this type variable cannot be generalized (and appears as a '_weak1 in your error message. So if your expression is closed (the argument of B is computed once and for all) then you can just put it in an auxiliary variable. The following should work:
type _ foo = B : int list -> [> `B ] foo
module M : sig
val bar : [> `B ] foo
end = struct
let bar_aux = Seq.ints 0 |> Seq.take 5 |> List.of_seq
let bar = B bar_aux
end
If the expression is not fixed, then there should be no problem changing your API to require the parameters, making it a function and therefore a (syntactic) value:
let bar n = B (Seq.ints n |> Seq.take 5 |> List.of_seq)
EDIT: Note that this works because bar_aux is not itself polymorphic and the only polymorphic variables comes from the application of B. If bar_aux were polymorphic, then you’d also have a problem here making it a polymorphic toplevel definition because of the value restriction.
Buried in the manual: " the type checker considers that any value returned by a function might rely on persistent mutable states behind the scene and should be given a weak type."
But (Seq.ints 0 |> Seq.take 5 |> List.of_seq) is a function application, sugar for List.of_seq (Seq.ints 0 |> Seq.take 5), so the type engine infers a weak type.
Note that it seems to get a different weak type whenever evaluated:
# let bar = B (Seq.ints 0 |> Seq.take 5 |> List.of_seq) ;;
val bar : ([> `B ] as '_weak1) foo = B [0; 1; 2; 3; 4]
# bar ;;
- : ([> `B ] as '_weak2) foo = B [0; 1; 2; 3; 4]
# bar ;;
- : ([> `B ] as '_weak3) foo = B [0; 1; 2; 3; 4]
(Un)fortunately, I don’t get the comics (probably cultural differences ), but Copilot is quite good at explaining problems, suggesting solutions/libraries for a task or generating code for both OCaml and Haskell so I find it a nice companion for programming. And as a bonus it saves a lot of (googling) time.
.
)
But maybe it will lead you in the right direction.