This report extends our behavioral type and effect system for detecting dealocks in  by polymorphism and formalizing type inference (wrt. the lock types. Our inference is defined for a simple concurrent, first-order language. From the inferred effects, after suitable abstractions to keep the state space finite, we either obtain the verdict that the program will not deadlock, or that it may deadlock. We show soundness and completeness of the type inference.