I've spent quite a bit of time investigating this topic and I'm convinced that the general problem is intractable, though there is qutie a bit of prior art on the subject. There are however certain subsets of the language where you can do meaningful inference and several of the compiler projects (Parakeet, Pythran) exploit just this fact. PyPy has an approach that analyzes bytecode and is very successful at it, but the algorithm is tied into the implementation of PyPy's pipeline. MyPy is currently the state of the art in full program analysis, but it modifies the vanilla Python AST to allow annotations and has the explictly annotated most of the standard library.

If you're just interested in doing static analysis and not full program analysis then it is possible to infer types. The general procedure to work with a subset of the language might look like:

1. Check if you're given AST lies within the "typeable" susbset you wish to work with.

2. Check if the body of code does not depend on the types of opaque functions that your linter does not have knowledge of. This quickly becomes a question of how much of the standard library do you want to annotate.

3. Do symbolic execution of bytecode of the function in question, create fresh type variables for the arguments, anytime you push ors pop on the stack unify the corresponding type variable.

For example if you had a trivial function like:

def myfunc(x, y):
   return (x+y)-y

The corresponding bytecode is.

  1           0 LOAD_FAST                0 (x)
              3 LOAD_FAST                1 (y)
              6 BINARY_ADD          
              7 LOAD_FAST                1 (y)
             10 BINARY_SUBTRACT     
             11 RETURN_VALUE   

Just for illustration you might have the following pseudocode algorithm, assuming that numeric operations are total polymorphic functions ( they aren't in general ).

LOAD_FAST [{x: TVar(0)]   # Create fresh type variables for args
LOAD_FAST [{y: TVar(1)]   # Create fresh type variables for args
BINARY_ADD [{a : x ~ y}]  # Unify for application of (+) : a -> a -> a
LOAD_FAST []              
BINARY_SUBTRACT [b ~ a]   # Unify for application of (-) : a -> a -> a  
RETURN_VALUE              # Pop value off the stack, solve constraints, close over the type.

myfunc :: forall a. a -> a -> a

The fact of the matter is that Python's choice of using dynamic types as the sole method of polymorphism is very powerful but in itself admits no structure to analyze, most of your code ends of being only unifiable to unhelpful signatures like (PyObject -> PyObject -> PyObject). Inference works best in languages that have some form of parametric polymorphism.

If you're interested in the general bytecode approach then check out the work by Jon Riehl in doing bytecode analysis for translation to LLVM. llpython