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 ):

```
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?