Confusing Behaviour with Polymorphic Variants

Learning
1

I’m currently trying to modify some code that uses polymorphic variants, and am running into a strange issue.

The toy version of my problem is as follows (copying the output from utop):

module Test : sig
 val test : [> `Int] -> [> `Int | `Float]
end =
struct
 let test (input : [> `Int]) : [> `Int | `Float] = input
end;;
Error: Signature mismatch:
       Modules do not match:
         sig val test : ([> `Float | `Int ] as 'a) -> 'a end
       is not included in
         sig val test : [> `Int ] -> [> `Float | `Int ] end
       Values do not match:
         val test : ([> `Float | `Int ] as 'a) -> 'a
       is not included in
         val test : [> `Int ] -> [> `Float | `Int ]

What I don’t understand is why does the compiler not like the projection of the input into the larger type? I guess I am missing a subtlety here, but surely [> 'Int] is compatible with [> 'Int | 'Float]?

If I remove all of the > modifiers from the types, the example still fails, but I have kept them in here in case the resolution is different in this case.

If I just constantly return an 'Int then everything works as expected:

module Test : sig
 val test : [> `Int] -> [> `Int | `Float]
end =
struct
 let test (input : [> `Int]) : [> `Int | `Float] = `Int
end;;
module Test : sig val test : [> `Int ] -> [> `Float | `Int ] end

Any help with this would be appreciated - either in understanding what the cause of the problem is, or in any workarounds (unfortunately I have to keep the polymorphic variants in the code, but maybe there are type hints or similar that could be added).

1 Like
2

Consider what would happen if you did test (`Float 0). The signature in your module type would accept it, but the value produced would have type [`Float of int] which is incompatible with [`Float].

In order to prevent such issues, [> `Foo] is actually [> `Foo] as 'a for some fresh 'a, which means "some 'a with the constraint that it contains at least `Foo". So the signature you wrote means test : 'a -> 'b for any 'a containing at least `Int and any 'b containing at least `Int and `Float, and the one in the error message says 'a and 'b actually have to be the same thing (with the union of the constraints).

The confusing part is that 'a doesn’t quite mean the same thing in a val vs in a let ... in: the following code (without polymorphic variants) produces an error even though it looks like we wrote the same type in the signature and in the implementation:

module M : sig
  val foo : 'a -> 'b
end = struct
  let foo : 'a -> 'b = fun x -> x
end

this is because in a letin variables like 'a may be unified as necessary to make the type go through, but in a signature there’s no unification to do so they’re always independent.

1 Like
3

Is it correct to conclude that if OCaml did not allow polymorphic variant constructors with the same name for different numbers of arguments (such as `Float vs `Float of int) then this problem would not exist?

4

You’d get the same kind of issue if you had test : [>`Int] -> [> `Int | `Float of bool] and passed `Float 0 so no

1 Like
5

Ah yes. So going further, would the problem go away if all polymorphic constructors were required to use globally unique tags, so that `Float of int and `Float of bool in the same program would be rejected?

(Are such globally unique tags infeasible/undesirable?)

6

@SkySkimmer: Thanks for the help with this. I think I understand a bit better, but I have a follow-up question if you have time to answer.

I’ve been looking a bit more, and it seems like an example without 'Float also causes an error:

module Test : sig
val test : [> `Int] -> [> `Int]
end =
struct
let test input = input
end;;
Error: Signature mismatch:
      Modules do not match:
        sig val test : 'a -> 'a end
      is not included in
        sig val test : [> `Int ] -> [> `Int ] end
      Values do not match:
        val test : 'a -> 'a
      is not included in
        val test : [> `Int ] -> [> `Int ]

This doesn’t seem to fit the pattern, as I could call test ('Float 0) happily, but I couldn’t call test ('Int 0) to hit the same issue. Interestingly, this example works if you remove the >s, so it must be something to do with subtyping.

7

`Float 0 still doesn’t fit in every type 'b containing `Int, it only fits in the specific one that was passed as input.

8

Another point is that the following function has the right type:

let test = function
| `Int -> `Int
| _ -> `Float

because it does not propagate the unknown variant tags, and thus it does not impose any shared constraints between the input and return type.

1 Like
9

@SkySkimmer, @octachron: Thanks both. That makes more sense.