We implement the classical Damas-Milner type inference algorithm in a calculus with higher-order abstractions and 1st-order constraints. We encode mono(morphic) types as constraints, and poly(morphic) types as abstractions over monotypes. Our calculus Rho_deep is intended as computation model of a concrete programming language, i.e., to be what the Lambda-calculus is for ML, or the Gamma-calculus for Oz. Unlike usual in programming language research, Rho_deep allows reduction below abstraction. This allows to simplify our encoding of polytypes before usage. In the envisaged programming language, the type inferencer can be run just as specified. We claim that deep reduction is one of the essential features for such a high-level implementation of type inference or abstract interpretation algorithms. The algorithm can also be viewed as an extension of Wand's type inference algorithm towards let-polymorphism. Like Wand's, our algorithm is easily modified to supply other monomorphic type systems with ML style polymorphism.