Remove name visibility check

It doesn't seem to serve any useful purpose, other than to annoy!

Author: edwinb

src/TTImp/ProcessData.idr

@@ -111,12 +111,6 @@ 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
@@ -288,13 +282,6 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
               _ => 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)
     = do n <- inCurrentNS n_in
          ty_raw <- bindTypeNames [] vars ty_raw

src/TTImp/ProcessType.idr

@@ -275,11 +275,6 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
 
          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

src/TTImp/Utils.idr

@@ -350,16 +350,3 @@ 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)