The astute reader has probably noticed in the definition above that, in OCaml 5.4.0, the typechecker does accept 

type int_gmp
let ok: (int_gmp, [` A] ) Type.eq -> _ = function _ -> .

as total.

Indeed until OCaml 5.5.0, abstract types defined in the current module

were considered as unique and provably different 

let f: 'x. (a,b) Type.eq -> 'x = function _ -> .

However, this special rule for local definition of abstract types was very brittle. As soon as one moved outside of the current module, it was no longer possible to prove that the types were different. 

module M = struct
  type a
  type b
end
let fail: 'x. (M.a,M.b) Type.eq -> 'x = function _ -> .

Error: This match case could not be refuted.
       Here is an example of a value that would reach it: Equal

This special typechecking rule has been removed in OCaml 5.5.0. If you were relying on it, for instance, because you used an abstract type as type-level label in a GADTs, you can change your abstract type definition to a possibly private abbreviation of a polymorphic variant 

type a = private [`A]
type b = [`B]

or a (possibly private) sum type 

type a = A
type b = private B

If you were using an abstract type as both a type-level label and a FFI type, you can now use an external type definition which will give you a provably distinct type even outside of the current module.