Discrimination trees for instance search (#7109)

agda · Mar 9, 2024 · aa5d8bb · aa5d8bb
1 parent 426d699
commit aa5d8bb
Show file tree

Hide file tree

Showing 24 changed files with 906 additions and 103 deletions.
diff --git a/Agda.cabal b/Agda.cabal
@@ -631,6 +631,8 @@ library
       Agda.TypeChecking.DeadCode
       Agda.TypeChecking.DisplayForm
       Agda.TypeChecking.DropArgs
+      Agda.TypeChecking.DiscrimTree
+      Agda.TypeChecking.DiscrimTree.Types
       Agda.TypeChecking.Empty
       Agda.TypeChecking.EtaContract
       Agda.TypeChecking.Errors

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -87,6 +87,16 @@ Language
 
 Changes to type checker and other components defining the Agda language.
 
+* Agda now uses *discrimination trees* to store and look up instance
+  definitions, rather than linearly searching through all instances for
+  a given "class" ([PR #7109](https://github.com/agda/agda/pull/7109)).
+
+  This is a purely internal change, and should not result in any change
+  to which programs are accepted or rejected. However, it significantly
+  improves the performance of instance search, especially for the case
+  of a "type class" indexed by a single type argument. The new lookup
+  procedure should never be slower than the previous implementation.
+
 Reflection
 ----------
 

diff --git a/src/full/Agda/Benchmarking.hs b/src/full/Agda/Benchmarking.hs
@@ -97,6 +97,14 @@ data Phase
     -- ^ Subphase for 'Typing': generalizing over `variable`s
   | InstanceSearch
     -- ^ Subphase for 'Typing': solving instance goals
+  | Reflection
+    -- ^ Subphase for 'Typing': evaluating elaborator reflection
+  | InitialCandidates
+    -- ^ Subphase for 'InstanceSearch': collecting initial candidates
+  | FilterCandidates
+    -- ^ Subphase for 'InstanceSearch': checking candidates for validity
+  | OrderCandidates
+    -- ^ Subphase for 'InstanceSearch': ordering candidates for specificity
   | UnifyIndices
     -- ^ Subphase for 'CheckLHS': unification of the indices
   | InverseScopeLookup

diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs
@@ -64,6 +64,7 @@ import Agda.Syntax.Scope.Base
 import Agda.Syntax.TopLevelModuleName
 import Agda.Syntax.Translation.ConcreteToAbstract as CToA
 
+import Agda.TypeChecking.InstanceArguments
 import Agda.TypeChecking.Errors
 import Agda.TypeChecking.Warnings hiding (warnings)
 import Agda.TypeChecking.Reduce
@@ -277,7 +278,6 @@ addImportedThings isig metas ibuiltin patsyns display userwarn
   stTCWarnings           `modifyTCLens` \ imp -> imp `List.union` warnings
   stOpaqueBlocks         `modifyTCLens` \ imp -> imp `Map.union` oblock
   stOpaqueIds            `modifyTCLens` \ imp -> imp `Map.union` oid
-  addImportedInstances isig
 
 -- | Scope checks the given module. A proper version of the module
 -- name (with correct definition sites) is returned.
@@ -1058,6 +1058,10 @@ createInterface mname file isMain msrc = do
 
     unfreezeMetas
 
+    -- Remove any instances that now have visible arguments from the
+    -- instance tree before serialising.
+    pruneTemporaryInstances
+
     -- Profiling: Count number of metas.
     whenProfile Profile.Metas $ do
       m <- fresh