Dependent types in OCaml

Question

There's a lot of information about dependent types in Haskell and Scala. For OCaml, not so much. Is anyone skilled enough to provide a coding example on how to achieve this in OCaml (if it's possible at all)? There is of course (the abandoned) Dependent ML, but it seems not possible to incorporate such stuff in "regular" OCaml code.

Basically, what I want to do is to remove code like assert(n > 0) and check it at compile time.

EDIT

As a side note, it's worth mentioning the OCaml Hybrid Contract Checking branch, that could fill some of the needs of a dependent type system. Instead of assert(n > 0) you would then write a contract:

contract f = {x : x > 0} -> int
let f x = x + 1
let dummy_variable = f (-1) (* Won't compile *)

Edit 2: For anyone reading this, I think F* is an interesting ML-like language with dependent types.

Answer 1

A reference link is Oleg's lightweight static guarantees pages, with examples (in OCaml or that you can translate to OCaml) of dependent-like techniques used in ML languages. His paper on Lighweight static capabilities (PDF) with Chung-chieh Shan in 2007 is especially relevant.

Edit: Since version 4.00 (released after the document above was written), OCaml has GADTs, which allow to streamline a few techniques for refined static information (previously relying on phantom type techniques), in particular the "singleton types" pattern demonstrated in Omega. It has been shown that they're not essential to get strong typeful programming, but they may still be used by a variety of examples found in the wild.