Check names are visible/public

src/TTImp/Elab/App.idr

@@ -38,9 +38,10 @@ getNameType rigc env fc x
                  pure (Local fc (Just (isLet binder)) _ lv, gnf env bty)
            Nothing => 
               do defs <- get Ctxt
-                 [(fullname, i, def)] <- lookupCtxtName x (gamma defs)
+                 [(pname, i, def)] <- lookupCtxtName x (gamma defs)
                       | [] => throw (UndefinedName fc x)
                       | ns => throw (AmbiguousName fc (map fst ns))
+                 checkVisibleNS !(getFullName pname)
                  let nt = case definition def of
                                PMDef _ _ _ _ => Func
                                DCon t a => DataCon t a
@@ -59,6 +60,15 @@ getNameType rigc env fc x
     rigSafe Rig0 Rig1 = throw (LinearMisuse fc x Rig0 Rig1)
     rigSafe _ _ = pure ()
 
+    checkVisibleNS : Name -> Core ()
+    checkVisibleNS (NS ns x) 
+        = if !(isVisible ns)
+             then pure ()
+             else do defs <- get Ctxt
+                     throw $ InvisibleName fc (NS ns x)
+    checkVisibleNS _ = pure ()
+          
+
 -- Get the type of a variable, looking it up in the nested names first.
 getVarType : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->

src/TTImp/ProcessDef.idr

@@ -202,7 +202,7 @@ checkLHS {vars} mult hashit n opts nest env fc lhs_in
          log 5 $ "Checking " ++ show lhs
          logEnv 5 "In env" env
          (lhstm, lhstyg) <- 
-             wrapError (InLHS fc (Resolved n)) $
+             wrapError (InLHS fc !(getFullName (Resolved n))) $
                      elabTerm n (InLHS mult) opts nest env 
                                 (IBindHere fc PATTERN lhs) Nothing
          logTerm 10 "Checked LHS term" lhstm
@@ -344,7 +344,7 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
                       Rig0 => InType -- treat as used in type only
                       _ => InExpr
 
-         (wval, gwvalTy) <- wrapError (InRHS fc (Resolved n)) $
+         (wval, gwvalTy) <- wrapError (InRHS fc !(getFullName (Resolved n))) $
                 elabTermSub n wmode opts nest' env' env sub' wval_raw Nothing
          clearHoleLHS
          
@@ -397,7 +397,7 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
          let rhs_in = apply (IVar fc wname)
                         (map (maybe wval_raw (IVar fc)) wargNames)
 
-         rhs <- wrapError (InRHS fc (Resolved n)) $
+         rhs <- wrapError (InRHS fc !(getFullName (Resolved n))) $
              checkTermSub n wmode opts nest' env' env sub' rhs_in 
                           (gnf env' reqty)
 

src/TTImp/ProcessType.idr

@@ -65,7 +65,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
          idx <- resolveName n 
          
          (ty, _) <- 
-             wrapError (InType fc (Resolved idx)) $
+             wrapError (InType fc n) $
                     elabTerm idx InType (HolesOkay :: eopts) nest env 
                              (IBindHere fc (PI Rig0) ty_raw) 
                              (Just (gType fc))

tests/Main.idr

@@ -25,7 +25,7 @@ idrisTests : List String
 idrisTests
     = ["basic001",
        "coverage001", "coverage002",
-       "import001"]
+       "import001", "import002"]
 
 chdir : String -> IO Bool
 chdir dir 

tests/idris2/import002/Mult.idr

@@ -0,0 +1,8 @@
+module Mult
+
+import Nat
+
+public export
+mult : Nat -> Nat -> Nat
+mult Z y = Z
+mult (S k) y = plus y (mult k y)

tests/idris2/import002/Nat.idr

@@ -0,0 +1,10 @@
+module Nat
+
+public export
+data Nat = Z | S Nat
+
+public export
+plus : Nat -> Nat -> Nat
+plus Z y = y
+plus (S k) y = S (plus k y)
+

tests/idris2/import002/Test.idr

@@ -0,0 +1,7 @@
+module Test
+
+import Mult
+
+thing : Nat -> Nat
+thing x = mult x (plus x x)
+

tests/idris2/import002/expected

@@ -0,0 +1,8 @@
+1/3: Building Nat (Nat.idr)
+2/3: Building Mult (Mult.idr)
+3/3: Building Test (Test.idr)
+Test.idr:5:9--5:13:While processing type of Test.thing at Test.idr:5:1--6:1:
+Name Nat is inaccessible since Nat is not explicitly imported
+Test.idr:6:1--8:1:No type declaration for Test.thing
+Welcome to Idris 2 version 0.0. Please be gentle.
+Test> Bye for now!

tests/idris2/import002/run

@@ -0,0 +1,3 @@
+echo ':q' | $1 --no-prelude Test.idr
+
+rm -rf build

tests/ttimp/dot001/expected

@@ -2,14 +2,14 @@ Processing as TTImp
 Written TTC
 Yaffle> Bye for now!
 Processing as TTImp
-Dot2.yaff:15:1--16:1:When elaborating left hand side of $resolved79:
+Dot2.yaff:15:1--16:1:When elaborating left hand side of Main.half:
 Dot2.yaff:15:10--15:15:Can't match on ($resolved73 ?{P:n:79}_[] ?{P:m:79}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:n:79}_[] ?{P:n:79}_[])
 Yaffle> Bye for now!
 Processing as TTImp
-Dot3.yaff:18:1--20:1:When elaborating left hand side of $resolved82:
+Dot3.yaff:18:1--20:1:When elaborating left hand side of Main.addBaz3:
 Dot3.yaff:18:10--18:15:Can't match on ($resolved73 ?{P:x:82}_[] ?{P:y:82}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?Main.{_:8}_[] ?Main.{_:9}_[])
 Yaffle> Bye for now!
 Processing as TTImp
-Dot4.yaff:17:1--19:1:When elaborating left hand side of $resolved82:
+Dot4.yaff:17:1--19:1:When elaborating left hand side of Main.addBaz4:
 Dot4.yaff:17:10--17:15:Can't match on ($resolved73 ?Main.{_:7}_[] ?Main.{_:8}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved73 ?{P:x:82}_[] ?{P:y:82}_[])
 Yaffle> Bye for now!

tests/ttimp/qtt003/expected

@@ -1,4 +1,4 @@
 Processing as TTImp
-QTTEq.yaff:8:1--9:1:When elaborating left hand side of $resolved78:
+QTTEq.yaff:8:1--9:1:When elaborating left hand side of Main.okay:
 QTTEq.yaff:8:9--8:12:There are 2 uses of linear name x
 Yaffle> Yaffle> Yaffle> Yaffle> Yaffle> Bye for now!