Contractive Signatures with Recursive Types, Type Parameters, and Abstract Types

What contractiveness

However, in an advanced type system, such as OCaml, with recursive types, type parameters, abstract types, and modules, we cannot easily define the syntactic contractiveness of types.

Use semantic contractiveness to reject:

module type T = sig
  type 'a t
  type s = s t
  type u = u t
  val f : int -> s
  val g : u -> bool
end

module M : T = struct
  type 'a t = 'a
  type s = int
  type u = bool
  let f x = x
  let g x = x
end

where otherwise s and u will be considered structrually equivalent while they are not semantically equiv (requires different instantiation /witnesses of 'a t = 'a )

This paper can serve as a way to check whether the contractiveness check we have are natural (after anchoring back)