Do you have an example in mind?

The intuition behind my conjecture was that the essence of GADT is the equality GADT you wrote (as described on section 8.2 of these lecture notes). As @yallop and @lpw25 said, we can encode all GADTs using the equality GADT and regular ADTs.

```
type (_, _) eql = Refl : ('a, 'a) eql
type 'a adt =
| S of ('a, string) eql
| F of ('a, float) eql
type 'a gadt =
| Sg : string gadt
| Fg : float gadt
(* these two type are indeed isomorphic *)
let adt_to_gadt : type a. a adt -> a gadt = function
| S eql -> (match eql with Refl -> Sg)
| F eql -> (match eql with Refl -> Fg)
let gadt_to_adt : type a. a gadt -> a adt = function
| Sg -> S Refl
| Fg -> F Refl
```

Therefore, my intuition is that if we remove GADT from the type system the concrete type of an abstract type can never leak outside of its module. GADT is the only way to work with proofs and type equalities as first-class objects. So if a module doesn’t use the GADT functionalities, it cannot leak the concrete types of its abstract types. But, as you illustrate, if it defines functor which abstract over parametric type then it may leak the concrete types of its abstract ones.

I played a little bit with your last example, and it was funny. When we look at the signature of your module, we can prove (in the spirit of Wadler’s theorems for free) that its type `t`

is necessarily equal to `string`

. Without GADTs this proof is metalinguistic, but with them we can write it in the language itself.

```
module type S = sig
type t
module F :
functor (X : sig type 'a x val x : string x end) -> sig val x : t X.x end
end
(* the proof is straightforward, this is mostly the one you wrote *)
let leak_S_t (type a) (module M : S with type t = a) =
let module K = M.F(struct type 'a x = ('a, string) eql let x = Refl end) in
K.x;;
val leak_S_t : (module S with type t = 'a) -> ('a, string) eql = <fun>
(* the type of `leak_S_t' clearly say that any module which implements
the signature S, must have a type `t' equal to `string' *)
(* as shown if we apply it to your module implementation *)
leak_S_t (module M);;
- : (M.t, string) eql = Refl
```

We can go further with a variation of your example:

```
module type S = sig
type t
module F :
functor (X : sig type 'a x val x : string x val y : float x end) ->
sig val x : t X.x end
end
```

Here we can *statically* prove that for a module `M : S`

the concrete type of `M.t`

is `string`

or `float`

, and we can find *dynamically* which one it is.

```
(* here for the proof I use the previously defined 'a gadt type *)
let leak_S_t (type a) (module M : S with type t = a) =
let module K = M.F(struct type 'a x = 'a gadt let x = Sg let y = Fg end) in
K.x;;
val leak_S_t : (module S with type t = 'a) -> 'a gadt = <fun>
(* and with two examples *)
leak_S_t (module M);;
- : M.t gadt = Fg (* M.t = float *)
leak_S_t (module N);;
- : N.t gadt = Sg (* N.t = string *)
```

By the way, it may still be possible to improve the refutation algorithm (using a more refined criterion than the one I gave first) in such a way that for @Chimrod example, the type checker can prove that the pattern matching is exhaustive. Maybe @yallop or @lpw25 can enlighten us on this point?