fix: defaultInstance priorities for Neg Int and OfScientific Float

src/Init/Data/Int/Basic.lean

@@ -59,7 +59,14 @@ protected def mul (m n : @& Int) : Int :=
   | negSucc m, ofNat n   => negOfNat (succ m * n)
   | negSucc m, negSucc n => ofNat (succ m * succ n)
 
-@[defaultInstance]
+/-
+  The `Neg Int` default instance must have priority higher than `low` since
+  the default instance `OfNat Nat n` has `low` priority.
+  ```
+  #check -42
+  ```
+-/
+@[defaultInstance mid]
 instance : Neg Int where
   neg := Int.neg
 instance : Add Int where

src/Init/Data/OfScientific.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Meta
 import Init.Data.Float
 import Init.Data.Nat
 
@@ -15,6 +16,13 @@ import Init.Data.Nat
 class OfScientific (α : Type u) where
   ofScientific : Nat → Bool → Nat → α
 
-@[defaultInstance low]
+/-
+  The `OfScientifi Float` must have priority higher than `mid` since
+  the default instance `Neg Int` has `mid` priority.
+  ```
+  #check -42.0 -- must be Float
+  ```
+-/
+@[defaultInstance mid+1]
 instance : OfScientific Float where
   ofScientific m s e := Float.ofScientific m s e

src/Init/Notation.lean

@@ -32,6 +32,7 @@ macro "maxPrec!" : term => `(1024)
 
 macro "default" : prio => `(1000)
 macro "low"     : prio => `(100)
+macro "mid"     : prio => `(1000)
 macro "high"    : prio => `(10000)
 macro "(" p:prio ")" : prio => p
 

tests/lean/negFloat.lean

@@ -0,0 +1,6 @@
+#check 42
+#check -42
+#check -42.0
+#eval -42.0
+#eval Neg.neg 42.0
+#eval 1.0 * -42.0

tests/lean/negFloat.lean.expected.out

@@ -0,0 +1,6 @@
+42 : Nat
+-42 : Int
+-42.0 : Float
+-42.000000
+-42.000000
+-42.000000