From ea093ffaed7b003d28e35cb3b1114ac4bce4603d Mon Sep 17 00:00:00 2001 From: Adowrath Date: Wed, 25 Oct 2023 12:24:43 +0200 Subject: [PATCH] [ warning ] for incompatible visibilities on forward decls and definitions. (#3063) --- CHANGELOG.md | 9 +++ idris2api.ipkg | 1 + libs/base/Language/Reflection/TTImp.idr | 48 +++++++++++- src/Compiler/Common.idr | 9 ++- src/Compiler/Inline.idr | 7 +- src/Compiler/Opts/InlineHeuristics.idr | 3 +- src/Core/AutoSearch.idr | 6 +- src/Core/Binary/Prims.idr | 16 ++++ src/Core/Context.idr | 17 +++-- src/Core/Context/Context.idr | 3 +- src/Core/Context/Data.idr | 6 +- src/Core/Core.idr | 8 ++ src/Core/Normalise/Eval.idr | 4 +- src/Core/Reflect.idr | 23 ++++++ src/Core/SchemeEval/Compile.idr | 4 +- src/Core/TTC.idr | 7 +- src/Core/UnifyState.idr | 9 ++- src/Idris/Doc/Keywords.idr | 5 ++ src/Idris/Doc/String.idr | 10 ++- src/Idris/Elab/Interface.idr | 21 +++--- src/Idris/Error.idr | 9 +++ src/Idris/Package.idr | 3 +- src/Idris/Parser.idr | 17 +++-- src/Idris/REPL.idr | 5 +- src/Idris/REPL/FuzzySearch.idr | 3 +- src/Idris/Syntax.idr | 9 ++- src/Libraries/Data/WithDefault.idr | 74 +++++++++++++++++++ src/TTImp/Elab/Ambiguity.idr | 3 +- src/TTImp/Elab/App.idr | 6 +- src/TTImp/Elab/Case.idr | 5 +- src/TTImp/Elab/Check.idr | 7 +- src/TTImp/Elab/Local.idr | 7 +- src/TTImp/Interactive/Completion.idr | 4 +- src/TTImp/Interactive/ExprSearch.idr | 5 +- src/TTImp/Parser.idr | 13 ++-- src/TTImp/PartialEval.idr | 3 +- src/TTImp/ProcessData.idr | 29 +++++--- src/TTImp/ProcessDef.idr | 17 +++-- src/TTImp/ProcessRecord.idr | 19 +++-- src/TTImp/ProcessType.idr | 3 +- src/TTImp/Reflect.idr | 1 + src/TTImp/TTImp.idr | 7 +- src/TTImp/TTImp/TTC.idr | 2 + tests/idris2/error028/Issue1236.idr | 24 ++++++ tests/idris2/error028/expected | 13 ++++ tests/idris2/error028/run | 3 + .../reflection/reflection004/refdecl.idr | 2 +- .../reflection/reflection014/refdecl.idr | 2 +- .../reflection024/src/TypeProviders.idr | 2 +- 49 files changed, 401 insertions(+), 112 deletions(-) create mode 100644 src/Libraries/Data/WithDefault.idr create mode 100644 tests/idris2/error028/Issue1236.idr create mode 100644 tests/idris2/error028/expected create mode 100644 tests/idris2/error028/run diff --git a/CHANGELOG.md b/CHANGELOG.md index bd07ef654..20af96717 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -17,6 +17,10 @@ [#1066](https://github.com/idris-lang/idris2/issues/1066)). * `%hide` directives can now hide conflicting fixities from other modules. * Fixity declarations can now be kept private with export modifiers. +* Forward-declarations whose visibility differ from their + actual definition now emit a warning, unless the definition + has no specified visibility + (addressing Issue [#1236](https://github.com/idris-lang/Idris2/issues/1236)). * New `fromTTImp`, `fromName`, and `fromDecls` names for custom `TTImp`, `Name`, and `Decls` literals. * Call to `%macro`-functions do not require the `ElabReflection` extension. @@ -119,6 +123,9 @@ To avoid confusing tooling about which `.ipkg` to use, the package file is under the newly added `ipkg` sub-directory. +* Added `Libraries.Data.WithDefault` to facilitate consistent use + of a default-if-unspecified value, currently for `private` visibility. + ### Library changes #### Prelude @@ -211,6 +218,8 @@ * Adds `infixOfBy` and `isInfixOfBy` into `Data.List`. +* Adds `WithDefault` into `Language.Reflection.TTImp`, mirroring compiler addition. + * Adds updating functions to `SortedMap` and `SortedDMap`. * Adds `grouped` function to `Data.List` for splitting a list into equal-sized slices. diff --git a/idris2api.ipkg b/idris2api.ipkg index 88429b16d..812250083 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -189,6 +189,7 @@ modules = Libraries.Data.Tap, Libraries.Data.UserNameMap, Libraries.Data.Version, + Libraries.Data.WithDefault, Libraries.System.File, Libraries.System.File.Buffer, diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr index 34c6ac3ad..9f5a64212 100644 --- a/libs/base/Language/Reflection/TTImp.idr +++ b/libs/base/Language/Reflection/TTImp.idr @@ -178,17 +178,42 @@ mutual %name Clause cl + public export + data WithDefault : (a : Type) -> (def : a) -> Type where + DefaultedValue : WithDefault a def + SpecifiedValue : a -> WithDefault a def + + export + specified : a -> WithDefault a def + specified = SpecifiedValue + + export + defaulted : WithDefault a def + defaulted = DefaultedValue + + export + collapseDefault : {def : a} -> WithDefault a def -> a + collapseDefault DefaultedValue = def + collapseDefault (SpecifiedValue a) = a + + export + onWithDefault : (defHandler : Lazy b) -> (valHandler : a -> b) -> + WithDefault a def -> b + onWithDefault defHandler _ DefaultedValue = defHandler + onWithDefault _ valHandler (SpecifiedValue v) = valHandler v + public export data Decl : Type where IClaim : FC -> Count -> Visibility -> List FnOpt -> ITy -> Decl - IData : FC -> Visibility -> Maybe TotalReq -> Data -> Decl + IData : FC -> WithDefault Visibility Private -> Maybe TotalReq -> Data -> Decl IDef : FC -> Name -> (cls : List Clause) -> Decl IParameters : FC -> (params : List (Name, Count, PiInfo TTImp, TTImp)) -> (decls : List Decl) -> Decl IRecord : FC -> Maybe String -> -- nested namespace - Visibility -> Maybe TotalReq -> Record -> Decl + WithDefault Visibility Private -> + Maybe TotalReq -> Record -> Decl INamespace : FC -> Namespace -> (decls : List Decl) -> Decl ITransform : FC -> Name -> TTImp -> TTImp -> Decl IRunElabDecl : FC -> TTImp -> Decl @@ -300,6 +325,25 @@ Eq DataOpt where NoNewtype == NoNewtype = True _ == _ = False +public export +Eq a => Eq (WithDefault a def) where + DefaultedValue == DefaultedValue = True + DefaultedValue == SpecifiedValue _ = False + SpecifiedValue _ == DefaultedValue = False + SpecifiedValue x == SpecifiedValue y = x == y + +public export +Ord a => Ord (WithDefault a def) where + compare DefaultedValue DefaultedValue = EQ + compare DefaultedValue (SpecifiedValue _) = LT + compare (SpecifiedValue _) DefaultedValue = GT + compare (SpecifiedValue x) (SpecifiedValue y) = compare x y + +public export +{def : a} -> (Show a) => Show (WithDefault a def) where + show (SpecifiedValue x) = show x + show DefaultedValue = show def + public export Eq a => Eq (PiInfo a) where ImplicitArg == ImplicitArg = True diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index ebb5c24a0..49fc85a6a 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -16,13 +16,14 @@ import Core.Directory import Core.Options import Core.TT import Core.TTC -import Libraries.Data.IOArray -import Libraries.Utils.Scheme import Data.List import Data.List1 -import Libraries.Data.NameMap import Data.String as String +import Libraries.Data.NameMap +import Libraries.Data.IOArray +import Libraries.Data.WithDefault +import Libraries.Utils.Scheme import Idris.Syntax import Idris.Env @@ -151,7 +152,7 @@ getMinimalDef (Coded ns bin) name <- fromBuf b let def = MkGlobalDef fc name (Erased fc Placeholder) [] [] [] [] mul - [] Public (MkTotality Unchecked IsCovering) False + [] (specified Public) (MkTotality Unchecked IsCovering) False [] Nothing refsR False False True None cdef Nothing [] Nothing pure (def, Just (ns, bin)) diff --git a/src/Compiler/Inline.idr b/src/Compiler/Inline.idr index bf7e44cff..b66d4c8b9 100644 --- a/src/Compiler/Inline.idr +++ b/src/Compiler/Inline.idr @@ -14,11 +14,12 @@ import Core.Hash import Core.Options import Core.TT -import Libraries.Data.LengthMatch import Data.Maybe -import Libraries.Data.NameMap import Data.List import Data.Vect +import Libraries.Data.LengthMatch +import Libraries.Data.NameMap +import Libraries.Data.WithDefault %default covering @@ -561,7 +562,7 @@ addArityHash n Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure () let Just cexpr = compexpr def | Nothing => pure () let MkFun args _ = cexpr | _ => pure () - case visibility def of + case collapseDefault $ visibility def of Private => pure () _ => addHash (n, length args) diff --git a/src/Compiler/Opts/InlineHeuristics.idr b/src/Compiler/Opts/InlineHeuristics.idr index f33318de0..17ec698ad 100644 --- a/src/Compiler/Opts/InlineHeuristics.idr +++ b/src/Compiler/Opts/InlineHeuristics.idr @@ -4,6 +4,7 @@ import Compiler.CompileExpr import Core.Context import Core.Context.Log import Data.Vect +import Libraries.Data.WithDefault parameters (fn : Name) isVar : CExp vars -> Bool @@ -55,7 +56,7 @@ inlineHeuristics fn = do -- intervention by this function. -- We could lift this public restriction if we checked that the source def was _either -- public OR the destination was the same module as the source_. - let Public = gdef.visibility + let Public = collapseDefault $ gdef.visibility | _ => pure () unless (NoInline `elem` gdef.flags) $ do log "compiler.inline.heuristic" 25 $ "inlining heuristic decided to inline: " ++ show fn diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr index 03e02d4e6..9e893c848 100644 --- a/src/Core/AutoSearch.idr +++ b/src/Core/AutoSearch.idr @@ -13,6 +13,8 @@ import Data.Either import Data.List import Data.Maybe +import Libraries.Data.WithDefault + %default covering SearchEnv : List Name -> Type @@ -365,7 +367,7 @@ searchName : {vars : _} -> searchName fc rigc defaults trying depth def top env target (n, ndef) = do defs <- get Ctxt when (not (visibleInAny (!getNS :: !getNestedNS) - (fullname ndef) (visibility ndef))) $ + (fullname ndef) (collapseDefault $ visibility ndef))) $ throw (CantSolveGoal fc (gamma defs) [] top Nothing) when (BlockedHint `elem` flags ndef) $ throw (CantSolveGoal fc (gamma defs) [] top Nothing) @@ -416,7 +418,7 @@ searchNames fc rigc defaults trying depth defining topty env ambig (n :: ns) tar visible gam nspace n = do Just def <- lookupCtxtExact n gam | Nothing => pure Nothing - if visibleInAny nspace n (visibility def) + if visibleInAny nspace n (collapseDefault $ visibility def) then pure $ Just (n, def) else pure $ Nothing diff --git a/src/Core/Binary/Prims.idr b/src/Core/Binary/Prims.idr index adb22d210..6a5d18448 100644 --- a/src/Core/Binary/Prims.idr +++ b/src/Core/Binary/Prims.idr @@ -15,6 +15,7 @@ import Libraries.Data.PosMap import public Libraries.System.File.Meta as L -- Remove after release 0.7.0 import public Libraries.Utils.Binary import public Libraries.Utils.String +import Libraries.Data.WithDefault import System.Info import System.File @@ -281,6 +282,21 @@ TTC a => TTC (Maybe a) where pure (Just val) _ => corrupt "Maybe" +export +TTC a => TTC (WithDefault a def) where + toBuf b def = onWithDefault + (tag 0) + (\v => do tag 1 + toBuf b v) + def + + fromBuf b + = case !getTag of + 0 => pure defaulted + 1 => do val <- fromBuf b + pure (specified val) + _ => corrupt "WithDefault" + export (TTC a, TTC b) => TTC (Either a b) where toBuf b (Left val) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 4ce119459..6918bc370 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -28,6 +28,7 @@ import Data.Nat import Libraries.Data.NameMap import Libraries.Data.StringMap import Libraries.Data.UserNameMap +import Libraries.Data.WithDefault import Libraries.Text.Distance.Levenshtein import System.Clock @@ -319,11 +320,11 @@ commitCtxt ctxt ||| @rig quantity annotation ||| @vars local variables ||| @ty (closed) type -||| @vis Visibility +||| @vis Visibility, defaulting to private ||| @def actual definition export newDef : (fc : FC) -> (n : Name) -> (rig : RigCount) -> (vars : List Name) -> - (ty : ClosedTerm) -> (vis : Visibility) -> (def : Def) -> GlobalDef + (ty : ClosedTerm) -> (vis : WithDefault Visibility Private) -> (def : Def) -> GlobalDef newDef fc n rig vars ty vis def = MkGlobalDef { location = fc @@ -713,6 +714,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 (IncompatibleVisibility fc x y n) = IncompatibleVisibility fc x y <$> full gam n full gam w@(ShadowingLocalBindings _ _) = pure w full gam (Deprecated fc x y) = Deprecated fc x <$> traverseOpt (traversePair (full gam)) y full gam (GenericWarn fc x) = pure (GenericWarn fc x) @@ -721,6 +723,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 (IncompatibleVisibility fc x y n) = IncompatibleVisibility fc x y <$> resolved gam n resolved gam w@(ShadowingLocalBindings _ _) = pure w resolved gam (Deprecated fc x y) = Deprecated fc x <$> traverseOpt (traversePair (resolved gam)) y resolved gam (GenericWarn fc x) = pure (GenericWarn fc x) @@ -1132,7 +1135,7 @@ getSimilarNames nm = case show <$> userNameRoot nm of | False => pure Nothing Just def <- lookupCtxtExact nm (gamma defs) | Nothing => pure Nothing -- should be impossible - pure (Just (visibility def, dist)) + pure (Just (collapseDefault $ visibility def, dist)) kept <- NameMap.mapMaybeM @{CORE} test (resolvedAs (gamma defs)) pure $ Just (str, toList kept) @@ -1166,7 +1169,7 @@ showSimilarNames ns nm str kept getVisibility : {auto c : Ref Ctxt Defs} -> - FC -> Name -> Core Visibility + FC -> Name -> Core (WithDefault Visibility Private) getVisibility fc n = do defs <- get Ctxt Just def <- lookupCtxtExact n (gamma defs) @@ -1201,7 +1204,7 @@ ambiguousName : {auto c : Ref Ctxt Defs} -> FC -> Name -> List Name -> Core a ambiguousName fc n ns = do - ns <- filterM (\x => pure $ !(getVisibility fc x) /= Private) ns + ns <- filterM (\x => pure $ !(collapseDefault <$> getVisibility fc x) /= Private) ns case ns of [] => undefinedName fc n ns => throw $ AmbiguousName fc ns @@ -1329,7 +1332,7 @@ addBuiltin n ty tot op , inferrable = [] , multiplicity = top , localVars = [] - , visibility = Public + , visibility = specified Public , totality = tot , isEscapeHatch = False , flags = [Inline] @@ -1664,7 +1667,7 @@ setVisibility fc n vis = do defs <- get Ctxt Just def <- lookupCtxtExact n (gamma defs) | Nothing => undefinedName fc n - ignore $ addDef n ({ visibility := vis } def) + ignore $ addDef n ({ visibility := specified vis } def) public export record SearchData where diff --git a/src/Core/Context/Context.idr b/src/Core/Context/Context.idr index 4394ea6b8..c451f9252 100644 --- a/src/Core/Context/Context.idr +++ b/src/Core/Context/Context.idr @@ -14,6 +14,7 @@ import Libraries.Data.IntMap import Libraries.Data.IOArray import Libraries.Data.NameMap import Libraries.Data.UserNameMap +import Libraries.Data.WithDefault import Libraries.Utils.Binary import Libraries.Utils.Scheme @@ -342,7 +343,7 @@ record GlobalDef where inferrable : List Nat -- arguments which can be inferred from elsewhere in the type multiplicity : RigCount localVars : List Name -- environment name is defined in - visibility : Visibility + visibility : WithDefault Visibility Private totality : Totality isEscapeHatch : Bool flags : List DefFlag diff --git a/src/Core/Context/Data.idr b/src/Core/Context/Data.idr index 83bce4b39..72ace6d46 100644 --- a/src/Core/Context/Data.idr +++ b/src/Core/Context/Data.idr @@ -9,6 +9,8 @@ import Core.Normalise import Data.List import Data.Maybe +import Libraries.Data.WithDefault + %default covering -- If a name appears more than once in an argument list, only the first is @@ -102,7 +104,7 @@ addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons) log "declare.data.parameters" 20 $ "Positions of parameters for datatype" ++ show tyn ++ ": [" ++ showSep ", " (map show paramPositions) ++ "]" - let tydef = newDef dfc tyn top vars tycon vis + let tydef = newDef dfc tyn top vars tycon (specified vis) (TCon tag arity paramPositions allPos @@ -124,7 +126,7 @@ addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons) Context -> Core Context addDataConstructors tag [] gam = pure gam addDataConstructors tag (MkCon fc n a ty :: cs) gam - = do let condef = newDef fc n top vars ty (conVisibility vis) (DCon tag a Nothing) + = do let condef = newDef fc n top vars ty (specified $ conVisibility vis) (DCon tag a Nothing) -- Check 'n' is undefined Nothing <- lookupCtxtExact n gam | Just gdef => throw (AlreadyDefined fc n) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 9a743737d..4c6ebf693 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 + ||| Soft-breaking change, make an error later. + ||| @ original Originally declared visibility on forward decl + ||| @ new Incompatible new visibility on actual declaration. + IncompatibleVisibility : FC -> (original : Visibility) -> + (new : Visibility) -> Name -> Warning ||| First FC is type ||| @ shadowed list of names which are shadowed, ||| where they originally appear @@ -204,6 +209,7 @@ Show Warning where show (ParserWarning fc msg) = show fc ++ msg show (UnreachableClause fc _ _) = show fc ++ ":Unreachable clause" show (ShadowingGlobalDefs fc _) = show fc ++ ":Shadowing names" + show (IncompatibleVisibility fc _ _ _) = show fc ++ ":Incompatible Visibility" show (ShadowingLocalBindings fc _) = show fc ++ ":Shadowing names" show (Deprecated fc name _) = show fc ++ ":Deprecated " ++ name show (GenericWarn fc msg) = show fc ++ msg @@ -395,6 +401,7 @@ getWarningLoc : Warning -> FC getWarningLoc (ParserWarning fc _) = fc getWarningLoc (UnreachableClause fc _ _) = fc getWarningLoc (ShadowingGlobalDefs fc _) = fc +getWarningLoc (IncompatibleVisibility loc _ _ _) = loc getWarningLoc (ShadowingLocalBindings fc _) = fc getWarningLoc (Deprecated fc _ fcAndName) = fromMaybe fc (fst <$> fcAndName) getWarningLoc (GenericWarn fc _) = fc @@ -483,6 +490,7 @@ 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 (IncompatibleVisibility fc x y z) = IncompatibleVisibility emptyFC x y z killWarningLoc (ShadowingLocalBindings fc xs) = ShadowingLocalBindings emptyFC $ (\(n, _, _) => (n, emptyFC, emptyFC)) <$> xs killWarningLoc (Deprecated fc x y) = Deprecated emptyFC x (map ((emptyFC,) . snd) y) diff --git a/src/Core/Normalise/Eval.idr b/src/Core/Normalise/Eval.idr index 8d4ff22f7..c30b4936e 100644 --- a/src/Core/Normalise/Eval.idr +++ b/src/Core/Normalise/Eval.idr @@ -15,6 +15,8 @@ import Data.Nat import Data.String import Data.Vect +import Libraries.Data.WithDefault + %default covering -- A pair of a term and its normal form. This could be constructed either @@ -291,7 +293,7 @@ parameters (defs : Defs, topopts : EvalOpts) let redok1 = evalAll topopts let redok2 = reducibleInAny (currentNS defs :: nestedNS defs) (fullname res) - (visibility res) + (collapseDefault $ visibility res) -- want to shortcut that second check, if we're evaluating -- everything, so don't let bind unless we need that log! let redok = redok1 || redok2 diff --git a/src/Core/Reflect.idr b/src/Core/Reflect.idr index b5fe06eaf..8e9a6cc89 100644 --- a/src/Core/Reflect.idr +++ b/src/Core/Reflect.idr @@ -8,6 +8,8 @@ import Core.Normalise import Core.TT import Core.Value +import Libraries.Data.WithDefault + %default covering public export @@ -292,6 +294,27 @@ Reflect a => Reflect (Maybe a) where = do x' <- reflect fc defs lhs env x appCon fc defs (preludetypes "Just") [Erased fc Placeholder, x'] + +export +Reify a => Reify (WithDefault a def) where + reify defs val@(NDCon _ n _ _ args) + = case (dropAllNS !(full (gamma defs) n), args) of + (UN (Basic "DefaultedValue"), _) => pure defaulted + (UN (Basic "SpecifiedValue"), [_, _, (_, x)]) + => do x' <- reify defs !(evalClosure defs x) + pure (specified x') + _ => cantReify val "WithDefault" + reify defs val = cantReify val "WithDefault" + +export +Reflect a => Reflect (WithDefault a def) where + reflect fc defs lhs env def + = onWithDefault + (appCon fc defs (reflectionttimp "Default") [Erased fc Placeholder, Erased fc Placeholder]) + (\x => do x' <- reflect fc defs lhs env x + appCon fc defs (reflectionttimp "Value") [Erased fc Placeholder, Erased fc Placeholder, x']) + def + export (Reify a, Reify b) => Reify (a, b) where reify defs val@(NDCon _ n _ _ [_, _, (_, x), (_, y)]) diff --git a/src/Core/SchemeEval/Compile.idr b/src/Core/SchemeEval/Compile.idr index 41adcafc5..2f98457ac 100644 --- a/src/Core/SchemeEval/Compile.idr +++ b/src/Core/SchemeEval/Compile.idr @@ -24,6 +24,8 @@ import Data.List import Libraries.Utils.Scheme import System.Info +import Libraries.Data.WithDefault + schString : String -> String schString s = concatMap okchar (unpack s) where @@ -567,7 +569,7 @@ compileDef mode n_in let redok = mode == EvalAll || reducibleInAny (currentNS defs :: nestedNS defs) (fullname def) - (visibility def) + (collapseDefault $ visibility def) -- 'n' is used in compileBody for generating names for readback, -- and reading back resolved names is quicker because it's just -- an integer diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index fcc6f7934..186527939 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -11,10 +11,11 @@ import Core.Name import Core.Options import Core.TT -import Libraries.Data.NameMap -import Libraries.Data.IOArray import Data.Vect +import Libraries.Data.NameMap +import Libraries.Data.IOArray +import Libraries.Data.WithDefault import Libraries.Utils.Binary import Libraries.Utils.Scheme @@ -1149,7 +1150,7 @@ TTC GlobalDef where mul vars vis tot hatch fl refs refsR inv c True def cdef Nothing sc Nothing) else pure (MkGlobalDef loc name (Erased loc Placeholder) [] [] [] [] - mul [] Public unchecked False [] refs refsR + mul [] (specified Public) unchecked False [] refs refsR False False True def cdef Nothing [] Nothing) export diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index b698c16d6..24c8b3612 100644 --- a/src/Core/UnifyState.idr +++ b/src/Core/UnifyState.idr @@ -15,6 +15,7 @@ import Core.Value import Data.List import Libraries.Data.IntMap import Libraries.Data.NameMap +import Libraries.Data.WithDefault %default covering @@ -425,7 +426,7 @@ newMetaLets {vars} fc rig env n ty def nocyc lets = do let hty = if lets then abstractFullEnvType fc env ty else abstractEnvType fc env ty let hole = { noCycles := nocyc } - (newDef fc n rig [] hty Public def) + (newDef fc n rig [] hty (specified Public) def) log "unify.meta" 5 $ "Adding new meta " ++ show (n, fc, rig) logTerm "unify.meta" 10 ("New meta type " ++ show n) hty idx <- addDef n hole @@ -470,7 +471,7 @@ newConstant {vars} fc rig env tm ty constrs = do let def = mkConstant fc env tm let defty = abstractFullEnvType fc env ty cn <- genName "postpone" - let guess = newDef fc cn rig [] defty Public + let guess = newDef fc cn rig [] defty (specified Public) (Guess def (length env) constrs) log "unify.constant" 5 $ "Adding new constant " ++ show (cn, fc, rig) logTerm "unify.constant" 10 ("New constant type " ++ show cn) defty @@ -493,7 +494,7 @@ newSearch : {vars : _} -> Env Term vars -> Name -> Term vars -> Core (Int, Term vars) newSearch {vars} fc rig depth def env n ty = do let hty = abstractEnvType fc env ty - let hole = newDef fc n rig [] hty Public (BySearch rig depth def) + let hole = newDef fc n rig [] hty (specified Public) (BySearch rig depth def) log "unify.search" 10 $ "Adding new search " ++ show fc ++ " " ++ show n logTermNF "unify.search" 10 "New search type" [] hty idx <- addDef n hole @@ -514,7 +515,7 @@ newDelayed : {vars : _} -> (ty : Term vars) -> Core (Int, Term vars) newDelayed {vars} fc rig env n ty = do let hty = abstractEnvType fc env ty - let hole = newDef fc n rig [] hty Public Delayed + let hole = newDef fc n rig [] hty (specified Public) Delayed idx <- addDef n hole log "unify.delay" 10 $ "Added delayed elaborator " ++ show (n, idx) addHoleName fc n idx diff --git a/src/Idris/Doc/Keywords.idr b/src/Idris/Doc/Keywords.idr index 88bf47fdc..65084e008 100644 --- a/src/Idris/Doc/Keywords.idr +++ b/src/Idris/Doc/Keywords.idr @@ -137,6 +137,11 @@ visibility = vcat $ * `private` means that neither the declaration nor the definition will be exported. This is the default and is the ideal setting for auxiliary definitions. + """, "", + """ + If a forward-declaration for a definition exists, they cannot declare + incompatible visibility modifiers - they either have to match up or at most + one of the two can declare visibility. """] ifthenelse : Doc IdrisDocAnn diff --git a/src/Idris/Doc/String.idr b/src/Idris/Doc/String.idr index c6dbb1b43..4b99d7629 100644 --- a/src/Idris/Doc/String.idr +++ b/src/Idris/Doc/String.idr @@ -29,6 +29,7 @@ import Libraries.Data.SortedSet import Libraries.Data.SortedMap import Libraries.Data.StringMap as S import Libraries.Data.String.Extra +import Libraries.Data.WithDefault import public Libraries.Text.PrettyPrint.Prettyprinter import public Libraries.Text.PrettyPrint.Prettyprinter.Util @@ -417,11 +418,12 @@ getDocsForName fc n config | [ifacedata] => (Just "interface",) . pure <$> getIFaceDoc ifacedata | _ => pure (Nothing, []) -- shouldn't happen, we've resolved ambiguity by now case definition d of - PMDef _ _ _ _ _ => pure (Nothing, catMaybes [ showTotal (totality d) - , pure (showVisible (visibility d))]) + PMDef _ _ _ _ _ => pure ( Nothing + , catMaybes [ showTotal (totality d) + , pure (showVisible (collapseDefault $ visibility d))]) TCon _ _ _ _ _ _ cons _ => do let tot = catMaybes [ showTotal (totality d) - , pure (showVisible (visibility d))] + , pure (showVisible (collapseDefault $ visibility d))] cdocs <- traverse (getDConDoc <=< toFullNames) cons cdoc <- case cdocs of [] => pure (Just "data", []) @@ -697,7 +699,7 @@ getContents ns visible defs n = do Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure False - pure (visibility def /= Private) + pure (collapseDefault (visibility def) /= Private) inNS : Name -> Bool inNS (NS xns (UN _)) = ns `isParentOf` xns diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index 1eff8eb45..d90ada177 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -22,6 +22,7 @@ import TTImp.Utils import Libraries.Data.ANameMap import Libraries.Data.List.Extra import Data.List +import Libraries.Data.WithDefault %default covering @@ -104,11 +105,11 @@ mkDataTy fc ((n, (_, ty)) :: ps) mkIfaceData : {vars : _} -> {auto c : Ref Ctxt Defs} -> - FC -> Visibility -> Env Term vars -> + FC -> WithDefault Visibility Private -> Env Term vars -> List (Maybe Name, RigCount, RawImp) -> Name -> Name -> List (Name, (RigCount, RawImp)) -> List Name -> List (Name, RigCount, RawImp) -> Core ImpDecl -mkIfaceData {vars} ifc vis env constraints n conName ps dets meths +mkIfaceData {vars} ifc def_vis env constraints n conName ps dets meths = let opts = if isNil dets then [NoHints, UniqueSearch] else [NoHints, UniqueSearch, SearchBy dets] @@ -119,7 +120,7 @@ mkIfaceData {vars} ifc vis env constraints n conName ps dets meths con = MkImpTy vfc EmptyFC conName !(bindTypeNames ifc [] (pNames ++ map fst meths ++ vars) conty) bound = pNames ++ map fst meths ++ vars in - pure $ IData vfc vis Nothing {- ?? -} + pure $ IData vfc def_vis Nothing {- ?? -} $ MkImpData vfc n (Just !(bindTypeNames ifc [] bound (mkDataTy vfc ps))) opts [con] @@ -333,7 +334,7 @@ elabInterface : {vars : _} -> {auto s : Ref Syn SyntaxInfo} -> {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> - FC -> Visibility -> + FC -> WithDefault Visibility Private -> Env Term vars -> NestedNames vars -> (constraints : List (Maybe Name, RawImp)) -> Name -> @@ -342,7 +343,7 @@ elabInterface : {vars : _} -> (conName : Maybe (String, Name)) -> List ImpDecl -> Core () -elabInterface {vars} ifc vis env nest constraints iname params dets mcon body +elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon body = do fullIName <- getFullName iname ns_iname <- inCurrentNS fullIName let conName_in = maybe (mkCon vfc fullIName) snd mcon @@ -396,7 +397,7 @@ elabInterface {vars} ifc vis env nest constraints iname params dets mcon body consts <- traverse (getMethDecl env nest params meth_names . (top,)) constraints log "elab.interface" 5 $ "Constraints: " ++ show consts - dt <- mkIfaceData vfc vis env consts iname conName params + dt <- mkIfaceData vfc def_vis env consts iname conName params dets meths log "elab.interface" 10 $ "Methods: " ++ show meths log "elab.interface" 5 $ "Making interface data type " ++ show dt @@ -407,7 +408,8 @@ elabInterface {vars} ifc vis env nest constraints iname params dets mcon body Core () elabMethods conName meth_names meth_sigs = do -- Methods have same visibility as data declaration - fnsm <- traverse (getMethToplevel env vis iname conName + fnsm <- traverse (getMethToplevel env (collapseDefault def_vis) + iname conName (map fst constraints) meth_names params) meth_sigs @@ -452,7 +454,7 @@ elabInterface {vars} ifc vis env nest constraints iname params dets mcon body 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) + let dtydecl = IClaim vdfc rig (collapseDefault def_vis) [] (MkImpTy EmptyFC EmptyFC dn dty_imp) processDecl [] nest env dtydecl @@ -516,7 +518,8 @@ elabInterface {vars} ifc vis env nest constraints iname params dets mcon body Core () elabConstraintHints conName meth_names = do let nconstraints = nameCons 0 constraints - chints <- traverse (getConstraintHint vfc env vis iname conName + chints <- traverse (getConstraintHint vfc env (collapseDefault def_vis) + iname conName (map fst nconstraints) meth_names paramNames) nconstraints diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index ac6932e77..5289d466d 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -33,6 +33,8 @@ Eq Warning where ParserWarning fc1 x1 == ParserWarning fc2 x2 = fc1 == fc2 && x1 == x2 UnreachableClause fc1 rho1 s1 == UnreachableClause fc2 rho2 s2 = fc1 == fc2 ShadowingGlobalDefs fc1 xs1 == ShadowingGlobalDefs fc2 xs2 = fc1 == fc2 && xs1 == xs2 + IncompatibleVisibility fc1 x1 y1 n1 == IncompatibleVisibility fc2 x2 y2 n2 + = fc1 == fc2 && x1 == x2 && y1 == y2 && n1 == n2 Deprecated fc1 x1 y1 == Deprecated fc2 x2 y2 = fc1 == fc2 && x1 == x2 && y1 == y2 GenericWarn fc1 x1 == GenericWarn fc2 x2 = fc1 == fc2 && x1 == x2 _ == _ = False @@ -274,6 +276,13 @@ pwarningRaw (ShadowingGlobalDefs fc ns) :: reflow "is shadowing" :: punctuate comma (map pretty0 (forget ns)) +pwarningRaw (IncompatibleVisibility fc vx vy n) + = pure $ warning (code (pretty0 (sugarName n)) + <++> reflow "has been forward-declared with" + <++> keyword (pretty0 vx) <++> reflow "visibility, cannot change to" + <++> keyword (pretty0 vy) <+> reflow ". This will be an error in a later release.") + <+> line <+> !(ploc fc) + pwarningRaw (ShadowingLocalBindings fc ns) = pure $ vcat [ reflow "You may be unintentionally shadowing the following local bindings:" diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index db361786f..6bd20ba2e 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -26,6 +26,7 @@ import System.File import Libraries.Data.SortedMap import Libraries.Data.StringMap import Libraries.Data.StringTrie +import Libraries.Data.WithDefault import Libraries.Text.Parser import Libraries.Utils.Path import Libraries.Text.PrettyPrint.Prettyprinter.Render.String @@ -756,7 +757,7 @@ makeDoc pkg opts = visible : GlobalDef -> Bool visible def = case definition def of (DCon _ _ _) => False - _ => (visibility def /= Private) + _ => (collapseDefault (visibility def) /= Private) fileError : String -> FileError -> Core (List Error) fileError filename err = pure [FileErr filename err] diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 9fdfe742d..4d5c8e92d 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -19,6 +19,7 @@ import Data.Nat import Data.SnocList import Data.String import Libraries.Utils.String +import Libraries.Data.WithDefault import Idris.Parser.Let @@ -1125,11 +1126,12 @@ visOption fname <|> (decoratedKeyword fname "private" $> Private) -exportVisibility, visibility : OriginDesc -> EmptyRule Visibility +visibility : OriginDesc -> EmptyRule (WithDefault Visibility Private) visibility fname - = visOption fname - <|> pure Private + = (specified <$> visOption fname) + <|> pure defaulted +exportVisibility : OriginDesc -> EmptyRule Visibility exportVisibility fname = visOption fname <|> pure Export @@ -1327,11 +1329,11 @@ dataDeclBody fname indents simpleData fname b n indents <|> gadtData fname col b n indents -- a data declaration can have a visibility and an optional totality (#1404) -dataVisOpt : OriginDesc -> EmptyRule (Visibility, Maybe TotalReq) +dataVisOpt : OriginDesc -> EmptyRule (WithDefault Visibility Private, Maybe TotalReq) dataVisOpt fname - = do { vis <- visOption fname ; mbtot <- optional (totalityOpt fname) ; pure (vis, mbtot) } + = do { vis <- visOption fname ; mbtot <- optional (totalityOpt fname) ; pure (specified vis, mbtot) } <|> do { tot <- totalityOpt fname ; vis <- visibility fname ; pure (vis, Just tot) } - <|> pure (Private, Nothing) + <|> pure (defaulted, Nothing) dataDecl : OriginDesc -> IndentInfo -> Rule PDecl dataDecl fname indents @@ -1747,7 +1749,8 @@ recordParam fname indents -- A record without a where is a forward declaration recordBody : OriginDesc -> IndentInfo -> - String -> Visibility -> Maybe TotalReq -> + String -> WithDefault Visibility Private -> + Maybe TotalReq -> Int -> Name -> List (Name, RigCount, PiInfo PTerm, PTerm) -> diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 8a43944ae..e81487b4c 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -71,6 +71,7 @@ import Data.String import Libraries.Data.List.Extra import Libraries.Data.String.Extra import Libraries.Data.Tap +import Libraries.Data.WithDefault import Libraries.Text.PrettyPrint.Prettyprinter.Util import Libraries.Utils.Path import Libraries.System.Directory.Tree @@ -898,7 +899,7 @@ process (Eval itm) let norm = replEval emode evalResultName <- DN "it" <$> genName "evalResult" ignore $ addDef evalResultName - $ newDef replFC evalResultName top [] ty Private + $ newDef replFC evalResultName top [] ty defaulted $ PMDef defaultPI [] (STerm 0 ntm) (STerm 0 ntm) [] addToSave evalResultName put ROpts ({ evalResultName := Just evalResultName } opts) @@ -989,7 +990,7 @@ process (TypeSearch searchTerm) defs <- traverse (flip lookupCtxtExact ctxt) names let defs = flip mapMaybe defs $ \ md => do d <- md - guard (visibleIn curr (fullname d) (visibility d)) + guard (visibleIn curr (fullname d) (collapseDefault $ visibility d)) guard (isJust $ userNameRoot (fullname d)) pure d allDefs <- traverse (resolved ctxt) defs diff --git a/src/Idris/REPL/FuzzySearch.idr b/src/Idris/REPL/FuzzySearch.idr index 83c3156c6..fcd9f5a8d 100644 --- a/src/Idris/REPL/FuzzySearch.idr +++ b/src/Idris/REPL/FuzzySearch.idr @@ -17,6 +17,7 @@ import Data.Maybe import Data.String import Libraries.Data.List.Extra import Libraries.Data.String.Extra +import Libraries.Data.WithDefault %default covering @@ -49,7 +50,7 @@ fuzzySearch expr = do defs <- traverse (flip lookupCtxtExact ctxt) names let defs = flip mapMaybe defs $ \ md => do d <- md - guard (visibleIn curr (fullname d) (visibility d)) + guard (visibleIn curr (fullname d) (collapseDefault $ visibility d)) guard (isJust $ userNameRoot (fullname d)) pure d allDefs <- traverse (resolved ctxt) defs diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index f273e8efb..ed365477c 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -22,6 +22,7 @@ import Libraries.Data.NameMap import Libraries.Data.SortedMap import Libraries.Data.String.Extra import Libraries.Data.StringMap +import Libraries.Data.WithDefault import Libraries.Text.PrettyPrint.Prettyprinter import Parser.Lexer.Source @@ -428,14 +429,15 @@ mutual data PDecl' : Type -> Type where PClaim : FC -> RigCount -> Visibility -> List (PFnOpt' nm) -> PTypeDecl' nm -> PDecl' nm PDef : FC -> List (PClause' nm) -> PDecl' nm - PData : FC -> (doc : String) -> Visibility -> Maybe TotalReq -> PDataDecl' nm -> PDecl' nm + PData : FC -> (doc : String) -> WithDefault Visibility Private -> + Maybe TotalReq -> PDataDecl' nm -> PDecl' nm PParameters : FC -> List (Name, RigCount, PiInfo (PTerm' nm), PTerm' nm) -> List (PDecl' nm) -> PDecl' nm PUsing : FC -> List (Maybe Name, PTerm' nm) -> List (PDecl' nm) -> PDecl' nm PInterface : FC -> - Visibility -> + WithDefault Visibility Private -> (constraints : List (Maybe Name, PTerm' nm)) -> Name -> (doc : String) -> @@ -456,7 +458,8 @@ mutual PDecl' nm PRecord : FC -> (doc : String) -> - Visibility -> Maybe TotalReq -> + WithDefault Visibility Private -> + Maybe TotalReq -> PRecordDecl' nm -> PDecl' nm diff --git a/src/Libraries/Data/WithDefault.idr b/src/Libraries/Data/WithDefault.idr new file mode 100644 index 000000000..e30ca73f2 --- /dev/null +++ b/src/Libraries/Data/WithDefault.idr @@ -0,0 +1,74 @@ +module Libraries.Data.WithDefault + +export +data WithDefault : (0 a : Type) -> (0 def : a) -> Type where + DefaultedValue : WithDefault a def + SpecifiedValue : a -> WithDefault a def + +export +specified : a -> WithDefault a def +specified = SpecifiedValue + +export +defaulted : WithDefault a def +defaulted = DefaultedValue + +export +specifyValue : a -> WithDefault a def -> WithDefault a def +specifyValue v DefaultedValue = SpecifiedValue v +specifyValue _ v = v + +export +replaceSpecified : WithDefault a def -> WithDefault a def' +replaceSpecified DefaultedValue = DefaultedValue +replaceSpecified (SpecifiedValue v) = SpecifiedValue v + +export +collapseDefault : {def : a} -> WithDefault a def -> a +collapseDefault DefaultedValue = def +collapseDefault (SpecifiedValue v) = v + +export +onWithDefault : (defHandler : Lazy b) -> + (valHandler : a -> b) -> + WithDefault a def -> + b +onWithDefault defHandler _ DefaultedValue = defHandler +onWithDefault _ valHandler (SpecifiedValue v) = valHandler v + +export +collapseDefaults : Eq a => + {def : a} -> + WithDefault a def -> + WithDefault a def -> + Either (a, a) a +collapseDefaults (SpecifiedValue x) (SpecifiedValue y) = if x /= y + then Left (x, y) + else Right x +collapseDefaults (SpecifiedValue x) DefaultedValue = Right x +collapseDefaults DefaultedValue (SpecifiedValue y) = Right y +collapseDefaults DefaultedValue DefaultedValue = Right def + +export +isDefaulted : WithDefault a def -> Bool +isDefaulted DefaultedValue = True +isDefaulted _ = False + +export +isSpecified : WithDefault a def -> Bool +isSpecified DefaultedValue = False +isSpecified _ = True + +public export +Eq a => Eq (WithDefault a def) where + DefaultedValue == DefaultedValue = True + DefaultedValue == SpecifiedValue _ = False + SpecifiedValue _ == DefaultedValue = False + SpecifiedValue x == SpecifiedValue y = x == y + +public export +Ord a => Ord (WithDefault a def) where + compare DefaultedValue DefaultedValue = EQ + compare DefaultedValue (SpecifiedValue _) = LT + compare (SpecifiedValue _) DefaultedValue = GT + compare (SpecifiedValue x) (SpecifiedValue y) = compare x y diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index 09567214c..41932f8ef 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/src/TTImp/Elab/Ambiguity.idr @@ -23,6 +23,7 @@ import Data.String import Data.Vect import Libraries.Data.UserNameMap +import Libraries.Data.WithDefault %default covering @@ -85,7 +86,7 @@ expandAmbigName mode nest env orig args (IVar fc x) exp | _ => pure True if !(isVisible ns) then pure $ visibleInAny (!getNS :: !getNestedNS) (NS ns x) - (visibility def) + (collapseDefault $ visibility def) else pure False -- If there's multiple alternatives and all else fails, resort to using diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 31e4f5fc1..bcff05088 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -20,6 +20,8 @@ import TTImp.TTImp import Data.List import Data.Maybe +import Libraries.Data.WithDefault + %default covering checkVisibleNS : {auto c : Ref Ctxt Defs} -> @@ -71,7 +73,7 @@ getNameType elabMode rigc env fc x do defs <- get Ctxt [(pname, i, def)] <- lookupCtxtName x (gamma defs) | ns => ambiguousName fc x (map fst ns) - checkVisibleNS fc (fullname def) (visibility def) + checkVisibleNS fc (fullname def) (collapseDefault $ visibility def) when (not $ onLHS elabMode) $ checkDeprecation fc def rigSafe (multiplicity def) rigc @@ -126,7 +128,7 @@ getVarType elabMode rigc nest env fc x tm = tmf fc nt tyenv = useVars (getArgs tm) (embed (type ndef)) in - do checkVisibleNS fc (fullname ndef) (visibility ndef) + do checkVisibleNS fc (fullname ndef) (collapseDefault $ visibility ndef) logTerm "elab" 5 ("Type of " ++ show n') tyenv logTerm "elab" 5 ("Expands to") tm log "elab" 5 $ "Arg length " ++ show arglen diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index 95ca22585..e658e17b9 100644 --- a/src/TTImp/Elab/Case.idr +++ b/src/TTImp/Elab/Case.idr @@ -26,6 +26,7 @@ import Data.List import Data.Maybe import Data.String import Libraries.Data.NameMap +import Libraries.Data.WithDefault %default covering @@ -192,9 +193,9 @@ caseBlock {vars} rigc elabinfo fc nest env opts scr scrtm scrty caseRig alts exp let env = updateMults (linearUsed est) env defs <- get Ctxt parentDef <- lookupCtxtExact (Resolved (defining est)) (gamma defs) - let vis = case parentDef of + let vis = specified $ case parentDef of Just gdef => - if visibility gdef == Public + if collapseDefault (visibility gdef) == Public then Public else Private Nothing => Public diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr index 6b4fe3868..df43e0318 100644 --- a/src/TTImp/Elab/Check.idr +++ b/src/TTImp/Elab/Check.idr @@ -20,11 +20,12 @@ import Idris.Syntax import TTImp.TTImp import Data.Either -import Libraries.Data.IntMap import Data.List -import Libraries.Data.NameMap import Data.SnocList +import Libraries.Data.IntMap +import Libraries.Data.NameMap import Libraries.Data.UserNameMap +import Libraries.Data.WithDefault %default covering @@ -411,7 +412,7 @@ uniVar : {auto c : Ref Ctxt Defs} -> FC -> Core Name uniVar fc = do n <- genName "u" - idx <- addDef n (newDef fc n erased [] (Erased fc Placeholder) Public None) + idx <- addDef n (newDef fc n erased [] (Erased fc Placeholder) (specified Public) None) pure (Resolved idx) export diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr index 048208b39..688772733 100644 --- a/src/TTImp/Elab/Local.idr +++ b/src/TTImp/Elab/Local.idr @@ -17,6 +17,7 @@ import TTImp.TTImp import Libraries.Data.NameMap import Data.List +import Libraries.Data.WithDefault %default covering @@ -36,7 +37,7 @@ localHelper {vars} nest env nestdecls_in func let f = defining est defs <- get Ctxt gdef <- lookupCtxtExact (Resolved (defining est)) (gamma defs) - let vis = maybe Public visibility gdef + let vis = maybe Public (collapseDefault . visibility) gdef let mult = maybe linear GlobalDef.multiplicity gdef -- If the parent function is public, the nested definitions need @@ -143,8 +144,8 @@ localHelper {vars} nest env nestdecls_in func setPublic : ImpDecl -> ImpDecl setPublic (IClaim fc c _ opts ty) = IClaim fc c Public opts ty - setPublic (IData fc _ mbt d) = IData fc Public mbt d - setPublic (IRecord fc c _ mbt r) = IRecord fc c Public mbt r + setPublic (IData fc _ mbt d) = IData fc (specified Public) mbt d + setPublic (IRecord fc c _ mbt r) = IRecord fc c (specified Public) mbt r setPublic (IParameters fc ps decls) = IParameters fc ps (map setPublic decls) setPublic (INamespace fc ps decls) diff --git a/src/TTImp/Interactive/Completion.idr b/src/TTImp/Interactive/Completion.idr index 3747a4534..c0097266d 100644 --- a/src/TTImp/Interactive/Completion.idr +++ b/src/TTImp/Interactive/Completion.idr @@ -9,6 +9,8 @@ import Idris.Parser import Data.String +import Libraries.Data.WithDefault + ||| Completion tasks are varied: ||| are we trying to fill in a name, a REPL command, a pragma? data Task @@ -55,7 +57,7 @@ nameCompletion pref = do -- and it better be visible Just def <- lookupCtxtExact nsn (gamma defs) | Nothing => pure Nothing - let True = visibleIn cns nsn (visibility def) + let True = visibleIn cns nsn (collapseDefault $ visibility def) | False => pure Nothing pure (Just n) pure (map show $ nub nms) diff --git a/src/TTImp/Interactive/ExprSearch.idr b/src/TTImp/Interactive/ExprSearch.idr index 9d3c2ca12..eb56fd6cb 100644 --- a/src/TTImp/Interactive/ExprSearch.idr +++ b/src/TTImp/Interactive/ExprSearch.idr @@ -35,6 +35,7 @@ import TTImp.Utils import Data.List import Libraries.Data.Tap +import Libraries.Data.WithDefault %default covering @@ -283,7 +284,7 @@ searchName fc rigc opts hints env target topty (n, ndef) = do defs <- get Ctxt checkTimer let True = visibleInAny (!getNS :: !getNestedNS) - (fullname ndef) (visibility ndef) + (fullname ndef) (collapseDefault $ visibility ndef) | _ => noResult let ty = type ndef let True = usableName (fullname ndef) @@ -365,7 +366,7 @@ searchNames fc rig opts hints env ty topty (n :: ns) visible gam nspace n = do Just def <- lookupCtxtExact n gam | Nothing => pure Nothing - if visibleInAny nspace n (visibility def) + if visibleInAny nspace n (collapseDefault $ visibility def) then pure (Just (n, def)) else pure Nothing diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 427792ce5..bb31ff5ce 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -8,6 +8,7 @@ import TTImp.TTImp import public Libraries.Text.Parser import Data.List import Data.List1 +import Libraries.Data.WithDefault topDecl : OriginDesc -> IndentInfo -> Rule ImpDecl -- All the clauses get parsed as one-clause definitions. Collect any @@ -76,10 +77,10 @@ visOption <|> do keyword "private" pure Private -visibility : EmptyRule Visibility +visibility : EmptyRule (WithDefault Visibility Private) visibility - = visOption - <|> pure Private + = (specified <$> visOption) + <|> pure defaulted totalityOpt : Rule TotalReq totalityOpt @@ -90,11 +91,11 @@ totalityOpt <|> do keyword "covering" pure CoveringOnly -dataVisOpt : EmptyRule (Visibility, Maybe TotalReq) +dataVisOpt : EmptyRule (WithDefault Visibility Private, Maybe TotalReq) dataVisOpt - = do { vis <- visOption ; mbtot <- optional totalityOpt ; pure (vis, mbtot) } + = do { vis <- visOption ; mbtot <- optional totalityOpt ; pure (specified vis, mbtot) } <|> do { tot <- totalityOpt ; vis <- visibility ; pure (vis, Just tot) } - <|> pure (Private, Nothing) + <|> pure (defaulted, Nothing) fnOpt : Rule FnOpt fnOpt = do x <- totalityOpt diff --git a/src/TTImp/PartialEval.idr b/src/TTImp/PartialEval.idr index e57e50ac4..705635ddb 100644 --- a/src/TTImp/PartialEval.idr +++ b/src/TTImp/PartialEval.idr @@ -23,6 +23,7 @@ import Protocol.Hex import Data.List import Libraries.Data.NameMap +import Libraries.Data.WithDefault %default covering @@ -281,7 +282,7 @@ mkSpecDef {vars} fc gdef pename sargs fn stk log "specialise.flags" 20 "Defining \{show pename} with flags: \{show defflags}" peidx <- addDef pename $ the (GlobalDef -> GlobalDef) { flags := defflags } - $ newDef fc pename top [] sty Public None + $ newDef fc pename top [] sty (specified Public) None addToSave (Resolved peidx) -- Reduce the function to be specialised, and reduce any name in diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index f4d11791e..8bca0bfcb 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -24,6 +24,7 @@ import TTImp.TTImp import Data.DPair import Data.List import Libraries.Data.NameMap +import Libraries.Data.WithDefault %default covering @@ -400,9 +401,9 @@ processData : {vars : _} -> {auto o : Ref ROpts REPLOpts} -> List ElabOpt -> NestedNames vars -> Env Term vars -> FC -> - Visibility -> Maybe TotalReq -> + WithDefault Visibility Private -> Maybe TotalReq -> ImpData -> Core () -processData {vars} eopts nest env fc vis mbtot (MkImpLater dfc n_in ty_raw) +processData {vars} eopts nest env fc def_vis mbtot (MkImpLater dfc n_in ty_raw) = do n <- inCurrentNS n_in ty_raw <- bindTypeNames fc [] vars ty_raw @@ -424,7 +425,7 @@ processData {vars} eopts nest env fc vis mbtot (MkImpLater dfc n_in ty_raw) arity <- getArity defs [] fullty -- Add the type constructor as a placeholder - tidx <- addDef n (newDef fc n linear vars fullty vis + tidx <- addDef n (newDef fc n linear vars fullty def_vis (TCon 0 arity [] [] defaultFlags [] [] Nothing)) addMutData (Resolved tidx) defs <- get Ctxt @@ -434,13 +435,13 @@ processData {vars} eopts nest env fc vis mbtot (MkImpLater dfc n_in ty_raw) addToSave n log "declare.data" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty)) - case vis of + case collapseDefault def_vis of Private => pure () _ => do addHashWithNames n addHashWithNames fullty log "module.hash" 15 "Adding hash for data declaration with name \{show n}" -processData {vars} eopts nest env fc vis mbtot (MkImpData dfc n_in mty_raw opts cons_raw) +processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw opts cons_raw) = do n <- inCurrentNS n_in log "declare.data" 1 $ "Processing " ++ show n @@ -462,17 +463,23 @@ processData {vars} eopts nest env fc vis mbtot (MkImpData dfc n_in mty_raw opts let metas = maybe empty fst mmetasfullty let mfullty = map snd mmetasfullty - -- If n exists, check it's the same type as we have here, and is - -- a data constructor. + -- If n exists, check it's the same type as we have here, is + -- a type constructor, and has either the same visibility or we don't define one. -- When looking up, note the data types which were undefined at the -- point of declaration. ndefm <- lookupCtxtExact n (gamma defs) (mw, vis, fullty) <- the (Core (List Name, Visibility, ClosedTerm)) $ case ndefm of Nothing => case mfullty of Nothing => throw (GenericMsg fc "Missing telescope for data definition \{show n_in}") - Just fullty => pure ([], vis, fullty) - Just ndef => - let vis = max (visibility ndef) vis in + Just fullty => pure ([], collapseDefault def_vis, fullty) + Just ndef => do + vis <- the (Core Visibility) $ case collapseDefaults ndef.visibility def_vis of + Right finalVis => pure finalVis + Left (oldVis, newVis) => do + -- TODO : In a later release, replace this with an error. + recordWarning (IncompatibleVisibility fc oldVis newVis n) + pure (max oldVis newVis) + case definition ndef of TCon _ _ _ _ _ mw [] _ => case mfullty of Nothing => pure (mw, vis, type ndef) @@ -490,7 +497,7 @@ processData {vars} eopts nest env fc vis mbtot (MkImpData dfc n_in mty_raw opts -- Add the type constructor as a placeholder while checking -- data constructors - tidx <- addDef n (newDef fc n linear vars fullty vis + tidx <- addDef n (newDef fc n linear vars fullty (specified vis) (TCon 0 arity [] [] defaultFlags [] [] Nothing)) case vis of Private => pure () diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index d775148ec..0621717ec 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -36,9 +36,10 @@ import TTImp.WithClause import Data.Either import Data.List -import Libraries.Data.NameMap import Data.String import Data.Maybe +import Libraries.Data.NameMap +import Libraries.Data.WithDefault import Libraries.Text.PrettyPrint.Prettyprinter %default covering @@ -587,7 +588,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env wname <- genWithName !(prettyName !(toFullNames (Resolved n))) widx <- addDef wname ({flags $= (SetTotal totreq ::)} (newDef vfc wname (if isErased mult then erased else top) - vars wtype vis None)) + vars wtype (specified vis) None)) let toWarg : Maybe (PiInfo RawImp, Name) -> List (Maybe Name, RawImp) := flip maybe (\pn => [(Nothing, IVar vfc (snd pn))]) $ @@ -940,12 +941,12 @@ lookupOrAddAlias eopts nest env fc n [cl@(PatClause _ lhs _)] Just (str, kept) <- getSimilarNames n | Nothing => pure [] -- only keep the ones that haven't been defined yet - decls <- for kept $ \ (cand, weight) => do + decls <- for kept $ \ (cand, vis, weight) => do Just gdef <- lookupCtxtExact cand (gamma defs) | Nothing => pure Nothing -- should be impossible let None = definition gdef | _ => pure Nothing - pure (Just (cand, weight)) + pure (Just (cand, vis, weight)) pure $ showSimilarNames (currentNS defs) n str $ catMaybes decls | (x :: xs) => throw (MaybeMisspelling (NoDeclaration fc n) (x ::: xs)) -- 3) declare an alias @@ -988,7 +989,7 @@ processDef opts nest env fc n_in cs_in -- should include the definition (RHS) of anything that is public (available -- at compile time for elaboration) _or_ inlined (dropped into destination definitions -- during compilation). - let hashit = visibility gdef == Public || (Inline `elem` gdef.flags) + let hashit = (collapseDefault $ visibility gdef) == Public || (Inline `elem` gdef.flags) let mult = if isErased (multiplicity gdef) then erased else linear @@ -999,7 +1000,7 @@ processDef opts nest env fc n_in cs_in log "declare.def" 5 $ "Traversing clauses of " ++ show n ++ " with mult " ++ show mult let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef)) cs <- withTotality treq $ - traverse (checkClause mult (visibility gdef) treq + traverse (checkClause mult (collapseDefault $ visibility gdef) treq hashit nidx opts nest env) cs_in let pats = map toPats (rights cs) @@ -1026,11 +1027,11 @@ processDef opts nest env fc n_in cs_in ({ definition := PMDef pi cargs tree_ct tree_ct pats } gdef) - when (visibility gdef == Public) $ + when (collapseDefault (visibility gdef) == Public) $ do let rmetas = getMetas tree_ct log "declare.def" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys rmetas) traverse_ addToSave (keys rmetas) - when (isUserName n && visibility gdef /= Private) $ + when (isUserName n && collapseDefault (visibility gdef) /= Private) $ do let tymetas = getMetas (type gdef) traverse_ addToSave (keys tymetas) addToSave n diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr index 462035587..5ea003705 100644 --- a/src/TTImp/ProcessRecord.idr +++ b/src/TTImp/ProcessRecord.idr @@ -18,6 +18,8 @@ import TTImp.TTImp.Traversals import TTImp.Unelab import TTImp.Utils +import Libraries.Data.WithDefault + import Data.List import Data.String @@ -43,13 +45,14 @@ elabRecord : {vars : _} -> {auto o : Ref ROpts REPLOpts} -> List ElabOpt -> FC -> Env Term vars -> NestedNames vars -> Maybe String -> - Visibility -> Maybe TotalReq -> Name -> + WithDefault Visibility Private -> + Maybe TotalReq -> Name -> (params : List (Name, RigCount, PiInfo RawImp, RawImp)) -> (opts : List DataOpt) -> (conName : Name) -> List IField -> Core () -elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params0 opts conName_in fields +elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conName_in fields = do tn <- inCurrentNS tn_in conName <- inCurrentNS conName_in params <- preElabAsData tn @@ -145,7 +148,7 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params0 opts conName_i -- we don't use MkImpLater because users may have already declared the record ahead of time let dt = MkImpData fc tn (Just dataTy) opts [] log "declare.record" 10 $ "Pre-declare record data type: \{show dt}" - processDecl [] nest env (IData fc vis mbtot dt) + processDecl [] nest env (IData fc def_vis mbtot dt) defs <- get Ctxt Just ty <- lookupTyExact tn (gamma defs) | Nothing => throw (InternalError "Missing data type \{show tn}, despite having just declared it!") @@ -221,7 +224,7 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params0 opts conName_i !(bindTypeNames fc [] boundNames conty) let dt = MkImpData fc tn Nothing opts [con] log "declare.record" 5 $ "Record data type " ++ show dt - processDecl [] nest env (IData fc vis mbtot dt) + processDecl [] nest env (IData fc def_vis mbtot dt) countExp : Term vs -> Nat countExp (Bind _ _ (Pi _ _ Explicit _) sc) = S (countExp sc) @@ -245,7 +248,7 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params0 opts conName_i Core () elabGetters tn con params done upds tyenv (Bind bfc n b@(Pi _ rc imp ty_chk) sc) = let rig = if isErased rc then erased else top - isVis = projVis vis + isVis = projVis (collapseDefault def_vis) in if (n `elem` map fst params) || (n `elem` vars) then elabGetters tn con params (if imp == Explicit && not (n `elem` vars) @@ -339,7 +342,7 @@ processRecord : {vars : _} -> {auto o : Ref ROpts REPLOpts} -> List ElabOpt -> NestedNames vars -> Env Term vars -> Maybe String -> - Visibility -> Maybe TotalReq -> + WithDefault Visibility Private -> Maybe TotalReq -> ImpRecord -> Core () -processRecord eopts nest env newns vis mbtot (MkImpRecord fc n ps opts cons fs) - = do elabRecord eopts fc env nest newns vis mbtot n ps opts cons fs +processRecord eopts nest env newns def_vis mbtot (MkImpRecord fc n ps opts cons fs) + = do elabRecord eopts fc env nest newns def_vis mbtot n ps opts cons fs diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr index 748bd3c7e..d8e002781 100644 --- a/src/TTImp/ProcessType.idr +++ b/src/TTImp/ProcessType.idr @@ -25,6 +25,7 @@ import Data.List1 import Data.String import Libraries.Data.NameMap import Libraries.Data.StringMap +import Libraries.Data.WithDefault %default covering @@ -177,7 +178,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc nameFC n_in ty_ra ({ eraseArgs := erased, safeErase := dterased, inferrable := infargs } - (newDef fc n rig vars fullty vis def)) + (newDef fc n rig vars fullty (specified vis) def)) -- Flag it as checked, because we're going to check the clauses -- from the top level. -- But, if it's a case block, it'll be checked as part of the top diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr index edf9d4ce1..618ce77c1 100644 --- a/src/TTImp/Reflect.idr +++ b/src/TTImp/Reflect.idr @@ -8,6 +8,7 @@ import Core.TT import Core.Value import TTImp.TTImp +import Libraries.Data.WithDefault %default covering diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 12a3bb171..7b7780dda 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -14,6 +14,7 @@ import Data.List1 import Data.Maybe import Libraries.Data.SortedSet +import Libraries.Data.WithDefault %default covering @@ -450,14 +451,16 @@ mutual data ImpDecl' : Type -> Type where IClaim : FC -> RigCount -> Visibility -> List (FnOpt' nm) -> ImpTy' nm -> ImpDecl' nm - IData : FC -> Visibility -> Maybe TotalReq -> ImpData' nm -> ImpDecl' nm + IData : FC -> WithDefault Visibility Private -> + Maybe TotalReq -> ImpData' nm -> ImpDecl' nm IDef : FC -> Name -> List (ImpClause' nm) -> ImpDecl' nm IParameters : FC -> List (ImpParameter' nm) -> List (ImpDecl' nm) -> ImpDecl' nm IRecord : FC -> Maybe String -> -- nested namespace - Visibility -> Maybe TotalReq -> + WithDefault Visibility Private -> + Maybe TotalReq -> ImpRecord' nm -> ImpDecl' nm IFail : FC -> Maybe String -> List (ImpDecl' nm) -> ImpDecl' nm INamespace : FC -> Namespace -> List (ImpDecl' nm) -> ImpDecl' nm diff --git a/src/TTImp/TTImp/TTC.idr b/src/TTImp/TTImp/TTC.idr index c4521b194..c66714312 100644 --- a/src/TTImp/TTImp/TTC.idr +++ b/src/TTImp/TTImp/TTC.idr @@ -8,6 +8,8 @@ import Core.Context.TTC import TTImp.TTImp +import Libraries.Data.WithDefault + %default covering mutual diff --git a/tests/idris2/error028/Issue1236.idr b/tests/idris2/error028/Issue1236.idr new file mode 100644 index 000000000..94975191c --- /dev/null +++ b/tests/idris2/error028/Issue1236.idr @@ -0,0 +1,24 @@ +module Issue1236 + +private +data Mismatched1 : Type +export +data Mismatched1 : Type where + +public export +data Mismatched2 : Type +export +data Mismatched2 : Type where + +export +data Aligned : Type +export +data Aligned : Type where + +public export +data SpecifyOnce1 : Type +data SpecifyOnce1 : Type where + +data SpecifyOnce2 : Type +public export +data SpecifyOnce2 : Type where diff --git a/tests/idris2/error028/expected b/tests/idris2/error028/expected new file mode 100644 index 000000000..afdd1d6c8 --- /dev/null +++ b/tests/idris2/error028/expected @@ -0,0 +1,13 @@ +1/1: Building Issue1236 (Issue1236.idr) +Warning: Issue1236.Mismatched1 has been forward-declared with private visibility, cannot change to export. This will be an error in a later release. + +Issue1236:5:1--6:30 + 5 | export + 6 | data Mismatched1 : Type where + +Warning: Issue1236.Mismatched2 has been forward-declared with public export visibility, cannot change to export. This will be an error in a later release. + +Issue1236:10:1--11:30 + 10 | export + 11 | data Mismatched2 : Type where + diff --git a/tests/idris2/error028/run b/tests/idris2/error028/run new file mode 100644 index 000000000..e8570a1bc --- /dev/null +++ b/tests/idris2/error028/run @@ -0,0 +1,3 @@ +rm -rf build + +$1 --no-color --console-width 0 --check Issue1236.idr diff --git a/tests/idris2/reflection/reflection004/refdecl.idr b/tests/idris2/reflection/reflection004/refdecl.idr index 742230397..61f551e07 100644 --- a/tests/idris2/reflection/reflection004/refdecl.idr +++ b/tests/idris2/reflection/reflection004/refdecl.idr @@ -21,7 +21,7 @@ mkPoint : (n : Nat) -> {auto gt : GT n 0} -> {auto lte : LTE n 4} -> Decl mkPoint n = let type = "Point" ++ show n ++ "D" in let mkMainUN = NS (MkNS ["Main"]) . UN . Basic in - IRecord emptyFC Nothing Public Nothing + IRecord emptyFC Nothing (specified Public) Nothing (MkRecord emptyFC (mkMainUN type) [] [] (mkMainUN ("Mk" ++ type)) (toList $ map (\axis => MkIField emptyFC MW ExplicitArg (UN (Field axis)) `(Double)) (axes n))) diff --git a/tests/idris2/reflection/reflection014/refdecl.idr b/tests/idris2/reflection/reflection014/refdecl.idr index 87e9a5ea8..094cd6091 100644 --- a/tests/idris2/reflection/reflection014/refdecl.idr +++ b/tests/idris2/reflection/reflection014/refdecl.idr @@ -7,7 +7,7 @@ fc = EmptyFC mkEnum : (name : String) -> (cons : List String) -> Elab () mkEnum name cons = - let enumDecl = IData EmptyFC Public Nothing dat + let enumDecl = IData EmptyFC (specified Public) Nothing dat in declare [enumDecl] where enumName : Name enumName = UN $ Basic name diff --git a/tests/idris2/reflection/reflection024/src/TypeProviders.idr b/tests/idris2/reflection/reflection024/src/TypeProviders.idr index b5acc7590..648c3cf98 100644 --- a/tests/idris2/reflection/reflection024/src/TypeProviders.idr +++ b/tests/idris2/reflection/reflection024/src/TypeProviders.idr @@ -22,7 +22,7 @@ declareRecordFromSimpleText lk textPath dataName consName = do fs <- for fs $ \line => case words line of [name, type] => pure (name, type) _ => fail "Expected two strings in line in \{!errDesc}" - let dataDecl : Decl = IRecord EmptyFC Nothing Public Nothing $ + let dataDecl : Decl = IRecord EmptyFC Nothing (specified Public) Nothing $ MkRecord EmptyFC dataName [] [] consName $ fs <&> \(name, type) => do let (ns, n) = unsnoc $ split (== '.') type