Add variable name to error message

[Dragon-Hatcher]

Add the variable name to the error message when unification fails on initialization.

[tautschnig]

1. Underlying unifier error is dropped (fun _ => …). For init x : Map int bool := … where the right-hand side has type Map string bool, the original TC.unifyTypes (Core's, line 96 of Languages/Core/CmdType.lean) reports the constructor-level mismatch via Constraints.unify's formatted output. Substituting a generic expected/inferred message hides the why. Consider preserving the original message:

   let τ ← (TC.unifyTypes τ [(xty, ety)]).mapError fun e =>
     md.toDiagnosticF f!"Variable {x} expected type {xty} but initialization expression has inferred type {ety}: {TC.typeErrorFmt e}"

   TC.typeErrorFmt is already in the typeclass for exactly this reason.

2. No regression test exercises the new branch. I traced the closest existing test (StrataTest/Languages/Core/Tests/StatementTypeTests.lean:81, Impossible to unify bool with int) and it short-circuits inside inferType before reaching the outer unifyTypes [(xty, ety)] you patched, so the new message is currently uncovered by CI. A 3-line #guard_msgs for init x : bool := #2 (or any concrete-type mismatch where the RHS is well-typed on its own) would lock the wording in.

3. .set arm has the same pattern (line 63) but is not updated. If the rationale for the new wording is that the variable name + types make the error actionable, the same applies to x := expr mismatches. Worth doing in this PR for consistency, ideally via a small helper:

   private def unifyOrAnnotate (md : Md) (x : P.Ident) (xty ety : P.Ty)
       (τ : T) : Except DiagnosticModel T :=
     (TC.unifyTypes τ [(xty, ety)]).mapError fun e =>
       md.toDiagnosticF f!"Variable {x} expected type {xty} but expression has type {ety}: {TC.typeErrorFmt e}"

   then call from both .init and .set (and reuse anywhere else that surfaces type mismatches against a named binding).

Minor style nit: existing error messages in this file write Variable {x} (no quotes) — see lines 36 and 54. New message uses Variable '{x}'. Pick one. Suggest dropping the quotes for consistency.