Skip to content

Instantly share code, notes, and snippets.

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
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
module M = struct
type 'a t = int
let value = 1
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
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
( 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