How to type check recursive definitions using Algorithm W?
You could type check it using explicit recursion with a primitive fix having type (a -> a) -> a. You can insert the fix by hand or automatically.
If you want to extend the type inferences then that's quite easy too. When encountering a recursive function f, just generate a new unification variable and put f with this type in the environment. After type checking the body, unify the body type with this variable and then generalize as usual. I think this is what you suggest. It will not allow you to infer polymorphic recursion, but this in general undecidable.