Merge pull request #3017 from dunhamsteve/issue-3016

[ fix ] Ensure local defs with no claim are local

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,16 +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 (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
@@ -822,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)

tests/Main.idr

@@ -42,7 +42,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
        "basic051", "basic052", "basic053", "basic054", "basic055",
        "basic056", "basic057", "basic058", "basic059", "basic060",
        "basic061", "basic062", "basic063", "basic064", "basic065",
-       "basic066", "basic067", "basic068", "basic069",
+       "basic066", "basic067", "basic068", "basic069", "basic070",
        "idiom001",
        "dotted001",
        "rewrite001",

tests/idris2/basic070/Issue2592.idr

@@ -0,0 +1,4 @@
+bar = 3
+ where wat = 2
+baz = 3
+ where wat = 2

tests/idris2/basic070/Issue2593.idr

@@ -0,0 +1,6 @@
+two: Nat
+two = 2
+
+bar: a -> a
+bar x = x where
+ wat = two

tests/idris2/basic070/Issue2782.idr

@@ -0,0 +1,9 @@
+foo : Integer
+foo =
+  let z : Int
+      z = 1
+      y = 1
+  in y
+
+fee : Integer
+fee = y

tests/idris2/basic070/Issue3016.idr

@@ -0,0 +1,9 @@
+import Data.String
+
+test str = len
+  where
+    xs = words str
+    len = length xs
+
+parameters (n : Nat) (strs : List String)
+  len = List.length strs

tests/idris2/basic070/expected

@@ -0,0 +1,14 @@
+1/1: Building Issue3016 (Issue3016.idr)
+1/1: Building Issue2782 (Issue2782.idr)
+Error: While processing right hand side of fee. Undefined name y. 
+
+Issue2782:9:7--9:8
+ 5 |       y = 1
+ 6 |   in y
+ 7 | 
+ 8 | fee : Integer
+ 9 | fee = y
+           ^
+
+1/1: Building Issue2592 (Issue2592.idr)
+1/1: Building Issue2593 (Issue2593.idr)

tests/idris2/basic070/run

@@ -0,0 +1,6 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check Issue3016.idr
+$1 --no-color --console-width 0 --no-banner --check Issue2782.idr
+$1 --no-color --console-width 0 --no-banner --check Issue2592.idr
+$1 --no-color --console-width 0 --no-banner --check Issue2593.idr