Dear all,

many libraries like lwt, batteries or core provide a very nice idiom to be
used when a function uses a resource (file, connection, mutex, et cetera),
for instance in Core.In_channel, the function:

val with_file : ?binary:bool -> string -> f:(t -> 'a) -> 'a

opens a channel for [f] and ensures it is closed after the call to [f],
even if it raises an exception. So these functions basically prevent from
leaking resources. They fail, however, to prevent a user from using the
resource after it has been released. For instance, writing:

input_char (In_channel.with_file fn (fun x -> x))

is perfectly legal type-wise, but will fail at run-time. There are of
course less obvious situations, for instance if you define a function:

val lines : in_channel -> string Stream.t

then the following will also fail:

Stream.iter f (In_channel.with_file fn lines)

My question is the following: is there a way to have the compiler check
resources are not used after they are closed? I presume this can only be
achieved by strongly restricting the kind of function passed to
[with_file]. One simple restriction I see is to define a type of immediate
value, that roughly correspond to "simple" datatypes (no closures, no lazy
expressions):

module Immediate : sig
  type 'a t = private 'a
  val int : int -> int t
  val list : ('a -> 'a t) -> 'a list -> 'a list t
  val tuple : ('a -> 'a t) -> ('b -> 'b t) -> ('a * 'b) -> ('a * 'b) t
  (* for records, use the same trick than in
http://www.lexifi.com/blog/dynamic-types *)
  ...
end

and have the type of [with_file] changed to

val with_file : string -> f:(in_channel -> 'a Immediate.t) -> 'a

I'm sure there are lots of smarter solutions out there. Would anyone happen
to know some?

Cheers,
  Philippe.