Including and re-exporting types as abstract

As a follow up to this discussion: Returning abstract types - #3 by zbaylin

Again, let’s say I have a similar GADT as before:

type 'a s =
  | Int : int s 
  | Float : float s

If I write a module type that contains a GADT wrapper for this type like so

module type S0 = sig 
  type t = A : 'a s -> t
end

and then write a function that takes an instance of one of these wrappers:

let f0 (type a) (module M : S0 with type t = a) (x : a) = ...

This fails to compile with the following error message:

Error: In this `with' constraint, the new definition of t
does not match its original definition in the constrained signature:
Type declarations do not match:
  type t
is not included in
  type t = A : 'a s -> t
Their kinds differ.

This makes sense to me. I then tried making t private, which gives a similar error. This code, however, works as one would expect, since S0 is a subtype of S1:

module type S1 = sig
  type t
end

let f1 (type a) (module M : S1 with type t = a) (x : a) = ()

Is there a way to rewrite S1 such that it includes S0 but makes t abstract?

Your module S1 already includes S0, as you can check with

module M = struct
  type t = A (* having a GADT seems mostly irrelevant to the problem at hand *)
end
let f1 (type a) (module M : S1 with type t = a) (x : a) = ()
let () = f1 (module M) A

Ah, maybe I was unclear in my question, my mistake. I recognize that S0 ⊂ S1. My question is if it’s possible to write a version of this pseudocode:

module type S0 = sig
  type t = A
end

module type S1 = sig
  include S0 with type t abstract
end

The reason I ask is because I have some (relatively) complex module types that include this pattern (which is why I was using a GADT :slight_smile:):

module type T =
  type 'a t
  type wrapped_t = Wrap : 'a t -> wrapped_t
sig

I could obviously rewrite the module with type wrapped_t abstract, but would prefer not to have two signatures which express the same thing.

No, it is not possible to erase this kind of information. The reverse direction works

module type S1 = sig
  type wrapped_t = A: 'a t -> wrapped_t
  include S0 with type t := wrapped_t
end

To be honest, I do not really understand what you want to try to do. If you wrap your GADT in an existential, you just get a type equivalent to this two valued one:

type t = String | Int

So why do you want to use a GADT if, at the end, you finally use a plain ordinary variant?