Implicits as constructor arguments

[yallop]

It'd be convenient to have implicits as constructor arguments so that we could write

type showable = Show : {S: SHOW} * S.t -> showable;;
let f (Show ({M}, x)) = show x

It's currently possible to achieve something similar with first-class modules in a few cases:

type showable = Show : (module SHOW with type t = 'a) * 'a -> showable
let f (Show ((module M), x)) = let implicit module M = M in show x

but this technique doesn't work for higher-kinded examples, besides being rather cumbersome.

[lpw25]

I agree this would be a good idea. Syntactically, what about:

type showable = Show : {S: SHOW} -> S.t -> showable;;
let f (Show{M}(x)) = show x

[yallop]

Yes, that works. As a pleasant side effect, this also introduces a way to bind existential type variables in patterns, if you don't mind passing the types explictly during construction:

module type T = sig type t end
type t = T: {X:T} -> {Y:T} -> X.t * Y.t -> t

let f (T{X}{Y}(x, y)) =
   (* X.t and Y.t available as names for the types of x and y *)
   ...

f (T{Int}{String}(3, "four"))

Can implicit constructor arguments without value components be optimized away so that they don't have a runtime representation?

[lpw25]

Can implicit constructor arguments without value components be optimized away so that they don't have a runtime representation?

I'm not sure, but probably not. If you made the module type abstract then some users of the type would not be aware that the module contains only types.