Named Implementations aren't found by other Implementations with using clause

[fabianhjr]

Steps to Reproduce

module Test

interface MagmaT a where
  op: a -> a -> a

interface MagmaT a => SemigroupT a where
  assoc: (x, y, z: a) -> (x `op` y) `op` z = x `op` (y `op` z)

[NamedMagma] MagmaT Bool where
  False `op` False = False
  _     `op` _     = True

[NamedSemigroup] SemigroupT Bool using NamedMagma where
  assoc = ?hole

Expected Behavior

Typecheck with a hole named ?hole

Observed Behavior

1/1: Building Test (Test.idr)
Test.idr:7:26--9:1:While processing constructor SemigroupT at Test.idr:6:1--9:1 at Test.idr:6:1--9:1:
Can't find an implementation for MagmaT a

[fabianhjr]

I think this is happening in Idris.Desugar:692-714 but I don't have any idea of what is going on there. :?

[clayrat]

At least in Idris1 this is by design - because named implementations have all restrictions lifted, the auto-search is turned off for them.

[fabianhjr]

@clayrat, however they should be found with the using keywork and the name of the implementation to use.

[clayrat]

Ah sorry, missed the using.

[fabianhjr]

I think I found an issue that may be causing this behaviour. In Idris/Parser implDecl is defined as:

implDecl : FileName -> IndentInfo -> Rule PDecl
implDecl fname indents
    = do start <- location
         vis <- visibility
         col <- column
         option () (keyword "implementation")
         iname <- option Nothing (do symbol "["
                                     iname <- name
                                     symbol "]"
                                     pure (Just iname))
         impls <- implBinds fname indents
         cons <- constraints fname indents
         n <- identName
         params <- many (simpleExpr fname indents)
         nusing <- option [] (do keyword "using"
                                 names <- some name
                                 pure names)
         body <- optional (do keyword "where"
                              blockAfter col (topDecl fname))
         atEnd indents
         end <- location
         pure (PImplementation (MkFC fname start end)
                         vis Single impls cons n params iname nusing
                         (map (collectDefs . concat) body))

of which name in Parser/Support was defined as:

name : Rule Name
name
    = do ns <- namespace_
         (do symbol ".("
             op <- operator
             symbol ")"
             pure (NS ns (UN op))) <|>
           (either (\n => fail ("Can't use reserved name " ++ n))
                   pure (mkFullName ns))
  <|> do symbol "("
         op <- operator
         symbol ")"
         pure (UN op)
 where
   reserved : String -> Bool
   reserved n = n `elem` reservedNames

   mkFullName : List String -> Either String Name
   mkFullName [] = Right $ UN "NONE" -- Can't happen :)
   mkFullName [n]
       = if reserved n
            then Left n
            else Right (UN n)
   mkFullName (n :: ns)
       = if reserved n
            then Left n
            else Right (NS ns (UN n))

which seem off since it is parsing operators/symbols and not identifiers.

Upon testing by implementing

--- a/src/Parser/Support.idr
+++ b/src/Parser/Support.idr
@@ -328,6 +328,10 @@ namespace_
 export
 unqualifiedName : Rule String
 unqualifiedName = identPart
+qualifiedName : Rule Name
+qualifiedName = do ns <- namespace_
+                   n <- identPart
+                   pure (NS ns (UN n))

 export
 holeName : Rule String
@@ -342,6 +346,25 @@ reservedNames
     = ["Type", "Int", "Integer", "String", "Char", "Double",
        "Lazy", "Inf", "Force", "Delay"]

+isReservedName : String -> Bool
+isReservedName n = n `elem` reservedNames
+
+export
+identName : Rule Name
+identName
+    = do n <- qualifiedName
+         pure n <|>
+           (either (\n => fail ("Can't use reserved name " ++ show (nameRoot n)))
+                   pure (mkFullName n))
+    <|> do n <- unqualifiedName
+           pure (UN n)
+ where
+   mkFullName : Name -> Either Name Name
+   mkFullName n
+       = if isReservedName (nameRoot n)
+            then Left n
+            else Right n
+
 export
 name : Rule Name
 name
@@ -356,20 +379,17 @@ name
          op <- operator
          symbol ")"
          pure (UN op)
- where
-   reserved : String -> Bool
-   reserved n = n `elem` reservedNames
-
-   mkFullName : List String -> Either String Name
-   mkFullName [] = Right $ UN "NONE" -- Can't happen :)
-   mkFullName [n]
-       = if reserved n
-            then Left n
-            else Right (UN n)
-   mkFullName (n :: ns)
-       = if reserved n
-            then Left n
-            else Right (NS ns (UN n))
+  where
+    mkFullName : List String -> Either String Name
+    mkFullName [] = Right $ UN "NONE" -- Can't happen :)
+    mkFullName [n]
+        = if isReservedName n
+             then Left n
+             else Right (UN n)
+    mkFullName (n :: ns)
+        = if isReservedName n
+             then Left n
+             else Right (NS ns (UN n))

 export
 IndentInfo : Type

seems like interface stuff works but some other things get broken. I will try to clean up a Merge Request if I can get the borked tests to pass.