Seven years ago, a subtle unsoundness was discovered by Yallop in OCaml’s type system. It involved a combination of GADTs and abstraction, and uncovered how wrong assumptions about the injectivity of abstract types could lead to unsound type definitions. While it has been fixed by moving OCaml’s variance analysis from a naive view to a more complex one, which involves six flags, including one for injectivity, the new flags have not been given surface syntax. In this presentation, I would like to showcase two potential solutions to the problem of injectivity (two equal types must also have equal parameters), and the related problem of nominality (additionally, they must share the same head constructor). The first one is very simple: it adds surface syntax for the injectivity flag, allowing one to stipulate that an abstract type is injective in one of its parameters. The second one is more involved, and attempts to track the nominality of type definitions. Currently, the only truly nominal type definitions in OCaml are built-in types, types defined in the current module (excluding public type abbreviations), and concrete types (record and variants), the last one moreover lacking a proper identity. By tracking the nominality of types, it becomes possible to strengthen GADT unification, and infer more type equalities and incompatibilities.