fix: reduce type-level let (TLet) RHS in the interpreter

[hackworth-ltd-claude-code]

Fixes #1439.

Problem

Primer.EvalFullInterp.interpTy evaluates types in an environment whose values are meant to be normal forms — the TVar case returns a stored value verbatim. But the TLet case bound its right-hand side unevaluated:

TLet _ v s t -> interpTy (extendTyEnv' v s env) t

Every other binding site already interprets first — term-level Let, LetType, BETA/APP, the Case argument types, and TForall. TLet was the lone exception, so type-level lets were left partly unreduced, and could even leak a dangling, out-of-scope type variable into the result.

Structure

As requested on the issue, the PR is split so the bug is demonstrated before it's fixed:

1. test: adds two regression tests (unit_tlet_reduce_rhs, unit_tlet_reduce_rhs_let). They fail at this commit, demonstrating the bug:
   • tlet a = C in (tlet v = a in v) → reduces to a dangling TVar "a" instead of C.
   • tlet v = (tlet w = C in w) in (v -> v) → leaves residual tlets instead of C -> C.
2. fix: interprets the RHS before binding it (interpTy (extendTyEnv' v (interpTy env s) env) t), turning both tests green. It's safe and terminating, since type evaluation always terminates.

Notes

• Independent of Interpreter can't reduce top-level definitions #1247 / fix: reduce top-level definitions in the interpreter #1438: that work was term-level reduction; this is in interpTy.
• The existing unit_tlet* tests don't catch this because their RHSs are already normal forms (so the missing interpTy is a no-op). tasty_two_interp_agree rarely generates the failing shape, and a residual concrete TLet in a checkable position is masked by upsilon.

A note on the DCO check

I'm an automated agent (Hackworth Ltd Claude Code) and can't certify the Developer Certificate of Origin, so these commits aren't signed off and the check-dco status will be red. A human with authority to certify the sign-off will need to resolve that before merge.

[hackworth-ltd-claude-code]

The first commit (b4aed7e) is intentionally red: its two tests fail in CI exactly as expected, demonstrating the bug.

• tlet reduce rhs — tlet a = C in (tlet v = a in v) reduced to a dangling, out-of-scope TVar "a" instead of C.
• tlet reduce rhs let — tlet v = (tlet w = C in w) in (v -> v) left residual tlets instead of C -> C.

(2 out of 886 tests failed, both in primer-test's EvalFullInterp group.)

The second commit (de694f3) is the fix: interpTy now reduces the TLet right-hand side before binding it, just as every other binding site already does. Both tests then pass and the full suite is green (886/886).