Remove `LaurelTypes.lean`

[leo-leesco]

Provided type checking is correct and we have enough type information via Resolution.lean, we might want to remove LaurelTypes.lean altogether because it simply recomputes the types. This means :

• transporting types along with the AST
• theoretically making sure we have enough type information (because we prefer checking mode as much as possible, some/most constructors never synthesize) ; another way to put it is saying that we reject insufficient typing by the user by construction

Relates to #1121

[leo-leesco]

Some ideas we can explore to achieve that :

1. Cache per-node types on the AST

Add type : Option HighTypeMd := none to AstNode StmtExpr (or wrap StmtExpr in a typed-AST after resolution). Resolution writes the type as it synthesizes. Every pass reads expr.type.

2. Cache as a Std.HashMap Nat HighTypeMd on SemanticModel

Assign every expression node a fresh Nat ID during resolution (extend the existing fresh-ID counter). SemanticModel gets a nodeTypes : Std.HashMap Nat HighTypeMd. Consumers read model.nodeTypes.get? id.

I personally prefer option 2.