Type Inference with Recursive Types: Syntax and Semantics