Narrow down a module type with types dependent on each other

Learning
1

If we have a module

module type A = sig
  type a
  type t
end

we can narrow down the types like that:

module type A1 = A with
  type a = int and
  type t = int option

But how can I use the previously defined types, in this case t depending on a (this results in an error):

module type A2 = A with
  type a = int and
  type t = a option

I could achieve something similar with:

module AA (Z: sig type a end) = struct type a = Z.a type t = a option end
module A3 = AA(struct type a = int end)

but the downside is it requires a module implementation.
Are there any other alternatives?
OCaml Playground link

2

First class module types can encode the relations you want, but getting back to a regular module type is a bit hackish:

module type A = sig
  type a
  type t
end

type 'a m = (module A with type a = 'a and type t = 'a option)
module type A1 = module type of (val ((Obj.magic ()) : int m))

There is no safe use of Obj.magic, so I think your solution with functors is better (unless you only need first-class modules anyway, in which case you don’t need the definition of A1 and its magic).

3

The simplest option is

module type A1 = sig 
  type a = int
  type t = a option
  include A with type a := a and type b := b
end

but this is probably more a sign that you have simplified your example a bit too much.

4

For a toy example the following seems to work

module type A =
sig
  type t
  type a
  val f1 : t -> a
  val f2 : a -> t
end

module rec A_aux : A with
    type t = int and
    type a = A_aux.t option
= A_aux

module type A1 = (module type of A_aux)

I’m not sure how fast it breaks down though (meaning if your types are slightly more complex or you have
other definitions in A or if you want a and t to be mutually recursive).