diff --git a/src/Compiler/LambdaLift.idr b/src/Compiler/LambdaLift.idr index 674cb4ec3..d7a82c0d2 100644 --- a/src/Compiler/LambdaLift.idr +++ b/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)) -> diff --git a/src/Core/Context.idr b/src/Core/Context.idr index f1f4a8cf8..d55a021b6 100644 --- a/src/Core/Context.idr +++ b/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) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 679a9a3c2..f66a331f4 100644 --- a/src/Core/Core.idr +++ b/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 diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 911adf803..5d11685e5 100644 --- a/src/Idris/Error.idr +++ b/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 diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr index d93ef5608..5abcef658 100644 --- a/src/TTImp/ProcessType.idr +++ b/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 diff --git a/tests/idris2/basic049/Fld.idr b/tests/idris2/basic049/Fld.idr index 09e2c57d2..66e8c33ac 100644 --- a/tests/idris2/basic049/Fld.idr +++ b/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 diff --git a/tests/idris2/basic049/expected b/tests/idris2/basic049/expected index 20a2b99c6..1eac1bc7d 100644 --- a/tests/idris2/basic049/expected +++ b/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 - 62 | - 63 | public export - 64 | record R2 where - 65 | constructor MkR - 66 | {auto field : a} +Fld:68:11--68:20 + 64 | + 65 | public export + 66 | record R2 where + 67 | constructor MkR + 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 - 74 | interface Show a => (num : Num a) => MyIface a where -- Some interface with - 75 | constructor MkIface - 76 | -- constraints - 77 | data MyData : a -> Type -- and a data declaration. - 78 | 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 +Fld:76:1--81:38 + 76 | interface Show a => (num : Num a) => MyIface a where -- Some interface with + 77 | constructor MkIface + 78 | -- constraints + 79 | data MyData : a -> Type -- and a data declaration. + 80 | someFunc : a -> a -- Constraints are now elaborated as auto implicits (as one would expect) + 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 - 74 | interface Show a => (num : Num a) => MyIface a where -- Some interface with - 75 | constructor MkIface - 76 | -- constraints - 77 | data MyData : a -> Type -- and a data declaration. - 78 | 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 +Fld:76:1--81:38 + 76 | interface Show a => (num : Num a) => MyIface a where -- Some interface with + 77 | constructor MkIface + 78 | -- constraints + 79 | data MyData : a -> Type -- and a data declaration. + 80 | someFunc : a -> a -- Constraints are now elaborated as auto implicits (as one would expect) + 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 - 83 | data MyDataImpl : a -> Type where -- implementation of MyData - 84 | MkMyData : (x : a) -> MyDataImpl x +Fld:85:1--86:37 + 85 | data MyDataImpl : a -> Type where -- implementation of MyData + 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 - 80 | -- constructor) - 81 | - 82 | - 83 | data MyDataImpl : a -> Type where -- implementation of MyData - 84 | MkMyData : (x : a) -> MyDataImpl x +Fld:86:3--86:11 + 82 | -- constructor) + 83 | + 84 | + 85 | data MyDataImpl : a -> Type where -- implementation of MyData + 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 - 106 | Show' String where - 107 | show' = id - 108 | - 109 | %hint - 110 | showMaybe' : Show' a => Show' (Maybe a) +Fld:112:1--112:11 + 108 | Show' String where + 109 | show' = id + 110 | + 111 | %hint + 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 - 135 | setName : String -> OrdinaryDog -> OrdinaryDog - 136 | setName name' = {name := name'} - 137 | - 138 | data Three : Type -> Type -> Type -> Type where - 139 | MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c +Fld:141:3--141:10 + 137 | setName : String -> OrdinaryDog -> OrdinaryDog + 138 | setName name' = {name := name'} + 139 | + 140 | data Three : Type -> Type -> Type -> Type where + 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 - 137 | - 138 | data Three : Type -> Type -> Type -> Type where - 139 | MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c - 140 | - 141 | mapSetMap : (a -> a') -> b' -> (c -> c') -> Three a b c -> Three a' b' c' +Fld:143:1--143:10 + 139 | + 140 | data Three : Type -> Type -> Type -> Type where + 141 | MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c + 142 | + 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 - 213 | dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x - 214 | dontCare2 {} = plusCommutative {} - 215 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _ - 216 | - 217 | data Tree a = Leaf a | Node (Tree a) a (Tree a) +Fld:219:15--219:21 + 215 | dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x + 216 | dontCare2 {} = plusCommutative {} + 217 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _ + 218 | + 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 - 213 | dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x - 214 | dontCare2 {} = plusCommutative {} - 215 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _ - 216 | - 217 | data Tree a = Leaf a | Node (Tree a) a (Tree a) +Fld:219:24--219:48 + 215 | dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x + 216 | dontCare2 {} = plusCommutative {} + 217 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _ + 218 | + 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 - 215 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _ - 216 | - 217 | data Tree a = Leaf a | Node (Tree a) a (Tree a) +Fld:221:1--221:7 + 217 | -- dontCare2 _ _ _ _ _ = plusCommutative _ _ 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 - 223 | data IsNode : Tree a -> Type where - 224 | Is : IsNode (Node {}) +Fld:225:1--226:24 + 225 | data IsNode : Tree a -> Type where + 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 - 222 | - 223 | data IsNode : Tree a -> Type where - 224 | Is : IsNode (Node {}) - 225 | - 226 | decIsNode : (x : Tree a) -> Dec (IsNode x) +Fld:228:1--228:10 + 224 | + 225 | data IsNode : Tree a -> Type where + 226 | Is : IsNode (Node {}) + 227 | + 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 - 68 | r1 : R1 -- explicit fields access - 69 | r1 = MkR {field = "string"} - 70 | - 71 | r2_shouldNotTypecheck1 : ? - 72 | r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate +Fld:74:26--74:29 + 70 | r1 : R1 -- explicit fields access + 71 | r1 = MkR {field = "string"} + 72 | + 73 | r2_shouldNotTypecheck1 : ? + 74 | r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate ^^^ Main> Main.myDog : OrdinaryDog