Typing issue with polymorphic phantom type parameters


Having a hard time understanding what is going on with this line of code: ocaml-pari/examples/kzg.ml at macos-nix · jtcoolen/ocaml-pari · GitHub.

Here, the labeled argument n is supposed to be of type Integer.t=(integer, ring) typ, the type of residue_class is (finite_field, field) typ -> (finite_field, ring) typ Polynomial.t and Polynomial.( .%[] ) : ('a, ring) typ Polynomial.t -> int -> ('a, ring) typ.

However, the type of .%[] is actually Integer.t Polynomial.t -> int -> Integer.t, whereas I would expect it to be (finite_field, ring) typ Polynomial.t -> int -> (finite_field, ring) typ as it is applied to an output of the function residue_class.

I can try to come up with a minimized example if needed.
Thanks a lot for helping with this stuff!

The type of Polynomial.(%[]) is not Integer.t Polynomial.t -> int -> Integer.t, but the more general

val ( .%[] ) : 'a t -> int -> 'a


type 'a t = (polynomial, ring) typ constraint 'a = ('b, ring) typ

(see https://github.com/jtcoolen/ocaml-pari/blob/7b6853169de92a2311d7e935f24b530c2d1f969d/src/pari.mli#L269-L334)

This means that you can pass any ('b, ring) typ Polynomial.t to %[] and you will get back a ('b, ring) typ; in particular you can do so with 'b = finite_field. The constraint acts as a filter on which types can be used as argument of the Polynomial.t constructor, which then disappear (as they do not appear in the result type (polynomial, ring) typ).


Thanks a lot for the prompt response which clears things up!

Sorry, the question wasn’t very clear, what surprises me is that while the type of Polynomial.(x.%[0]) is Integer.t (since the function Elliptic_curve.mul expects one), the type of x on line 91 is (finite_field, ring) typ Polynomial.t, which doesn’t seem coherent with the type of .%[]: 'a t -> int -> 'a which would make x of type Integer.t Polynomial.t instead. Actually, annotating the x on line 91 with either Integer.t Polynomial.t or (finite_field, ring) typ Polynomial.t is accepted by the type checker.

That is because the argument 'a of 'a t does not appear in the result type (it is a phantom parameter), So both types are actually the same, namely: (polynomial, ring) typ.


Oh right, many thanks!

Changed the type of polynomial to type 'a polynomial = Polynomial of 'a and Polynomial.t to type 'a t = ('a polynomial, ring) typ constraint 'a = ('b, ring) typ for the record.