Add visibility rules on types

Can't export a type which refers to a private name. This has caught a
couple of visibility errors in the libraries, code and tests, so they've
been updated too.

docs/source/typedd/typedd.rst

@@ -312,6 +312,9 @@ In ``ArithCmd.idr``, update ``DivBy`` and ``import Data.Strings`` as above. Also
 since export rules are per-namespace now, rather than per-file, you need to
 export ``(>>=)`` from the namespaces ``CommandDo`` and ``ConsoleDo``.
 
+In ``ArithCmdDo.idr``, since ``(>>=)`` is ``export``, ``Command`` and ``ConsoleIO``
+also have to be ``export``.
+
 In ``StreamFail.idr``, add a ``partial`` annotation to ``labelWith``.
 
 Chapter 12
@@ -322,6 +325,9 @@ Also the ``(>>=)`` operators need to be set as ``export`` since they are in thei
 own namespaces, and in ``getRandom``, ``DivBy`` needs to take additional
 arguments ``div`` and ``rem``.
 
+In ``ArithState.idr``, since ``(>>=)`` is ``export``, ``Command`` and ``ConsoleIO``
+also have to be ``export``.
+
 Chapter 13
 ----------
 

libs/base/Control/App.idr

@@ -58,11 +58,9 @@ data App1Res : Usage -> Type -> Type where
 PrimApp : Type -> Type
 PrimApp a = (1 x : %World) -> AppRes a
 
-export
 prim_app_pure : a -> PrimApp a
 prim_app_pure x = \w => MkAppRes x w
 
-export
 prim_app_bind : (1 act : PrimApp a) -> (1 k : a -> PrimApp b) -> PrimApp b
 prim_app_bind fn k w
     = let MkAppRes x' w' = fn w in k x' w'

libs/base/System/Clock.idr

@@ -69,6 +69,7 @@ data OSClock : Type where [external]
 
 ||| Note: Back-ends are required to implement UTC, monotonic time, CPU time
 ||| in current process/thread, and time duration; the rest are optional.
+export
 data ClockTypeMandatory
   = Mandatory
   | Optional

libs/contrib/System/Path.idr

@@ -146,7 +146,6 @@ pathTokenMap = toTokenMap $
   , (some $ non $ oneOf "/\\:?", PTText)
   ]
 
-export
 lexPath : String -> List PathToken
 lexPath str = let (tokens, _, _, _) = lex pathTokenMap str in 
                 map TokenData.tok tokens

libs/contrib/Text/Lexer/Core.idr

@@ -101,7 +101,6 @@ strIndex (MkStrLen str len) i
 mkStr : String -> StrLen
 mkStr str = MkStrLen str (length str)
 
-export
 strTail : Nat -> StrLen -> StrLen
 strTail start (MkStrLen str len)
     = MkStrLen (substr start len str) (minus len start)

src/Algebra/ZeroOneOmega.idr

@@ -8,6 +8,7 @@ import Algebra.Preorder
 export
 data ZeroOneOmega = Rig0 | Rig1 | RigW
 
+export
 Preorder ZeroOneOmega where
   Rig0 <= _ = True
   Rig1 <= Rig1 = True

src/Idris/Error.idr

@@ -195,8 +195,8 @@ perror (SolvedNamedHole _ env h tm)
     = pure $ "Named hole " ++ show h ++ " has been solved by unification\n"
               ++ "Result: " ++ !(pshow env tm)
 perror (VisibilityError fc vx x vy y)
-    = pure $ show vx ++ " " ++ sugarName x ++
-             " cannot refer to " ++ show vy ++ " " ++ sugarName y
+    = pure $ show vx ++ " " ++ sugarName !(toFullNames x) ++
+             " cannot refer to " ++ show vy ++ " " ++ sugarName !(toFullNames y)
 perror (NonLinearPattern _ n) = pure $ "Non linear pattern " ++ sugarName n
 perror (BadPattern _ n) = pure $ "Pattern not allowed here: " ++ show n
 perror (NoDeclaration _ n) = pure $ "No type declaration for " ++ show n

src/TTImp/Elab/Case.idr

@@ -208,7 +208,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
          -- the alternative of fixing up the environment
          when (not (isNil fullImps)) $ findImpsIn fc [] [] casefnty
          cidx <- addDef casen (newDef fc casen (if isErased rigc then erased else top)
-                                      [] casefnty Private None)
+                                      [] casefnty Public None)
          -- don't worry about totality of the case block; it'll be handled
          -- by the totality of the parent function
          setFlag fc (Resolved cidx) (SetTotal PartialOK)

src/TTImp/ProcessData.idr

@@ -14,6 +14,7 @@ import TTImp.Elab.Check
 import TTImp.Elab.Utils
 import TTImp.Elab
 import TTImp.TTImp
+import TTImp.Utils
 
 import Data.List
 import Data.NameMap
@@ -110,6 +111,12 @@ checkCon {vars} opts nest env vis tn_in tn (MkImpTy fc cn_in ty_raw)
               Public => do addHashWithNames cn
                            addHashWithNames fullty
               _ => pure ()
+
+         -- Check name visibility: unless it's a private name, any names in
+         -- the type must be greater than private
+         when (vis /= Private) $
+              traverse_ (checkRefVisibility fc cn vis Private)
+                        (keys (getRefs (UN "") fullty))
          pure (MkCon fc cn !(getArity defs [] fullty) fullty)
 
 conName : Constructor -> Name
@@ -280,6 +287,12 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
               Private => pure ()
               _ => do addHashWithNames n
                       addHashWithNames fullty
+
+         -- Check name visibility: unless it's a private name, any names in
+         -- the type must be greater than private
+         when (vis /= Private) $
+              traverse_ (checkRefVisibility fc n vis Private)
+                        (keys (getRefs (UN "") fullty))
          pure ()
 
 processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)

src/TTImp/ProcessRecord.idr

@@ -24,6 +24,11 @@ mkDataTy fc [] = IType fc
 mkDataTy fc ((n, c, p, ty) :: ps)
     = IPi fc c p (Just n) ty (mkDataTy fc ps)
 
+-- Projections are only visible if the record is public export
+projVis : Visibility -> Visibility
+projVis Public = Public
+projVis _ = Private
+
 elabRecord : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
@@ -148,7 +153,7 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
                    processDecl [] nest env
                        (IClaim fc (if isErased rc
                                       then erased
-                                      else top) vis [Inline] (MkImpTy fc projNameNS projTy))
+                                      else top) (projVis vis) [Inline] (MkImpTy fc projNameNS projTy))
 
                    -- Define the LHS and RHS
                    let lhs_exp

src/TTImp/ProcessType.idr

@@ -15,6 +15,7 @@ import TTImp.Elab.Check
 import TTImp.Elab.Utils
 import TTImp.Elab
 import TTImp.TTImp
+import TTImp.Utils
 
 import Data.List
 import Data.NameMap
@@ -271,10 +272,15 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
                              (IBindHere fc (PI erased) ty_raw)
                              (gType fc)
          logTermNF 3 ("Type of " ++ show n) [] (abstractFullEnvType tfc env ty)
-         -- TODO: Check name visibility
 
          def <- initDef n env ty opts
          let fullty = abstractFullEnvType tfc env ty
+         -- Check name visibility: unless it's a private name, any names in
+         -- the type must be greater than private
+         when (vis /= Private) $
+              traverse_ (checkRefVisibility fc n vis Private)
+                        (keys (getRefs (UN "") fullty))
+
          (erased, dterased) <- findErased fullty
          defs <- get Ctxt
          empty <- clearDefs defs
@@ -298,7 +304,6 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
          addTyDecl fc (Resolved idx) env ty -- for definition generation
          addNameType fc (Resolved idx) env ty -- for looking up types
 
-
          traverse_ addToSave (keys (getMetas ty))
          addToSave n
          log 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))

src/TTImp/Utils.idr

@@ -286,3 +286,16 @@ uniqueName defs used n
     next str
         = let (n, i) = nameNum str in
               n ++ "_" ++ show (i + 1)
+
+export
+checkRefVisibility : {auto c : Ref Ctxt Defs} ->
+                     FC -> Name ->
+                     Visibility -> -- Visibility of the name
+                     Visibility -> -- Minimum visibility of references
+                     Name -> Core ()
+checkRefVisibility fc fn vis min ref
+    = do defs <- get Ctxt
+         Just gdef <- lookupCtxtExact ref (gamma defs)
+              | Nothing => pure ()
+         when (visibility gdef <= min) $
+              throw (VisibilityError fc vis fn (visibility gdef) ref)

src/Utils/Path.idr

@@ -146,7 +146,6 @@ pathTokenMap = toTokenMap $
   , (some $ non $ oneOf "/\\:?", PTText)
   ]
 
-export
 lexPath : String -> List PathToken
 lexPath str = let (tokens, _, _, _) = lex pathTokenMap str in 
                 map TokenData.tok tokens

tests/idris2/basic003/Ambig2.idr

@@ -1,9 +1,13 @@
 infixr 5 ::
 
+export
 data List a = Nil | (::) a (List a)
+export
 data Nat = Z | S Nat
 
+export
 data Vect : Type -> Type where
+export
 data Set : Type -> Type where
 
 namespace Vect

tests/idris2/basic003/expected

@@ -1,7 +1,7 @@
 1/1: Building Ambig1 (Ambig1.idr)
 Main> Bye for now!
 1/1: Building Ambig2 (Ambig2.idr)
-Ambig2.idr:22:21--22:28:While processing right hand side of keepUnique at Ambig2.idr:22:1--24:1:
+Ambig2.idr:26:21--26:28:While processing right hand side of keepUnique at Ambig2.idr:26:1--28:1:
 Ambiguous elaboration. Possible correct results:
 	Main.Set.toList ?arg
 	Main.Vect.toList ?arg

tests/idris2/perf004/bigdpair.idr

@@ -11,6 +11,7 @@ bigEx (S k) = ((2 ** [0,0]), bigEx k)
 data VWrap : Type -> Type where
      MkVWrap : (0 n : Nat) -> Vect n a -> VWrap a
 
+export
 MkBig' : Nat -> Type
 MkBig' Z = Int
 MkBig' (S k) = (VWrap Int, MkBig' k)

tests/idris2/real002/Control/App.idr

@@ -81,11 +81,9 @@ data App1Res : Usage -> Type -> Type where
 PrimApp : Type -> Type
 PrimApp a = (1 x : %World) -> AppRes a
 
-export
 prim_app_pure : a -> PrimApp a
 prim_app_pure x = \w => MkAppRes x w
 
-export
 prim_app_bind : (1 act : PrimApp a) -> (1 k : a -> PrimApp b) -> PrimApp b
 prim_app_bind fn k w
     = let MkAppRes x' w' = fn w in k x' w'

tests/idris2/reg008/Vending.idr

@@ -16,6 +16,7 @@ strToInput x = if all isDigit (unpack x)
                   then Just (REFILL (stringToNatOrZ x))
                   else Nothing
 
+export
 data MachineCmd : Type ->
                   VendState -> VendState ->
                   Type where
@@ -35,6 +36,7 @@ data MachineCmd : Type ->
           (a -> MachineCmd b state2 state3) ->
           MachineCmd b state1 state3
 
+export
 data MachineIO : VendState -> Type where
   Do : {state1 : _} ->
        MachineCmd a state1 state2 ->

tests/ttimp/basic005/Ambig.yaff

@@ -1,3 +1,4 @@
+public export
 data Nat : Type where
      Z : Nat
      S : Nat -> Nat

tests/ttimp/basic006/Ambig.yaff

@@ -1,3 +1,4 @@
+public export
 data Nat : Type where
      Z : Nat
      S : Nat -> Nat

tests/typedd-book/chapter11/ArithCmdDo.idr

@@ -4,6 +4,7 @@ import System
 
 -- %default total
 
+export
 data Command : Type -> Type where
      PutStr : String -> Command ()
      GetLine : Command String
@@ -11,6 +12,7 @@ data Command : Type -> Type where
      Pure : ty -> Command ty
      Bind : Command a -> (a -> Command b) -> Command b
 
+export
 data ConsoleIO : Type -> Type where
      Quit : a -> ConsoleIO a
      Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

tests/typedd-book/chapter12/ArithState.idr

@@ -32,6 +32,7 @@ addCorrect = record { score.correct $= (+1),
 setDifficulty : Int -> GameState -> GameState
 setDifficulty newDiff state = record { difficulty = newDiff } state
 
+export
 data Command : Type -> Type where
      PutStr : String -> Command ()
      GetLine : Command String
@@ -43,6 +44,7 @@ data Command : Type -> Type where
      Pure : ty -> Command ty
      Bind : Command a -> (a -> Command b) -> Command b
 
+export
 data ConsoleIO : Type -> Type where
      Quit : a -> ConsoleIO a
      Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

tests/typedd-book/chapter13/StackIO.idr

@@ -1,5 +1,6 @@
 import Data.Vect
 
+export
 data StackCmd : Type -> Nat -> Nat -> Type where
   Push : Integer -> StackCmd ()      height     (S height)
   Pop :             StackCmd Integer (S height) height
@@ -35,6 +36,7 @@ testAdd = do Push 10
              val2 <- Pop
              PutStr (show (val1 + val2) ++ "\n")
 
+export
 data StackIO : Nat -> Type where
   Do : StackCmd a height1 height2 ->
        (a -> Inf (StackIO height2)) -> StackIO height1

tests/typedd-book/chapter13/Vending.idr

@@ -16,6 +16,7 @@ strToInput x = if all isDigit (unpack x)
                   then Just (REFILL (stringToNatOrZ x))
                   else Nothing
 
+export
 data MachineCmd : Type ->
                   VendState -> VendState ->
                   Type where
@@ -35,6 +36,7 @@ data MachineCmd : Type ->
           (a -> MachineCmd b state2 state3) ->
           MachineCmd b state1 state3
 
+export
 data MachineIO : VendState -> Type where
   Do : {state1 : _} ->
        MachineCmd a state1 state2 ->

tests/typedd-book/chapter14/Hangman.idr

@@ -6,6 +6,7 @@ import Decidable.Equality
 
 %default total
 
+public export
 data GameState : Type where
   NotRunning : GameState
   Running : (guesses : Nat) -> (letters : Nat) -> GameState
@@ -15,6 +16,7 @@ letters str = nub (map toUpper (unpack str))
 
 data GuessResult = Correct | Incorrect
 
+export
 data GameCmd : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
   NewGame : (word : String) ->
             GameCmd () NotRunning (const (Running 6 (length (letters word))))