This work formalizes type inference for GADTs as done in OCaml. The novelty is the introduction of ambivalent types to retain the use of equations and type conversions within the type structure. It enables a more precise definition of type ambiguities and so rule out situations that are not actually ambiguous.
See the authors PDF of the conference absract presented in in 11th Asian Symposium on Programming Languages and Systems, Melbourne, December 2013. Springer-Verlag LNCS 8301, pages 257-272, the slides of the presentation and the extended version.
See also the talk given at the IFIP-WG2.8 2013 meeting and the extended abstract of the talk given at the ML workshop.
This work explores the interaction of GADT with subtyping and, in particular the safety of variance annotaions on GADT in the presence of subtyping, e.g. as can be found in the OCaml language.
See the extended abstract of the talk given at the ML workshop. (You may also see also the slides and video of the talk.) ).
There is also a short paper without proofs and a research report including more details and all proofs, also availble on HAL.