Type Inference with Structural Subtyping: A Faithful Formalization of an Efficient Constraint Solver