Warning for shadowed local bindings (#2623)

* Warning for shadowed local bindings

* [ lint ]

* Remove name shadowing in compiler src

* [ fix ] spelling & test cases

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>

src/Compiler/LambdaLift.idr

@@ -541,7 +541,7 @@ mutual
   dropIdx (_::xs) unused (Later p) = Var.later $ dropIdx xs unused p
 
   dropUnused : {vars : _} ->
-               {auto l : Ref Lifts LDefs} ->
+               {auto _ : Ref Lifts LDefs} ->
                {outer : List Name} ->
                (unused : Vect (length vars) Bool) ->
                (l : Lifted (outer ++ vars)) ->

src/Core/Context.idr

@@ -702,6 +702,7 @@ HasNames Warning where
   full gam (UnreachableClause fc rho s) = UnreachableClause fc <$> full gam rho <*> full gam s
   full gam (ShadowingGlobalDefs fc xs)
     = ShadowingGlobalDefs fc <$> traverseList1 (traversePair (traverseList1 (full gam))) xs
+  full gam w@(ShadowingLocalBindings _ _) = pure w
   full gam (Deprecated x y) = Deprecated x <$> traverseOpt (traversePair (full gam)) y
   full gam (GenericWarn x) = pure (GenericWarn x)
 
@@ -709,6 +710,7 @@ HasNames Warning where
   resolved gam (UnreachableClause fc rho s) = UnreachableClause fc <$> resolved gam rho <*> resolved gam s
   resolved gam (ShadowingGlobalDefs fc xs)
     = ShadowingGlobalDefs fc <$> traverseList1 (traversePair (traverseList1 (resolved gam))) xs
+  resolved gam w@(ShadowingLocalBindings _ _) = pure w
   resolved gam (Deprecated x y) = Deprecated x <$> traverseOpt (traversePair (resolved gam)) y
   resolved gam (GenericWarn x) = pure (GenericWarn x)
 

src/Core/Core.idr

@@ -66,6 +66,11 @@ data Warning : Type where
      UnreachableClause : {vars : _} ->
                          FC -> Env Term vars -> Term vars -> Warning
      ShadowingGlobalDefs : FC -> List1 (String, List1 Name) -> Warning
+     ||| First FC is type
+     ||| @ shadowed list of names which are shadowed,
+     |||   where they originally appear
+     |||   and where they are shadowed
+     ShadowingLocalBindings : FC -> (shadowed : List1 (String, FC, FC)) -> Warning
      ||| A warning about a deprecated definition. Supply an FC and Name to
      ||| have the documentation for the definition printed with the warning.
      Deprecated : String -> Maybe (FC, Name) -> Warning
@@ -197,6 +202,7 @@ Show Warning where
     show (ParserWarning _ msg) = msg
     show (UnreachableClause _ _ _) = ":Unreachable clause"
     show (ShadowingGlobalDefs _ _) = ":Shadowing names"
+    show (ShadowingLocalBindings _ _) = ":Shadowing names"
     show (Deprecated name _) = ":Deprecated " ++ name
     show (GenericWarn msg) = msg
 
@@ -385,6 +391,7 @@ getWarningLoc : Warning -> Maybe FC
 getWarningLoc (ParserWarning fc _) = Just fc
 getWarningLoc (UnreachableClause fc _ _) = Just fc
 getWarningLoc (ShadowingGlobalDefs fc _) = Just fc
+getWarningLoc (ShadowingLocalBindings fc _) = Just fc
 getWarningLoc (Deprecated _ fcAndName) = fst <$> fcAndName
 getWarningLoc (GenericWarn _) = Nothing
 
@@ -470,6 +477,8 @@ killWarningLoc : Warning -> Warning
 killWarningLoc (ParserWarning fc x) = ParserWarning emptyFC x
 killWarningLoc (UnreachableClause fc x y) = UnreachableClause emptyFC x y
 killWarningLoc (ShadowingGlobalDefs fc xs) = ShadowingGlobalDefs emptyFC xs
+killWarningLoc (ShadowingLocalBindings fc xs) =
+    ShadowingLocalBindings emptyFC $ (\(n, _, _) => (n, emptyFC, emptyFC)) <$> xs
 killWarningLoc (Deprecated x y) = Deprecated x (map ((emptyFC,) . snd) y)
 killWarningLoc (GenericWarn x) = GenericWarn x
 

src/Idris/Error.idr

@@ -274,6 +274,13 @@ pwarningRaw (ShadowingGlobalDefs fc ns)
                         :: reflow "is shadowing"
                         :: punctuate comma (map pretty0 (forget ns))
 
+pwarningRaw (ShadowingLocalBindings fc ns)
+    = pure $ vcat
+    [ reflow "You may be unintentionally shadowing the following local bindings:"
+    , indent 2 $ hcat $ pretty0 . fst <$> (forget ns)
+    , !(ploc fc)
+    ]
+
 pwarningRaw (Deprecated s fcAndName)
     = do docs <- traverseOpt (\(fc, name) => getDocsForName fc name justUserDoc) fcAndName
          pure . vsep $ catMaybes [ Just $ "Deprecation warning:" <++> pretty0 s

src/TTImp/ProcessType.idr

@@ -23,6 +23,7 @@ import Data.List
 import Data.List1
 import Data.String
 import Libraries.Data.NameMap
+import Libraries.Data.StringMap
 
 %default covering
 
@@ -288,6 +289,15 @@ findInferrable defs ty = fi 0 0 [] [] ty
              pure rest
     fi pos i args acc ret = findInf acc args ret
 
+checkForShadowing : (env : StringMap FC) -> RawImp -> List (String, FC, FC)
+checkForShadowing env (IPi fc _ _ (Just (UN (Basic name))) argTy retTy) =
+    let argShadowing = checkForShadowing empty argTy
+     in (case lookup name env of
+        Just origFc => (name, origFc, fc) :: checkForShadowing env retTy
+        Nothing => checkForShadowing (insert name fc env) retTy)
+        ++ argShadowing
+checkForShadowing env t = []
+
 export
 processType : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
@@ -365,3 +375,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc nameFC n_in ty_ra
               do addHashWithNames n
                  addHashWithNames ty
                  log "module.hash" 15 "Adding hash for type with name \{show n}"
+
+         when (showShadowingWarning !getSession) $
+            whenJust (fromList (checkForShadowing StringMap.empty ty_raw))
+                $ recordWarning . ShadowingLocalBindings fc

tests/idris2/basic049/Fld.idr

@@ -56,6 +56,8 @@ namespace R1
   public export
   record R1 where
     constructor MkR
+    -- `a` is out of scope here so
+    -- this silently declares an implicit field `0 a : Type`
     field : a
 
 namespace R2

tests/idris2/basic049/expected

@@ -3,68 +3,68 @@ Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R1.R1.a
 
-Fld:66:11--66:20
+Fld:68:11--68:20
- 62 | 
+ 64 | 
- 63 |   public export
+ 65 |   public export
- 64 |   record R2 where
+ 66 |   record R2 where
- 65 |     constructor MkR
+ 67 |     constructor MkR
- 66 |     {auto field : a}
+ 68 |     {auto field : a}
                 ^^^^^^^^^
 
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
 
-Fld:74:1--79:38
+Fld:76:1--81:38
- 74 | interface Show a => (num : Num a) => MyIface a where -- Some interface with
+ 76 | interface Show a => (num : Num a) => MyIface a where -- Some interface with
- 75 |   constructor MkIface
+ 77 |   constructor MkIface
- 76 |                                              -- constraints
+ 78 |                                              -- constraints
- 77 |   data MyData : a -> Type                    -- and a data declaration.
+ 79 |   data MyData : a -> Type                    -- and a data declaration.
- 78 |   someFunc : a -> a                          -- Constraints are now elaborated as auto implicits (as one would expect)
+ 80 |   someFunc : a -> a                          -- Constraints are now elaborated as auto implicits (as one would expect)
- 79 |   giveBack : {x : a} -> MyData x -> a        -- (previously as explicit arguments of the interface
+ 81 |   giveBack : {x : a} -> MyData x -> a        -- (previously as explicit arguments of the interface
 
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
 
-Fld:74:1--79:38
+Fld:76:1--81:38
- 74 | interface Show a => (num : Num a) => MyIface a where -- Some interface with
+ 76 | interface Show a => (num : Num a) => MyIface a where -- Some interface with
- 75 |   constructor MkIface
+ 77 |   constructor MkIface
- 76 |                                              -- constraints
+ 78 |                                              -- constraints
- 77 |   data MyData : a -> Type                    -- and a data declaration.
+ 79 |   data MyData : a -> Type                    -- and a data declaration.
- 78 |   someFunc : a -> a                          -- Constraints are now elaborated as auto implicits (as one would expect)
+ 80 |   someFunc : a -> a                          -- Constraints are now elaborated as auto implicits (as one would expect)
- 79 |   giveBack : {x : a} -> MyData x -> a        -- (previously as explicit arguments of the interface
+ 81 |   giveBack : {x : a} -> MyData x -> a        -- (previously as explicit arguments of the interface
 
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
 
-Fld:83:1--84:37
+Fld:85:1--86:37
- 83 | data MyDataImpl : a -> Type where            -- implementation of MyData
+ 85 | data MyDataImpl : a -> Type where            -- implementation of MyData
- 84 |   MkMyData : (x : a) -> MyDataImpl x
+ 86 |   MkMyData : (x : a) -> MyDataImpl x
 
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
 
-Fld:84:3--84:11
+Fld:86:3--86:11
- 80 |                                              -- constructor)
+ 82 |                                              -- constructor)
- 81 | 
+ 83 | 
- 82 | 
+ 84 | 
- 83 | data MyDataImpl : a -> Type where            -- implementation of MyData
+ 85 | data MyDataImpl : a -> Type where            -- implementation of MyData
- 84 |   MkMyData : (x : a) -> MyDataImpl x
+ 86 |   MkMyData : (x : a) -> MyDataImpl x
         ^^^^^^^^
 
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
 
-Fld:110:1--110:11
+Fld:112:1--112:11
- 106 | Show' String where
+ 108 | Show' String where
- 107 |    show' = id
+ 109 |    show' = id
- 108 | 
+ 110 | 
- 109 | %hint
+ 111 | %hint
- 110 | showMaybe' : Show' a => Show' (Maybe a)
+ 112 | showMaybe' : Show' a => Show' (Maybe a)
        ^^^^^^^^^^
 
 Warning: We are about to implicitly bind the following lowercase names.
@@ -72,12 +72,12 @@ You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
   b is shadowing Main.Other.b
 
-Fld:139:3--139:10
+Fld:141:3--141:10
- 135 | setName : String -> OrdinaryDog -> OrdinaryDog
+ 137 | setName : String -> OrdinaryDog -> OrdinaryDog
- 136 | setName name' = {name := name'}
+ 138 | setName name' = {name := name'}
- 137 | 
+ 139 | 
- 138 | data Three : Type -> Type -> Type -> Type where
+ 140 | data Three : Type -> Type -> Type -> Type where
- 139 |   MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c
+ 141 |   MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c
          ^^^^^^^
 
 Warning: We are about to implicitly bind the following lowercase names.
@@ -85,80 +85,124 @@ You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
   b is shadowing Main.Other.b
 
-Fld:141:1--141:10
+Fld:143:1--143:10
- 137 | 
+ 139 | 
- 138 | data Three : Type -> Type -> Type -> Type where
+ 140 | data Three : Type -> Type -> Type -> Type where
- 139 |   MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c
+ 141 |   MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c
- 140 | 
+ 142 | 
- 141 | mapSetMap : (a -> a') -> b' -> (c -> c') -> Three a b c -> Three a' b' c'
+ 143 | mapSetMap : (a -> a') -> b' -> (c -> c') -> Three a b c -> Three a' b' c'
        ^^^^^^^^^
 
+Warning: You may be unintentionally shadowing the following local bindings:
+  a
+
+Fld:154:1--154:70
+ 150 | 
+ 151 | --------- Applications in presence of duplicate names ----------
+ 152 | 
+ 153 | -- Duplicate names are ok and treated sequentially
+ 154 | testDuplicateNames : {auto a : String} -> {auto a : String} -> String
+       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Warning: You may be unintentionally shadowing the following local bindings:
+  a
+
+Fld:162:1--162:52
+ 158 | -- a function on RHS
+ 159 | -- unnamed arguments always take priority over named,
+ 160 | -- i.e they are bound/applied first,
+ 161 | -- regardless of their relative positions to named ones
+ 162 | testOrder1 : (a : String) -> (a : String) -> String
+       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Warning: You may be unintentionally shadowing the following local bindings:
+  a
+
+Fld:176:1--176:57
+ 172 | -- Two arguments with the same name can be successfully bound
+ 173 | -- if one of them is renamed in patterns.
+ 174 | -- As both arguments are requested by name
+ 175 | -- They are bound in the same order they are given
+ 176 | sameNamesOk : (a : String) -> (a : Nat) -> (String, Nat)
+       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Warning: You may be unintentionally shadowing the following local bindings:
+  aa
+
+Fld:181:1--181:74
+ 177 | sameNamesOk {a {- = a-}, a = b} = (a, b)
+ 178 | 
+ 179 | -- All arguments are named and are of different `plicities`. Binds occur sequentially.
+ 180 | -- Arguments are renamed on LHS
+ 181 | eachArgType : (a : String) -> {a : String} -> {auto a : String} -> String
+       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
 
-Fld:217:15--217:21
+Fld:219:15--219:21
- 213 | dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
+ 215 | dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
- 214 | dontCare2 {} = plusCommutative {}
+ 216 | dontCare2 {} = plusCommutative {}
- 215 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _
+ 217 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _
- 216 | 
+ 218 | 
- 217 | data Tree a = Leaf a | Node (Tree a) a (Tree a)
+ 219 | data Tree a = Leaf a | Node (Tree a) a (Tree a)
                      ^^^^^^
 
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
 
-Fld:217:24--217:48
+Fld:219:24--219:48
- 213 | dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
+ 215 | dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
- 214 | dontCare2 {} = plusCommutative {}
+ 216 | dontCare2 {} = plusCommutative {}
- 215 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _
+ 217 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _
- 216 | 
+ 218 | 
- 217 | data Tree a = Leaf a | Node (Tree a) a (Tree a)
+ 219 | data Tree a = Leaf a | Node (Tree a) a (Tree a)
                               ^^^^^^^^^^^^^^^^^^^^^^^^
 
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
 
-Fld:219:1--219:7
+Fld:221:1--221:7
- 215 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _
+ 217 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _
- 216 | 
- 217 | data Tree a = Leaf a | Node (Tree a) a (Tree a)
  218 | 
- 219 | isNode : Tree a -> Bool
+ 219 | data Tree a = Leaf a | Node (Tree a) a (Tree a)
+ 220 | 
+ 221 | isNode : Tree a -> Bool
        ^^^^^^
 
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
 
-Fld:223:1--224:24
+Fld:225:1--226:24
- 223 | data IsNode : Tree a -> Type where
+ 225 | data IsNode : Tree a -> Type where
- 224 |   Is : IsNode (Node {})
+ 226 |   Is : IsNode (Node {})
 
 Warning: We are about to implicitly bind the following lowercase names.
 You may be unintentionally shadowing the associated global definitions:
   a is shadowing Main.R2.R2.a, Main.R1.R1.a
 
-Fld:226:1--226:10
+Fld:228:1--228:10
- 222 | 
+ 224 | 
- 223 | data IsNode : Tree a -> Type where
+ 225 | data IsNode : Tree a -> Type where
- 224 |   Is : IsNode (Node {})
+ 226 |   Is : IsNode (Node {})
- 225 | 
+ 227 | 
- 226 | decIsNode : (x : Tree a) -> Dec (IsNode x)
+ 228 | decIsNode : (x : Tree a) -> Dec (IsNode x)
        ^^^^^^^^^
 
 Error: While processing right hand side of r2_shouldNotTypecheck1. Ambiguous elaboration. Possible results:
     Main.R2.MkR
     Main.R1.MkR (Prelude.the Prelude.Nat 22)
 
-Fld:72:26--72:29
+Fld:74:26--74:29
- 68 | r1 : R1 -- explicit fields access
+ 70 | r1 : R1 -- explicit fields access
- 69 | r1 = MkR {field = "string"}
+ 71 | r1 = MkR {field = "string"}
- 70 | 
+ 72 | 
- 71 | r2_shouldNotTypecheck1 : ?
+ 73 | r2_shouldNotTypecheck1 : ?
- 72 | r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
+ 74 | r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
                                ^^^
 
 Main> Main.myDog : OrdinaryDog