fix: fixes #1813

Remark: modifies the value for the `mid` priority.
See new note at `Init/Notation.lean`

src/Init/Notation.lean

@@ -131,13 +131,30 @@ macro "max_prec" : term => `(1024)
 macro "default" : prio => `(prio| 1000)
 /-- The standardized "low" priority `low = 100`, for things that should be lower than default priority. -/
 macro "low"     : prio => `(prio| 100)
-/-- The standardized "medium" priority `med = 1000`. This is the same as `default`. -/
-macro "mid"     : prio => `(prio| 1000)
+/--
+The standardized "medium" priority `med = 1000`. This is lower than `default`, and higher than `low`.
+-/
+macro "mid"     : prio => `(prio| 500)
 /-- The standardized "high" priority `high = 10000`, for things that should be higher than default priority. -/
 macro "high"    : prio => `(prio| 10000)
 /-- Parentheses are used for grouping priority expressions. -/
 macro "(" p:prio ")" : prio => return p
 
+/-
+Note regarding priorities. We want `low < mid < default` because we have the following default instances:
+```
+@[default_instance low] instance (n : Nat) : OfNat Nat n where ...
+@[default_instance mid] instance : Neg Int where ...
+@[default_instance default] instance [Add α] : HAdd α α α where ...
+@[default_instance default] instance [Sub α] : HSub α α α where ...
+...
+```
+
+Monomorphic default instances must always "win" to preserve the Lean 3 monomorphic "look&feel".
+The `Neg Int` instance must have precedence over the `OfNat Nat n` one, otherwise we fail to elaborate `#check -42`
+See issue #1813 for an example that failed when `mid = default`.
+-/
+
 -- Basic notation for defining parsers
 -- NOTE: precedence must be at least `arg` to be used in `macro` without parentheses
 

tests/lean/1007.lean

@@ -8,7 +8,7 @@ structure ℝ where
 instance instFoo1 {X : Type u} {Y : Type v} [Vec X] [Vec Y] : Vec (X × Y) := sorry
 instance instProblem {α : Type u} {X : Type v} [Vec X] : Vec (α → X) := sorry
 
-instance (priority := mid+1) instFoo2 : Vec ℝ := sorry
+instance (priority := default+1) instFoo2 : Vec ℝ := sorry
 
 --------------
 

tests/lean/1007.lean.expected.out

@@ -1,6 +1,6 @@
 1007.lean:8:9-8:17: warning: declaration uses 'sorry'
 1007.lean:9:9-9:20: warning: declaration uses 'sorry'
-1007.lean:11:29-11:37: warning: declaration uses 'sorry'
+1007.lean:11:33-11:41: warning: declaration uses 'sorry'
 1007.lean:15:9-15:20: warning: declaration uses 'sorry'
 1007.lean:34:0-34:8: warning: declaration uses 'sorry'
 1007.lean:35:0-35:8: warning: declaration uses 'sorry'

tests/lean/run/1813.lean

@@ -0,0 +1,4 @@
+example [Add α] [Neg α] [Mul α] [∀ n, OfNat α n] {a b : α} :=
+  calc
+    4 + 5 * b = -6 + 5 * (b + 2) := sorry
+            _ = -6 + 5 * 3 := sorry