We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index objects are drawn from a constraint domain {\it C}, leading to the DML({\it C}) language schema. this allows specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. A major complication resulting from introducing dependent types is that pure type inference for the enriched system is no longer possible, but we show that type-checking a sufficiently annotated program in DML({\it C}) can be reduced to constraint satisfaction in the constraint domain {\it C}. We exhibit the unobtrusiveness of our approach through practical examples and prove that DML({\it C}) is conservative over ML. The main contribution of the paper lies in our languages design, including the formulation of type-checking rules which makes the approach practical. To our knowledge, no previous type system for a general purpose programming language such as ML has combined dependent types with features including datatype declarations, higher-order functions, general recursions, let-polymorphism, mutable references, and exceptions. In addition, we have finished a prototype implementation of DML({\it C}) for an integer constraint domain {\it C}, where constrains are linear inequalities (Xi and Pfenning 1998)