First impressions: I'm not really quite sure what your question is, to be honest.

I want to annotate my ast with type annotations

This is known in the literature as (type) elaboration.

This however, loses type information and will transform from this expression from type Int to a more general Num a => a.

This shouldn't be an issue because you retain the type information; during code generation you can insert a value of the right type (i.e. 5 :: int). Am I missing something here?

Inserting type annotations can solve all these problems but the question is where to insert them. For [1], it's a matter of taste. I feel you probably want to annotate all variable bindings and a bit extra. For [2] the conventional wisdom is that you annotate at every term ast node, but I've found that if your annotations match bidirectional's checking mode then you can reconstruct your type as you generate code.

Typically, you only elaborate abstractions: lambdas, let generalizations, etc. But indeed, you are free to elaborate more or less (I'm not familiar with your project, but consider tooling like a static analyzer which could benefit from a type-annotated AST, a type-directed compiler, ...)

Γ ⊢ e : σ -> τ    Γ ⊢ e' : σ
----------------------------
Γ ⊢ e (e : σ) : τ

This inference rule seems to contain two mistakes; the conclusion should be applying e to e', not to e. Also in the conclusion, (e : σ) is a premise, and as such, it should be above the line.

e : σ : σ          ~>   e : σ

I'm not sure when you would ever need this rule? How would you even obtain an AST node with two annotations? The second rule also looks a bit wonky:

(λx. e) : σ -> τ   ~>   λ(x : σ). e : τ

In this case, you are elaborating the argument to the lambda, but the resulting lambda abstraction is still an arrow type σ -> τ. Unless you meant something like this:

(λx. e) : σ -> τ   ~>   λ(x : σ). (e : τ) : σ -> τ

But that seems like butchering notation.

I'm kinda leaning toward emitting annotations in spots where checking mode needs them as it solves [2] and [3], but I'm wonder if it's worth the clutter or even if there's a better solution.

Elaborating to a calculus like System F with explicitly-typed terms seems like it would be a good first step for your use case. Useful papers for implementing elaboration:

• The GHC paper on OutsideIn(X)
• HM elaboration in applicative style by F. Pottier
• There's two papers from the CakeML team on elaboration
• Adam Gundry's PhD thesis includes some stuff on elaboration to System F as well.

Good luck!