diff --git a/idris2api.ipkg b/idris2api.ipkg index dd6ffb7e1..7346929f1 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -70,6 +70,7 @@ modules = Idris.CommandLine, Idris.Desugar, + Idris.Desugar.Mutual, Idris.Env, Idris.Doc.HTML, Idris.DocString, diff --git a/libs/base/Data/List1.idr b/libs/base/Data/List1.idr index d16ded94e..946d105a7 100644 --- a/libs/base/Data/List1.idr +++ b/libs/base/Data/List1.idr @@ -18,6 +18,11 @@ record List1 a where ------------------------------------------------------------------------ -- Basic functions +public export +fromList : List a -> Maybe (List1 a) +fromList [] = Nothing +fromList (x :: xs) = Just (x ::: xs) + public export singleton : (x : a) -> List1 a singleton a = a ::: [] diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg index ad3459d26..89298e363 100644 --- a/libs/base/base.ipkg +++ b/libs/base/base.ipkg @@ -1,7 +1,7 @@ package base version = 0.3.0 -opts = "--ignore-missing-ipkg" +opts = "--ignore-missing-ipkg --no-shadowing-warning" modules = Control.App, Control.App.Console, diff --git a/libs/contrib/Data/List/HasLength.idr b/libs/contrib/Data/List/HasLength.idr index b8d2efb5b..fb9429af8 100644 --- a/libs/contrib/Data/List/HasLength.idr +++ b/libs/contrib/Data/List/HasLength.idr @@ -124,7 +124,7 @@ listTerminating p = case view p of data P : List Nat -> Type where PNil : P [] - PCon : P (map id xs) -> P (x :: xs) + PCon : P (map f xs) -> P (x :: xs) covering notListTerminating : (p : Subset Nat (HasLength xs)) -> P xs diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg index 0a65bf2e5..d3f47ee83 100644 --- a/libs/contrib/contrib.ipkg +++ b/libs/contrib/contrib.ipkg @@ -1,7 +1,7 @@ package contrib version = 0.3.0 -opts = "--ignore-missing-ipkg" +opts = "--ignore-missing-ipkg --no-shadowing-warning" modules = Control.ANSI, Control.ANSI.SGR, diff --git a/src/Compiler/ANF.idr b/src/Compiler/ANF.idr index ab571ac76..46214b24f 100644 --- a/src/Compiler/ANF.idr +++ b/src/Compiler/ANF.idr @@ -30,7 +30,9 @@ mutual AApp : FC -> (lazy : Maybe LazyReason) -> (closure : AVar) -> (arg : AVar) -> ANF ALet : FC -> (var : Int) -> ANF -> ANF -> ANF ACon : FC -> Name -> ConInfo -> (tag : Maybe Int) -> List AVar -> ANF - AOp : FC -> (lazy : Maybe LazyReason) -> PrimFn arity -> Vect arity AVar -> ANF + AOp : {0 arity : Nat} -> FC -> (lazy : Maybe LazyReason) -> PrimFn arity -> Vect arity AVar -> ANF + -- ^ we explicitly bind arity here to silence the warning that it shadows + -- existing functions called arity. AExtPrim : FC -> (lazy : Maybe LazyReason) -> Name -> List AVar -> ANF AConCase : FC -> AVar -> List AConAlt -> Maybe ANF -> ANF AConstCase : FC -> AVar -> List AConstAlt -> Maybe ANF -> ANF diff --git a/src/Compiler/ES/ES.idr b/src/Compiler/ES/ES.idr index dc0340852..c8c775e08 100644 --- a/src/Compiler/ES/ES.idr +++ b/src/Compiler/ES/ES.idr @@ -22,7 +22,6 @@ record ESSt where preamble : SortedMap String String ccTypes : List String - jsString : String -> String jsString s = "'" ++ (concatMap okchar (unpack s)) ++ "'" where @@ -90,6 +89,7 @@ addStringIteratorToPreamble = let newName = esName name addToPreamble name newName defs + jsIdent : String -> String jsIdent s = concatMap okchar (unpack s) where @@ -285,7 +285,6 @@ div (Just k) x y = else pure $ jsIntOfDouble k (x ++ " / " ++ y) div Nothing x y = pure $ binOp "/" x y - -- Creates the definition of a binary arithmetic operation. -- Rounding / truncation behavior is determined from the -- `IntKind`. @@ -366,7 +365,8 @@ constPrimitives = MkConstantPrimitives { (Unsigned m, Signed n) => if n > P m then pure expanded else shrunk -jsOp : {auto c : Ref ESs ESSt} -> PrimFn arity -> Vect arity String -> Core String +jsOp : {0 arity : Nat} -> {auto c : Ref ESs ESSt} -> + PrimFn arity -> Vect arity String -> Core String jsOp (Add ty) [x, y] = arithOp (intKind ty) "+" x y jsOp (Sub ty) [x, y] = arithOp (intKind ty) "-" x y jsOp (Mul ty) [x, y] = mult (intKind ty) x y diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index 7e6f6eb12..052eb964a 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -174,7 +174,7 @@ plainOp op args = op ++ "(" ++ (showSep ", " args) ++ ")" ||| Generate scheme for a primitive function. -cOp : PrimFn arity -> Vect arity String -> String +cOp : {0 arity : Nat} -> PrimFn arity -> Vect arity String -> String cOp (Neg ty) [x] = "negate_" ++ cConstant ty ++ "(" ++ x ++ ")" cOp StrLength [x] = "stringLength(" ++ x ++ ")" cOp StrHead [x] = "head(" ++ x ++ ")" @@ -427,7 +427,7 @@ showTag : Maybe Int -> String showTag Nothing = "-1" showTag (Just i) = show i -cArgsVectANF : Vect arity AVar -> Core (Vect arity String) +cArgsVectANF : {0 arity : Nat} -> Vect arity AVar -> Core (Vect arity String) cArgsVectANF [] = pure [] cArgsVectANF (x :: xs) = pure $ (varName x) :: !(cArgsVectANF xs) diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index 9cf5d0011..a5a88c08e 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/src/Compiler/Scheme/Common.idr @@ -131,7 +131,7 @@ constPrimitives = MkConstantPrimitives { if n >= m then x else op "blodwen-toUnsignedInt" [x,show n] ||| Generate scheme for a primitive function. -schOp : PrimFn arity -> Vect arity String -> Core String +schOp : {0 arity : Nat} -> PrimFn arity -> Vect arity String -> Core String schOp (Add ty) [x, y] = pure $ add (intKind ty) x y schOp (Sub ty) [x, y] = pure $ sub (intKind ty) x y schOp (Mul ty) [x, y] = pure $ mul (intKind ty) x y diff --git a/src/Compiler/VMCode.idr b/src/Compiler/VMCode.idr index 1242d1aaf..889016817 100644 --- a/src/Compiler/VMCode.idr +++ b/src/Compiler/VMCode.idr @@ -36,7 +36,9 @@ data VMInst : Type where APPLY : Reg -> (f : Reg) -> (a : Reg) -> VMInst CALL : Reg -> (tailpos : Bool) -> Name -> (args : List Reg) -> VMInst - OP : Reg -> PrimFn arity -> Vect arity Reg -> VMInst + OP : {0 arity : Nat} -> Reg -> PrimFn arity -> Vect arity Reg -> VMInst + -- ^ we explicitly bind arity here to silence the warnings it is shadowing + -- an existing global definition EXTPRIM : Reg -> Name -> List Reg -> VMInst CASE : Reg -> -- scrutinee diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr index cbcf3f364..11a7e3559 100644 --- a/src/Core/AutoSearch.idr +++ b/src/Core/AutoSearch.idr @@ -253,7 +253,7 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe ambig (AmbiguousSearch _ _ _ _) = True ambig _ = False - clearEnvType : {idx : Nat} -> (0 p : IsVar name idx vs) -> + clearEnvType : {idx : Nat} -> (0 p : IsVar nm idx vs) -> FC -> Env Term vs -> Env Term vs clearEnvType First fc (b :: env) = Lam (binderLoc b) (multiplicity b) Explicit (Erased fc False) :: env diff --git a/src/Core/CaseBuilder.idr b/src/Core/CaseBuilder.idr index 3f059fb22..26780f7c5 100644 --- a/src/Core/CaseBuilder.idr +++ b/src/Core/CaseBuilder.idr @@ -152,12 +152,12 @@ substInPats fc n tm (p :: ps) pure (p' :: !(substInPats fc n tm ps')) getPat : {idx : Nat} -> - (0 el : IsVar name idx ps) -> NamedPats ns ps -> PatInfo name ns + (0 el : IsVar nm idx ps) -> NamedPats ns ps -> PatInfo nm ns getPat First (x :: xs) = x getPat (Later p) (x :: xs) = getPat p xs dropPat : {idx : Nat} -> - (0 el : IsVar name idx ps) -> + (0 el : IsVar nm idx ps) -> NamedPats ns ps -> NamedPats ns (dropVar ps el) dropPat First (x :: xs) = xs dropPat (Later p) (x :: xs) = x :: dropPat p xs @@ -600,7 +600,7 @@ groupCons fc fn pvars cs pure (g :: gs') addGroup : {vars, todo, idx : _} -> - Pat -> (0 p : IsVar name idx vars) -> + Pat -> (0 p : IsVar nm idx vars) -> NamedPats vars todo -> Int -> Term vars -> List (Group vars todo) -> Core (List (Group vars todo)) @@ -778,12 +778,12 @@ pickNext {ps = q :: qs} fc phase fn npss _ => do (_ ** MkNVar var) <- pickNext fc phase fn (map tail npss) pure (_ ** MkNVar (Later var)) -moveFirst : {idx : Nat} -> (0 el : IsVar name idx ps) -> NamedPats ns ps -> - NamedPats ns (name :: dropVar ps el) +moveFirst : {idx : Nat} -> (0 el : IsVar nm idx ps) -> NamedPats ns ps -> + NamedPats ns (nm :: dropVar ps el) moveFirst el nps = getPat el nps :: dropPat el nps -shuffleVars : {idx : Nat} -> (0 el : IsVar name idx todo) -> PatClause vars todo -> - PatClause vars (name :: dropVar todo el) +shuffleVars : {idx : Nat} -> (0 el : IsVar nm idx todo) -> PatClause vars todo -> + PatClause vars (nm :: dropVar todo el) shuffleVars el (MkPatClause pvars lhs pid rhs) = MkPatClause pvars (moveFirst el lhs) pid rhs diff --git a/src/Core/CompileExpr.idr b/src/Core/CompileExpr.idr index 60849d161..675437f76 100644 --- a/src/Core/CompileExpr.idr +++ b/src/Core/CompileExpr.idr @@ -534,16 +534,16 @@ namespace SubstCEnv (::) : CExp vars -> SubstCEnv ds vars -> SubstCEnv (d :: ds) vars -findDrop : FC -> Var (drop ++ vars) -> - SubstCEnv drop vars -> CExp vars +findDrop : FC -> Var (dropped ++ vars) -> + SubstCEnv dropped vars -> CExp vars findDrop fc (MkVar p) [] = CLocal fc p findDrop fc (MkVar First) (tm :: env) = tm findDrop fc (MkVar (Later p)) (tm :: env) = findDrop fc (MkVar p) env find : FC -> SizeOf outer -> - Var (outer ++ (drop ++ vars)) -> - SubstCEnv drop vars -> + Var (outer ++ (dropped ++ vars)) -> + SubstCEnv dropped vars -> CExp (outer ++ vars) find fc outer var env = case sizedView outer of Z => findDrop fc var env @@ -554,8 +554,8 @@ find fc outer var env = case sizedView outer of mutual substEnv : SizeOf outer -> - SubstCEnv drop vars -> - CExp (outer ++ (drop ++ vars)) -> + SubstCEnv dropped vars -> + CExp (outer ++ (dropped ++ vars)) -> CExp (outer ++ vars) substEnv outer env (CLocal fc prf) = find fc outer (MkVar prf) env @@ -589,35 +589,35 @@ mutual substEnv _ _ (CCrash fc x) = CCrash fc x substConAlt : SizeOf outer -> - SubstCEnv drop vars -> - CConAlt (outer ++ (drop ++ vars)) -> + SubstCEnv dropped vars -> + CConAlt (outer ++ (dropped ++ vars)) -> CConAlt (outer ++ vars) - substConAlt {vars} {outer} {drop} p env (MkConAlt x ci tag args sc) + substConAlt {vars} {outer} {dropped} p env (MkConAlt x ci tag args sc) = MkConAlt x ci tag args (rewrite appendAssociative args outer vars in substEnv (mkSizeOf args + p) env - (rewrite sym (appendAssociative args outer (drop ++ vars)) in + (rewrite sym (appendAssociative args outer (dropped ++ vars)) in sc)) substConstAlt : SizeOf outer -> - SubstCEnv drop vars -> - CConstAlt (outer ++ (drop ++ vars)) -> + SubstCEnv dropped vars -> + CConstAlt (outer ++ (dropped ++ vars)) -> CConstAlt (outer ++ vars) substConstAlt outer env (MkConstAlt x sc) = MkConstAlt x (substEnv outer env sc) export -substs : {drop, vars : _} -> - SubstCEnv drop vars -> CExp (drop ++ vars) -> CExp vars +substs : {dropped, vars : _} -> + SubstCEnv dropped vars -> CExp (dropped ++ vars) -> CExp vars substs env tm = substEnv zero env tm -resolveRef : SizeOf later -> +resolveRef : SizeOf outer -> SizeOf done -> Bounds bound -> FC -> Name -> - Maybe (CExp (later ++ (done ++ bound ++ vars))) + Maybe (CExp (outer ++ (done ++ bound ++ vars))) resolveRef _ _ None _ _ = Nothing -resolveRef {later} {vars} {done} p q (Add {xs} new old bs) fc n +resolveRef {outer} {vars} {done} p q (Add {xs} new old bs) fc n = if n == old - then rewrite appendAssociative later done (new :: xs ++ vars) in + then rewrite appendAssociative outer done (new :: xs ++ vars) in let MkNVar p = weakenNVar (p + q) (MkNVar First) in Just (CLocal fc p) else rewrite appendAssociative done [new] (xs ++ vars) @@ -625,10 +625,10 @@ resolveRef {later} {vars} {done} p q (Add {xs} new old bs) fc n mutual export - mkLocals : SizeOf later -> + mkLocals : SizeOf outer -> Bounds bound -> - CExp (later ++ vars) -> - CExp (later ++ (bound ++ vars)) + CExp (outer ++ vars) -> + CExp (outer ++ (bound ++ vars)) mkLocals later bs (CLocal {idx} {x} fc p) = let MkNVar p' = addVars later bs (MkNVar p) in CLocal {x} fc p' mkLocals later bs (CRef fc var) @@ -663,21 +663,21 @@ mutual mkLocals later bs (CErased fc) = CErased fc mkLocals later bs (CCrash fc x) = CCrash fc x - mkLocalsConAlt : SizeOf later -> + mkLocalsConAlt : SizeOf outer -> Bounds bound -> - CConAlt (later ++ vars) -> - CConAlt (later ++ (bound ++ vars)) - mkLocalsConAlt {bound} {later} {vars} p bs (MkConAlt x ci tag args sc) - = let sc' : CExp ((args ++ later) ++ vars) - = rewrite sym (appendAssociative args later vars) in sc in + CConAlt (outer ++ vars) -> + CConAlt (outer ++ (bound ++ vars)) + mkLocalsConAlt {bound} {outer} {vars} p bs (MkConAlt x ci tag args sc) + = let sc' : CExp ((args ++ outer) ++ vars) + = rewrite sym (appendAssociative args outer vars) in sc in MkConAlt x ci tag args - (rewrite appendAssociative args later (bound ++ vars) in + (rewrite appendAssociative args outer (bound ++ vars) in mkLocals (mkSizeOf args + p) bs sc') - mkLocalsConstAlt : SizeOf later -> + mkLocalsConstAlt : SizeOf outer -> Bounds bound -> - CConstAlt (later ++ vars) -> - CConstAlt (later ++ (bound ++ vars)) + CConstAlt (outer ++ vars) -> + CConstAlt (outer ++ (bound ++ vars)) mkLocalsConstAlt later bs (MkConstAlt x sc) = MkConstAlt x (mkLocals later bs sc) export diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 392cf3746..dfe5e85df 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -271,7 +271,7 @@ record GlobalDef where specArgs : List Nat -- arguments to specialise by inferrable : List Nat -- arguments which can be inferred from elsewhere in the type multiplicity : RigCount - vars : List Name -- environment name is defined in + localVars : List Name -- environment name is defined in visibility : Visibility totality : Totality flags : List DefFlag @@ -624,7 +624,7 @@ newDef fc n rig vars ty vis def , specArgs = [] , inferrable = [] , multiplicity = rig - , vars = vars + , localVars = vars , visibility = vis , totality = unchecked , flags = [] @@ -1329,7 +1329,7 @@ addBuiltin n ty tot op , specArgs = [] , inferrable = [] , multiplicity = top - , vars = [] + , localVars = [] , visibility = Public , totality = tot , flags = [Inline] diff --git a/src/Core/Core.idr b/src/Core/Core.idr index ee547da60..63cc415a3 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -160,6 +160,7 @@ public export data Warning : Type where UnreachableClause : {vars : _} -> FC -> Env Term vars -> Term vars -> Warning + ShadowingGlobalDefs : FC -> List1 (String, List1 Name) -> Warning Deprecated : String -> Warning export @@ -412,6 +413,7 @@ getErrorLoc (MaybeMisspelling err _) = getErrorLoc err export getWarningLoc : Warning -> Maybe FC getWarningLoc (UnreachableClause fc _ _) = Just fc +getWarningLoc (ShadowingGlobalDefs fc _) = Just fc getWarningLoc (Deprecated _) = Nothing -- Core is a wrapper around IO that is specialised for efficiency. diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr index 80ab67c1e..c39f5d72b 100644 --- a/src/Core/Normalise.idr +++ b/src/Core/Normalise.idr @@ -182,7 +182,7 @@ parameters (defs : Defs, topopts : EvalOpts) {free, vars : _} -> Env Term free -> FC -> Maybe Bool -> - (idx : Nat) -> (0 p : IsVar name idx (vars ++ free)) -> + (idx : Nat) -> (0 p : IsVar nm idx (vars ++ free)) -> Stack free -> LocalEnv free vars -> Core (NF free) @@ -203,7 +203,7 @@ parameters (defs : Defs, topopts : EvalOpts) env fc mrig (S idx) (Later p) stk (_ :: locs) = evalLocal {vars = xs} env fc mrig idx p stk locs - updateLocal : (idx : Nat) -> (0 p : IsVar name idx (vars ++ free)) -> + updateLocal : (idx : Nat) -> (0 p : IsVar nm idx (vars ++ free)) -> LocalEnv free vars -> NF free -> LocalEnv free vars updateLocal Z First (x :: locs) nf = MkNFClosure nf :: locs diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 041832712..33c417ee6 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -157,6 +157,7 @@ record Session where dumpanf : Maybe String -- file to output ANF definitions dumpvmcode : Maybe String -- file to output VM code definitions profile : Bool -- generate profiling information, if supported + showShadowingWarning : Bool public export record PPrinter where @@ -205,7 +206,7 @@ export defaultSession : Session defaultSession = MkSessionOpts False False False Chez [] False defaultLogLevel False False False Nothing Nothing - Nothing Nothing False + Nothing Nothing False True export defaultElab : ElabDirectives diff --git a/src/Core/Primitives.idr b/src/Core/Primitives.idr index 27dfbde52..853904d9c 100644 --- a/src/Core/Primitives.idr +++ b/src/Core/Primitives.idr @@ -586,7 +586,7 @@ castTo DoubleType = castDouble castTo _ = const Nothing export -getOp : PrimFn arity -> +getOp : {0 arity : Nat} -> PrimFn arity -> {vars : List Name} -> Vect arity (NF vars) -> Maybe (NF vars) getOp (Add ty) = binOp add getOp (Sub ty) = binOp sub @@ -637,7 +637,7 @@ prim : String -> Name prim str = UN $ "prim__" ++ str export -opName : PrimFn arity -> Name +opName : {0 arity : Nat} -> PrimFn arity -> Name opName (Add ty) = prim $ "add_" ++ show ty opName (Sub ty) = prim $ "sub_" ++ show ty opName (Mul ty) = prim $ "mul_" ++ show ty diff --git a/src/Core/TT.idr b/src/Core/TT.idr index dcd07c71d..8fcc2a6e3 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -556,11 +556,21 @@ Functor Binder where map func (PLet fc c val ty) = PLet fc c (func val) (func ty) map func (PVTy fc c ty) = PVTy fc c (func ty) + public export data IsVar : Name -> Nat -> List Name -> Type where First : IsVar n Z (n :: ns) Later : IsVar n i ns -> IsVar n (S i) (m :: ns) +export +dropLater : IsVar nm (S idx) (v :: vs) -> IsVar nm idx vs +dropLater (Later p) = p + +export +mkVar : (wkns : List Name) -> IsVar nm (length wkns) (wkns ++ nm :: vars) +mkVar [] = First +mkVar (w :: ws) = Later (mkVar ws) + public export dropVar : (ns : List Name) -> {idx : Nat} -> (0 p : IsVar name idx ns) -> List Name dropVar (n :: xs) First = xs @@ -1328,49 +1338,49 @@ namespace Bounds sizeOf (Add _ _ b) = suc (sizeOf b) export -addVars : SizeOf later -> Bounds bound -> - NVar name (later ++ vars) -> - NVar name (later ++ (bound ++ vars)) +addVars : SizeOf outer -> Bounds bound -> + NVar name (outer ++ vars) -> + NVar name (outer ++ (bound ++ vars)) addVars p = insertNVarNames p . sizeOf -resolveRef : SizeOf later -> SizeOf done -> Bounds bound -> FC -> Name -> - Maybe (Term (later ++ (done ++ bound ++ vars))) +resolveRef : SizeOf outer -> SizeOf done -> Bounds bound -> FC -> Name -> + Maybe (Term (outer ++ (done ++ bound ++ vars))) resolveRef p q None fc n = Nothing -resolveRef {later} {done} p q (Add {xs} new old bs) fc n +resolveRef {outer} {done} p q (Add {xs} new old bs) fc n = if n == old - then rewrite appendAssociative later done (new :: xs ++ vars) in + then rewrite appendAssociative outer done (new :: xs ++ vars) in let MkNVar p = weakenNVar (p + q) (MkNVar First) in Just (Local fc Nothing _ p) else rewrite appendAssociative done [new] (xs ++ vars) in resolveRef p (sucR q) bs fc n -mkLocals : SizeOf later -> Bounds bound -> - Term (later ++ vars) -> Term (later ++ (bound ++ vars)) -mkLocals later bs (Local fc r idx p) - = let MkNVar p' = addVars later bs (MkNVar p) in Local fc r _ p' -mkLocals later bs (Ref fc Bound name) - = maybe (Ref fc Bound name) id (resolveRef later zero bs fc name) -mkLocals later bs (Ref fc nt name) +mkLocals : SizeOf outer -> Bounds bound -> + Term (outer ++ vars) -> Term (outer ++ (bound ++ vars)) +mkLocals outer bs (Local fc r idx p) + = let MkNVar p' = addVars outer bs (MkNVar p) in Local fc r _ p' +mkLocals outer bs (Ref fc Bound name) + = maybe (Ref fc Bound name) id (resolveRef outer zero bs fc name) +mkLocals outer bs (Ref fc nt name) = Ref fc nt name -mkLocals later bs (Meta fc name y xs) - = maybe (Meta fc name y (map (mkLocals later bs) xs)) - id (resolveRef later zero bs fc name) -mkLocals later bs (Bind fc x b scope) - = Bind fc x (map (mkLocals later bs) b) - (mkLocals (suc later) bs scope) -mkLocals later bs (App fc fn arg) - = App fc (mkLocals later bs fn) (mkLocals later bs arg) -mkLocals later bs (As fc s as tm) - = As fc s (mkLocals later bs as) (mkLocals later bs tm) -mkLocals later bs (TDelayed fc x y) - = TDelayed fc x (mkLocals later bs y) -mkLocals later bs (TDelay fc x t y) - = TDelay fc x (mkLocals later bs t) (mkLocals later bs y) -mkLocals later bs (TForce fc r x) - = TForce fc r (mkLocals later bs x) -mkLocals later bs (PrimVal fc c) = PrimVal fc c -mkLocals later bs (Erased fc i) = Erased fc i -mkLocals later bs (TType fc) = TType fc +mkLocals outer bs (Meta fc name y xs) + = maybe (Meta fc name y (map (mkLocals outer bs) xs)) + id (resolveRef outer zero bs fc name) +mkLocals outer bs (Bind fc x b scope) + = Bind fc x (map (mkLocals outer bs) b) + (mkLocals (suc outer) bs scope) +mkLocals outer bs (App fc fn arg) + = App fc (mkLocals outer bs fn) (mkLocals outer bs arg) +mkLocals outer bs (As fc s as tm) + = As fc s (mkLocals outer bs as) (mkLocals outer bs tm) +mkLocals outer bs (TDelayed fc x y) + = TDelayed fc x (mkLocals outer bs y) +mkLocals outer bs (TDelay fc x t y) + = TDelay fc x (mkLocals outer bs t) (mkLocals outer bs y) +mkLocals outer bs (TForce fc r x) + = TForce fc r (mkLocals outer bs x) +mkLocals outer bs (PrimVal fc c) = PrimVal fc c +mkLocals outer bs (Erased fc i) = Erased fc i +mkLocals outer bs (TType fc) = TType fc export refsToLocals : Bounds bound -> Term vars -> Term (bound ++ vars) @@ -1429,8 +1439,8 @@ namespace SubstEnv SubstEnv ds vars -> SubstEnv (d :: ds) vars findDrop : FC -> Maybe Bool -> - Var (drop ++ vars) -> - SubstEnv drop vars -> + Var (dropped ++ vars) -> + SubstEnv dropped vars -> Term vars findDrop fc r (MkVar var) [] = Local fc r _ var findDrop fc r (MkVar First) (tm :: env) = tm @@ -1439,8 +1449,8 @@ namespace SubstEnv find : FC -> Maybe Bool -> SizeOf outer -> - Var (outer ++ (drop ++ vars)) -> - SubstEnv drop vars -> + Var (outer ++ (dropped ++ vars)) -> + SubstEnv dropped vars -> Term (outer ++ vars) find fc r outer var env = case sizedView outer of Z => findDrop fc r var env @@ -1450,8 +1460,8 @@ namespace SubstEnv -- TODO: refactor to only weaken once? substEnv : SizeOf outer -> - SubstEnv drop vars -> - Term (outer ++ (drop ++ vars)) -> + SubstEnv dropped vars -> + Term (outer ++ (dropped ++ vars)) -> Term (outer ++ vars) substEnv outer env (Local fc r _ prf) = find fc r outer (MkVar prf) env @@ -1474,7 +1484,7 @@ namespace SubstEnv substEnv outer env (TType fc) = TType fc export - substs : SubstEnv drop vars -> Term (drop ++ vars) -> Term vars + substs : SubstEnv dropped vars -> Term (dropped ++ vars) -> Term vars substs env tm = substEnv zero env tm export diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index 88bcb6a2f..5c67de938 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -1021,7 +1021,7 @@ TTC GlobalDef where toBuf b (safeErase gdef) toBuf b (specArgs gdef) toBuf b (inferrable gdef) - toBuf b (vars gdef) + toBuf b (localVars gdef) toBuf b (visibility gdef) toBuf b (totality gdef) toBuf b (flags gdef) diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr index 86de6e23d..1ab9482c5 100644 --- a/src/Core/Unify.idr +++ b/src/Core/Unify.idr @@ -510,7 +510,7 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm isSimple _ = False updateIVar : {v : Nat} -> - forall vs, newvars . IVars vs newvars -> (0 p : IsVar name v newvars) -> + forall vs, newvars . IVars vs newvars -> (0 p : IsVar nm v newvars) -> Maybe (Var vs) updateIVar {v} (ICons Nothing rest) prf = do MkVar prf' <- updateIVar rest prf diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index 27110f7e3..4bcbe0174 100644 --- a/src/Core/UnifyState.idr +++ b/src/Core/UnifyState.idr @@ -1,3 +1,4 @@ + module Core.UnifyState import Core.CaseTree @@ -292,11 +293,6 @@ mkConstantAppArgs {done} {vars = x :: xs} lets fc (b :: env) wkns then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) :: rewrite (appendAssociative wkns [x] (xs ++ done)) in rec else rewrite (appendAssociative wkns [x] (xs ++ done)) in rec - where - mkVar : (wkns : List Name) -> - IsVar name (length wkns) (wkns ++ name :: vars ++ done) - mkVar [] = First - mkVar (w :: ws) = Later (mkVar ws) mkConstantAppArgsSub : {vars : _} -> Bool -> FC -> Env Term vars -> @@ -319,11 +315,6 @@ mkConstantAppArgsSub {done} {vars = x :: xs} then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) :: rewrite appendAssociative wkns [x] (xs ++ done) in rec else rewrite appendAssociative wkns [x] (xs ++ done) in rec - where - mkVar : (wkns : List Name) -> - IsVar name (length wkns) (wkns ++ name :: vars ++ done) - mkVar [] = First - mkVar (w :: ws) = Later (mkVar ws) mkConstantAppArgsOthers : {vars : _} -> Bool -> FC -> Env Term vars -> @@ -346,12 +337,6 @@ mkConstantAppArgsOthers {done} {vars = x :: xs} then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) :: rewrite appendAssociative wkns [x] (xs ++ done) in rec else rewrite appendAssociative wkns [x] (xs ++ done) in rec - where - mkVar : (wkns : List Name) -> - IsVar name (length wkns) (wkns ++ name :: vars ++ done) - mkVar [] = First - mkVar (w :: ws) = Later (mkVar ws) - export applyTo : {vars : _} -> diff --git a/src/Core/Value.idr b/src/Core/Value.idr index 9443a9d13..454e21ec2 100644 --- a/src/Core/Value.idr +++ b/src/Core/Value.idr @@ -65,7 +65,7 @@ mutual -- The head of a value: things you can apply arguments to public export data NHead : List Name -> Type where - NLocal : Maybe Bool -> (idx : Nat) -> (0 p : IsVar name idx vars) -> + NLocal : Maybe Bool -> (idx : Nat) -> (0 p : IsVar nm idx vars) -> NHead vars NRef : NameType -> Name -> NHead vars NMeta : Name -> Int -> List (Closure vars) -> NHead vars diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index e5705d8a5..e30166b2e 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -119,6 +119,8 @@ data CLOpt Timing | DebugElabCheck | BlodwenPaths | + ||| Do not print shadowing warnings + IgnoreShadowingWarnings | ||| Generate bash completion info BashCompletion String String | ||| Generate bash completion script @@ -202,6 +204,10 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] MkOpt ["--profile"] [] [Profile] (Just "Generate profile data when compiling, if supported"), + optSeparator, + MkOpt ["--no-shadowing-warning"] [] [IgnoreShadowingWarnings] + (Just "Do not print shadowing warnings"), + optSeparator, MkOpt ["--prefix"] [] [ShowPrefix] (Just "Show installation prefix"), diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 6b6145012..bbb38f6b4 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -22,6 +22,8 @@ import Idris.Syntax import Idris.Elab.Implementation import Idris.Elab.Interface +import Idris.Desugar.Mutual + import Parser.Lexer.Source import TTImp.BindImplicits @@ -653,7 +655,7 @@ mutual desugarType ps (MkPTy fc nameFC n d ty) = do addDocString n d syn <- get Syn - pure $ MkImpTy fc nameFC n !(bindTypeNames (usingImpl syn) + pure $ MkImpTy fc nameFC n !(bindTypeNames fc (usingImpl syn) ps !(desugar AnyExpr ps ty)) getClauseFn : RawImp -> Core Name @@ -727,14 +729,14 @@ mutual = do addDocString n doc syn <- get Syn pure $ MkImpData fc n - !(bindTypeNames (usingImpl syn) + !(bindTypeNames fc (usingImpl syn) ps !(desugar AnyExpr ps tycon)) opts !(traverse (desugarType ps) datacons) desugarData ps doc (MkPLater fc n tycon) = do addDocString n doc syn <- get Syn - pure $ MkImpLater fc n !(bindTypeNames (usingImpl syn) + pure $ MkImpLater fc n !(bindTypeNames fc (usingImpl syn) ps !(desugar AnyExpr ps tycon)) desugarField : {auto s : Ref Syn SyntaxInfo} -> @@ -747,53 +749,9 @@ mutual = do addDocStringNS ns n doc syn <- get Syn pure (MkIField fc rig !(traverse (desugar AnyExpr ps) p ) - n !(bindTypeNames (usingImpl syn) + n !(bindTypeNames fc (usingImpl syn) ps !(desugar AnyExpr ps ty))) - -- Get the declaration to process on each pass of a mutual block - -- Essentially: types on the first pass - -- i.e. type constructors of data declarations - -- function types - -- interfaces (in full, since it includes function types) - -- records (just the generated type constructor) - -- implementation headers (i.e. note their existence, but not the bodies) - -- Everything else on the second pass - getDecl : Pass -> PDecl -> Maybe PDecl - getDecl p (PImplementation fc vis opts _ is cons n ps iname nusing ds) - = Just (PImplementation fc vis opts p is cons n ps iname nusing ds) - - getDecl p (PNamespace fc ns ds) - = Just (PNamespace fc ns (mapMaybe (getDecl p) ds)) - - getDecl AsType d@(PClaim _ _ _ _ _) = Just d - getDecl AsType (PData fc doc vis (MkPData dfc tyn tyc _ _)) - = Just (PData fc doc vis (MkPLater dfc tyn tyc)) - getDecl AsType d@(PInterface _ _ _ _ _ _ _ _ _) = Just d - getDecl AsType d@(PRecord fc doc vis n ps _ _) - = Just (PData fc doc vis (MkPLater fc n (mkRecType ps))) - where - mkRecType : List (Name, RigCount, PiInfo PTerm, PTerm) -> PTerm - mkRecType [] = PType fc - mkRecType ((n, c, p, t) :: ts) = PPi fc c p (Just n) t (mkRecType ts) - getDecl AsType d@(PFixity _ _ _ _) = Just d - getDecl AsType d@(PDirective _ _) = Just d - getDecl AsType d = Nothing - - getDecl AsDef (PClaim _ _ _ _ _) = Nothing - getDecl AsDef d@(PData _ _ _ (MkPLater _ _ _)) = Just d - getDecl AsDef (PInterface _ _ _ _ _ _ _ _ _) = Nothing - getDecl AsDef d@(PRecord _ _ _ _ _ _ _) = Just d - getDecl AsDef (PFixity _ _ _ _) = Nothing - getDecl AsDef (PDirective _ _) = Nothing - getDecl AsDef d = Just d - - getDecl p (PParameters fc ps pds) - = Just (PParameters fc ps (mapMaybe (getDecl p) pds)) - getDecl p (PUsing fc ps pds) - = Just (PUsing fc ps (mapMaybe (getDecl p) pds)) - - getDecl Single d = Just d - export desugarFnOpt : {auto s : Ref Syn SyntaxInfo} -> {auto c : Ref Ctxt Defs} -> @@ -844,11 +802,11 @@ mutual i' <- traverse (desugar AnyExpr ps) i pure (n, rig, i', tm')) params -- Look for implicitly bindable names in the parameters - let pnames = ifThenElse !isUnboundImplicits - (concatMap (findBindableNames True - (ps ++ map Builtin.fst params) []) - (map (Builtin.snd . Builtin.snd . Builtin.snd) params')) - [] + pnames <- ifThenElse (not !isUnboundImplicits) (pure []) + $ map concat + $ for (map (Builtin.snd . Builtin.snd . Builtin.snd) params') + $ findUniqueBindableNames fc True (ps ++ map Builtin.fst params) [] + let paramsb = map (\(n, rig, info, tm) => (n, rig, info, doBind pnames tm)) params' pure [IParameters fc paramsb (concat pds')] @@ -856,7 +814,7 @@ mutual = do syn <- get Syn let oldu = usingImpl syn uimpls' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm) - btm <- bindTypeNames oldu ps tm' + btm <- bindTypeNames fc oldu ps tm' pure (fst ntm, btm)) uimpls put Syn (record { usingImpl = uimpls' ++ oldu } syn) uds' <- traverse (desugarDecl ps) uds @@ -880,14 +838,11 @@ mutual params -- Look for bindable names in all the constraints and parameters let mnames = map dropNS (definedIn body) - let bnames = ifThenElse !isUnboundImplicits - (concatMap (findBindableNames True - (ps ++ mnames ++ paramNames) []) - (map Builtin.snd cons') ++ - concatMap (findBindableNames True - (ps ++ mnames ++ paramNames) []) - (map (snd . snd) params')) - [] + bnames <- ifThenElse (not !isUnboundImplicits) (pure []) + $ map concat + $ for (map Builtin.snd cons' ++ map (snd . snd) params') + $ findUniqueBindableNames fc True (ps ++ mnames ++ paramNames) [] + let paramsb = map (\ (nm, (rig, tm)) => let tm' = doBind bnames tm in (nm, (rig, tm'))) @@ -924,11 +879,10 @@ mutual params' <- traverse (desugar AnyExpr ps) params let _ = the (List RawImp) params' -- Look for bindable names in all the constraints and parameters - let bnames = if !isUnboundImplicits - then - concatMap (findBindableNames True ps []) (map snd cons') ++ - concatMap (findBindableNames True ps []) params' - else [] + bnames <- ifThenElse (not !isUnboundImplicits) (pure []) + $ map concat + $ for (map snd cons' ++ params') + $ findUniqueBindableNames fc True ps [] let paramsb = map (doBind bnames) params' let isb = map (\ (n, r, tm) => (n, r, doBind bnames tm)) is' @@ -1006,8 +960,8 @@ mutual desugarDecl ps (PFixity fc _ _ _) = throw (GenericMsg fc "Fixity declarations must be for unqualified names") desugarDecl ps (PMutual fc ds) - = do let mds = mapMaybe (getDecl AsType) ds ++ mapMaybe (getDecl AsDef) ds - mds' <- traverse (desugarDecl ps) mds + = do let (tys, defs) = splitMutual ds + mds' <- traverse (desugarDecl ps) (tys ++ defs) pure (concat mds') desugarDecl ps (PNamespace fc ns decls) = withExtendedNS ns $ do diff --git a/src/Idris/Desugar/Mutual.idr b/src/Idris/Desugar/Mutual.idr new file mode 100644 index 000000000..c788d7fdf --- /dev/null +++ b/src/Idris/Desugar/Mutual.idr @@ -0,0 +1,53 @@ +module Idris.Desugar.Mutual + +import Idris.Syntax + +%default total + +-- Get the declaration to process on each pass of a mutual block +-- Essentially: types on the first pass +-- i.e. type constructors of data declarations +-- function types +-- interfaces (in full, since it includes function types) +-- records (just the generated type constructor) +-- implementation headers (i.e. note their existence, but not the bodies) +-- Everything else on the second pass +getDecl : Pass -> PDecl -> Maybe PDecl +getDecl p (PImplementation fc vis opts _ is cons n ps iname nusing ds) + = Just (PImplementation fc vis opts p is cons n ps iname nusing ds) + +getDecl p (PNamespace fc ns ds) + = Just (PNamespace fc ns (assert_total $ mapMaybe (getDecl p) ds)) + +getDecl AsType d@(PClaim _ _ _ _ _) = Just d +getDecl AsType (PData fc doc vis (MkPData dfc tyn tyc _ _)) + = Just (PData fc doc vis (MkPLater dfc tyn tyc)) +getDecl AsType d@(PInterface _ _ _ _ _ _ _ _ _) = Just d +getDecl AsType d@(PRecord fc doc vis n ps _ _) + = Just (PData fc doc vis (MkPLater fc n (mkRecType ps))) + where + mkRecType : List (Name, RigCount, PiInfo PTerm, PTerm) -> PTerm + mkRecType [] = PType fc + mkRecType ((n, c, p, t) :: ts) = PPi fc c p (Just n) t (mkRecType ts) +getDecl AsType d@(PFixity _ _ _ _) = Just d +getDecl AsType d@(PDirective _ _) = Just d +getDecl AsType d = Nothing + +getDecl AsDef (PClaim _ _ _ _ _) = Nothing +getDecl AsDef d@(PData _ _ _ (MkPLater _ _ _)) = Just d +getDecl AsDef (PInterface _ _ _ _ _ _ _ _ _) = Nothing +getDecl AsDef d@(PRecord _ _ _ _ _ _ _) = Just d +getDecl AsDef (PFixity _ _ _ _) = Nothing +getDecl AsDef (PDirective _ _) = Nothing +getDecl AsDef d = Just d + +getDecl p (PParameters fc ps pds) + = Just (PParameters fc ps (assert_total $ mapMaybe (getDecl p) pds)) +getDecl p (PUsing fc ps pds) + = Just (PUsing fc ps (assert_total $ mapMaybe (getDecl p) pds)) + +getDecl Single d = Just d + +export +splitMutual : List PDecl -> (List PDecl, List PDecl) +splitMutual ds = (mapMaybe (getDecl AsType) ds, mapMaybe (getDecl AsDef) ds) diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr index 2920846df..8fc3b39f9 100644 --- a/src/Idris/Elab/Implementation.idr +++ b/src/Idris/Elab/Implementation.idr @@ -407,7 +407,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i mty_params let ibound = findImplicits mbase - mty <- bindTypeNamesUsed ibound vars mbase + mty <- bindTypeNamesUsed ifc ibound vars mbase log "elab.implementation" 3 $ "Method " ++ show meth.name ++ " ==> " ++ diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index c50aeca2e..57cbf2a18 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -120,9 +120,9 @@ mkIfaceData {vars} ifc vis env constraints n conName ps dets meths retty = apply (IVar vfc n) (map (IVar EmptyFC) pNames) conty = mkTy Implicit (map jname ps) $ mkTy AutoImplicit (map bhere constraints) (mkTy Explicit (map bname meths) retty) - con = MkImpTy EmptyFC EmptyFC conName !(bindTypeNames [] (pNames ++ map fst meths ++ vars) conty) in + con = MkImpTy EmptyFC EmptyFC conName !(bindTypeNames ifc [] (pNames ++ map fst meths ++ vars) conty) in pure $ IData vfc vis (MkImpData vfc n - !(bindTypeNames [] (pNames ++ map fst meths ++ vars) + !(bindTypeNames ifc [] (pNames ++ map fst meths ++ vars) (mkDataTy vfc ps)) opts [con]) where @@ -156,7 +156,7 @@ getMethDecl : {vars : _} -> Core (nm, RigCount, RawImp) getMethDecl {vars} env nest params mnames (c, nm, ty) = do let paramNames = map fst params - ty_imp <- bindTypeNames [] (paramNames ++ mnames ++ vars) ty + ty_imp <- bindTypeNames EmptyFC [] (paramNames ++ mnames ++ vars) ty pure (nm, c, stripParams paramNames ty_imp) where -- We don't want the parameters to explicitly appear in the method @@ -191,7 +191,7 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig -- which appear in other method types let ty_constr = substNames vars (map applyCon allmeths) sig.type - ty_imp <- bindTypeNames [] vars (bindPs params $ bindIFace vfc ity ty_constr) + ty_imp <- bindTypeNames EmptyFC [] vars (bindPs params $ bindIFace vfc ity ty_constr) cn <- inCurrentNS sig.name let tydecl = IClaim vfc sig.count vis (if sig.isData then [Inline, Invertible] else [Inline]) @@ -255,7 +255,7 @@ getConstraintHint : {vars : _} -> getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, con) = do let ity = apply (IVar fc iname) (map (IVar fc) params) let fty = IPi fc top Explicit Nothing ity con - ty_imp <- bindTypeNames [] (meths ++ vars) fty + ty_imp <- bindTypeNames fc [] (meths ++ vars) fty let hintname = DN ("Constraint " ++ show con) (UN ("__" ++ show iname ++ "_" ++ show con)) @@ -449,7 +449,7 @@ elabInterface {vars} ifc vis env nest constraints iname params dets mcon body $ bindIFace vdfc ity -- bind interface (?!) $ substNames vars methNameMap dty - dty_imp <- bindTypeNames [] (map name tydecls ++ vars) dty + dty_imp <- bindTypeNames dfc [] (map name tydecls ++ vars) dty log "elab.interface.default" 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp let dtydecl = IClaim vdfc rig vis [] (MkImpTy EmptyFC EmptyFC dn dty_imp) diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index fef3d6490..1f89abcec 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -478,6 +478,15 @@ pwarning (UnreachableClause fc env tm) = pure $ errorDesc (reflow "Unreachable clause:" <++> code !(pshow env tm)) <+> line <+> !(ploc fc) +pwarning (ShadowingGlobalDefs _ ns) + = pure $ vcat + $ reflow "We are about to implicitly bind the following lowercase names." + :: reflow "You may be unintentionally shadowing the associated global definitions:" + :: map (\ (n, ns) => indent 2 $ hsep $ pretty n + :: reflow "is shadowing" + :: punctuate comma (map pretty (forget ns))) + (forget ns) + pwarning (Deprecated s) = pure $ pretty "Deprecation warning:" <++> pretty s diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index ab7d3be0e..2e12f7033 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1212,7 +1212,7 @@ namespaceDecl fname indents ds <- blockAfter col (topDecl fname) pure (doc, ns, ds)) (doc, ns, ds) <- pure b.val - pure (PNamespace (boundToFC fname b) ns (concat ds)) + pure (PNamespace (boundToFC fname b) ns (collectDefs $ concat ds)) transformDecl : FileName -> IndentInfo -> Rule PDecl transformDecl fname indents diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index 97755f004..7a15bb65d 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -20,6 +20,7 @@ import TTImp.ProcessDecls import TTImp.TTImp import Idris.Desugar +import Idris.Desugar.Mutual import Idris.Parser import Idris.REPL.Common import Idris.REPL.Opts @@ -33,31 +34,40 @@ import System.File %default covering -processDecl : {auto c : Ref Ctxt Defs} -> - {auto u : Ref UST UState} -> - {auto s : Ref Syn SyntaxInfo} -> - {auto m : Ref MD Metadata} -> - PDecl -> Core (Maybe Error) -processDecl decl - = catch (do impdecls <- desugarDecl [] decl - traverse_ (Check.processDecl [] (MkNested []) []) impdecls - pure Nothing) - (\err => do giveUpConstraints -- or we'll keep trying... - pure (Just err)) - processDecls : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> {auto m : Ref MD Metadata} -> List PDecl -> Core (List Error) + +processDecl : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + PDecl -> Core (List Error) + +-- Special cases to avoid treating these big blocks as units +-- This should give us better error recovery (the whole block won't fail +-- as soon as one of the definitions fails) +processDecl (PNamespace fc ns ps) + = withExtendedNS ns $ processDecls ps +processDecl (PMutual fc ps) + = let (tys, defs) = splitMutual ps in + processDecls (tys ++ defs) + +processDecl decl + = catch (do impdecls <- desugarDecl [] decl + traverse_ (Check.processDecl [] (MkNested []) []) impdecls + pure []) + (\err => do giveUpConstraints -- or we'll keep trying... + pure [err]) + processDecls decls - = do xs <- traverse processDecl decls + = do xs <- concat <$> traverse processDecl decls Nothing <- checkDelayedHoles - | Just err => pure (case mapMaybe id xs of - [] => [err] - errs => errs) + | Just err => pure (if null xs then [err] else xs) errs <- logTime ("+++ Totality check overall") getTotalityErrors - pure (mapMaybe id xs ++ errs) + pure (xs ++ errs) readModule : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index a000abcc8..c627b8043 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -819,7 +819,7 @@ process (TypeSearch searchTerm) let curr = currentNS defs let ctxt = gamma defs rawTy <- desugar AnyExpr [] searchTerm - let bound = piBindNames replFC [] rawTy + bound <- piBindNames replFC [] rawTy (ty, _) <- elabTerm 0 InType [] (MkNested []) [] bound Nothing ty' <- toResolvedNames ty filteredDefs <- diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 180c57a3c..e9acd7e63 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -329,7 +329,7 @@ mutual let args' = if fenv then args - else drop (length (vars def)) args + else drop (length (localVars def)) args mkApp fn' args' toPTermApp fn args = do fn' <- toPTerm appPrec fn diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 309c1d350..91143013d 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -340,6 +340,9 @@ preOptions (ConsoleWidth n :: opts) preOptions (Color b :: opts) = do setColor b preOptions opts +preOptions (IgnoreShadowingWarnings :: opts) + = do setSession (record { showShadowingWarning = False } !getSession) + preOptions opts preOptions (BashCompletion a b :: _) = do os <- opts a b coreLift $ putStr $ unlines os diff --git a/src/Libraries/Data/List1.idr b/src/Libraries/Data/List1.idr index 261b75db3..2273c6bdf 100644 --- a/src/Libraries/Data/List1.idr +++ b/src/Libraries/Data/List1.idr @@ -4,6 +4,14 @@ import public Data.List1 %default total +-- TODO: Remove this, once Data.List1.fromList from base is available +-- to the compiler + +public export +fromList : List a -> Maybe (List1 a) +fromList [] = Nothing +fromList (x :: xs) = Just (x ::: xs) + -- TODO: Remove this, once Data.List1.unsnoc from base is available -- to the compiler export diff --git a/src/TTImp/BindImplicits.idr b/src/TTImp/BindImplicits.idr index f7f3e58d1..989390acd 100644 --- a/src/TTImp/BindImplicits.idr +++ b/src/TTImp/BindImplicits.idr @@ -162,29 +162,30 @@ addUsing uimpls tm export bindTypeNames : {auto c : Ref Ctxt Defs} -> - List (Maybe Name, RawImp) -> + FC -> List (Maybe Name, RawImp) -> List Name -> RawImp-> Core RawImp -bindTypeNames uimpls env tm +bindTypeNames fc uimpls env tm = if !isUnboundImplicits - then let ns = nub (findBindableNames True env [] tm) - btm = doBind ns tm in - pure (addUsing uimpls btm) + then do ns <- findUniqueBindableNames fc True env [] tm + let btm = doBind ns tm + pure (addUsing uimpls btm) else pure tm export bindTypeNamesUsed : {auto c : Ref Ctxt Defs} -> - List String -> List Name -> RawImp -> Core RawImp -bindTypeNamesUsed used env tm + FC -> List String -> List Name -> RawImp -> Core RawImp +bindTypeNamesUsed fc used env tm = if !isUnboundImplicits - then do let ns = nub (findBindableNames True env used tm) + then do ns <- findUniqueBindableNames fc True env used tm pure (doBind ns tm) else pure tm export -piBindNames : FC -> List Name -> RawImp -> RawImp +piBindNames : {auto c : Ref Ctxt Defs} -> + FC -> List Name -> RawImp -> Core RawImp piBindNames loc env tm - = let ns = nub (findBindableNames True env [] tm) in - piBind (map fst ns) tm + = do ns <- findUniqueBindableNames loc True env [] tm + pure $ piBind (map fst ns) tm where piBind : List String -> RawImp -> RawImp piBind [] ty = ty diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index 55f3477dc..fc9665734 100644 --- a/src/TTImp/Elab/Case.idr +++ b/src/TTImp/Elab/Case.idr @@ -53,14 +53,14 @@ findLater {older} x (_ :: xs) = let MkVar p = findLater {older} x xs in MkVar (Later p) -toRig1 : {idx : Nat} -> (0 p : IsVar name idx vs) -> Env Term vs -> Env Term vs +toRig1 : {idx : Nat} -> (0 p : IsVar nm idx vs) -> Env Term vs -> Env Term vs toRig1 First (b :: bs) = if isErased (multiplicity b) then setMultiplicity b linear :: bs else b :: bs toRig1 (Later p) (b :: bs) = b :: toRig1 p bs -toRig0 : {idx : Nat} -> (0 p : IsVar name idx vs) -> Env Term vs -> Env Term vs +toRig0 : {idx : Nat} -> (0 p : IsVar nm idx vs) -> Env Term vs -> Env Term vs toRig0 First (b :: bs) = setMultiplicity b erased :: bs toRig0 (Later p) (b :: bs) = b :: toRig0 p bs diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr index 75b452b01..89f54b628 100644 --- a/src/TTImp/Elab/Check.idr +++ b/src/TTImp/Elab/Check.idr @@ -219,11 +219,6 @@ strengthenedEState {n} {vars} c e fc env dropSub (DropCons sub) = pure sub dropSub _ = throw (InternalError "Badly formed weakened environment") - -- This helps persuade the erasure checker that it can erase IsVar, - -- because there's no matching on it in removeArgVars below. - dropLater : IsVar name (S idx) (v :: vs) -> IsVar name idx vs - dropLater (Later p) = p - -- Remove any instance of the top level local variable from an -- application. Fail if it turns out to be necessary. -- NOTE: While this isn't strictly correct given the type of the hole diff --git a/src/TTImp/Elab/ImplicitBind.idr b/src/TTImp/Elab/ImplicitBind.idr index 4fec8cf34..9080fe965 100644 --- a/src/TTImp/Elab/ImplicitBind.idr +++ b/src/TTImp/Elab/ImplicitBind.idr @@ -152,7 +152,7 @@ bindUnsolved {vars} fc elabmode _ _ => inTerm) fc env tm bindtm -swapIsVarH : {idx : Nat} -> (0 p : IsVar name idx (x :: y :: xs)) -> +swapIsVarH : {idx : Nat} -> (0 p : IsVar nm idx (x :: y :: xs)) -> Var (y :: x :: xs) swapIsVarH First = MkVar (Later First) swapIsVarH (Later p) = swapP p -- it'd be nice to do this all at the top @@ -165,7 +165,7 @@ swapIsVarH (Later p) = swapP p -- it'd be nice to do this all at the top swapP (Later x) = MkVar (Later (Later x)) swapIsVar : (vs : List Name) -> - {idx : Nat} -> (0 p : IsVar name idx (vs ++ x :: y :: xs)) -> + {idx : Nat} -> (0 p : IsVar nm idx (vs ++ x :: y :: xs)) -> Var (vs ++ y :: x :: xs) swapIsVar [] prf = swapIsVarH prf swapIsVar (x :: xs) First = MkVar First diff --git a/src/TTImp/Interactive/ExprSearch.idr b/src/TTImp/Interactive/ExprSearch.idr index a85f5960c..0496af67e 100644 --- a/src/TTImp/Interactive/ExprSearch.idr +++ b/src/TTImp/Interactive/ExprSearch.idr @@ -38,9 +38,9 @@ import Data.List -- of the LHS. Only recursive calls with a different structure are okay. record RecData where constructor MkRecData - {vars : List Name} + {localVars : List Name} recname : Name -- resolved name - lhsapp : Term vars + lhsapp : Term localVars -- Additional definitions required to support the result ExprDefs : Type diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index a1487ad84..424ff9621 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -346,7 +346,7 @@ processData : {vars : _} -> ImpData -> Core () processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw) = do n <- inCurrentNS n_in - ty_raw <- bindTypeNames [] vars ty_raw + ty_raw <- bindTypeNames fc [] vars ty_raw defs <- get Ctxt -- Check 'n' is undefined @@ -382,7 +382,7 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw) processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_raw) = do n <- inCurrentNS n_in - ty_raw <- bindTypeNames [] vars ty_raw + ty_raw <- bindTypeNames fc [] vars ty_raw log "declare.data" 1 $ "Processing " ++ show n defs <- get Ctxt diff --git a/src/TTImp/ProcessDecls.idr b/src/TTImp/ProcessDecls.idr index 98301fa1a..0e64b04f0 100644 --- a/src/TTImp/ProcessDecls.idr +++ b/src/TTImp/ProcessDecls.idr @@ -139,22 +139,22 @@ processTTImpDecls {vars} nest env decls where bindConNames : ImpTy -> Core ImpTy bindConNames (MkImpTy fc nameFC n ty) - = do ty' <- bindTypeNames [] vars ty + = do ty' <- bindTypeNames fc [] vars ty pure (MkImpTy fc nameFC n ty') bindDataNames : ImpData -> Core ImpData bindDataNames (MkImpData fc n t opts cons) - = do t' <- bindTypeNames [] vars t + = do t' <- bindTypeNames fc [] vars t cons' <- traverse bindConNames cons pure (MkImpData fc n t' opts cons') bindDataNames (MkImpLater fc n t) - = do t' <- bindTypeNames [] vars t + = do t' <- bindTypeNames fc [] vars t pure (MkImpLater fc n t') -- bind implicits to make raw TTImp source a bit friendlier bindNames : ImpDecl -> Core ImpDecl bindNames (IClaim fc c vis opts (MkImpTy tfc nameFC n ty)) - = do ty' <- bindTypeNames [] vars ty + = do ty' <- bindTypeNames fc [] vars ty pure (IClaim fc c vis opts (MkImpTy tfc nameFC n ty')) bindNames (IData fc vis d) = do d' <- bindDataNames d diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index 95ad1c7de..bca98afc9 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -629,7 +629,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env -- If it's 'KeepCons/SubRefl' in 'outprf', that means it was in the outer -- environment so we need to keep it in the same place in the 'with' -- function. Hence, turn it to KeepCons whatever - keepOldEnv : {vs : _} -> + keepOldEnv : {0 outer : _} -> {vs : _} -> (outprf : SubVars outer vs) -> SubVars vs' vs -> (vs'' : List Name ** SubVars vs'' vs) keepOldEnv {vs} SubRefl p = (vs ** SubRefl) diff --git a/src/TTImp/ProcessParams.idr b/src/TTImp/ProcessParams.idr index a43e22480..a87fc055a 100644 --- a/src/TTImp/ProcessParams.idr +++ b/src/TTImp/ProcessParams.idr @@ -40,7 +40,7 @@ processParams {vars} {c} {m} {u} nest env fc ps ds -- then read off the environment from the elaborated type. This way -- we'll get all the implicit names we need let pty_raw = mkParamTy ps - pty_imp <- bindTypeNames [] vars (IBindHere fc (PI erased) pty_raw) + pty_imp <- bindTypeNames fc [] vars (IBindHere fc (PI erased) pty_raw) log "declare.param" 10 $ "Checking " ++ show pty_imp pty <- checkTerm (-1) InType [] nest env pty_imp (gType fc) diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr index c348c43b7..18cab9138 100644 --- a/src/TTImp/ProcessRecord.idr +++ b/src/TTImp/ProcessRecord.idr @@ -99,9 +99,9 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields = do let fc = virtualiseFC fc let conty = mkTy paramTelescope $ mkTy (map farg fields) recTy - let con = MkImpTy EmptyFC EmptyFC cname !(bindTypeNames [] (map fst params ++ + let con = MkImpTy EmptyFC EmptyFC cname !(bindTypeNames fc [] (map fst params ++ map fname fields ++ vars) conty) - let dt = MkImpData fc tn !(bindTypeNames [] (map fst params ++ + let dt = MkImpData fc tn !(bindTypeNames fc [] (map fst params ++ map fname fields ++ vars) (mkDataTy fc params)) [] [con] log "declare.record" 5 $ "Record data type " ++ show dt @@ -144,7 +144,7 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields let rname = MN "rec" 0 -- Claim the projection type - projTy <- bindTypeNames [] + projTy <- bindTypeNames fc [] (map fst params ++ map fname fields ++ vars) $ mkTy paramTelescope $ IPi bfc top Explicit (Just rname) recTy ty' diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index a7cd16706..69bdec7d0 100644 --- a/src/TTImp/Utils.idr +++ b/src/TTImp/Utils.idr @@ -1,12 +1,14 @@ module TTImp.Utils import Core.Context +import Core.Options import Core.TT import TTImp.TTImp import Data.List import Data.Strings +import Libraries.Data.List1 as Lib import Libraries.Utils.String %default covering @@ -66,6 +68,22 @@ findBindableNames arg env used (IAlternative fc u alts) -- name should be bound, leave it to the programmer findBindableNames arg env used tm = [] +export +findUniqueBindableNames : + {auto c : Ref Ctxt Defs} -> + FC -> (arg : Bool) -> (env : List Name) -> (used : List String) -> + RawImp -> Core (List (String, String)) +findUniqueBindableNames fc arg env used t + = do let assoc = nub (findBindableNames arg env used t) + when (showShadowingWarning !getSession) $ + do defs <- get Ctxt + let ctxt = gamma defs + ns <- map catMaybes $ for assoc $ \ (n, _) => do + ns <- lookupCtxtName (UN n) ctxt + pure $ MkPair n . map fst <$> Lib.fromList ns + whenJust (Lib.fromList ns) $ recordWarning . ShadowingGlobalDefs fc + pure assoc + export findAllNames : (env : List Name) -> RawImp -> List Name findAllNames env (IVar fc n) diff --git a/tests/Main.idr b/tests/Main.idr index 6f213088c..4046cf938 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -62,6 +62,10 @@ idrisTestsCasetree = MkTestPool "Case tree building" [] -- Case tree building ["casetree001"] +idrisTestsWarning : TestPool +idrisTestsWarning = MkTestPool "Warnings" [] + ["warning001"] + idrisTestsError : TestPool idrisTestsError = MkTestPool "Error messages" [] -- Error messages @@ -296,6 +300,7 @@ main = runner , testPaths "idris2" idrisTestsCoverage , testPaths "idris2" idrisTestsCasetree , testPaths "idris2" idrisTestsError + , testPaths "idris2" idrisTestsWarning , testPaths "idris2" idrisTestsInteractive , testPaths "idris2" idrisTestsInterface , testPaths "idris2" idrisTestsLiterate diff --git a/tests/idris2/basic049/expected b/tests/idris2/basic049/expected index 40f1a1878..b54626a51 100644 --- a/tests/idris2/basic049/expected +++ b/tests/idris2/basic049/expected @@ -1,4 +1,45 @@ 1/1: Building Fld (Fld.idr) +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 +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 +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 +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 +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 +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 +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 + b is shadowing Main.Other.b +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 + b is shadowing Main.Other.b +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 +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 +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 +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 +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 Error: While processing right hand side of r2_shouldNotTypecheck1. Ambiguous elaboration. Possible results: Main.R2.MkR Main.R1.MkR Type diff --git a/tests/idris2/coverage015/expected b/tests/idris2/coverage015/expected index e77581f1d..1984dd745 100644 --- a/tests/idris2/coverage015/expected +++ b/tests/idris2/coverage015/expected @@ -37,6 +37,15 @@ Missing cases: test'' _ 1/1: Building Issue1366 (Issue1366.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + f is shadowing Main.f +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + f is shadowing Main.f +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + f is shadowing Main.f Error: decode is not covering. Issue1366.idr:33:1--33:45 diff --git a/tests/idris2/interface008/expected b/tests/idris2/interface008/expected index 3ef283542..1baa24c29 100644 --- a/tests/idris2/interface008/expected +++ b/tests/idris2/interface008/expected @@ -1,4 +1,7 @@ 1/1: Building Deps (Deps.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + card is shadowing Main.card Error: While processing right hand side of badcard. k is not accessible in this context. Deps.idr:18:13--18:14 diff --git a/tests/idris2/real001/expected b/tests/idris2/real001/expected index 783e875cc..83252d8ba 100644 --- a/tests/idris2/real001/expected +++ b/tests/idris2/real001/expected @@ -1,3 +1,6 @@ 1/3: Building Linear (Linear.idr) 2/3: Building Channel (Channel.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + any is shadowing Prelude.Interfaces.any 3/3: Building TestProto (TestProto.idr) diff --git a/tests/idris2/real002/expected b/tests/idris2/real002/expected index 70081228a..ce479c7a6 100644 --- a/tests/idris2/real002/expected +++ b/tests/idris2/real002/expected @@ -1,4 +1,10 @@ 1/3: Building Control.App (Control/App.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + any is shadowing Prelude.Interfaces.any +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + any is shadowing Prelude.Interfaces.any 2/3: Building Control.App.Console (Control/App/Console.idr) 3/3: Building Store (Store.idr) 3/3: Building StoreL (StoreL.idr) diff --git a/tests/idris2/reflection006/expected b/tests/idris2/reflection006/expected index 6b945263b..d933b9619 100644 --- a/tests/idris2/reflection006/expected +++ b/tests/idris2/reflection006/expected @@ -2,6 +2,12 @@ LOG 0: [x, y] LOG 0: Left: ((Prelude.Types.plus x) y) LOG 0: Right: ((Prelude.Types.plus y) x) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + any is shadowing Prelude.Interfaces.any +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + any is shadowing Prelude.Interfaces.any Error: While processing right hand side of commutes. Error during reflection: Not done refleq.idr:24:16--24:21 diff --git a/tests/idris2/warning001/Issue1401.idr b/tests/idris2/warning001/Issue1401.idr new file mode 100644 index 000000000..53b285db8 --- /dev/null +++ b/tests/idris2/warning001/Issue1401.idr @@ -0,0 +1,3 @@ +fstDup: (xs : List a) -> map fst (map dup xs) === xs +fstDup Nil = Refl +fstDup (x::xs) = ?a diff --git a/tests/idris2/warning001/Issue539.idr b/tests/idris2/warning001/Issue539.idr new file mode 100644 index 000000000..9e75f6665 --- /dev/null +++ b/tests/idris2/warning001/Issue539.idr @@ -0,0 +1,11 @@ +idF : a -> a +idF = id + +extensionality : (f : a -> b) -> (g : a -> b) -> ((x : a) -> f x = g x) -> f = g +extensionality f g = believe_me + +leftIdPoint : (f : a -> b) -> (x : a) -> idF (f x) = f x +leftIdPoint f x = Refl + +leftId : (f : a -> b) -> (idF . f = f) +leftId f = ?hole diff --git a/tests/idris2/warning001/Issue621.idr b/tests/idris2/warning001/Issue621.idr new file mode 100644 index 000000000..48341c922 --- /dev/null +++ b/tests/idris2/warning001/Issue621.idr @@ -0,0 +1,9 @@ + +a1 : Char +a1 = 'a' + +a2 : Char +a2 = 'a' + +whyNot : a1 = a2 +whyNot = ?hole diff --git a/tests/idris2/warning001/PR1407.idr b/tests/idris2/warning001/PR1407.idr new file mode 100644 index 000000000..dd9b2019a --- /dev/null +++ b/tests/idris2/warning001/PR1407.idr @@ -0,0 +1,16 @@ +namespace Hoo + + f : Either a b -> Either b a + f (Left a) = Right a + f (Right b) = Left b + + natural : (xs : Either a b) -> ((f . f) . map g) xs === (map g . (f . f)) xs + natural = ?l + +mutual + + g : h === h + g = Refl + + h : g === g + h = Refl diff --git a/tests/idris2/warning001/expected b/tests/idris2/warning001/expected new file mode 100644 index 000000000..02845b5a9 --- /dev/null +++ b/tests/idris2/warning001/expected @@ -0,0 +1,21 @@ +1/1: Building Issue539 (Issue539.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + idF is shadowing Main.idF +1/1: Building Issue621 (Issue621.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + a1 is shadowing Main.a1 + a2 is shadowing Main.a2 +1/1: Building Issue1401 (Issue1401.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + fst is shadowing Builtin.fst, Builtin.DPair.DPair.fst + dup is shadowing Prelude.Basics.dup +1/1: Building PR1407 (PR1407.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + f is shadowing Main.Hoo.f +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + g is shadowing Main.g diff --git a/tests/idris2/warning001/run b/tests/idris2/warning001/run new file mode 100755 index 000000000..d4b5948db --- /dev/null +++ b/tests/idris2/warning001/run @@ -0,0 +1,6 @@ +$1 --no-color --console-width 0 --check Issue539.idr +$1 --no-color --console-width 0 --check Issue621.idr +$1 --no-color --console-width 0 --check Issue1401.idr +$1 --no-color --console-width 0 --check PR1407.idr + +rm -rf build diff --git a/tests/typedd-book/chapter03/expected b/tests/typedd-book/chapter03/expected index c192fa082..bf796a403 100644 --- a/tests/typedd-book/chapter03/expected +++ b/tests/typedd-book/chapter03/expected @@ -1,6 +1,21 @@ 1/8: Building IsEven (IsEven.idr) 2/8: Building Matrix (Matrix.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Data.Vect.elem, Prelude.Types.elem +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Data.Vect.elem, Prelude.Types.elem +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Data.Vect.elem, Prelude.Types.elem 3/8: Building VecSort (VecSort.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Data.Vect.elem, Prelude.Types.elem +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Data.Vect.elem, Prelude.Types.elem 4/8: Building Vectors (Vectors.idr) 5/8: Building WordLength (WordLength.idr) 6/8: Building WordLength_vec (WordLength_vec.idr) diff --git a/tests/typedd-book/chapter04/expected b/tests/typedd-book/chapter04/expected index 6187e2cff..51ec61665 100644 --- a/tests/typedd-book/chapter04/expected +++ b/tests/typedd-book/chapter04/expected @@ -1,4 +1,13 @@ 1/12: Building BSTree (BSTree.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Prelude.Types.elem +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Prelude.Types.elem +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Prelude.Types.elem 2/12: Building DataStore (DataStore.idr) 3/12: Building Direction (Direction.idr) 4/12: Building Generic (Generic.idr) @@ -6,7 +15,19 @@ 6/12: Building Shape (Shape.idr) 7/12: Building SumInputs (SumInputs.idr) 8/12: Building Tree (Tree.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Prelude.Types.elem +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Prelude.Types.elem +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Prelude.Types.elem 9/12: Building TryIndex (TryIndex.idr) 10/12: Building Vect (Vect.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Prelude.Types.elem 11/12: Building Vehicle (Vehicle.idr) 12/12: Building All (All.idr) diff --git a/tests/typedd-book/chapter06/expected b/tests/typedd-book/chapter06/expected index 75e236301..1263e446f 100644 --- a/tests/typedd-book/chapter06/expected +++ b/tests/typedd-book/chapter06/expected @@ -1,6 +1,36 @@ 1/8: Building Adder (Adder.idr) 2/8: Building DataStore (DataStore.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema 3/8: Building DataStoreHoles (DataStoreHoles.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema 4/8: Building Maybe (Maybe.idr) 5/8: Building Printf (Printf.idr) 6/8: Building TypeFuns (TypeFuns.idr) diff --git a/tests/typedd-book/chapter07/expected b/tests/typedd-book/chapter07/expected index 047b80226..1cad5425f 100644 --- a/tests/typedd-book/chapter07/expected +++ b/tests/typedd-book/chapter07/expected @@ -3,4 +3,16 @@ 3/6: Building Expr (Expr.idr) 4/6: Building Fold (Fold.idr) 5/6: Building Tree (Tree.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Prelude.Types.elem +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Prelude.Types.elem +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Prelude.Types.elem +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Prelude.Types.elem 6/6: Building All (All.idr) diff --git a/tests/typedd-book/chapter08/expected b/tests/typedd-book/chapter08/expected index 3180d8f40..0f1fd2ab2 100644 --- a/tests/typedd-book/chapter08/expected +++ b/tests/typedd-book/chapter08/expected @@ -1,4 +1,13 @@ 1/10: Building AppendVec (AppendVec.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Data.Vect.elem, Prelude.Types.elem +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Data.Vect.elem, Prelude.Types.elem +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Data.Vect.elem, Prelude.Types.elem 2/10: Building CheckEqDec (CheckEqDec.idr) 3/10: Building CheckEqMaybe (CheckEqMaybe.idr) 4/10: Building EqNat (EqNat.idr) diff --git a/tests/typedd-book/chapter11/expected b/tests/typedd-book/chapter11/expected index d197689b1..8b1364462 100644 --- a/tests/typedd-book/chapter11/expected +++ b/tests/typedd-book/chapter11/expected @@ -5,6 +5,9 @@ 5/12: Building Greet (Greet.idr) 6/12: Building InfIO (InfIO.idr) 7/12: Building InfList (InfList.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + elem is shadowing Prelude.Types.elem 8/12: Building Label (Label.idr) 9/12: Building RunIO (RunIO.idr) 10/12: Building Streams (Streams.idr) diff --git a/tests/typedd-book/chapter12/expected b/tests/typedd-book/chapter12/expected index 9804dc3c6..4ca97fe52 100644 --- a/tests/typedd-book/chapter12/expected +++ b/tests/typedd-book/chapter12/expected @@ -1,5 +1,17 @@ 1/10: Building ArithState (ArithState.idr) 2/10: Building DataStore (DataStore.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + schema is shadowing Main.DataStore.schema 3/10: Building Record (Record.idr) 4/10: Building State (State.idr) 5/10: Building StateMonad (StateMonad.idr) diff --git a/tests/typedd-book/chapter14/expected b/tests/typedd-book/chapter14/expected index 5d1474513..4c0e8c666 100644 --- a/tests/typedd-book/chapter14/expected +++ b/tests/typedd-book/chapter14/expected @@ -1,4 +1,7 @@ 1/4: Building DoorJam (DoorJam.idr) 2/4: Building ATM (ATM.idr) 3/4: Building Hangman (Hangman.idr) +Warning: We are about to implicitly bind the following lowercase names. +You may be unintentionally shadowing the associated global definitions: + letters is shadowing Main.letters 4/4: Building All (All.idr)