Type inference for the (TODO: linear) π-calculus with product and sum types (TODO: and recursion/replication). Type inference here is "co-contextual": given a process P, we try to infer Γ such that Γ ⊢ P. The context Γ is built from the usages in P. The soundness of type inference is intrinsic. TODO: show that type inference is complete.