The orginal workshop version was titled: Weak Subsumption Constraints for Type Diagnosis: An Incremental Algorithm. We present an incremental constraint solver as the nucleus of a soft type checker for a higher-order concurrent constraint language. Designed as a variation of rational tree unification, our algorithm additionally decides satisfiability of weak subtype constraints of the form y. It allows for a number of extensions such as record types, sorts, union types, and type declarations, which we discuss by example. Hard disjunctive constraints are handeled as incomplete propagators which incrementally make as many simple constraints explicit as feasible. These extensions let our algorithm become suitable for type checking of a full-fledged programming language.