How to statically type polymorphic lambdas using hindley milner style type inference
You should use a polymorphic lambda calculus, e.g. System F for representing typed terms. Then, when you generalize a let binding, you also insert lambdas which abstract over types, and when you check a function application, you also insert type applications as needed. This is precisely what GHC Haskell does, and is the standard solution.

Now, your concrete example does not fit into pure H-M inference, because you seem to be using an overloaded + operation. Unless + is implemented for every type or fails at runtime for some types, (T1, T1) -&gt; T1 is not a valid polymorphic type for add. 

For a pure H-M example program, elaborating to System F would look something like the following, with input:

id := func a begin a end
a  := id 'hello'
b  := id 100


And output:

id := Func A (func (a : A) begin a end)
a  := id [String] 'hello'
b  := id [Int] 100


Where I use Func A to mean a lambda binding a type (corresponding to big lambda in System F), and id [String] to mean applying the polymorphic id to a String type. The point of type lambdas and applications is to have an explicit internal representation of polymorphic functions.