Original bug ID: 5867
Reporter: mbarbin
Assigned to: @garrigue
Status: closed (set by @alainfrisch on 2015-12-07T08:55:56Z)
Resolution: duplicate
Severity: feature
Version: 4.00.1
Category: typing
Duplicate of: #7074
Child of: #5998
Monitored by: @gasche "Julien Signoles" @hcarty @alainfrisch

Bug description

(* Given these two ways of encoding an existential type *)

type t = A : 'a -> t

module type S = sig
type a
val a : a
end

(* one can easily go from one to the other *)

let to_gadt (module S : S) = A S.a

(* however, the other way around lacks of a syntax to name the ex#i type: *)

let f = function
| A a ->
(fun (type aa) (a:aa) ->
(module (struct
type a = aa
let a = a
end) : S)
) a

(* since the scope of 'a would be the entire function the following does not work and complain that the type ex#i would escape its scope *)

let f = function
| A (a:'a) ->
(module (struct
type a = 'a
let a = a
end) : S)