diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index d2dc1b0434..cfb3508279 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -328,6 +328,8 @@ instance [ToMessageData α] : ToMessageData (List α)  := ⟨fun as => MessageDa
 instance [ToMessageData α] : ToMessageData (Array α) := ⟨fun as => toMessageData as.toList⟩
 instance [ToMessageData α] : ToMessageData (Subarray α) := ⟨fun as => toMessageData as.toArray.toList⟩
 instance [ToMessageData α] : ToMessageData (Option α) := ⟨fun | none => "none" | some e => "some (" ++ toMessageData e ++ ")"⟩
+instance [ToMessageData α] [ToMessageData β] : ToMessageData (α × β) :=
+  ⟨fun (a, b) => .paren <| toMessageData a ++ "," ++ Format.line ++ toMessageData b⟩
 instance : ToMessageData (Option Expr) := ⟨fun | none => "<not-available>" | some e => toMessageData e⟩
 
 syntax:max "m!" interpolatedStr(term) : term