#7085: Mimer not recognising qualified hints (#7088)

fix #7085: Mimer not recognising qualified hints
agda · Feb 5, 2024 · 208f2bf · 208f2bf
1 parent 2925d77
commit 208f2bf
Show file tree

Hide file tree

Showing 4 changed files with 27 additions and 1 deletion.
diff --git a/src/full/Agda/Mimer/Mimer.hs b/src/full/Agda/Mimer/Mimer.hs
@@ -449,7 +449,7 @@ collectComponents opts costs ii mDefName whereNames metaId = do
         }
   metaVar <- lookupLocalMeta metaId
   hintNames <- getEverythingInScope metaVar
-  components' <- foldM go components hintNames
+  components' <- foldM go components $ explicitHints ++ (hintNames \\ explicitHints)
   return BaseComponents
     { hintFns = doSort $ hintFns components'
     , hintDataTypes = doSort $ hintDataTypes components'

diff --git a/test/interaction/Issue7085.agda b/test/interaction/Issue7085.agda
@@ -0,0 +1,13 @@
+
+postulate A : Set
+
+module M where
+  postulate a : A
+
+x : A
+x = {! M.a !} -- No solution found
+
+open M
+
+y : A
+y = {! M.a !} -- works
diff --git a/test/interaction/Issue7085.in b/test/interaction/Issue7085.in
@@ -0,0 +1,3 @@
+top_command (cmd_load currentFile [])
+goal_command 0 cmd_autoOne "M.a"
+goal_command 1 cmd_autoOne "M.a"
diff --git a/test/interaction/Issue7085.out b/test/interaction/Issue7085.out
@@ -0,0 +1,10 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "?0 : A ?1 : A " nil)
+((last . 1) . (agda2-goals-action '(0 1)))
+(agda2-give-action 0 "M.a")
+((last . 1) . (agda2-goals-action '(1)))
+(agda2-give-action 1 "a")
+((last . 1) . (agda2-goals-action '()))