New UnquoteError CannotDeclareHiddenFunction with reproducer

Also factor out `tcDeclareDef_`.

src/full/Agda/TypeChecking/Errors.hs

@@ -363,13 +363,14 @@ interactionErrorString = \case
 
 unquoteErrorString :: UnquoteError -> String
 unquoteErrorString = \case
-  BadVisibility        {} -> "BadVisibility"
-  ConInsteadOfDef      {} -> "ConInsteadOfDef"
-  DefInsteadOfCon      {} -> "DefInsteadOfCon"
-  NonCanonical         {} -> "NonCanonical"
-  BlockedOnMeta        {} -> "BlockedOnMeta"
-  PatLamWithoutClauses {} -> "PatLamWithoutClauses"
-  UnquotePanic         {} -> "UnquotePanic"
+  BadVisibility               {} -> "BadVisibility"
+  CannotDeclareHiddenFunction {} -> "CannotDeclareHiddenFunction"
+  ConInsteadOfDef             {} -> "ConInsteadOfDef"
+  DefInsteadOfCon             {} -> "DefInsteadOfCon"
+  NonCanonical                {} -> "NonCanonical"
+  BlockedOnMeta               {} -> "BlockedOnMeta"
+  PatLamWithoutClauses        {} -> "PatLamWithoutClauses"
+  UnquotePanic                {} -> "UnquotePanic"
 
 
 instance PrettyTCM TCErr where
@@ -1813,6 +1814,9 @@ instance PrettyTCM UnquoteError where
     BadVisibility msg arg -> fsep $
       pwords $ "Unable to unquote the argument. It should be `" ++ msg ++ "'."
 
+    CannotDeclareHiddenFunction f -> fsep $
+      pwords "Cannot declare hidden function" ++ [ prettyTCM f ]
+
     ConInsteadOfDef x def con -> fsep $
       pwords ("Use " ++ con ++ " instead of " ++ def ++ " for constructor") ++
       [prettyTCM x]

src/full/Agda/TypeChecking/Monad/Base.hs

@@ -4663,6 +4663,8 @@ data UnificationFailure
 
 data UnquoteError
   = BadVisibility String (Arg I.Term)
+  | CannotDeclareHiddenFunction QName
+      -- ^ Attempt to @unquoteDecl@ with 'Hiding' other than 'NotHidden'.
   | ConInsteadOfDef QName String String
   | DefInsteadOfCon QName String String
   | NonCanonical String I.Term
@@ -5795,6 +5797,9 @@ typeError_ = withCallerCallStack . flip typeError'_
 interactionError :: (HasCallStack, MonadTCError m) => InteractionError -> m a
 interactionError = locatedTypeError InteractionError
 
+unquoteError :: (HasCallStack, MonadTCError m) => UnquoteError -> m a
+unquoteError = locatedTypeError UnquoteFailed
+
 -- | Running the type checking monad (most general form).
 {-# SPECIALIZE runTCM :: TCEnv -> TCState -> TCM a -> IO (a, TCState) #-}
 runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState)

src/full/Agda/TypeChecking/Unquote.hs

@@ -948,44 +948,32 @@ evalTCM v = Bench.billTo [Bench.Typing, Bench.Reflection] do
     setDirty :: UnquoteM ()
     setDirty = modify (first $ const Dirty)
 
-    tcDeclareDef :: Arg QName -> R.Type -> UnquoteM Term
-    tcDeclareDef (Arg i x) a = inOriginalContext $ do
+    tcDeclareDef_ :: Arg QName -> R.Type -> String -> Defn -> UnquoteM Term
+    tcDeclareDef_ (Arg i x) a doc defn = inOriginalContext $ do
       setDirty
-      when (hidden i) $ liftTCM $ typeError . GenericDocError =<<
-        "Cannot declare hidden function" <+> prettyTCM x
+      when (hidden i) $ liftTCM $ unquoteError $ CannotDeclareHiddenFunction x
       tell [x]
       liftTCM $ do
         alwaysReportSDoc "tc.unquote.decl" 10 $ sep
-          [ "declare" <+> prettyTCM x <+> ":"
+          [ "declare" <+> text doc <+> prettyTCM x <+> ":"
           , nest 2 $ prettyR a
           ]
         a <- locallyReduceAllDefs $ isType_ =<< toAbstract_ a
         alreadyDefined <- isRight <$> getConstInfo' x
         when alreadyDefined $ genericError $ "Multiple declarations of " ++ prettyShow x
-        addConstant' x i x a =<< emptyFunction
+        addConstant' x i x a defn
         when (isInstance i) $ addTypedInstance x a
         primUnitUnit
 
+    tcDeclareDef :: Arg QName -> R.Type -> UnquoteM Term
+    tcDeclareDef arg a = tcDeclareDef_ arg a "" =<< emptyFunction
+
     tcDeclarePostulate :: Arg QName -> R.Type -> UnquoteM Term
-    tcDeclarePostulate (Arg i x) a = inOriginalContext $ do
+    tcDeclarePostulate arg@(Arg i x) a = do
       clo <- commandLineOptions
       when (Lens.getSafeMode clo) $ liftTCM $ typeError . GenericDocError =<<
         "Cannot postulate '" <+> prettyTCM x <+> ":" <+> prettyR a <+> "' with safe flag"
-      setDirty
-      when (hidden i) $ liftTCM $ typeError . GenericDocError =<<
-        "Cannot declare hidden function" <+> prettyTCM x
-      tell [x]
-      liftTCM $ do
-        alwaysReportSDoc "tc.unquote.decl" 10 $ sep
-          [ "declare Postulate" <+> prettyTCM x <+> ":"
-          , nest 2 $ prettyR a
-          ]
-        a <- locallyReduceAllDefs $ isType_ =<< toAbstract_ a
-        alreadyDefined <- isRight <$> getConstInfo' x
-        when alreadyDefined $ genericError $ "Multiple declarations of " ++ prettyShow x
-        addConstant' x i x a defaultAxiom
-        when (isInstance i) $ addTypedInstance x a
-        primUnitUnit
+      tcDeclareDef_ arg a "Postulate" defaultAxiom
 
     -- A datatype is expected to be declared with a function type.
     -- The second argument indicates how many preceding types are parameters.

test/Fail/UnquoteCannotDeclareHiddenFunction.agda

@@ -0,0 +1,8 @@
+
+open import Common.Prelude
+open import Common.Reflection
+
+pattern `Nat = def (quote Nat) []
+
+unquoteDecl x =
+  define (hArg x) (funDef `Nat (clause [] [] (quoteTerm 15) ∷ []))

test/Fail/UnquoteCannotDeclareHiddenFunction.err

@@ -0,0 +1,2 @@
+UnquoteCannotDeclareHiddenFunction.agda:7,1-8,67: error: [Unquote.CannotDeclareHiddenFunction]
+Cannot declare hidden function x