From e4406664a3f4eac790817d0d9f0f207c771fc6aa Mon Sep 17 00:00:00 2001 From: Dragon-Hatcher Date: Wed, 20 May 2026 10:34:02 -0700 Subject: [PATCH] Add variable name to error message --- Strata/DL/Imperative/CmdType.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Strata/DL/Imperative/CmdType.lean b/Strata/DL/Imperative/CmdType.lean index 9ea4b7d37f..7952d17d46 100644 --- a/Strata/DL/Imperative/CmdType.lean +++ b/Strata/DL/Imperative/CmdType.lean @@ -37,7 +37,9 @@ def Cmd.typeCheck {P C T} [ToFormat P.Ident] [ToFormat P.Ty] [ToFormat (Cmd P)] else let (xty, τ) ← TC.preprocess ctx τ xty let (expr, ety, τ) ← TC.inferType ctx τ c expr - let τ ← TC.unifyTypes τ [(xty, ety)] + let τ ← (TC.unifyTypes τ [(xty, ety)]).mapError fun _ => + md.toDiagnosticF f!"Variable '{x}' expected type {xty} but \ + initialization expression has inferred type {ety}." let (xty, τ) ← TC.postprocess ctx τ xty let τ := TC.update τ x xty let c := Cmd.init x xty (.det expr) md