Join GitHub today
GitHub is home to over 50 million developers working together to host and review code, manage projects, and build software together.Sign up
Top-level custom printing for GADTs: interface change in 4.02.2 #6908
Original bug ID: 6908
PR5958 changed the behaviour of #install_printer to make it possible to install printers for parameterised types. Unfortunately the change has broken some existing code for printing GADTs.
For example, if I have the following GADT definition
type (_, _) eql = Refl : ('a, 'a) eql
then the following printer works with #install_printer in 4.02.1, but is rejected in 4.02.2:
let format_eql : 'a 'b. Format.formatter -> ('a, 'b) eql -> unit =
and the following printer works with #install_printer in 4.02.2 but is rejected in 4.02.1:
let format_eql : 'a 'b.
This is a problem in practice. For example, top-level printing no longer works in ctypes, which installs a number of printers of the first form:
Comment author: @gasche
I see no better solution than making the directive code more clever to detect types that (1) have type parameters but (2) do not expect printers for those parameters, and use the old behavior on those.
Maybe we could generalize this to accept that only a subset of the parameters expect printers (synthesizing printers does not make sense for phantom or even contravariant parameters). But a first goal should be to have a safe patch that solve ctypes immediate problem.