From 085c7e59ba675fbad89eb29f401a210accfdef9e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Nov 2020 16:43:12 -0800
Subject: [PATCH] feat: apply default instances using priorities

---
 src/Lean/Elab/SyntheticMVars.lean | 42 ++++++++++++++++++-------------
 src/Lean/Meta/Instances.lean      | 14 ++++++++---
 2 files changed, 36 insertions(+), 20 deletions(-)

diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 645f012f07..24a3773700 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -146,36 +146,33 @@ def tryToSynthesizeUsingDefaultInstance (mvarId : MVarId) (defaultInstance : Nam
     else
       return none
 
-def tryToSynthesizeUsingDefaultInstances (mvarId : MVarId) : MetaM (Option (List SyntheticMVarDecl)) :=
+def tryToSynthesizeUsingDefaultInstances (mvarId : MVarId) (prio : Nat) : MetaM (Option (List SyntheticMVarDecl)) :=
   withMVarContext mvarId do
     let mvarType := (← Meta.getMVarDecl mvarId).type
-     match (← isClass? mvarType) with
-     | none => return none
-     | some className =>
-       match (← getDefaultInstances className) with
-       | [] => return none
-       | defaultInstances =>
-         for (defaultInstance, prio) in defaultInstances do
+    match (← isClass? mvarType) with
+    | none => return none
+    | some className =>
+      match (← getDefaultInstances className) with
+      | [] => return none
+      | defaultInstances =>
+        for (defaultInstance, instPrio) in defaultInstances do
+          if instPrio == prio then
             match (← tryToSynthesizeUsingDefaultInstance mvarId defaultInstance) with
             | some newMVarDecls => return some newMVarDecls
             | none => continue
-         return none
+        return none
 
-/--
-  Apply default value to any pending synthetic metavariable of kind `SyntheticMVarKind.withDefault`
-  Return true if something was synthesized. -/
-def synthesizeUsingDefault : TermElabM Bool := do
-  let s ← get
-  let currLength := s.syntheticMVars.length
+/- Used to implement `synthesizeUsingDefault`. This method only consider default instances with the given priority. -/
+def synthesizeUsingDefaultPrio (prio : Nat) : TermElabM Bool := do
   let mut syntheticMVarsNew := []
   let mut modified := false
   /- Recall that s.syntheticMVars is essentially a stack. The first metavariable was the last one created.
      We want to apply the default instance in reverse creation order. Otherwise,
      `toString 0` will produce a `OfNat String` cannot be synthesized error. -/
-  for mvarDecl in s.syntheticMVars.reverse do
+  for mvarDecl in (← get).syntheticMVars.reverse do
     match mvarDecl.kind with
     | SyntheticMVarKind.typeClass =>
-        match (← withRef mvarDecl.stx <| tryToSynthesizeUsingDefaultInstances mvarDecl.mvarId) with
+        match (← withRef mvarDecl.stx <| tryToSynthesizeUsingDefaultInstances mvarDecl.mvarId prio) with
         | none =>
           syntheticMVarsNew := mvarDecl :: syntheticMVarsNew
         | some newMVarDecls =>
@@ -185,6 +182,17 @@ def synthesizeUsingDefault : TermElabM Bool := do
   modify fun s => { s with syntheticMVars := syntheticMVarsNew }
   return modified
 
+/--
+  Apply default value to any pending synthetic metavariable of kind `SyntheticMVarKind.withDefault`
+  Return true if something was synthesized. -/
+def synthesizeUsingDefault : TermElabM Bool := do
+  let prioSet ← getDefaultInstancesPriorities
+  /- Recall that `prioSet` is stored in descending order -/
+  for prio in prioSet do
+    if (← synthesizeUsingDefaultPrio prio) then
+      return true
+  return false
+
 /-- Report an error for each synthetic metavariable that could not be resolved. -/
 private def reportStuckSyntheticMVars : TermElabM Unit := do
   let s ← get
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index ead51f892d..44ed2ab6d1 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -78,7 +78,7 @@ structure DefaultInstanceEntry where
   instanceName : Name
   priority     : Nat
 
-abbrev PrioritySet := Std.RBTree Nat (.<.)
+abbrev PrioritySet := Std.RBTree Nat (.>.)
 
 structure DefaultInstances where
   defaultInstances : NameMap (List (Name × Nat)) := {}
@@ -117,9 +117,17 @@ builtin_initialize
     name  := `defaultInstance,
     descr := "type class default instance",
     add   := fun declName args persistent => do
-      if args.hasArgs then throwError "invalid attribute 'defaultInstance', unexpected argument"
+      let prio ←
+        if args.isNone then
+          pure 0
+        else if args.getNumArgs == 1 then
+          match args[0].isNatLit? with
+          | none => throwErrorAt args[0] "unexpected argument at attribute 'defaultInstance', numeral expected"
+          | some n => pure n
+        else
+          throwErrorAt args "too many arguments at attribute 'defaultInstance', numeral expected"
       unless persistent do throwError "invalid attribute 'defaultInstance', must be persistent"
-      addDefaultInstance declName |>.run {} {}
+      addDefaultInstance declName prio |>.run {} {}
       pure ()
   }