Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
(* this is an elaboration for:
let test (f : ((module S) [@ident M]) -> 'a M.t) =
let x : (module M) = M in
f x;;
which is a variant of the example at https://github.com/ocaml/ocaml/pull/9187#issuecomment-778476951
The goal here is to show that is posssible to describe the same code as above using FCM
and achieve type inference, but this can be generated from the code above programatically
with a ppx. And can also be inferred by doing typed PPX.
By changing `(module M)` to `(module S)` it gives the an error as you would expect,
saying that the type would escape it's scope, this will happen because OCaml types
needs an actual path while FCM doesn't have this requirement, same stuff as GADTs.
But if you have a concrete module type like `(module M)` you can even do stuff like
`((if x then (module A) else (module B)) : module M)` which is something that explicits
cannot describe at all.
*)
module type S = sig
type 'a t
val value : 'a t
end
module M = struct
type 'a t = int
let value = 1
end
module type M = module type of M
module type HKT_Magic_f = sig
module M : S
type a
type return_type
type ('a, 'b) eq = Eq : ('a, 'a) eq
val eq : (return_type, a M.t) eq
end
let test (type a)
(f :
(module HKT_Magic_f with type return_type = 'return_type and type a = a) ->
'return_type) =
let x = (module M : M) in
f
( module struct
module M = (val x)
type nonrec a = a
type return_type = a M.t
type ('a, 'b) eq = Eq : ('a, 'a) eq
let eq = (Eq : (return_type, a M.t) eq)
end )
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment