[ fix agda#5787 ] Leave checking of modality of instance candidates t…

…o later phase
jespercockx · Feb 11, 2022 · dcc2ae8 · dcc2ae8
1 parent ba99b8e
commit dcc2ae8
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/src/full/Agda/TypeChecking/InstanceArguments.hs b/src/full/Agda/TypeChecking/InstanceArguments.hs
@@ -86,7 +86,6 @@ initialInstanceCandidates t = do
           vars = [ Candidate LocalCandidate x t (isOverlappable info)
                  | (x, Dom{domInfo = info, unDom = (_, t)}) <- varsAndRaisedTypes
                  , isInstance info
-                 , usableModality info
                  ]
 
       -- {{}}-fields of variables are also candidates

diff --git a/test/Succeed/Issue5787.agda b/test/Succeed/Issue5787.agda
@@ -0,0 +1,7 @@
+
+postulate
+  A B : Set
+  f : @0 {{A}} → B
+
+g : @0 {{A}} → B
+g = f