fix: Repr instances for Int and Float

closes #4677

src/Init/Data/Float.lean

@@ -101,13 +101,13 @@ Returns an undefined value if `x` is not finite.
 instance : ToString Float where
   toString := Float.toString
 
+@[extern "lean_uint64_to_float"] opaque UInt64.toFloat (n : UInt64) : Float
+
 instance : Repr Float where
-  reprPrec n _ := Float.toString n
+  reprPrec n prec := if n < UInt64.toFloat 0 then Repr.addAppParen (toString n) prec else toString n
 
 instance : ReprAtom Float  := ⟨⟩
 
-@[extern "lean_uint64_to_float"] opaque UInt64.toFloat (n : UInt64) : Float
-
 @[extern "sin"] opaque Float.sin : Float → Float
 @[extern "cos"] opaque Float.cos : Float → Float
 @[extern "tan"] opaque Float.tan : Float → Float

src/Init/Data/Repr.lean

@@ -230,7 +230,7 @@ protected def Int.repr : Int → String
     | negSucc m => "-" ++ Nat.repr (succ m)
 
 instance : Repr Int where
-  reprPrec i _ := i.repr
+  reprPrec i prec := if i < 0 then Repr.addAppParen i.repr prec else i.repr
 
 def hexDigitRepr (n : Nat) : String :=
   String.singleton <| Nat.digitChar n

tests/lean/run/4677.lean

@@ -0,0 +1,53 @@
+inductive Bob where | mk (x : Int)
+deriving Repr
+
+/--
+info: Bob.mk (-1)
+-/
+#guard_msgs in
+#eval Bob.mk (-1)
+
+/--
+info: [-1, 2]
+-/
+#guard_msgs in
+#eval [(3 : Int) - 4, 2]
+
+/--
+info: -2
+-/
+#guard_msgs in
+#eval -3 + 1
+
+/--
+info: Bob.mk 2
+-/
+#guard_msgs in
+#eval Bob.mk 2
+
+inductive Boo where | mk (x : Float)
+deriving Repr
+
+/--
+info: [-1.000000, 2.000000]
+-/
+#guard_msgs in
+#eval [-1.0, 2.0]
+
+/--
+info: Boo.mk (-1.000000)
+-/
+#guard_msgs in
+#eval Boo.mk (-1.0)
+
+/--
+info: Boo.mk 1.000000
+-/
+#guard_msgs in
+#eval Boo.mk 1.0
+
+/--
+info: -1.000000
+-/
+#guard_msgs in
+#eval -1.0