Typing error with polymorphic variant

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 :thinking: .

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

Version of OCaml: 5.1.0

This works (with the help of GitHub Copilot :slight_smile:)

type _ foo = B : int list -> [> `B ] foo

module M : sig
  val bar : [> `B ] foo
end = struct
  let bar = B [ 0; 1; 2; 3; 4 ]
end

Indeed, there are workarounds, I have mentioned another one in my initial post. But I don’t understand why there is a typing error in the first place.

Have you tried asking GitHub Copilot? It gives this explanation, but unfortunately the suggested fix doesn’t work :confused: 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.

Cheers,
Nicolas

2 Likes

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.

1 Like

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]
1 Like

“Next time you should ask a person for help.” :slight_smile: Reference: Calvin and Hobbes by Bill Watterson for July 28, 1988 - GoComics .

9 Likes

(Un)fortunately, I don’t get the comics (probably cultural differences :slight_smile: ), 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.

1 Like