Cannot solve a type mismatching with GADT

Question

I have following type definition of x with a GADT.

type x = X : 'a option -> x

and I'm trying to write a function to get the value of option accompanying with tag X

I first tried the following

let get = fun (X a)->a

and obtained the following error message

Error: This expression has type $X_'a option
       but an expression was expected of type 'a
       The type constructor $X_'a would escape its scope

secondly I tried this

let get : type a.x-> a option =  fun (X a)->a

and following

Error: This expression has type $X_'a option
       but an expression was expected of type a option
       Type $X_'a is not compatible with type a

I think since the type 'a given to the option inside type x doesn't appear in type annotation, there is no way to write what 'a actually is in type annotation explicitly.

Answer 1

You're exactly right. You can't access that type. It's an existential type, which means it can't be recovered. There's no magic trick to reconstruct such a type from a runtime value, as that would require the compiler to know about the runtime value of an expression at compile-time.

Perhaps you meant to include the type 'a as part of the type of x?

type 'a x = X : 'a option -> 'a x

which doesn't require the GADT syntax anymore and can be written more succinctly as

type 'a x = X of 'a option