refactor: break DiscrTree -> WHNF dependency

Motivation: we want to use `whnfCore` at `DiscrTree.lean`

src/Lean/Meta/GetConst.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Lean.Meta.Instances
+import Lean.Meta.GlobalInstances
 
 namespace Lean.Meta
 

src/Lean/Meta/GlobalInstances.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Basic
+import Lean.ScopedEnvExtension
+
+namespace Lean.Meta
+
+builtin_initialize globalInstanceExtension : SimpleScopedEnvExtension Name (Std.PersistentHashMap Name Unit)  ←
+  registerSimpleScopedEnvExtension {
+    name     := `ginstanceExt
+    initial  := {}
+    addEntry := fun s n => s.insert n ()
+  }
+
+def addGlobalInstance (declName : Name) (attrKind : AttributeKind) : MetaM Unit := do
+  globalInstanceExtension.add declName attrKind
+
+@[export lean_is_instance]
+def isGlobalInstance (env : Environment) (declName : Name) : Bool :=
+  globalInstanceExtension.getState env |>.contains declName
+
+end Lean.Meta

src/Lean/Meta/Instances.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.ScopedEnvExtension
+import Lean.Meta.GlobalInstances
 import Lean.Meta.DiscrTree
 
 namespace Lean.Meta
@@ -25,16 +26,10 @@ instance : ToFormat InstanceEntry where
 
 structure Instances where
   discrTree       : DiscrTree InstanceEntry := DiscrTree.empty
-  globalInstances : NameSet := {}
   deriving Inhabited
 
-def addInstanceEntry (d : Instances) (e : InstanceEntry) : Instances := {
-  d with
-    discrTree := d.discrTree.insertCore e.keys e
-    globalInstances := match e.globalName? with
-      | some n => d.globalInstances.insert n
-      | none   => d.globalInstances
-}
+def addInstanceEntry (d : Instances) (e : InstanceEntry) : Instances :=
+  { d with discrTree := d.discrTree.insertCore e.keys e }
 
 builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry Instances ←
   registerSimpleScopedEnvExtension {
@@ -52,6 +47,7 @@ private def mkInstanceKey (e : Expr) : MetaM (Array DiscrTree.Key) := do
 def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
   let c ← mkConstWithLevelParams declName
   let keys ← mkInstanceKey c
+  addGlobalInstance declName attrKind
   instanceExtension.add { keys := keys, val := c, priority := prio, globalName? := declName } attrKind
 
 builtin_initialize
@@ -63,10 +59,6 @@ builtin_initialize
       discard <| addInstance declName attrKind prio |>.run {} {}
   }
 
-@[export lean_is_instance]
-def isGlobalInstance (env : Environment) (declName : Name) : Bool :=
-  Meta.instanceExtension.getState env |>.globalInstances.contains declName
-
 def getGlobalInstancesIndex : MetaM (DiscrTree InstanceEntry) :=
   return Meta.instanceExtension.getState (← getEnv) |>.discrTree