diff --git a/Strata/DL/Imperative/CmdType.lean b/Strata/DL/Imperative/CmdType.lean
index 9ea4b7d37..7952d17d4 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