| So in general, if there is a partial type signature, the compiler | tries to infer a type under the assumption that there is no | polymorphic recursion, similar to what it does when there is no | signature. Yes. The way to think of it (at both term and type level) is this. A full type signature breaks dependency loops, and supports polymorphic recursion. A partial type signature is treated exactly like *no* type signature, except that extra typing constraints are added. Where the signature has a variable, we insist that the result is a variable; where the signature are distinct variables we insist that the final inferred type has distinct variables. Moreover, the explicitly mentioned variables can lexically scope over the definition. But no polymorphic recursion at all, with a partial type signature. Simon