How to statically type polymorphic lambdas using hindley milner style type inference

I am playing with a simple implicitly typed functional language and have implemented type checking using a Hindley Milner style system. In order to guide code generation, I want to tag each term with its type during type inference.

Of course my language uses lambda expressions and the implicit typing should enable nice polymorphic use of those lambdas. Unfortunately, this goal clashes with the static type tagging as each lambda can be tagged only once which specializes it for a particular set of argument and closure types. It is also not possible to statically copy lambdas on each use, as this requires dynamic knowledge.

I thought about dynamically copying and tagging lambdas at runtime but this would involve quite some work and possibly overhead. Is there a standard solution for this kind of problem?

Update 1
The following example might help to clarify my point.

add := func (a, b) begin a + b end
a   := add(2, 3)
b   := add('hello', 'world')

The lambda add has polymorphic type (T1, T1) -> T1 and during type checking add is first instantiated to (Int, Int) -> Int and then to (Str, Str) -> Str, everything fine so far. But, during compilation, I want to have the tree representing add to be annotated with conrete types. Unfortunately, add is a single tree and that tree is either tagged with the first or the second type instantiation.

I could create copies of the add tree for each application but it seems to me that this is only possible at runtime, when the actual target of a call is available. On the other hand, maybe I could somehow let bind copies of the lambda for each instantiation and mangle the type variant into the name? That would entail updating references and I'm not sure whether this is actually possible in general? What about lambda return values, conditionals and so forth?

Update 2
I still feel like I did not describe my problem sufficiently. My language is really rather simple and I would like to stick with a simple ty

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) -> 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.

StackExchange Computer Science Q#105359, answer score: 5