[ fix ] deduplicate definedInBlock results

src/TTImp/Elab/Local.idr

@@ -54,9 +54,7 @@ localHelper {vars} nest env nestdecls_in func
               else nestdeclsVis
 
          let defNames = definedInBlock emptyNS nestdeclsMult
-         names' <- traverse (applyEnv f)
-                            (nub defNames) -- binding names must be unique
-                                           -- fixes bug #115
+         names' <- traverse (applyEnv f) defNames
          let nest' = { names $= (names' ++) } nest
          let env' = dropLinear env
          -- We don't want to keep rechecking delayed elaborators in the

src/TTImp/TTImp.idr

@@ -13,6 +13,8 @@ import Data.List
 import Data.List1
 import Data.Maybe
 
+import Libraries.Data.SortedSet
+
 %default covering
 
 -- Information about names in nested blocks
@@ -772,7 +774,7 @@ export
 definedInBlock : Namespace -> -- namespace to resolve names
                  List ImpDecl -> List Name
 definedInBlock ns decls =
-    concatMap (defName ns) decls
+    SortedSet.toList $ foldl (defName ns) empty decls
   where
     getName : ImpTy -> Name
     getName (MkImpTy _ _ n _) = n
@@ -788,17 +790,17 @@ definedInBlock ns decls =
            DN _ _ => NS ns n
            _ => n
 
-    defName : Namespace -> ImpDecl -> List Name
-    defName ns (IClaim _ _ _ _ ty) = [expandNS ns (getName ty)]
-    defName ns (IDef _ nm _) = [expandNS ns nm]
-    defName ns (IData _ _ _ (MkImpData _ n _ _ cons))
-        = expandNS ns n :: map (expandNS ns) (map getName cons)
-    defName ns (IData _ _ _ (MkImpLater _ n _)) = [expandNS ns n]
-    defName ns (IParameters _ _ pds) = concatMap (defName ns) pds
-    defName ns (IFail _ _ nds) = concatMap (defName ns) nds
-    defName ns (INamespace _ n nds) = concatMap (defName (ns <.> n)) nds
-    defName ns (IRecord _ fldns _ _ (MkImpRecord _ n _ opts con flds))
-        = expandNS ns con :: all
+    defName : Namespace -> SortedSet Name -> ImpDecl -> SortedSet Name
+    defName ns acc (IClaim _ _ _ _ ty) = insert (expandNS ns (getName ty)) acc
+    defName ns acc (IDef _ nm _) = insert (expandNS ns nm) acc
+    defName ns acc (IData _ _ _ (MkImpData _ n _ _ cons))
+        = foldl (flip insert) acc $ expandNS ns n :: map (expandNS ns . getName) cons
+    defName ns acc (IData _ _ _ (MkImpLater _ n _)) = insert (expandNS ns n) acc
+    defName ns acc (IParameters _ _ pds) = foldl (defName ns) acc pds
+    defName ns acc (IFail _ _ nds) = foldl (defName ns) acc nds
+    defName ns acc (INamespace _ n nds) = foldl (defName (ns <.> n)) acc nds
+    defName ns acc (IRecord _ fldns _ _ (MkImpRecord _ n _ opts con flds))
+        = foldl (flip insert) acc $ expandNS ns con :: all
       where
         fldns' : Namespace
         fldns' = maybe ns (\ f => ns <.> mkNamespace f) fldns
@@ -823,8 +825,8 @@ definedInBlock ns decls =
         all : List Name
         all = expandNS ns n :: map (expandNS fldns') (fnsRF ++ fnsUN)
 
-    defName ns (IPragma _ pns _) = map (expandNS ns) pns
-    defName _ _ = []
+    defName ns acc (IPragma _ pns _) = foldl (flip insert) acc $ map (expandNS ns) pns
+    defName _ acc _ = acc
 
 export
 isIVar : RawImp' nm -> Maybe (FC, nm)