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!
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.
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.