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

`interpTy` bound the right-hand side of a type-level `tlet` into the type
environment unevaluated, while the `TVar` lookup returns stored values
verbatim -- relying on them being normal forms. Every other binding site
(term-level `Let`, `LetType`, `BETA`/`APP`, the `Case` argument types, and
`TForall`) already interprets its RHS first; `TLet` was the lone exception.

Interpret the RHS before binding it. This is safe and terminating, since
type evaluation always terminates. It fixes both witnesses from the
previous commit: type-level `let`s now fully reduce instead of leaving a
dangling out-of-scope variable or residual `tlet`s.

Fixes #1439.

Author: Hackworth Ltd Claude Code

primer/src/Primer/EvalFullInterp.hs

@@ -380,7 +380,11 @@ interpTy env = \case
   TForall _ v k t ->
     let v' = freshLikeTy v env
      in TForall () v' k (interpTy (extendTyEnv' v (TVar () v') env) t)
-  TLet _ v s t -> interpTy (extendTyEnv' v s env) t
+  -- We must reduce the RHS before binding it, just as every other binding site
+  -- does: the 'TVar' case returns stored values verbatim, relying on the
+  -- environment holding normal forms. (Type evaluation always terminates, so
+  -- this cannot loop.)
+  TLet _ v s t -> interpTy (extendTyEnv' v (interpTy env s) env) t
 
 extendTmEnv ::
   Either GVarName LVarName ->