    module Agda.TypeChecking.Unquote where

    import Prelude hiding (null)

    import Control.Arrow          ( first, second, (&&&) )
    import Control.Monad          ( (<=<) )
    import Control.Monad.Except   ( MonadError(..), ExceptT(..), runExceptT )
    import Control.Monad.IO.Class ( MonadIO(..) )
    import Control.Monad.Reader   ( ReaderT(..), runReaderT )
    import Control.Monad.State    ( gets, modify, StateT(..), runStateT )
    import Control.Monad.Writer   ( MonadWriter(..), WriterT(..), runWriterT )
    import Control.Monad.Trans    ( lift )

    import Data.Char
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Maybe (fromMaybe, mapMaybe)
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Text (Text)
    import qualified Data.Text as T
    import Data.Word

    import System.Directory (doesFileExist, getPermissions, executable)
    import System.Process.Text ( readProcessWithExitCode )
    import System.Exit ( ExitCode(..) )

    import Agda.Syntax.Common hiding ( Nat )
    import Agda.Syntax.Common.Pretty (prettyShow)
    import Agda.Syntax.Internal as I
    import qualified Agda.Syntax.Reflected as R
    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Abstract (TypedBindingInfo(tbTacticAttr))
    import Agda.Syntax.Abstract.Views
    import Agda.Syntax.Translation.InternalToAbstract
    import Agda.Syntax.Translation.ConcreteToAbstract
    import Agda.Syntax.Literal
    import qualified Agda.Syntax.Concrete as C
    import Agda.Syntax.Concrete.Name (simpleName)
    import Agda.Syntax.Position
    import Agda.Syntax.Info as Info
    import Agda.Syntax.Translation.ReflectedToAbstract
    import Agda.Syntax.Scope.Base (KindOfName(ConName, DataName)
                                  , scopeLocals, LocalVar(LocalVar), BindingSource(MacroBound) )
    import Agda.Syntax.Parser

    import Agda.Interaction.Library ( ExeName )
    import Agda.Interaction.Options ( optTrustedExecutables, optAllowExec )

    import qualified Agda.TypeChecking.Monad.Benchmark as Bench
    import Agda.TypeChecking.Constraints
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Quote
    import Agda.TypeChecking.Conversion
    import Agda.TypeChecking.EtaContract
    import Agda.TypeChecking.Primitive
    import Agda.TypeChecking.ReconstructParameters
    import Agda.TypeChecking.CheckInternal
    import Agda.TypeChecking.InstanceArguments
    import Agda.TypeChecking.Warnings

    import {-# SOURCE #-} Agda.TypeChecking.Rules.Term
    import {-# SOURCE #-} Agda.TypeChecking.Rules.Def
    import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl
    import Agda.TypeChecking.Rules.Data

    import Agda.Utils.CallStack           ( HasCallStack )
    import Agda.Utils.Either
    import Agda.Utils.Lens
    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import qualified Agda.Interaction.Options.Lenses as Lens

    import Agda.Utils.Impossible

    agdaTermType :: TCM Type
    agdaTermType :: TCM Type
    agdaTermType = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Integer -> Sort' Term
    mkType Integer
    0) (Term -> Type) -> TCMT IO Term -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTerm

    agdaTypeType :: TCM Type
    agdaTypeType :: TCM Type
    agdaTypeType = TCM Type
    agdaTermType

    qNameType :: TCM Type
    qNameType :: TCM Type
    qNameType = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Integer -> Sort' Term
    mkType Integer
    0) (Term -> Type) -> TCMT IO Term -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primQName

    data Dirty = Dirty | Clean
      deriving (Dirty -> Dirty -> Bool
    (Dirty -> Dirty -> Bool) -> (Dirty -> Dirty -> Bool) -> Eq Dirty
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Dirty -> Dirty -> Bool
    == :: Dirty -> Dirty -> Bool
    $c/= :: Dirty -> Dirty -> Bool
    /= :: Dirty -> Dirty -> Bool
    Eq)

    -- Keep track of the original context. We need to use that when adding new
    -- definitions. Also state snapshot from last commit and whether the state is
    -- dirty (definitions have been added).
    type UnquoteState = (Dirty, TCState)
    type UnquoteM = ReaderT Context (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))

    type UnquoteRes a = Either UnquoteError ((a, UnquoteState), [QName])

    unpackUnquoteM :: UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
    unpackUnquoteM :: forall a.
    UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
    unpackUnquoteM UnquoteM a
    m Context
    cxt UnquoteState
    s = ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
    -> TCMT IO (Either UnquoteError ((a, UnquoteState), [QName]))
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
     -> TCMT IO (Either UnquoteError ((a, UnquoteState), [QName])))
    -> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
    -> TCMT IO (Either UnquoteError ((a, UnquoteState), [QName]))
    forall a b. (a -> b) -> a -> b
    $ WriterT [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState)
    -> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT (WriterT [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState)
     -> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName]))
    -> WriterT
         [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState)
    -> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
    forall a b. (a -> b) -> a -> b
    $ StateT
      UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a
    -> UnquoteState
    -> WriterT
         [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (UnquoteM a
    -> Context
    -> StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT UnquoteM a
    m Context
    cxt) UnquoteState
    s

    packUnquoteM :: (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
    packUnquoteM :: forall a.
    (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
    packUnquoteM Context -> UnquoteState -> TCM (UnquoteRes a)
    f = (Context
     -> StateT
          UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
    ReaderT ((Context
      -> StateT
           UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a)
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          a)
    -> (Context
        -> StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall a b. (a -> b) -> a -> b
    $ \ Context
    cxt -> (UnquoteState
     -> WriterT
          [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState))
    -> StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StateT ((UnquoteState
      -> WriterT
           [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState))
     -> StateT
          UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a)
    -> (UnquoteState
        -> WriterT
             [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState))
    -> StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a
    forall a b. (a -> b) -> a -> b
    $ \ UnquoteState
    s -> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
    -> WriterT
         [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState)
    forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
    WriterT (ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
     -> WriterT
          [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState))
    -> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
    -> WriterT
         [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState)
    forall a b. (a -> b) -> a -> b
    $ TCM (UnquoteRes a)
    -> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
    forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
    ExceptT (TCM (UnquoteRes a)
     -> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName]))
    -> TCM (UnquoteRes a)
    -> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
    forall a b. (a -> b) -> a -> b
    $ Context -> UnquoteState -> TCM (UnquoteRes a)
    f Context
    cxt UnquoteState
    s

    runUnquoteM :: UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
    runUnquoteM :: forall a. UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
    runUnquoteM UnquoteM a
    m = do
      cxt <- TCMT IO Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
      s   <- getTC
      pid <- fresh  -- Create a fresh problem for the unquote call. Used in tcSolveInstances.
      z   <- localTC (\ TCEnv
    e -> TCEnv
    e { envUnquoteProblem = Just pid })
           $ solvingProblem pid
           $ unpackUnquoteM m cxt (Clean, s)
      case z of
        Left UnquoteError
    err              -> Either UnquoteError (a, [QName])
    -> TCMT IO (Either UnquoteError (a, [QName]))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either UnquoteError (a, [QName])
     -> TCMT IO (Either UnquoteError (a, [QName])))
    -> Either UnquoteError (a, [QName])
    -> TCMT IO (Either UnquoteError (a, [QName]))
    forall a b. (a -> b) -> a -> b
    $ UnquoteError -> Either UnquoteError (a, [QName])
    forall a b. a -> Either a b
    Left UnquoteError
    err
        Right ((a
    v, UnquoteState
    _), [QName]
    decls) -> (a, [QName]) -> Either UnquoteError (a, [QName])
    forall a b. b -> Either a b
    Right (a
    v, [QName]
    decls) Either UnquoteError (a, [QName])
    -> TCMT IO () -> TCMT IO (Either UnquoteError (a, [QName]))
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ (QName -> TCMT IO ()) -> [QName] -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ QName -> TCMT IO ()
    forall {m :: * -> *}.
    (HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
    QName -> m ()
    isDefined [QName]
    decls
      where
        isDefined :: QName -> m ()
    isDefined QName
    x = do
          QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x m Definition -> (Definition -> Defn) -> m Defn
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> Definition -> Defn
    theDef m Defn -> (Defn -> m ()) -> m ()
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            FunctionDefn FunctionData{ _funClauses :: FunctionData -> [Clause]
    _funClauses = [Clause]
    cl } -> Bool -> m () -> m ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when ([Clause] -> Bool
    forall a. Null a => a -> Bool
    null [Clause]
    cl) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
              UnquoteError -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    UnquoteError -> m a
    unquoteError (UnquoteError -> m ()) -> UnquoteError -> m ()
    forall a b. (a -> b) -> a -> b
    $ QName -> UnquoteError
    MissingDefinition QName
    x
            -- Andreas, 2024-10-11:
            -- some of the following cases might be __IMPOSSIBLE__
            AxiomDefn         {} -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            DataOrRecSigDefn  {} -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            GeneralizableVar  {} -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            AbstractDefn      {} -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            DatatypeDefn      {} -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            RecordDefn        {} -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            ConstructorDefn   {} -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            PrimitiveDefn     {} -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            PrimitiveSortDefn {} -> () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    liftU1 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b)) -> UnquoteM a -> UnquoteM b
    liftU1 :: forall a b.
    (TCM (UnquoteRes a) -> TCM (UnquoteRes b))
    -> UnquoteM a -> UnquoteM b
    liftU1 TCM (UnquoteRes a) -> TCM (UnquoteRes b)
    f UnquoteM a
    m = (Context -> UnquoteState -> TCM (UnquoteRes b)) -> UnquoteM b
    forall a.
    (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
    packUnquoteM ((Context -> UnquoteState -> TCM (UnquoteRes b)) -> UnquoteM b)
    -> (Context -> UnquoteState -> TCM (UnquoteRes b)) -> UnquoteM b
    forall a b. (a -> b) -> a -> b
    $ \ Context
    cxt UnquoteState
    s -> TCM (UnquoteRes a) -> TCM (UnquoteRes b)
    f (UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
    forall a.
    UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
    unpackUnquoteM UnquoteM a
    m Context
    cxt UnquoteState
    s)

    liftU2 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c)) -> UnquoteM a -> UnquoteM b -> UnquoteM c
    liftU2 :: forall a b c.
    (TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c))
    -> UnquoteM a -> UnquoteM b -> UnquoteM c
    liftU2 TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c)
    f UnquoteM a
    m1 UnquoteM b
    m2 = (Context -> UnquoteState -> TCM (UnquoteRes c)) -> UnquoteM c
    forall a.
    (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
    packUnquoteM ((Context -> UnquoteState -> TCM (UnquoteRes c)) -> UnquoteM c)
    -> (Context -> UnquoteState -> TCM (UnquoteRes c)) -> UnquoteM c
    forall a b. (a -> b) -> a -> b
    $ \ Context
    cxt UnquoteState
    s -> TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c)
    f (UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
    forall a.
    UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
    unpackUnquoteM UnquoteM a
    m1 Context
    cxt UnquoteState
    s) (UnquoteM b -> Context -> UnquoteState -> TCM (UnquoteRes b)
    forall a.
    UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
    unpackUnquoteM UnquoteM b
    m2 Context
    cxt UnquoteState
    s)

    inOriginalContext :: UnquoteM a -> UnquoteM a
    inOriginalContext :: forall a. UnquoteM a -> UnquoteM a
    inOriginalContext UnquoteM a
    m =
      (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
    forall a.
    (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
    packUnquoteM ((Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a)
    -> (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
    forall a b. (a -> b) -> a -> b
    $ \ Context
    cxt UnquoteState
    s -> do
        n <- TCMT IO Int
    forall (m :: * -> *). MonadTCEnv m => m Int
    getContextSize
        escapeContext __IMPOSSIBLE__ (n - length cxt) $ unpackUnquoteM m cxt s

    isCon :: ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    isCon :: ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    isCon ConHead
    con TCM (Maybe Term)
    tm = do t <- TCM (Maybe Term)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Maybe Term)
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM TCM (Maybe Term)
    tm
                      case t of
                        Just (Con ConHead
    con' ConInfo
    _ Elims
    _) -> Bool -> UnquoteM Bool
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ConHead
    con ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    con')
                        Maybe Term
    _ -> Bool -> UnquoteM Bool
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    isDef :: QName -> TCM (Maybe Term) -> UnquoteM Bool
    isDef :: QName -> TCM (Maybe Term) -> UnquoteM Bool
    isDef QName
    f TCM (Maybe Term)
    tm = Bool -> (Term -> Bool) -> Maybe Term -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False Term -> Bool
    loop (Maybe Term -> Bool)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Maybe Term)
    -> UnquoteM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM (Maybe Term)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Maybe Term)
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM TCM (Maybe Term)
    tm
      where
        loop :: Term -> Bool
    loop (Def QName
    g Elims
    _) = QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    g
        loop (Lam ArgInfo
    _ Abs Term
    b) = Term -> Bool
    loop (Term -> Bool) -> Term -> Bool
    forall a b. (a -> b) -> a -> b
    $ Abs Term -> Term
    forall a. Abs a -> a
    unAbs Abs Term
    b
        loop Term
    _         = Bool
    False

    reduceQuotedTerm :: Term -> UnquoteM Term
    reduceQuotedTerm :: Term -> UnquoteM Term
    reduceQuotedTerm Term
    t = UnquoteM Term -> UnquoteM Term
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    locallyReduceAllDefs (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ do
      Term
    -> (Blocker -> Term -> UnquoteM Term)
    -> (NotBlocked -> Term -> UnquoteM Term)
    -> UnquoteM Term
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked Term
    t {-then-} (\ Blocker
    m Term
    _ -> do s <- (UnquoteState -> TCState)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         TCState
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets UnquoteState -> TCState
    forall a b. (a, b) -> b
    snd; throwError $ BlockedOnMeta s m)
                  {-else-} (\ NotBlocked
    _ Term
    t -> Term -> UnquoteM Term
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    t)

    class Unquote a where
      unquote :: I.Term -> UnquoteM a

    -- | Unquote an @'Arg' 'Term'@ assuming the 'ArgInfo' does not contain information.
    -- (This means, it should be visible, relevant, etc., like 'defaultArg').
    unquoteN :: (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN :: forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN (Arg ArgInfo
    info Term
    v) =
      if ArgInfo -> Bool
    forall a. Null a => a -> Bool
    null ArgInfo
    info then Term -> UnquoteM a
    forall a. Unquote a => Term -> UnquoteM a
    unquote Term
    v else UnquoteM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        -- because we have a CallStack, this also includes the caller

    choice :: Monad m => [(m Bool, m a)] -> m a -> m a
    choice :: forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice [] m a
    dflt = m a
    dflt
    choice ((m Bool
    mb, m a
    mx) : [(m Bool, m a)]
    mxs) m a
    dflt = m Bool -> m a -> m a -> m a
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM m Bool
    mb m a
    mx (m a -> m a) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ [(m Bool, m a)] -> m a -> m a
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice [(m Bool, m a)]
    mxs m a
    dflt

    ensureDef :: QName -> UnquoteM QName
    ensureDef :: QName -> UnquoteM QName
    ensureDef QName
    x = do
      i <- (SigError -> Defn)
    -> (Definition -> Defn) -> Either SigError Definition -> Defn
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (Defn -> SigError -> Defn
    forall a b. a -> b -> a
    const Defn
    defaultAxiom) Definition -> Defn
    theDef (Either SigError Definition -> Defn)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Either SigError Definition)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    x  -- for recursive unquoteDecl
      case i of
        Constructor{} -> do
          def <- TCMT IO Doc
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Doc
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Doc
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Doc)
    -> TCMT IO Doc
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Term -> TCMT IO Doc) -> TCMT IO Term -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTermDef
          con <- liftTCM $ prettyTCM =<< primAgdaTermCon
          throwError $ ConInsteadOfDef x (show def) (show con)
        Defn
    _ -> QName -> UnquoteM QName
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    x

    ensureCon :: QName -> UnquoteM QName
    ensureCon :: QName -> UnquoteM QName
    ensureCon QName
    x = do
      i <- (SigError -> Defn)
    -> (Definition -> Defn) -> Either SigError Definition -> Defn
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (Defn -> SigError -> Defn
    forall a b. a -> b -> a
    const Defn
    defaultAxiom) Definition -> Defn
    theDef (Either SigError Definition -> Defn)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Either SigError Definition)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    x  -- for recursive unquoteDecl
      case i of
        Constructor{} -> QName -> UnquoteM QName
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    x
        Defn
    _ -> do
          def <- TCMT IO Doc
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Doc
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Doc
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Doc)
    -> TCMT IO Doc
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Term -> TCMT IO Doc) -> TCMT IO Term -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaTermDef
          con <- liftTCM $ prettyTCM =<< primAgdaTermCon
          throwError $ DefInsteadOfCon x (show def) (show con)

    pickName :: R.Type -> String
    pickName :: Type -> [Char]
    pickName Type
    a =
      case Type
    a of
        R.Pi{}   -> [Char]
    "f"
        R.Sort{} -> [Char]
    "A"
        R.Def QName
    d Elims
    _
          | Char
    c : [Char]
    cs  <- Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (QName -> Name
    qnameName QName
    d),
            Just Char
    lc <- Char -> Maybe Char
    reallyToLower Char
    c,
            Bool -> Bool
    not ([Char] -> Bool
    forall a. Null a => a -> Bool
    null [Char]
    cs) Bool -> Bool -> Bool
    || Char -> Bool
    isUpper Char
    c -> [Char
    lc]
        Type
    _        -> [Char]
    "_"
      where
        -- Heuristic (see #5048 for some discussion):
        -- If first character can be `toLower`ed use that, unless the name has only one character and is
        -- already lower case. (to avoid using the same name for the type and the bound variable).
        reallyToLower :: Char -> Maybe Char
    reallyToLower Char
    c
          | Char -> Char
    toUpper Char
    lc Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    lc = Char -> Maybe Char
    forall a. a -> Maybe a
    Just Char
    lc
          | Bool
    otherwise        = Maybe Char
    forall a. Maybe a
    Nothing
          where lc :: Char
    lc = Char -> Char
    toLower Char
    c

    -- TODO: reflect Cohesion
    -- TODO: reflect ModalPolarity
    instance Unquote Modality where
      unquote :: Term -> UnquoteM Modality
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    r,Arg Term
    q] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool, UnquoteM Modality)]
    -> UnquoteM Modality -> UnquoteM Modality
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinModalityConstructor,
                  Relevance -> Quantity -> Cohesion -> PolarityModality -> Modality
    Modality (Relevance -> Quantity -> Cohesion -> PolarityModality -> Modality)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Relevance
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Quantity -> Cohesion -> PolarityModality -> Modality)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Relevance
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    r
                           ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Quantity -> Cohesion -> PolarityModality -> Modality)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Quantity
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Cohesion -> PolarityModality -> Modality)
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Quantity
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    q
                           ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Cohesion -> PolarityModality -> Modality)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Cohesion
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (PolarityModality -> Modality)
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Cohesion
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Cohesion
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Cohesion
    defaultCohesion
                           ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (PolarityModality -> Modality)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         PolarityModality
    -> UnquoteM Modality
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> PolarityModality
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         PolarityModality
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure PolarityModality
    defaultPolarity)]
              UnquoteM Modality
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    _ -> UnquoteM Modality
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError -> UnquoteM Modality
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM Modality)
    -> UnquoteError -> UnquoteM Modality
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "modality" Term
    t

    instance Unquote ArgInfo where
      unquote :: Term -> UnquoteM ArgInfo
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    h,Arg Term
    m] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool, UnquoteM ArgInfo)]
    -> UnquoteM ArgInfo -> UnquoteM ArgInfo
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinArgArgInfo,
                  Hiding
    -> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo
    ArgInfo (Hiding
     -> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Hiding
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Hiding
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    h
                          ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo)
    -> UnquoteM Modality
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Origin -> FreeVariables -> Annotation -> ArgInfo)
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term -> UnquoteM Modality
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    m
                          ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Origin -> FreeVariables -> Annotation -> ArgInfo)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Origin
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (FreeVariables -> Annotation -> ArgInfo)
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Origin
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Origin
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Origin
    Reflected
                          ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (FreeVariables -> Annotation -> ArgInfo)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         FreeVariables
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Annotation -> ArgInfo)
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> FreeVariables
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         FreeVariables
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure FreeVariables
    unknownFreeVariables
                          ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Annotation -> ArgInfo)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Annotation
    -> UnquoteM ArgInfo
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Annotation
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Annotation
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Annotation
    defaultAnnotation)]
              UnquoteM ArgInfo
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    _ -> UnquoteM ArgInfo
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError -> UnquoteM ArgInfo
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM ArgInfo)
    -> UnquoteError -> UnquoteM ArgInfo
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "arg info" Term
    t

    instance Unquote a => Unquote (Arg a) where
      unquote :: Term -> UnquoteM (Arg a)
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    info,Arg Term
    x] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool, UnquoteM (Arg a))]
    -> UnquoteM (Arg a) -> UnquoteM (Arg a)
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinArgArg, ArgInfo -> a -> Arg a
    forall e. ArgInfo -> e -> Arg e
    Arg (ArgInfo -> a -> Arg a)
    -> UnquoteM ArgInfo
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (a -> Arg a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM ArgInfo
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    info ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> Arg a)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> UnquoteM (Arg a)
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)]
              UnquoteM (Arg a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    _ -> UnquoteM (Arg a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError -> UnquoteM (Arg a)
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM (Arg a))
    -> UnquoteError -> UnquoteM (Arg a)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "arg" Term
    t

    -- Andreas, 2013-10-20: currently, post-fix projections are not part of the
    -- quoted syntax.
    instance Unquote R.Elim where
      unquote :: Term -> UnquoteM Elim
    unquote Term
    t = Arg Type -> Elim
    forall a. Arg a -> Elim' a
    R.Apply (Arg Type -> Elim)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Arg Type)
    -> UnquoteM Elim
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Arg Type)
    forall a. Unquote a => Term -> UnquoteM a
    unquote Term
    t

    instance Unquote Bool where
      unquote :: Term -> UnquoteM Bool
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ [] ->
            [(UnquoteM Bool, UnquoteM Bool)] -> UnquoteM Bool -> UnquoteM Bool
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice [ (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinTrue,  Bool -> UnquoteM Bool
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    True)
                   , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinFalse, Bool -> UnquoteM Bool
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False) ]
                   UnquoteM Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError -> UnquoteM Bool
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM Bool) -> UnquoteError -> UnquoteM Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "boolean" Term
    t

    instance Unquote Integer where
      unquote :: Term -> UnquoteM Integer
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Lit (LitNat Integer
    n) -> Integer -> UnquoteM Integer
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Integer
    n
          Term
    _ -> UnquoteError -> UnquoteM Integer
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM Integer)
    -> UnquoteError -> UnquoteM Integer
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "integer" Term
    t

    instance Unquote Word64 where
      unquote :: Term -> UnquoteM Word64
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Lit (LitWord64 Word64
    n) -> Word64 -> UnquoteM Word64
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Word64
    n
          Term
    _ -> UnquoteError -> UnquoteM Word64
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM Word64)
    -> UnquoteError -> UnquoteM Word64
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "word64" Term
    t

    instance Unquote Double where
      unquote :: Term -> UnquoteM Double
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Lit (LitFloat Double
    x) -> Double -> UnquoteM Double
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Double
    x
          Term
    _ -> UnquoteError -> UnquoteM Double
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM Double)
    -> UnquoteError -> UnquoteM Double
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "float" Term
    t

    instance Unquote Char where
      unquote :: Term -> UnquoteM Char
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Lit (LitChar Char
    x) -> Char -> UnquoteM Char
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Char
    x
          Term
    _ -> UnquoteError -> UnquoteM Char
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM Char) -> UnquoteError -> UnquoteM Char
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "char" Term
    t

    instance Unquote Text where
      unquote :: Term -> UnquoteM ExeName
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Lit (LitString ExeName
    x) -> ExeName -> UnquoteM ExeName
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ExeName
    x
          Term
    _ -> UnquoteError -> UnquoteM ExeName
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM ExeName)
    -> UnquoteError -> UnquoteM ExeName
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "string" Term
    t

    unquoteString :: Term -> UnquoteM String
    unquoteString :: Term -> UnquoteM [Char]
    unquoteString Term
    x = ExeName -> [Char]
    T.unpack (ExeName -> [Char]) -> UnquoteM ExeName -> UnquoteM [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> UnquoteM ExeName
    forall a. Unquote a => Term -> UnquoteM a
    unquote Term
    x

    unquoteNString :: Arg Term -> UnquoteM Text
    unquoteNString :: Arg Term -> UnquoteM ExeName
    unquoteNString = Arg Term -> UnquoteM ExeName
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN

    data ErrorPart = StrPart String | TermPart A.Expr | PattPart A.Pattern | NamePart QName

    instance PrettyTCM ErrorPart where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => ErrorPart -> m Doc
    prettyTCM (StrPart [Char]
    s)  = [Char] -> m Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    s
      prettyTCM (TermPart Expr
    t) = Expr -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Expr -> m Doc
    prettyTCM Expr
    t
      prettyTCM (PattPart Pattern
    p) = Pattern -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Pattern -> m Doc
    prettyTCM Pattern
    p
      prettyTCM (NamePart QName
    x) = QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    x

    -- | We do a little bit of work here to make it possible to generate nice
    --   layout for multi-line error messages. Specifically we split the parts
    --   into lines (indicated by \n in a string part) and vcat all the lines.
    renderErrorParts :: [ErrorPart] -> TCM Doc
    renderErrorParts :: [ErrorPart] -> TCMT IO Doc
    renderErrorParts = [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([TCMT IO Doc] -> TCMT IO Doc)
    -> ([ErrorPart] -> [TCMT IO Doc]) -> [ErrorPart] -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([ErrorPart] -> TCMT IO Doc) -> [[ErrorPart]] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hcat ([TCMT IO Doc] -> TCMT IO Doc)
    -> ([ErrorPart] -> [TCMT IO Doc]) -> [ErrorPart] -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ErrorPart -> TCMT IO Doc) -> [ErrorPart] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ErrorPart -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => ErrorPart -> m Doc
    prettyTCM) ([[ErrorPart]] -> [TCMT IO Doc])
    -> ([ErrorPart] -> [[ErrorPart]]) -> [ErrorPart] -> [TCMT IO Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ErrorPart] -> [[ErrorPart]]
    splitLines
      where
        splitLines :: [ErrorPart] -> [[ErrorPart]]
    splitLines [] = []
        splitLines (StrPart [Char]
    s : [ErrorPart]
    ss) =
          case (Char -> Bool) -> [Char] -> ([Char], [Char])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '\n') [Char]
    s of
            ([Char]
    s0, Char
    '\n' : [Char]
    s1) -> [[Char] -> ErrorPart
    StrPart [Char]
    s0] [ErrorPart] -> [[ErrorPart]] -> [[ErrorPart]]
    forall a. a -> [a] -> [a]
    : [ErrorPart] -> [[ErrorPart]]
    splitLines ([Char] -> ErrorPart
    StrPart [Char]
    s1 ErrorPart -> [ErrorPart] -> [ErrorPart]
    forall a. a -> [a] -> [a]
    : [ErrorPart]
    ss)
            ([Char]
    s0, [Char]
    "")        -> ErrorPart -> [[ErrorPart]] -> [[ErrorPart]]
    forall {a}. a -> [[a]] -> [[a]]
    consLine ([Char] -> ErrorPart
    StrPart [Char]
    s0) ([ErrorPart] -> [[ErrorPart]]
    splitLines [ErrorPart]
    ss)
            ([Char], [Char])
    _               -> [[ErrorPart]]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        splitLines (p :: ErrorPart
    p@TermPart{} : [ErrorPart]
    ss) = ErrorPart -> [[ErrorPart]] -> [[ErrorPart]]
    forall {a}. a -> [[a]] -> [[a]]
    consLine ErrorPart
    p ([ErrorPart] -> [[ErrorPart]]
    splitLines [ErrorPart]
    ss)
        splitLines (p :: ErrorPart
    p@PattPart{} : [ErrorPart]
    ss) = ErrorPart -> [[ErrorPart]] -> [[ErrorPart]]
    forall {a}. a -> [[a]] -> [[a]]
    consLine ErrorPart
    p ([ErrorPart] -> [[ErrorPart]]
    splitLines [ErrorPart]
    ss)
        splitLines (p :: ErrorPart
    p@NamePart{} : [ErrorPart]
    ss) = ErrorPart -> [[ErrorPart]] -> [[ErrorPart]]
    forall {a}. a -> [[a]] -> [[a]]
    consLine ErrorPart
    p ([ErrorPart] -> [[ErrorPart]]
    splitLines [ErrorPart]
    ss)

        consLine :: a -> [[a]] -> [[a]]
    consLine a
    l []        = [[a
    l]]
        consLine a
    l ([a]
    l' : [[a]]
    ls) = (a
    l a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    l') [a] -> [[a]] -> [[a]]
    forall a. a -> [a] -> [a]
    : [[a]]
    ls

    instance Unquote ErrorPart where
      unquote :: Term -> UnquoteM ErrorPart
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    x] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool, UnquoteM ErrorPart)]
    -> UnquoteM ErrorPart -> UnquoteM ErrorPart
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice [ (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaErrorPartString, [Char] -> ErrorPart
    StrPart ([Char] -> ErrorPart)
    -> (ExeName -> [Char]) -> ExeName -> ErrorPart
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExeName -> [Char]
    T.unpack (ExeName -> ErrorPart) -> UnquoteM ExeName -> UnquoteM ErrorPart
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM ExeName
    unquoteNString Arg Term
    x)
                   , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaErrorPartTerm,   Expr -> ErrorPart
    TermPart (Expr -> ErrorPart)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Expr
    -> UnquoteM ErrorPart
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((TCM Expr
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Expr
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Expr
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Expr)
    -> (Type -> TCM Expr)
    -> Type
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> TCM Expr
    Type -> TCMT IO (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
     MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
     HasConstInfo m) =>
    r -> m (AbsOfRef r)
    toAbstractWithoutImplicit) (Type
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Expr)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x :: UnquoteM R.Term)))
                   , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaErrorPartPatt,   Pattern -> ErrorPart
    PattPart (Pattern -> ErrorPart)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    -> UnquoteM ErrorPart
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((TCM Pattern
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Pattern
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Pattern)
    -> (Pattern -> TCM Pattern)
    -> Pattern
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Pattern -> TCM Pattern
    Pattern -> TCMT IO (AbsOfRef Pattern)
    forall r (m :: * -> *).
    (ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
     MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
     HasConstInfo m) =>
    r -> m (AbsOfRef r)
    toAbstractWithoutImplicit) (Pattern
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Pattern)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x :: UnquoteM R.Pattern)))
                   , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaErrorPartName,   QName -> ErrorPart
    NamePart (QName -> ErrorPart) -> UnquoteM QName -> UnquoteM ErrorPart
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM QName
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x) ]
                   UnquoteM ErrorPart
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError -> UnquoteM ErrorPart
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM ErrorPart)
    -> UnquoteError -> UnquoteM ErrorPart
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "error part" Term
    t

    instance Unquote a => Unquote [a] where
      unquote :: Term -> UnquoteM [a]
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    x,Arg Term
    xs] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool, UnquoteM [a])] -> UnquoteM [a] -> UnquoteM [a]
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinCons, (:) (a -> [a] -> [a])
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ([a] -> [a])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ([a] -> [a])
    -> UnquoteM [a] -> UnquoteM [a]
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term -> UnquoteM [a]
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    xs)]
              UnquoteM [a]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ [] ->
            [(UnquoteM Bool, UnquoteM [a])] -> UnquoteM [a] -> UnquoteM [a]
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinNil, [a] -> UnquoteM [a]
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [])]
              UnquoteM [a]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    _ -> UnquoteM [a]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError -> UnquoteM [a]
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM [a]) -> UnquoteError -> UnquoteM [a]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "list" Term
    t

    instance (Unquote a, Unquote b) => Unquote (a, b) where
      unquote :: Term -> UnquoteM (a, b)
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        SigmaKit{..} <- fromMaybe __IMPOSSIBLE__ <$> getSigmaKit
        case t of
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    x,Arg Term
    y] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool, UnquoteM (a, b))]
    -> UnquoteM (a, b) -> UnquoteM (a, b)
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [(Bool -> UnquoteM Bool
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    sigmaCon), (,) (a -> b -> (a, b))
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (b -> (a, b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (b -> (a, b))
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    -> UnquoteM (a, b)
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    y)]
              UnquoteM (a, b)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError -> UnquoteM (a, b)
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM (a, b))
    -> UnquoteError -> UnquoteM (a, b)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "pair" Term
    t

    instance Unquote Hiding where
      unquote :: Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Hiding
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ [] ->
            [(UnquoteM Bool,
      ReaderT
        Context
        (StateT
           UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
        Hiding)]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Hiding
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Hiding
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinHidden,  Hiding
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Hiding
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Hiding
    Hidden)
              ,(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinInstance, Hiding
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Hiding
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Overlappable -> Hiding
    Instance Overlappable
    NoOverlap))
              ,(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinVisible, Hiding
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Hiding
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Hiding
    NotHidden)]
              ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Hiding
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    vs -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Hiding
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _        -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Hiding
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Hiding)
    -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Hiding
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "visibility" Term
    t

    instance Unquote Relevance where
      unquote :: Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Relevance
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ [] ->
            [(UnquoteM Bool,
      ReaderT
        Context
        (StateT
           UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
        Relevance)]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Relevance
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Relevance
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinRelevant,   Relevance
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Relevance
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Relevance
    relevant)
              ,(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinIrrelevant, Relevance
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Relevance
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Relevance
    irrelevant)]
              ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Relevance
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    vs -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Relevance
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _        -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Relevance
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Relevance)
    -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Relevance
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "relevance" Term
    t

    instance Unquote Quantity where
      unquote :: Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Quantity
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ [] ->
            [(UnquoteM Bool,
      ReaderT
        Context
        (StateT
           UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
        Quantity)]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Quantity
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Quantity
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinQuantityω, Quantity
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Quantity
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Quantity
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Quantity)
    -> Quantity
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Quantity
    forall a b. (a -> b) -> a -> b
    $ QωOrigin -> Quantity
    Quantityω QωOrigin
    QωInferred)
              ,(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinQuantity0, Quantity
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Quantity
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Quantity
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Quantity)
    -> Quantity
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Quantity
    forall a b. (a -> b) -> a -> b
    $ Q0Origin -> Quantity
    Quantity0 Q0Origin
    Q0Inferred)]
              ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Quantity
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    vs -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Quantity
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _        -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Quantity
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Quantity)
    -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Quantity
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "quantity" Term
    t

    instance Unquote QName where
      unquote :: Term -> UnquoteM QName
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Lit (LitQName QName
    x) -> QName -> UnquoteM QName
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    x
          Term
    _ -> UnquoteError -> UnquoteM QName
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM QName) -> UnquoteError -> UnquoteM QName
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "name" Term
    t

    instance Unquote a => Unquote (R.Abs a) where
      unquote :: Term -> UnquoteM (Abs a)
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    x,Arg Term
    y] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool, UnquoteM (Abs a))]
    -> UnquoteM (Abs a) -> UnquoteM (Abs a)
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAbsAbs, [Char] -> a -> Abs a
    forall a. [Char] -> a -> Abs a
    R.Abs ([Char] -> a -> Abs a)
    -> UnquoteM [Char]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (a -> Abs a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Char] -> [Char]
    forall {a}. (Null a, IsString a) => a -> a
    hint ([Char] -> [Char]) -> (ExeName -> [Char]) -> ExeName -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExeName -> [Char]
    T.unpack (ExeName -> [Char]) -> UnquoteM ExeName -> UnquoteM [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM ExeName
    unquoteNString Arg Term
    x) ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> Abs a)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> UnquoteM (Abs a)
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    y)]
              UnquoteM (Abs a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    _ -> UnquoteM (Abs a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError -> UnquoteM (Abs a)
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM (Abs a))
    -> UnquoteError -> UnquoteM (Abs a)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "abstraction" Term
    t

        where hint :: a -> a
    hint a
    x | Bool -> Bool
    not (a -> Bool
    forall a. Null a => a -> Bool
    null a
    x) = a
    x
                     | Bool
    otherwise    = a
    "_"

    instance Unquote Blocker where
      unquote :: Term -> UnquoteM Blocker
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    x] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool, UnquoteM Blocker)]
    -> UnquoteM Blocker -> UnquoteM Blocker
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [ (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaBlockerAny, Set Blocker -> Blocker
    UnblockOnAny (Set Blocker -> Blocker)
    -> ([Blocker] -> Set Blocker) -> [Blocker] -> Blocker
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Blocker] -> Set Blocker
    forall a. Ord a => [a] -> Set a
    Set.fromList ([Blocker] -> Blocker)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [Blocker]
    -> UnquoteM Blocker
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [Blocker]
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaBlockerAll, Set Blocker -> Blocker
    UnblockOnAll (Set Blocker -> Blocker)
    -> ([Blocker] -> Set Blocker) -> [Blocker] -> Blocker
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Blocker] -> Set Blocker
    forall a. Ord a => [a] -> Set a
    Set.fromList ([Blocker] -> Blocker)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [Blocker]
    -> UnquoteM Blocker
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [Blocker]
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaBlockerMeta, MetaId -> Blocker
    UnblockOnMeta (MetaId -> Blocker)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         MetaId
    -> UnquoteM Blocker
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         MetaId
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)]
              UnquoteM Blocker
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    _ -> UnquoteM Blocker
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError -> UnquoteM Blocker
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM Blocker)
    -> UnquoteError -> UnquoteM Blocker
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "blocker" Term
    t

    instance Unquote MetaId where
      unquote :: Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         MetaId
    unquote Term
    t = do
        Term -> UnquoteM Term
    reduceQuotedTerm Term
    t UnquoteM Term
    -> (Term
        -> ReaderT
             Context
             (StateT
                UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
             MetaId)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         MetaId
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      a
    -> (a
        -> ReaderT
             Context
             (StateT
                UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
             b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Lit (LitMeta TopLevelModuleName' Range
    m MetaId
    x) -> MetaId
    x MetaId
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         MetaId
    forall a b.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ do
            -- We cannot unquote a meta from a different file.
            UnquoteM Bool
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM ((TopLevelModuleName' Range -> Maybe (TopLevelModuleName' Range)
    forall a. a -> Maybe a
    Just TopLevelModuleName' Range
    m Maybe (TopLevelModuleName' Range)
    -> Maybe (TopLevelModuleName' Range) -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Maybe (TopLevelModuleName' Range) -> Bool)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Maybe (TopLevelModuleName' Range))
    -> UnquoteM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Maybe (TopLevelModuleName' Range))
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    m (Maybe (TopLevelModuleName' Range))
    currentTopLevelModule) do
              UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          ())
    -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName' Range -> MetaId -> UnquoteError
    StaleMeta TopLevelModuleName' Range
    m MetaId
    x
          Term
    t -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         MetaId
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          MetaId)
    -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         MetaId
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "meta variable" Term
    t

    instance Unquote a => Unquote (Dom a) where
      unquote :: Term -> UnquoteM (Dom a)
    unquote Term
    t = Arg a -> Dom a
    forall a. Arg a -> Dom a
    domFromArg (Arg a -> Dom a)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Arg a)
    -> UnquoteM (Dom a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Arg a)
    forall a. Unquote a => Term -> UnquoteM a
    unquote Term
    t

    instance Unquote R.Sort where
      unquote :: Term -> UnquoteM Sort
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ [] ->
            [(UnquoteM Bool, UnquoteM Sort)] -> UnquoteM Sort -> UnquoteM Sort
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [(ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaSortUnsupported, Sort -> UnquoteM Sort
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    R.UnknownS)]
              UnquoteM Sort
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    u] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool, UnquoteM Sort)] -> UnquoteM Sort -> UnquoteM Sort
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [ (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaSortSet, Type -> Sort
    R.SetS (Type -> Sort)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    -> UnquoteM Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    u)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaSortLit, Integer -> Sort
    R.LitS (Integer -> Sort) -> UnquoteM Integer -> UnquoteM Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM Integer
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    u)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaSortProp, Type -> Sort
    R.PropS (Type -> Sort)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    -> UnquoteM Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    u)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaSortPropLit, Integer -> Sort
    R.PropLitS (Integer -> Sort) -> UnquoteM Integer -> UnquoteM Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM Integer
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    u)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaSortInf, Integer -> Sort
    R.InfS (Integer -> Sort) -> UnquoteM Integer -> UnquoteM Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM Integer
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    u)
              ]
              UnquoteM Sort
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    _ -> UnquoteM Sort
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError -> UnquoteM Sort
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM Sort) -> UnquoteError -> UnquoteM Sort
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "sort" Term
    t

    instance Unquote Literal where
      unquote :: Term -> UnquoteM Literal
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    x] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool, UnquoteM Literal)]
    -> UnquoteM Literal -> UnquoteM Literal
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [ (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaLitNat,    Integer -> Literal
    LitNat    (Integer -> Literal) -> UnquoteM Integer -> UnquoteM Literal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM Integer
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaLitFloat,  Double -> Literal
    LitFloat  (Double -> Literal) -> UnquoteM Double -> UnquoteM Literal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM Double
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaLitChar,   Char -> Literal
    LitChar   (Char -> Literal) -> UnquoteM Char -> UnquoteM Literal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM Char
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaLitString, ExeName -> Literal
    LitString (ExeName -> Literal) -> UnquoteM ExeName -> UnquoteM Literal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM ExeName
    unquoteNString Arg Term
    x)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaLitQName,  QName -> Literal
    LitQName  (QName -> Literal) -> UnquoteM QName -> UnquoteM Literal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM QName
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaLitMeta,
                 TopLevelModuleName' Range -> MetaId -> Literal
    LitMeta
                   (TopLevelModuleName' Range -> MetaId -> Literal)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (TopLevelModuleName' Range)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (MetaId -> Literal)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TopLevelModuleName' Range
    -> Maybe (TopLevelModuleName' Range) -> TopLevelModuleName' Range
    forall a. a -> Maybe a -> a
    fromMaybe TopLevelModuleName' Range
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (TopLevelModuleName' Range) -> TopLevelModuleName' Range)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Maybe (TopLevelModuleName' Range))
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (TopLevelModuleName' Range)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Maybe (TopLevelModuleName' Range))
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    m (Maybe (TopLevelModuleName' Range))
    currentTopLevelModule)
                   ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (MetaId -> Literal)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         MetaId
    -> UnquoteM Literal
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         MetaId
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)
              ]
              UnquoteM Literal
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    _ -> UnquoteM Literal
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError -> UnquoteM Literal
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM Literal)
    -> UnquoteError -> UnquoteM Literal
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "literal" Term
    t

    instance Unquote R.Term where
      unquote :: Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ [] ->
            [(UnquoteM Bool,
      ReaderT
        Context
        (StateT
           UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
        Type)]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [ (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTermUnsupported, Type
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    R.Unknown) ]
              ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    x] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool,
      ReaderT
        Context
        (StateT
           UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
        Type)]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [ (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTermSort,      Sort -> Type
    R.Sort      (Sort -> Type)
    -> UnquoteM Sort
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM Sort
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTermLit,       Literal -> Type
    R.Lit       (Literal -> Type)
    -> UnquoteM Literal
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM Literal
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)
              ]
              ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    x, Arg Term
    y] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool,
      ReaderT
        Context
        (StateT
           UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
        Type)]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [ (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTermVar,     Int -> Elims -> Type
    R.Var     (Int -> Elims -> Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Int
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Elims -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Int)
    -> UnquoteM Integer
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM Integer
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x) ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Elims -> Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Elims
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Elims
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    y)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTermCon,     QName -> Elims -> Type
    R.Con     (QName -> Elims -> Type)
    -> UnquoteM QName
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Elims -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName -> UnquoteM QName
    ensureCon (QName -> UnquoteM QName) -> UnquoteM QName -> UnquoteM QName
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Arg Term -> UnquoteM QName
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x) ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Elims -> Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Elims
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Elims
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    y)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTermDef,     QName -> Elims -> Type
    R.Def     (QName -> Elims -> Type)
    -> UnquoteM QName
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Elims -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName -> UnquoteM QName
    ensureDef (QName -> UnquoteM QName) -> UnquoteM QName -> UnquoteM QName
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Arg Term -> UnquoteM QName
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x) ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Elims -> Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Elims
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Elims
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    y)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTermMeta,    MetaId -> Elims -> Type
    R.Meta    (MetaId -> Elims -> Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         MetaId
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Elims -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         MetaId
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Elims -> Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Elims
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Elims
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    y)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTermLam,     Hiding -> Abs Type -> Type
    R.Lam     (Hiding -> Abs Type -> Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Hiding
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Abs Type -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Hiding
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Abs Type -> Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Abs Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Abs Type)
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    y)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTermPi,      Dom Type -> Abs Type -> Type
    mkPi      (Dom Type -> Abs Type -> Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Dom Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Abs Type -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Dom Type)
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Abs Type -> Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Abs Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Abs Type)
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    y)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTermExtLam,  do
                  ps <- Arg Term -> UnquoteM [Clause]
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x
                  es <- unquoteN y
                  case ps of
                    []     -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Type)
    -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a b. (a -> b) -> a -> b
    $ Term -> UnquoteError
    PatLamWithoutClauses Term
    t
                    Clause
    p : [Clause]
    ps -> Type
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Type
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Type)
    -> Type
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a b. (a -> b) -> a -> b
    $ List1 Clause -> Elims -> Type
    R.ExtLam (Clause
    p Clause -> [Clause] -> List1 Clause
    forall a. a -> [a] -> NonEmpty a
    :| [Clause]
    ps) Elims
    es
                )
              ]
              ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            where
              mkPi :: Dom R.Type -> R.Abs R.Type -> R.Term
              -- TODO: implement Free for reflected syntax so this works again
              --mkPi a (R.Abs "_" b) = R.Pi a (R.Abs x b)
              --  where x | 0 `freeIn` b = pickName (unDom a)
              --          | otherwise    = "_"
              mkPi :: Dom Type -> Abs Type -> Type
    mkPi Dom Type
    a (R.Abs [Char]
    "_" Type
    b) = Dom Type -> Abs Type -> Type
    R.Pi Dom Type
    a ([Char] -> Type -> Abs Type
    forall a. [Char] -> a -> Abs a
    R.Abs (Type -> [Char]
    pickName (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a)) Type
    b)
              mkPi Dom Type
    a Abs Type
    b = Dom Type -> Abs Type -> Type
    R.Pi Dom Type
    a Abs Type
    b

          Con{} -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Lit{} -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Type)
    -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "term" Term
    t

    instance Unquote R.Pattern where
      unquote :: Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    x] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool,
      ReaderT
        Context
        (StateT
           UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
        Pattern)]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [ (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaPatVar,    Int -> Pattern
    R.VarP    (Int -> Pattern) -> (Integer -> Int) -> Integer -> Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Pattern)
    -> UnquoteM Integer
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM Integer
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaPatAbsurd, Int -> Pattern
    R.AbsurdP (Int -> Pattern) -> (Integer -> Int) -> Integer -> Pattern
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Pattern)
    -> UnquoteM Integer
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM Integer
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaPatDot,    Type -> Pattern
    R.DotP  (Type -> Pattern)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaPatProj,   QName -> Pattern
    R.ProjP (QName -> Pattern)
    -> UnquoteM QName
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM QName
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x)
              , (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaPatLit,    Literal -> Pattern
    R.LitP  (Literal -> Pattern)
    -> UnquoteM Literal
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM Literal
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x) ]
              ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    x, Arg Term
    y] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool,
      ReaderT
        Context
        (StateT
           UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
        Pattern)]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [ (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaPatCon, QName -> [Arg Pattern] -> Pattern
    R.ConP (QName -> [Arg Pattern] -> Pattern)
    -> UnquoteM QName
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ([Arg Pattern] -> Pattern)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term -> UnquoteM QName
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ([Arg Pattern] -> Pattern)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [Arg Pattern]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [Arg Pattern]
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    y) ]
              ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    _ -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Pattern
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Pattern)
    -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Pattern
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "pattern" Term
    t

    instance Unquote R.Clause where
      unquote :: Term -> UnquoteM Clause
    unquote Term
    t = do
        t <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    t
        case t of
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    x, Arg Term
    y] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool, UnquoteM Clause)]
    -> UnquoteM Clause -> UnquoteM Clause
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [ (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaClauseAbsurd, [(ExeName, Arg Type)] -> [Arg Pattern] -> Clause
    R.AbsurdClause ([(ExeName, Arg Type)] -> [Arg Pattern] -> Clause)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [(ExeName, Arg Type)]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ([Arg Pattern] -> Clause)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [(ExeName, Arg Type)]
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ([Arg Pattern] -> Clause)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [Arg Pattern]
    -> UnquoteM Clause
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [Arg Pattern]
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    y) ]
              UnquoteM Clause
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    es | Just [Arg Term
    x, Arg Term
    y, Arg Term
    z] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es ->
            [(UnquoteM Bool, UnquoteM Clause)]
    -> UnquoteM Clause -> UnquoteM Clause
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice
              [ (ConHead
    c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
    `isCon` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaClauseClause, [(ExeName, Arg Type)] -> [Arg Pattern] -> Type -> Clause
    R.Clause ([(ExeName, Arg Type)] -> [Arg Pattern] -> Type -> Clause)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [(ExeName, Arg Type)]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ([Arg Pattern] -> Type -> Clause)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [(ExeName, Arg Type)]
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    x ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ([Arg Pattern] -> Type -> Clause)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [Arg Pattern]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Type -> Clause)
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [Arg Pattern]
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    y ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Type -> Clause)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    -> UnquoteM Clause
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (a -> b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Arg Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Type
    forall a. (HasCallStack, Unquote a) => Arg Term -> UnquoteM a
    unquoteN Arg Term
    z) ]
              UnquoteM Clause
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Con ConHead
    c ConInfo
    _ Elims
    _ -> UnquoteM Clause
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Term
    _ -> UnquoteError -> UnquoteM Clause
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM Clause)
    -> UnquoteError -> UnquoteM Clause
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "clause" Term
    t

    -- Unquoting TCM computations ---------------------------------------------

    -- | Argument should be a term of type @Term → TCM A@ for some A. Returns the
    --   resulting term of type @A@. The second argument is the term for the hole,
    --   which will typically be a metavariable. This is passed to the computation
    --   (quoted).
    unquoteTCM :: I.Term -> I.Term -> UnquoteM I.Term
    unquoteTCM :: Term -> Term -> UnquoteM Term
    unquoteTCM Term
    m Term
    hole = do
      qhole <- TCMT IO Term -> UnquoteM Term
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Term
    quoteTerm Term
    hole
      evalTCM (m `apply` [defaultArg qhole])

    evalTCM :: I.Term -> UnquoteM I.Term
    evalTCM :: Term -> UnquoteM Term
    evalTCM Term
    v = Account
      (BenchPhase
         (ReaderT
            Context
            (StateT
               UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))))
    -> UnquoteM Term -> UnquoteM Term
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    Bench.billTo [BenchPhase
      (ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO)))))
    Phase
    Bench.Typing, BenchPhase
      (ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO)))))
    Phase
    Bench.Reflection] do
      v <- Term -> UnquoteM Term
    reduceQuotedTerm Term
    v
      liftTCM $ reportSDoc "tc.unquote.eval" 90 $ "evalTCM" <+> prettyTCM v
      let failEval = UnquoteError -> UnquoteM Term
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM Term) -> UnquoteError -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> UnquoteError
    NonCanonical [Char]
    "type checking computation" Term
    v

      case v of
        I.Def QName
    f [] ->
          [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice [ (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMGetContext,       UnquoteM Term
    tcGetContext)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMCommit,           UnquoteM Term
    tcCommit)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMAskNormalisation, UnquoteM Term
    tcAskNormalisation)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMAskReconstructed, UnquoteM Term
    tcAskReconstructed)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMAskExpandLast,    UnquoteM Term
    tcAskExpandLast)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMAskReduceDefs,    UnquoteM Term
    tcAskReduceDefs)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMSolveInstances,   UnquoteM Term
    tcSolveInstances)
                 ]
                 UnquoteM Term
    failEval
        I.Def QName
    f [Elim
    u] ->
          [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice [ (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMInferType,                  (Type -> TCMT IO Term) -> Elim -> UnquoteM Term
    forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
    tcFun1 Type -> TCMT IO Term
    tcInferType                  Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMNormalise,                  (Type -> TCMT IO Term) -> Elim -> UnquoteM Term
    forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
    tcFun1 Type -> TCMT IO Term
    tcNormalise                  Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMReduce,                     (Type -> TCMT IO Term) -> Elim -> UnquoteM Term
    forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
    tcFun1 Type -> TCMT IO Term
    tcReduce                     Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMGetType,                    (QName -> TCMT IO Term) -> Elim -> UnquoteM Term
    forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
    tcFun1 QName -> TCMT IO Term
    tcGetType                    Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMGetDefinition,              (QName -> TCMT IO Term) -> Elim -> UnquoteM Term
    forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
    tcFun1 QName -> TCMT IO Term
    tcGetDefinition              Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMFormatErrorParts,           ([ErrorPart] -> TCMT IO Term) -> Elim -> UnquoteM Term
    forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
    tcFun1 [ErrorPart] -> TCMT IO Term
    tcFormatErrorParts           Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMIsMacro,                    (QName -> TCMT IO Term) -> Elim -> UnquoteM Term
    forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
    tcFun1 QName -> TCMT IO Term
    tcIsMacro                    Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMFreshName,                  (ExeName -> TCMT IO Term) -> Elim -> UnquoteM Term
    forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
    tcFun1 ExeName -> TCMT IO Term
    tcFreshName                  Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMGetInstances,               (MetaId -> UnquoteM Term) -> Elim -> UnquoteM Term
    forall a b. Unquote a => (a -> UnquoteM b) -> Elim -> UnquoteM b
    uqFun1 MetaId -> UnquoteM Term
    tcGetInstances               Elim
    u)
                 ]
                 UnquoteM Term
    failEval
        I.Def QName
    f [Elim
    u, Elim
    v] ->
          [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice [ (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMUnify,      (Type -> Type -> TCMT IO Term) -> Elim -> Elim -> UnquoteM Term
    forall a b c.
    (Unquote a, Unquote b) =>
    (a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
    tcFun2 Type -> Type -> TCMT IO Term
    tcUnify      Elim
    u Elim
    v)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMCheckType,  (Type -> Type -> TCMT IO Term) -> Elim -> Elim -> UnquoteM Term
    forall a b c.
    (Unquote a, Unquote b) =>
    (a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
    tcFun2 Type -> Type -> TCMT IO Term
    tcCheckType  Elim
    u Elim
    v)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMDeclareDef, (Arg QName -> Type -> UnquoteM Term)
    -> Elim -> Elim -> UnquoteM Term
    forall a b c.
    (Unquote a, Unquote b) =>
    (a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
    uqFun2 Arg QName -> Type -> UnquoteM Term
    tcDeclareDef Elim
    u Elim
    v)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMDeclarePostulate, (Arg QName -> Type -> UnquoteM Term)
    -> Elim -> Elim -> UnquoteM Term
    forall a b c.
    (Unquote a, Unquote b) =>
    (a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
    uqFun2 Arg QName -> Type -> UnquoteM Term
    tcDeclarePostulate Elim
    u Elim
    v)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMDefineData, (QName -> [(QName, (Quantity, Type))] -> UnquoteM Term)
    -> Elim -> Elim -> UnquoteM Term
    forall a b c.
    (Unquote a, Unquote b) =>
    (a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
    uqFun2 QName -> [(QName, (Quantity, Type))] -> UnquoteM Term
    tcDefineData Elim
    u Elim
    v)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMDefineFun,  (QName -> [Clause] -> UnquoteM Term)
    -> Elim -> Elim -> UnquoteM Term
    forall a b c.
    (Unquote a, Unquote b) =>
    (a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
    uqFun2 QName -> [Clause] -> UnquoteM Term
    tcDefineFun  Elim
    u Elim
    v)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMQuoteOmegaTerm, Type -> Term -> UnquoteM Term
    tcQuoteTerm (Sort' Term -> Type
    sort (Sort' Term -> Type) -> Sort' Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Univ -> Integer -> Sort' Term
    forall t. Univ -> Integer -> Sort' t
    Inf Univ
    UType Integer
    0) (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    v))
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMPragmaForeign, (ExeName -> ExeName -> TCMT IO Term)
    -> Elim -> Elim -> UnquoteM Term
    forall a b c.
    (Unquote a, Unquote b) =>
    (a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
    tcFun2 ExeName -> ExeName -> TCMT IO Term
    tcPragmaForeign Elim
    u Elim
    v)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMCheckFromString, (ExeName -> Type -> TCMT IO Term) -> Elim -> Elim -> UnquoteM Term
    forall a b c.
    (Unquote a, Unquote b) =>
    (a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
    tcFun2 ExeName -> Type -> TCMT IO Term
    tcCheckFromString Elim
    u Elim
    v)
                 ]
                 UnquoteM Term
    failEval
        I.Def QName
    f [Elim
    l, Elim
    a, Elim
    u] ->
          [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice [ (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMReturn,             Term -> UnquoteM Term
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    u))
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMTypeError,          ([ErrorPart] -> TCMT IO Term) -> Elim -> UnquoteM Term
    forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
    tcFun1 [ErrorPart] -> TCMT IO Term
    forall a. [ErrorPart] -> TCM a
    tcTypeError   Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMQuoteTerm,          Type -> Term -> UnquoteM Term
    tcQuoteTerm (Term -> Term -> Type
    forall {t} {a}. t -> a -> Type'' t a
    mkT (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    l) (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    a)) (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    u))
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMUnquoteTerm,        (Type -> TCMT IO Term) -> Elim -> UnquoteM Term
    forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
    tcFun1 (Type -> Type -> TCMT IO Term
    tcUnquoteTerm (Term -> Term -> Type
    forall {t} {a}. t -> a -> Type'' t a
    mkT (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    l) (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    a))) Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMBlock,              (Blocker -> UnquoteM Term) -> Elim -> UnquoteM Term
    forall a b. Unquote a => (a -> UnquoteM b) -> Elim -> UnquoteM b
    uqFun1 Blocker -> UnquoteM Term
    tcBlock Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMDebugPrint,         (ExeName -> Integer -> [ErrorPart] -> TCMT IO Term)
    -> Elim -> Elim -> Elim -> UnquoteM Term
    forall a b c d.
    (Unquote a, Unquote b, Unquote c) =>
    (a -> b -> c -> TCM d) -> Elim -> Elim -> Elim -> UnquoteM d
    tcFun3 ExeName -> Integer -> [ErrorPart] -> TCMT IO Term
    tcDebugPrint Elim
    l Elim
    a Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMNoConstraints,      Term -> UnquoteM Term
    tcNoConstraints (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    u))
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMDeclareData, (QName -> Integer -> Type -> UnquoteM Term)
    -> Elim -> Elim -> Elim -> UnquoteM Term
    forall a b c d.
    (Unquote a, Unquote b, Unquote c) =>
    (a -> b -> c -> UnquoteM d) -> Elim -> Elim -> Elim -> UnquoteM d
    uqFun3 QName -> Integer -> Type -> UnquoteM Term
    tcDeclareData Elim
    l Elim
    a Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMRunSpeculative,     Term -> UnquoteM Term
    tcRunSpeculative (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    u))
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMExec, (ExeName -> [ExeName] -> ExeName -> TCMT IO Term)
    -> Elim -> Elim -> Elim -> UnquoteM Term
    forall a b c d.
    (Unquote a, Unquote b, Unquote c) =>
    (a -> b -> c -> TCM d) -> Elim -> Elim -> Elim -> UnquoteM d
    tcFun3 ExeName -> [ExeName] -> ExeName -> TCMT IO Term
    tcExec Elim
    l Elim
    a Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMPragmaCompile, (ExeName -> QName -> ExeName -> TCMT IO Term)
    -> Elim -> Elim -> Elim -> UnquoteM Term
    forall a b c d.
    (Unquote a, Unquote b, Unquote c) =>
    (a -> b -> c -> TCM d) -> Elim -> Elim -> Elim -> UnquoteM d
    tcFun3 ExeName -> QName -> ExeName -> TCMT IO Term
    tcPragmaCompile Elim
    l Elim
    a Elim
    u)
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMWorkOnTypes, Term -> UnquoteM Term
    tcWorkOnTypes (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    u))
                 ]
                 UnquoteM Term
    failEval
        I.Def QName
    f [Elim
    _, Elim
    _, Elim
    u, Elim
    v] ->
          [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice [ (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMCatchError,        Term -> Term -> UnquoteM Term
    tcCatchError    (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    u) (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    v))
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMWithNormalisation, Term -> Term -> UnquoteM Term
    tcWithNormalisation (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    u) (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    v))
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMWithReconstructed, Term -> Term -> UnquoteM Term
    tcWithReconstructed (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    u) (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    v))
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMWithExpandLast,    Term -> Term -> UnquoteM Term
    tcWithExpandLast (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    u) (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    v))
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMWithReduceDefs,    Term -> Term -> UnquoteM Term
    tcWithReduceDefs (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    u) (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    v))
                 , (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMInContext,         Term -> Term -> UnquoteM Term
    tcInContext     (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    u) (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    v))
                 ]
                 UnquoteM Term
    failEval
        I.Def QName
    f [Elim
    _, Elim
    _, Elim
    u, Elim
    v, Elim
    w] ->
          [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice [ (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMExtendContext, Term -> Term -> Term -> UnquoteM Term
    tcExtendContext (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    u) (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    v) (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    w))
                 ]
                 UnquoteM Term
    failEval
        I.Def QName
    f [Elim
    _, Elim
    _, Elim
    _, Elim
    _, Elim
    m, Elim
    k] ->
          [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
    forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
    choice [ (QName
    f QName -> TCM (Maybe Term) -> UnquoteM Bool
    `isDef` BuiltinId -> TCM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinAgdaTCMBind, Term -> Term -> UnquoteM Term
    tcBind (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    m) (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    k)) ]
                 UnquoteM Term
    failEval
        Term
    _ -> UnquoteM Term
    failEval
      where
        unElim :: Elim' c -> c
    unElim = Arg c -> c
    forall e. Arg e -> e
    unArg (Arg c -> c) -> (Elim' c -> Arg c) -> Elim' c -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg c -> Maybe (Arg c) -> Arg c
    forall a. a -> Maybe a -> a
    fromMaybe Arg c
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (Arg c) -> Arg c)
    -> (Elim' c -> Maybe (Arg c)) -> Elim' c -> Arg c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim' c -> Maybe (Arg c)
    forall a. Elim' a -> Maybe (Arg a)
    isApplyElim
        tcBind :: Term -> Term -> UnquoteM Term
    tcBind Term
    m Term
    k = do v <- Term -> UnquoteM Term
    evalTCM Term
    m
                        evalTCM (k `apply` [defaultArg v])

        process :: (InstantiateFull a, Normalise a) => a -> TCM a
        process :: forall a. (InstantiateFull a, Normalise a) => a -> TCM a
    process a
    v = do
          norm <- Lens' TCEnv Bool -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eUnquoteNormalise
          if norm then normalise v else instantiateFull v

        mkT :: t -> a -> Type'' t a
    mkT t
    l a
    a = Sort' t -> a -> Type'' t a
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' t
    s a
    a
          where s :: Sort' t
    s = Level' t -> Sort' t
    forall t. Level' t -> Sort' t
    Type (Level' t -> Sort' t) -> Level' t -> Sort' t
    forall a b. (a -> b) -> a -> b
    $ t -> Level' t
    forall t. t -> Level' t
    atomicLevel t
    l

        -- Don't catch Unquote errors!
        tcCatchError :: Term -> Term -> UnquoteM Term
        tcCatchError :: Term -> Term -> UnquoteM Term
    tcCatchError Term
    m Term
    h =
          (TCM (UnquoteRes Term)
     -> TCM (UnquoteRes Term) -> TCM (UnquoteRes Term))
    -> UnquoteM Term -> UnquoteM Term -> UnquoteM Term
    forall a b c.
    (TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c))
    -> UnquoteM a -> UnquoteM b -> UnquoteM c
    liftU2 (\ TCM (UnquoteRes Term)
    m1 TCM (UnquoteRes Term)
    m2 -> TCM (UnquoteRes Term)
    m1 TCM (UnquoteRes Term)
    -> (TCErr -> TCM (UnquoteRes Term)) -> TCM (UnquoteRes Term)
    forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \ TCErr
    _ -> TCM (UnquoteRes Term)
    m2) (Term -> UnquoteM Term
    evalTCM Term
    m) (Term -> UnquoteM Term
    evalTCM Term
    h)

        tcAskLens :: ToTerm a => Lens' TCEnv a -> UnquoteM Term
        tcAskLens :: forall a. ToTerm a => Lens' TCEnv a -> UnquoteM Term
    tcAskLens Lens' TCEnv a
    l = TCMT IO Term -> UnquoteM Term
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ do
          toTm <- TCM (a -> TCMT IO Term)
    forall a. ToTerm a => TCM (a -> TCMT IO Term)
    toTermTCM
          toTm =<< asksTC (\ TCEnv
    e -> TCEnv
    e TCEnv -> Lens' TCEnv a -> a
    forall o i. o -> Lens' o i -> i
    ^. (a -> f a) -> TCEnv -> f TCEnv
    Lens' TCEnv a
    l)

        tcWithLens :: Unquote a => Lens' TCEnv a -> Term -> Term -> UnquoteM Term
        tcWithLens :: forall a.
    Unquote a =>
    Lens' TCEnv a -> Term -> Term -> UnquoteM Term
    tcWithLens Lens' TCEnv a
    l Term
    b Term
    m = do
          v <- Term -> UnquoteM a
    forall a. Unquote a => Term -> UnquoteM a
    unquote Term
    b
          liftU1 (locallyTC l $ const v) (evalTCM m)

        tcWithNormalisation, tcWithReconstructed, tcWithExpandLast, tcWithReduceDefs :: Term -> Term -> UnquoteM Term
        tcWithNormalisation :: Term -> Term -> UnquoteM Term
    tcWithNormalisation = Lens' TCEnv Bool -> Term -> Term -> UnquoteM Term
    forall a.
    Unquote a =>
    Lens' TCEnv a -> Term -> Term -> UnquoteM Term
    tcWithLens (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eUnquoteNormalise
        tcWithReconstructed :: Term -> Term -> UnquoteM Term
    tcWithReconstructed = Lens' TCEnv Bool -> Term -> Term -> UnquoteM Term
    forall a.
    Unquote a =>
    Lens' TCEnv a -> Term -> Term -> UnquoteM Term
    tcWithLens (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eReconstructed
        tcWithExpandLast :: Term -> Term -> UnquoteM Term
    tcWithExpandLast    = Lens' TCEnv Bool -> Term -> Term -> UnquoteM Term
    forall a.
    Unquote a =>
    Lens' TCEnv a -> Term -> Term -> UnquoteM Term
    tcWithLens (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eExpandLastBool
        tcWithReduceDefs :: Term -> Term -> UnquoteM Term
    tcWithReduceDefs    = Lens' TCEnv (Bool, [QName]) -> Term -> Term -> UnquoteM Term
    forall a.
    Unquote a =>
    Lens' TCEnv a -> Term -> Term -> UnquoteM Term
    tcWithLens ((Bool, [QName]) -> f (Bool, [QName])) -> TCEnv -> f TCEnv
    Lens' TCEnv (Bool, [QName])
    eReduceDefsPair

        tcAskNormalisation, tcAskReconstructed, tcAskExpandLast, tcAskReduceDefs :: UnquoteM Term
        tcAskNormalisation :: UnquoteM Term
    tcAskNormalisation = Lens' TCEnv Bool -> UnquoteM Term
    forall a. ToTerm a => Lens' TCEnv a -> UnquoteM Term
    tcAskLens (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eUnquoteNormalise
        tcAskReconstructed :: UnquoteM Term
    tcAskReconstructed = Lens' TCEnv Bool -> UnquoteM Term
    forall a. ToTerm a => Lens' TCEnv a -> UnquoteM Term
    tcAskLens (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eReconstructed
        tcAskExpandLast :: UnquoteM Term
    tcAskExpandLast    = Lens' TCEnv Bool -> UnquoteM Term
    forall a. ToTerm a => Lens' TCEnv a -> UnquoteM Term
    tcAskLens (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eExpandLastBool
        tcAskReduceDefs :: UnquoteM Term
    tcAskReduceDefs    = Lens' TCEnv (Bool, [QName]) -> UnquoteM Term
    forall a. ToTerm a => Lens' TCEnv a -> UnquoteM Term
    tcAskLens ((Bool, [QName]) -> f (Bool, [QName])) -> TCEnv -> f TCEnv
    Lens' TCEnv (Bool, [QName])
    eReduceDefsPair

        uqFun1 :: Unquote a => (a -> UnquoteM b) -> Elim -> UnquoteM b
        uqFun1 :: forall a b. Unquote a => (a -> UnquoteM b) -> Elim -> UnquoteM b
    uqFun1 a -> UnquoteM b
    fun Elim
    a = do
          a <- Term -> UnquoteM a
    forall a. Unquote a => Term -> UnquoteM a
    unquote (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    a)
          fun a

        tcFun1 :: Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
        tcFun1 :: forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
    tcFun1 a -> TCM b
    fun = (a -> UnquoteM b) -> Elim -> UnquoteM b
    forall a b. Unquote a => (a -> UnquoteM b) -> Elim -> UnquoteM b
    uqFun1 (TCM b -> UnquoteM b
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM b -> UnquoteM b) -> (a -> TCM b) -> a -> UnquoteM b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> TCM b
    fun)

        uqFun2 :: (Unquote a, Unquote b) => (a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
        uqFun2 :: forall a b c.
    (Unquote a, Unquote b) =>
    (a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
    uqFun2 a -> b -> UnquoteM c
    fun Elim
    a Elim
    b = do
          a <- Term -> UnquoteM a
    forall a. Unquote a => Term -> UnquoteM a
    unquote (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    a)
          b <- unquote (unElim b)
          fun a b

        uqFun3 :: (Unquote a, Unquote b, Unquote c) => (a -> b -> c -> UnquoteM d) -> Elim -> Elim -> Elim -> UnquoteM d
        uqFun3 :: forall a b c d.
    (Unquote a, Unquote b, Unquote c) =>
    (a -> b -> c -> UnquoteM d) -> Elim -> Elim -> Elim -> UnquoteM d
    uqFun3 a -> b -> c -> UnquoteM d
    fun Elim
    a Elim
    b Elim
    c = do
          a <- Term -> UnquoteM a
    forall a. Unquote a => Term -> UnquoteM a
    unquote (Elim -> Term
    forall {c}. Elim' c -> c
    unElim Elim
    a)
          b <- unquote (unElim b)
          c <- unquote (unElim c)
          fun a b c

        tcFun2 :: (Unquote a, Unquote b) => (a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
        tcFun2 :: forall a b c.
    (Unquote a, Unquote b) =>
    (a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
    tcFun2 a -> b -> TCM c
    fun = (a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
    forall a b c.
    (Unquote a, Unquote b) =>
    (a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
    uqFun2 (\ a
    x b
    y -> TCM c -> UnquoteM c
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (a -> b -> TCM c
    fun a
    x b
    y))

        tcFun3 :: (Unquote a, Unquote b, Unquote c) => (a -> b -> c -> TCM d) -> Elim -> Elim -> Elim -> UnquoteM d
        tcFun3 :: forall a b c d.
    (Unquote a, Unquote b, Unquote c) =>
    (a -> b -> c -> TCM d) -> Elim -> Elim -> Elim -> UnquoteM d
    tcFun3 a -> b -> c -> TCM d
    fun = (a -> b -> c -> UnquoteM d) -> Elim -> Elim -> Elim -> UnquoteM d
    forall a b c d.
    (Unquote a, Unquote b, Unquote c) =>
    (a -> b -> c -> UnquoteM d) -> Elim -> Elim -> Elim -> UnquoteM d
    uqFun3 (\ a
    x b
    y c
    z -> TCM d -> UnquoteM d
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (a -> b -> c -> TCM d
    fun a
    x b
    y c
    z))

        tcFreshName :: Text -> TCM Term
        tcFreshName :: ExeName -> TCMT IO Term
    tcFreshName ExeName
    s = do
          TCMT IO Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (Lens' TCEnv Bool -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
    viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eCurrentlyElaborating) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TypeError
    NotSupported [Char]
    "declaring new names from an edit-time macro"
          m <- TCMT IO ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
          quoteName . qualify m <$> freshName_ (T.unpack s)

        tcUnify :: R.Term -> R.Term -> TCM Term
        tcUnify :: Type -> Type -> TCMT IO Term
    tcUnify Type
    u Type
    v = do
          (u, a) <- TCMT IO (Term, Type) -> TCMT IO (Term, Type)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    locallyReduceAllDefs (TCMT IO (Term, Type) -> TCMT IO (Term, Type))
    -> TCMT IO (Term, Type) -> TCMT IO (Term, Type)
    forall a b. (a -> b) -> a -> b
    $ Expr -> TCMT IO (Term, Type)
    inferExpr        (Expr -> TCMT IO (Term, Type)) -> TCM Expr -> TCMT IO (Term, Type)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> TCMT IO (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
     MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
     HasConstInfo m) =>
    r -> m (AbsOfRef r)
    toAbstract_ Type
    u
          v      <- locallyReduceAllDefs $ flip checkExpr a =<< toAbstract_ v
          equalTerm a u v
          primUnitUnit

        tcBlock :: Blocker -> UnquoteM Term
        tcBlock :: Blocker -> UnquoteM Term
    tcBlock Blocker
    x = do
          s <- (UnquoteState -> TCState)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         TCState
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets UnquoteState -> TCState
    forall a b. (a, b) -> b
    snd
          liftTCM $ reportSDoc "tc.unquote.block" 10 $ pretty (show x)
          throwError (BlockedOnMeta s x)

        tcCommit :: UnquoteM Term
        tcCommit :: UnquoteM Term
    tcCommit = do
          dirty <- (UnquoteState -> Dirty)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Dirty
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets UnquoteState -> Dirty
    forall a b. (a, b) -> a
    fst
          when (dirty == Dirty) $ throwError CommitAfterDef
          s <- getTC
          modify (second $ const s)
          liftTCM primUnitUnit

        tcFormatErrorParts :: [ErrorPart] -> TCM Term
        tcFormatErrorParts :: [ErrorPart] -> TCMT IO Term
    tcFormatErrorParts [ErrorPart]
    msg = [Char] -> Term
    quoteString ([Char] -> Term) -> (Doc -> [Char]) -> Doc -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (Doc -> Term) -> TCMT IO Doc -> TCMT IO Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [ErrorPart] -> TCMT IO Doc
    renderErrorParts [ErrorPart]
    msg

        tcTypeError :: [ErrorPart] -> TCM a
        tcTypeError :: forall a. [ErrorPart] -> TCM a
    tcTypeError [ErrorPart]
    err = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [ErrorPart] -> TCMT IO Doc
    renderErrorParts [ErrorPart]
    err

        tcDebugPrint :: Text -> Integer -> [ErrorPart] -> TCM Term
        tcDebugPrint :: ExeName -> Integer -> [ErrorPart] -> TCMT IO Term
    tcDebugPrint ExeName
    s Integer
    n [ErrorPart]
    msg = do
          [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    alwaysReportSDoc (ExeName -> [Char]
    T.unpack ExeName
    s) (Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Integer
    n) (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [ErrorPart] -> TCMT IO Doc
    renderErrorParts [ErrorPart]
    msg
          TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primUnitUnit

        tcNoConstraints :: Term -> UnquoteM Term
        tcNoConstraints :: Term -> UnquoteM Term
    tcNoConstraints Term
    m = (TCM (UnquoteRes Term) -> TCM (UnquoteRes Term))
    -> UnquoteM Term -> UnquoteM Term
    forall a b.
    (TCM (UnquoteRes a) -> TCM (UnquoteRes b))
    -> UnquoteM a -> UnquoteM b
    liftU1 TCM (UnquoteRes Term) -> TCM (UnquoteRes Term)
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    reallyNoConstraints (Term -> UnquoteM Term
    evalTCM Term
    m)

        tcWorkOnTypes :: Term -> UnquoteM Term
        tcWorkOnTypes :: Term -> UnquoteM Term
    tcWorkOnTypes Term
    m = (TCM (UnquoteRes Term) -> TCM (UnquoteRes Term))
    -> UnquoteM Term -> UnquoteM Term
    forall a b.
    (TCM (UnquoteRes a) -> TCM (UnquoteRes b))
    -> UnquoteM a -> UnquoteM b
    liftU1 TCM (UnquoteRes Term) -> TCM (UnquoteRes Term)
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    workOnTypes (Term -> UnquoteM Term
    evalTCM Term
    m)

        tcInferType :: R.Term -> TCM Term
        tcInferType :: Type -> TCMT IO Term
    tcInferType Type
    v = do
          r <- TCMT IO Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    isReconstructed
          (_, a) <- inferExpr =<< toAbstract_ v
          if r then do
            a <- process a
            a <- locallyReduceAllDefs $ reconstructParametersInType a
            reportSDoc "tc.reconstruct" 50 $ "Infer after reconstruct:"
              <+> pretty a
            locallyReconstructed (quoteType a)
          else
            quoteType =<< process a

        tcCheckType :: R.Term -> R.Type -> TCM Term
        tcCheckType :: Type -> Type -> TCMT IO Term
    tcCheckType Type
    v Type
    a = do
          r <- TCMT IO Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    isReconstructed
          a <- workOnTypes $ locallyReduceAllDefs $ isType_ =<< toAbstract_ a
          e <- toAbstract_ v
          v <- checkExpr e a
          if r then do
            v <- process v
            v <- locallyReduceAllDefs $ reconstructParameters a v
            locallyReconstructed (quoteTerm v)
          else
            quoteTerm =<< process v

        tcCheckFromString :: Text -> R.Type -> TCM Term
        tcCheckFromString :: ExeName -> Type -> TCMT IO Term
    tcCheckFromString ExeName
    str Type
    a = do
          (C.ExprWhere c wh , _) <- PM (ExprWhere, Attributes) -> TCM (ExprWhere, Attributes)
    forall a. PM a -> TCM a
    runPM (PM (ExprWhere, Attributes) -> TCM (ExprWhere, Attributes))
    -> PM (ExprWhere, Attributes) -> TCM (ExprWhere, Attributes)
    forall a b. (a -> b) -> a -> b
    $ Parser ExprWhere
    -> Position -> [Char] -> PM (ExprWhere, Attributes)
    forall a. Parser a -> Position -> [Char] -> PM (a, Attributes)
    parsePosString Parser ExprWhere
    exprWhereParser (Maybe RangeFile -> Position
    startPos Maybe RangeFile
    forall a. Maybe a
    Nothing) (ExeName -> [Char]
    T.unpack ExeName
    str)
          r <- isReconstructed
          e <- concreteToAbstract_ c
          a <- workOnTypes $ locallyReduceAllDefs $ isType_ =<< toAbstract_ a

          v <- checkExpr e a
          if r then do
            v <- process v
            v <- locallyReduceAllDefs $ reconstructParameters a v
            locallyReconstructed (quoteTerm v)
          else
            quoteTerm =<< process v

        tcQuoteTerm :: Type -> Term -> UnquoteM Term
        tcQuoteTerm :: Type -> Term -> UnquoteM Term
    tcQuoteTerm Type
    a Term
    v = TCMT IO Term -> UnquoteM Term
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ do
          r <- TCMT IO Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    isReconstructed
          if r then do
            v <- process v
            v <- locallyReduceAllDefs $ reconstructParameters a v
            locallyReconstructed (quoteTerm v)
          else
            quoteTerm =<< process v

        tcUnquoteTerm :: Type -> R.Term -> TCM Term
        tcUnquoteTerm :: Type -> Type -> TCMT IO Term
    tcUnquoteTerm Type
    a Type
    v = do
          e <- Type -> TCMT IO (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
     MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
     HasConstInfo m) =>
    r -> m (AbsOfRef r)
    toAbstract_ Type
    v
          checkExpr e a

        tcNormalise :: R.Term -> TCM Term
        tcNormalise :: Type -> TCMT IO Term
    tcNormalise Type
    v = do
          r <- TCMT IO Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    isReconstructed
          (v, t) <- locallyReduceAllDefs $ inferExpr  =<< toAbstract_ v
          if r then do
            v <- normalise v
            t <- normalise t
            v <- locallyReduceAllDefs $ reconstructParameters' defaultAction t v
            reportSDoc "tc.reconstruct" 50 $ "Normalise reconstruct:" <+> pretty v
            locallyReconstructed $ quoteTerm v
          else
           quoteTerm =<< normalise v

        tcReduce :: R.Term -> TCM Term
        tcReduce :: Type -> TCMT IO Term
    tcReduce Type
    v = do
          r <- TCMT IO Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    isReconstructed
          (v, t) <- locallyReduceAllDefs $ inferExpr =<< toAbstract_ v
          if r then do
            v <- reduce =<< instantiateFull v
            t <- reduce =<< instantiateFull t
            v <- locallyReduceAllDefs $ reconstructParameters' defaultAction t v
            reportSDoc "tc.reconstruct" 50 $ "Reduce reconstruct:" <+> pretty v
            locallyReconstructed $ quoteTerm v
          else
            quoteTerm =<< reduce =<< instantiateFull v

        tcGetContext :: UnquoteM Term
        tcGetContext :: UnquoteM Term
    tcGetContext = TCMT IO Term -> UnquoteM Term
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ do
          r <- TCMT IO Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    isReconstructed
          let getVar (CtxVar Name
    x Dom Type
    a) = (Name -> [Char]
    nameToArgName Name
    x, Dom Type
    a)
          as <- map getVar <$> getContext
          as <- etaContract =<< process as
          if r then do
            as <- recons (reverse as)
            locallyReconstructed $ buildList <*> mapM quoteDomWithName as
          else
            buildList <*> mapM quoteDomWithName as
          where
            recons :: [(ArgName, Dom Type)] -> TCM [(ArgName, Dom Type)]
            recons :: [([Char], Dom Type)] -> TCMT IO [([Char], Dom Type)]
    recons []                        = [([Char], Dom Type)] -> TCMT IO [([Char], Dom Type)]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
            recons (([Char]
    s, d :: Dom Type
    d@Dom {unDom :: forall t e. Dom' t e -> e
    unDom=Type
    t}):[([Char], Dom Type)]
    ds) = do
              t <- TCM Type -> TCM Type
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    locallyReduceAllDefs (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Type -> TCM Type
    reconstructParametersInType Type
    t
              let d' = Dom Type
    d{unDom=t}
              ds' <- addContext (s, d') $ recons ds
              return $ (s, d'):ds'

            quoteDomWithName :: (ArgName, Dom Type) -> TCM Term
            quoteDomWithName :: ([Char], Dom Type) -> TCMT IO Term
    quoteDomWithName ([Char]
    x, Dom Type
    a) = do
              toTm <- TCM ((ExeName, Dom Type) -> TCMT IO Term)
    forall a. ToTerm a => TCM (a -> TCMT IO Term)
    toTermTCM
              toTm (T.pack x, a)

        extendCxt :: Text -> Arg R.Type -> UnquoteM a -> UnquoteM a
        extendCxt :: forall a. ExeName -> Arg Type -> UnquoteM a -> UnquoteM a
    extendCxt ExeName
    s' Arg Type
    a UnquoteM a
    m = Range -> [Char] -> (Name -> UnquoteM a) -> UnquoteM a
    forall a.
    Range
    -> [Char]
    -> (Name
        -> ReaderT
             Context
             (StateT
                UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
             a)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> [Char] -> (Name -> m a) -> m a
    withFreshName Range
    forall a. Range' a
    noRange (ExeName -> [Char]
    T.unpack ExeName
    s') ((Name -> UnquoteM a) -> UnquoteM a)
    -> (Name -> UnquoteM a) -> UnquoteM a
    forall a b. (a -> b) -> a -> b
    $ \Name
    s -> do
          a <- ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Arg Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Arg Type)
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    workOnTypes (ReaderT
       Context
       (StateT
          UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
       (Arg Type)
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          (Arg Type))
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Arg Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Arg Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Arg Type)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    locallyReduceAllDefs (ReaderT
       Context
       (StateT
          UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
       (Arg Type)
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          (Arg Type))
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Arg Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ TCM (Arg Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Arg Type)
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Arg Type)
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          (Arg Type))
    -> TCM (Arg Type)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ (Type -> TCM Type) -> Arg Type -> TCM (Arg Type)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse (Expr -> TCM Type
    isType_ (Expr -> TCM Type) -> (Type -> TCM Expr) -> Type -> TCM Type
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Type -> TCM Expr
    Type -> TCMT IO (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
     MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
     HasConstInfo m) =>
    r -> m (AbsOfRef r)
    toAbstract_) Arg Type
    a

          locallyScope scopeLocals ((simpleName (T.unpack s') , LocalVar s MacroBound []) :)
              $ liftU1 (addContext (s, domFromArg a :: Dom Type)) m

        tcExtendContext :: Term -> Term -> Term -> UnquoteM Term
        tcExtendContext :: Term -> Term -> Term -> UnquoteM Term
    tcExtendContext Term
    s Term
    a Term
    m = do
          s <- Term -> UnquoteM ExeName
    forall a. Unquote a => Term -> UnquoteM a
    unquote Term
    s
          a <- unquote a
          fmap (strengthen impossible) $ extendCxt s a $ do
            v <- evalTCM $ raise 1 m
            -- 2024-04-20: free variable analysis only really makes sense on normal forms; see #7227
            v <- normalise v
            when (freeIn 0 v) $ liftTCM $ genericDocError =<<
              hcat ["Local variable '", prettyTCM (var 0), "' escaping in result of extendContext:"]
                <?> prettyTCM v
            return v

        tcInContext :: Term -> Term -> UnquoteM Term
        tcInContext :: Term -> Term -> UnquoteM Term
    tcInContext Term
    c Term
    m = do
          c <- Term
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         [(ExeName, Arg Type)]
    forall a. Unquote a => Term -> UnquoteM a
    unquote Term
    c
          inOriginalContext $ go c (evalTCM m)
          where
            go :: [(Text , Arg R.Type)] -> UnquoteM Term -> UnquoteM Term
            go :: [(ExeName, Arg Type)] -> UnquoteM Term -> UnquoteM Term
    go []             UnquoteM Term
    m = UnquoteM Term
    m
            go ((ExeName
    s , Arg Type
    a) : [(ExeName, Arg Type)]
    as) UnquoteM Term
    m = [(ExeName, Arg Type)] -> UnquoteM Term -> UnquoteM Term
    go [(ExeName, Arg Type)]
    as (ExeName -> Arg Type -> UnquoteM Term -> UnquoteM Term
    forall a. ExeName -> Arg Type -> UnquoteM a -> UnquoteM a
    extendCxt ExeName
    s Arg Type
    a UnquoteM Term
    m)

        constInfo :: QName -> TCM Definition
        constInfo :: QName -> TCM Definition
    constInfo QName
    x = (SigError -> TCM Definition)
    -> (Definition -> TCM Definition)
    -> Either SigError Definition
    -> TCM Definition
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either SigError -> TCM Definition
    err Definition -> TCM Definition
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either SigError Definition -> TCM Definition)
    -> TCMT IO (Either SigError Definition) -> TCM Definition
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    x
          where err :: SigError -> TCM Definition
    err SigError
    _ = UnquoteError -> TCM Definition
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    UnquoteError -> m a
    unquoteError (UnquoteError -> TCM Definition) -> UnquoteError -> TCM Definition
    forall a b. (a -> b) -> a -> b
    $ QName -> UnquoteError
    UnboundName QName
    x

        tcGetType :: QName -> TCM Term
        tcGetType :: QName -> TCMT IO Term
    tcGetType QName
    x = do
          r  <- TCMT IO Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    isReconstructed
          ci <- constInfo x >>= instantiateDef
          let t = Definition -> Type
    defType Definition
    ci
          if r then do
            t <- locallyReduceAllDefs $ reconstructParametersInType t
            quoteType t
          else
            quoteType t

        tcIsMacro :: QName -> TCM Term
        tcIsMacro :: QName -> TCMT IO Term
    tcIsMacro QName
    x = do
          true  <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primTrue
          false <- primFalse
          let qBool Bool
    True  = Term
    true
              qBool Bool
    False = Term
    false
          qBool . isMacro . theDef <$> constInfo x

        tcGetDefinition :: QName -> TCM Term
        tcGetDefinition :: QName -> TCMT IO Term
    tcGetDefinition QName
    x = do
          r <- TCMT IO Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    isReconstructed
          if r then
            tcGetDefinitionRecons x
          else
            quoteDefn =<< instantiateDef =<< constInfo x

        tcGetDefinitionRecons :: QName -> TCM Term
        tcGetDefinitionRecons :: QName -> TCMT IO Term
    tcGetDefinitionRecons QName
    x = do
          ci@(Defn {theDef=d}) <- QName -> TCM Definition
    constInfo QName
    x TCM Definition -> (Definition -> TCM Definition) -> TCM Definition
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Definition -> TCM Definition
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    Definition -> m Definition
    instantiateDef
          case d of
            f :: Defn
    f@(Function {funClauses :: Defn -> [Clause]
    funClauses=[Clause]
    cs}) -> do
              cs' <- (Clause -> TCMT IO Clause) -> [Clause] -> TCMT IO [Clause]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Clause -> TCMT IO Clause
    reconsClause [Clause]
    cs
              locallyReconstructed $ quoteDefn ci{theDef=f{funClauses=cs'}}

            Defn
    _ -> Definition -> TCMT IO Term
    quoteDefn Definition
    ci

          where
            reconsClause :: Clause -> TCM Clause
            reconsClause :: Clause -> TCMT IO Clause
    reconsClause Clause
    c = do
              tel' <- Tele (Dom Type) -> TCM (Tele (Dom Type))
    reconsTel (Tele (Dom Type) -> TCM (Tele (Dom Type)))
    -> Tele (Dom Type) -> TCM (Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $ Clause -> Tele (Dom Type)
    clauseTel Clause
    c
              b' <- case (clauseType c, clauseBody c) of
                    (Just Arg Type
    t, Just Term
    b) ->
                      Tele (Dom Type) -> TCM (Maybe Term) -> TCM (Maybe Term)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Tele (Dom Type) -> m a -> m a
    addContext (Clause -> Tele (Dom Type)
    clauseTel Clause
    c) (TCM (Maybe Term) -> TCM (Maybe Term))
    -> TCM (Maybe Term) -> TCM (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ do
                         bb <- TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    locallyReduceAllDefs
                               (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ Action (TCMT IO) -> Type -> Term -> TCMT IO Term
    reconstructParameters' Action (TCMT IO)
    forall (m :: * -> *). PureTCM m => Action m
    defaultAction (Arg Type -> Type
    forall e. Arg e -> e
    unArg Arg Type
    t) Term
    b
                         return $ Just bb
                    (Maybe (Arg Type), Maybe Term)
    _ -> Maybe Term -> TCM (Maybe Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Term -> TCM (Maybe Term)) -> Maybe Term -> TCM (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ Clause -> Maybe Term
    clauseBody Clause
    c
              let c' = Clause
    c{clauseBody=b', clauseTel=tel'}
              reportSDoc "tc.reconstruct" 50
                       $ "getDefinition reconstructed clause:" <+> pretty c'
              return c'

            reconsTel :: Telescope -> TCM Telescope
            reconsTel :: Tele (Dom Type) -> TCM (Tele (Dom Type))
    reconsTel Tele (Dom Type)
    EmptyTel = Tele (Dom Type) -> TCM (Tele (Dom Type))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Tele (Dom Type)
    forall a. Tele a
    EmptyTel
            reconsTel (ExtendTel Dom Type
    _ NoAbs{}) = TCM (Tele (Dom Type))
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            reconsTel (ExtendTel (d :: Dom Type
    d@Dom{unDom :: forall t e. Dom' t e -> e
    unDom=Type
    t}) ds :: Abs (Tele (Dom Type))
    ds@Abs{unAbs :: forall a. Abs a -> a
    unAbs=Tele (Dom Type)
    ts}) = do
               t <- TCM Type -> TCM Type
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    locallyReduceAllDefs (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Type -> TCM Type
    reconstructParametersInType Type
    t
               let d' = Dom Type
    d{unDom=t}
               ts' <- addContext d' $ reconsTel ts
               return $ ExtendTel d' ds{unAbs=ts'}

        setDirty :: UnquoteM ()
        setDirty :: ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ()
    setDirty = (UnquoteState -> UnquoteState)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((Dirty -> Dirty) -> UnquoteState -> UnquoteState
    forall b c d. (b -> c) -> (b, d) -> (c, d)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first ((Dirty -> Dirty) -> UnquoteState -> UnquoteState)
    -> (Dirty -> Dirty) -> UnquoteState -> UnquoteState
    forall a b. (a -> b) -> a -> b
    $ Dirty -> Dirty -> Dirty
    forall a b. a -> b -> a
    const Dirty
    Dirty)

        tcDeclareDef_ :: Arg QName -> R.Type -> String -> Defn -> UnquoteM Term
        tcDeclareDef_ :: Arg QName -> Type -> [Char] -> Defn -> UnquoteM Term
    tcDeclareDef_ (Arg ArgInfo
    i QName
    x) Type
    a [Char]
    doc Defn
    defn = UnquoteM Term -> UnquoteM Term
    forall a. UnquoteM a -> UnquoteM a
    inOriginalContext (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ do
          ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ()
    setDirty
          Bool
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (ArgInfo -> Bool
    forall a. LensHiding a => a -> Bool
    hidden ArgInfo
    i) (ReaderT
       Context
       (StateT
          UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
       ()
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          ())
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO ()
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO ()
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          ())
    -> TCMT IO ()
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall a b. (a -> b) -> a -> b
    $ UnquoteError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    UnquoteError -> m a
    unquoteError (UnquoteError -> TCMT IO ()) -> UnquoteError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> UnquoteError
    CannotDeclareHiddenFunction QName
    x
          [QName]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [QName
    x]
          TCMT IO Term -> UnquoteM Term
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ do
            [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    alwaysReportSDoc [Char]
    "tc.unquote.decl" Int
    10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
              [ TCMT IO Doc
    "declare" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    doc TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":"
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall r (m :: * -> *).
    (ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m,
     MonadError TCErr m) =>
    r -> m Doc
    prettyR Type
    a
              ]
            a <- TCM Type -> TCM Type
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    locallyReduceAllDefs (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Expr -> TCM Type
    isType_ (Expr -> TCM Type) -> TCM Expr -> TCM Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> TCMT IO (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
     MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
     HasConstInfo m) =>
    r -> m (AbsOfRef r)
    toAbstract_ Type
    a
            getConstInfo' x >>= \case
              Left SigError
    _    -> () -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
              Right Definition
    def -> TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> QName -> Maybe NiceDeclaration -> TypeError
    ClashingDefinition (QName -> QName
    qnameToConcrete QName
    x) (Definition -> QName
    defName Definition
    def) Maybe NiceDeclaration
    forall a. Maybe a
    Nothing
            addConstant' x i a defn
            when (isInstance i) $ addTypedInstance x a
            primUnitUnit

        tcDeclareDef :: Arg QName -> R.Type -> UnquoteM Term
        tcDeclareDef :: Arg QName -> Type -> UnquoteM Term
    tcDeclareDef Arg QName
    arg Type
    a = Arg QName -> Type -> [Char] -> Defn -> UnquoteM Term
    tcDeclareDef_ Arg QName
    arg Type
    a [Char]
    "" (Defn -> UnquoteM Term)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Defn
    -> UnquoteM Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Defn
    forall (m :: * -> *). HasOptions m => m Defn
    emptyFunction

        tcDeclarePostulate :: Arg QName -> R.Type -> UnquoteM Term
        tcDeclarePostulate :: Arg QName -> Type -> UnquoteM Term
    tcDeclarePostulate arg :: Arg QName
    arg@(Arg ArgInfo
    i QName
    x) Type
    a = do
          clo <- ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
          when (Lens.getSafeMode clo) $ liftTCM $ warning $ SafeFlagPostulate x
          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.
        tcDeclareData :: QName -> Integer -> R.Type -> UnquoteM Term
        tcDeclareData :: QName -> Integer -> Type -> UnquoteM Term
    tcDeclareData QName
    x Integer
    npars Type
    t = UnquoteM Term -> UnquoteM Term
    forall a. UnquoteM a -> UnquoteM a
    inOriginalContext (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ do
          ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ()
    setDirty
          [QName]
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell [QName
    x]
          [Char]
    -> Int
    -> TCMT IO Doc
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    alwaysReportSDoc [Char]
    "tc.unquote.decl" Int
    10 (TCMT IO Doc
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          ())
    -> TCMT IO Doc
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "declare Data" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":"
            , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall r (m :: * -> *).
    (ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m,
     MonadError TCErr m) =>
    r -> m Doc
    prettyR Type
    t
            ]
          QName
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    x ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Either SigError Definition)
    -> (Either SigError Definition
        -> ReaderT
             Context
             (StateT
                UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
             ())
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      a
    -> (a
        -> ReaderT
             Context
             (StateT
                UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
             b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Left SigError
    _    -> ()
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
            Right Definition
    def -> TCMT IO ()
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO ()
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          ())
    -> TCMT IO ()
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> QName -> Maybe NiceDeclaration -> TypeError
    ClashingDefinition (QName -> QName
    qnameToConcrete QName
    x) (Definition -> QName
    defName Definition
    def) Maybe NiceDeclaration
    forall a. Maybe a
    Nothing
          e <- TCM Expr
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Expr
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Expr
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Expr)
    -> TCM Expr
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Expr
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO (AbsOfRef Type)
    forall r (m :: * -> *).
    (ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
     MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
     HasConstInfo m) =>
    r -> m (AbsOfRef r)
    toAbstract_ Type
    t
          -- The type to be checked with @checkSig@ is without parameters.
          (tel, e') <- splitPars (fromInteger npars) e
          ac <- asksTC (^. lensIsAbstract)
          let defIn = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
    forall t.
    Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
    mkDefInfo (Name -> Name
    nameConcrete (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    x) Fixity'
    noFixity' Access
    PublicAccess IsAbstract
    ac Range
    forall a. Range' a
    noRange
          liftTCM $ checkSig DataName defIn defaultErased x (A.GeneralizeTel Map.empty tel) e'
          liftTCM primUnitUnit

        tcDefineData :: QName -> [(QName, (Quantity, R.Type))] -> UnquoteM Term
        tcDefineData :: QName -> [(QName, (Quantity, Type))] -> UnquoteM Term
    tcDefineData QName
    x [(QName, (Quantity, Type))]
    cs = UnquoteM Term -> UnquoteM Term
    forall a. UnquoteM a -> UnquoteM a
    inOriginalContext (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ (ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ()
    setDirty ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ()
    -> UnquoteM Term -> UnquoteM Term
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>) (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ QName
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    x ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Either SigError Definition)
    -> (Either SigError Definition -> UnquoteM Term) -> UnquoteM Term
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      a
    -> (a
        -> ReaderT
             Context
             (StateT
                UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
             b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Left SigError
    _    -> UnquoteError -> UnquoteM Term
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM Term) -> UnquoteError -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ QName -> UnquoteError
    MissingDeclaration QName
    x
          Right Definition
    def -> do
            npars <- case Definition -> Defn
    theDef Definition
    def of
                       DataOrRecSig Int
    n -> Int
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Int
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    n
                       Defn
    _              -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Int
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          Int)
    -> UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         Int
    forall a b. (a -> b) -> a -> b
    $ QName -> UnquoteError
    DefineDataNotData QName
    x

            -- For some reasons, reifying parameters and adding them to the context via
            -- `addContext` before `toAbstract_` is different from substituting the type after
            -- `toAbstract_, so some dummy parameters are added and removed later.
            es <- liftTCM $ mapM (toAbstract_ . addDummy npars . snd . snd) cs
            alwaysReportSDoc "tc.unquote.def" 10 $ vcat $
              [ "declaring constructors of" <+> prettyTCM x <+> ":" ] ++ map prettyA es

            -- Translate parameters from internal definitions back to abstract syntax.
            t   <- instantiateFull . defType =<< instantiateDef def
            tel <- reify =<< theTel <$> telViewUpTo npars t

            es' <- forM es \ Expr
    e -> do
              (ptel, core) <- Int -> Expr -> UnquoteM ([TypedBinding], Expr)
    splitPars Int
    npars Expr
    e
              -- Mario, 2024-10-18: cannot trigger this error:
              -- genericError "Number of parameters doesn't match!"
              return $ fromMaybe __IMPOSSIBLE__ $ substNames' tel ptel core

            ac <- asksTC (^. lensIsAbstract)
            let i = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
    forall t.
    Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
    mkDefInfo (Name -> Name
    nameConcrete (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    x) Fixity'
    noFixity' Access
    PublicAccess IsAbstract
    ac Range
    forall a. Range' a
    noRange
                conNames = ((QName, (Quantity, Type)) -> QName)
    -> [(QName, (Quantity, Type))] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map (QName, (Quantity, Type)) -> QName
    forall a b. (a, b) -> a
    fst [(QName, (Quantity, Type))]
    cs
                conQuantities = ((QName, (Quantity, Type)) -> Quantity)
    -> [(QName, (Quantity, Type))] -> [Quantity]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Quantity, Type) -> Quantity
    forall a b. (a, b) -> a
    fst ((Quantity, Type) -> Quantity)
    -> ((QName, (Quantity, Type)) -> (Quantity, Type))
    -> (QName, (Quantity, Type))
    -> Quantity
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QName, (Quantity, Type)) -> (Quantity, Type)
    forall a b. (a, b) -> b
    snd) [(QName, (Quantity, Type))]
    cs
                toAxiom QName
    c Quantity
    q Expr
    e = KindOfName
    -> DefInfo' Expr
    -> ArgInfo
    -> Maybe PragmaPolarities
    -> QName
    -> Expr
    -> Declaration
    A.Axiom KindOfName
    ConName DefInfo' Expr
    i (Quantity -> ArgInfo -> ArgInfo
    forall a. LensQuantity a => Quantity -> a -> a
    setQuantity Quantity
    q ArgInfo
    defaultArgInfo) Maybe PragmaPolarities
    forall a. Maybe a
    Nothing QName
    c Expr
    e
                as = (QName -> Quantity -> Expr -> Declaration)
    -> [QName] -> [Quantity] -> [Expr] -> [Declaration]
    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
    zipWith3 QName -> Quantity -> Expr -> Declaration
    toAxiom [QName]
    conNames [Quantity]
    conQuantities [Expr]
    es'
                lams = (TypedBinding -> LamBinding) -> [TypedBinding] -> [LamBinding]
    forall a b. (a -> b) -> [a] -> [b]
    map (\case {A.TBind Range
    _ TypedBindingInfo
    tac (NamedArg Binder
    b :| []) Expr
    _ -> TacticAttribute -> NamedArg Binder -> LamBinding
    A.DomainFree (TypedBindingInfo -> TacticAttribute
    tbTacticAttr TypedBindingInfo
    tac) NamedArg Binder
    b
                                  ;TypedBinding
    _ -> LamBinding
    forall a. HasCallStack => a
    __IMPOSSIBLE__ }) [TypedBinding]
    tel
            alwaysReportSDoc "tc.unquote.def" 10 $ vcat $
              [ "checking datatype: " <+> prettyTCM x <+> " with constructors:"
              , nest 2 (vcat (map prettyTCM conNames))
              ]
            liftTCM $ checkDataDef i x YesUniverseCheck (A.DataDefParams Set.empty lams) as
            liftTCM primUnitUnit
          where
            addDummy :: Int -> R.Type -> R.Type
            addDummy :: Int -> Type -> Type
    addDummy Int
    0 Type
    t = Type
    t
            addDummy Int
    n Type
    t = Dom Type -> Abs Type -> Type
    R.Pi (Type -> Dom Type
    forall a. a -> Dom a
    defaultDom (Sort -> Type
    R.Sort (Sort -> Type) -> Sort -> Type
    forall a b. (a -> b) -> a -> b
    $ Integer -> Sort
    R.LitS Integer
    0)) ([Char] -> Type -> Abs Type
    forall a. [Char] -> a -> Abs a
    R.Abs [Char]
    "dummy" (Type -> Abs Type) -> Type -> Abs Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Type -> Type
    addDummy (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Type
    t)

            substNames' :: [A.TypedBinding] -> [A.TypedBinding] -> A.Expr -> Maybe A.Expr
            substNames' :: [TypedBinding] -> [TypedBinding] -> Expr -> Maybe Expr
    substNames' (TypedBinding
    a : [TypedBinding]
    as) (TypedBinding
    b : [TypedBinding]
    bs) Expr
    e = do
              let (A.TBind Range
    _ TypedBindingInfo
    _ (NamedArg Binder
    na :| [NamedArg Binder]
    _) Expr
    expra) = TypedBinding
    a
                  (A.TBind Range
    _ TypedBindingInfo
    _ (NamedArg Binder
    nb :| [NamedArg Binder]
    _) Expr
    exprb) = TypedBinding
    b
                  getName :: NamedArg Binder -> Name
    getName NamedArg Binder
    n = BindName -> Name
    A.unBind (BindName -> Name) -> (Binder -> BindName) -> Binder -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Binder -> BindName
    forall a. Binder' a -> a
    A.binderName (Binder -> Name) -> Binder -> Name
    forall a b. (a -> b) -> a -> b
    $ NamedArg Binder -> Binder
    forall a. NamedArg a -> a
    namedArg NamedArg Binder
    n
              e' <- [TypedBinding] -> [TypedBinding] -> Expr -> Maybe Expr
    substNames' [TypedBinding]
    as [TypedBinding]
    bs Expr
    e
              return $ mapExpr (substName (getName na) (getName nb)) e'
              where
                -- Substitute @Var x@ for @Var y@ in an @Expr@.
                substName :: Name -> Name -> (A.Expr -> A.Expr)
                substName :: Name -> Name -> Expr -> Expr
    substName Name
    x Name
    y e :: Expr
    e@(A.Var Name
    n)
                        | Name
    y Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    n    = Name -> Expr
    A.Var Name
    x
                        | Bool
    otherwise = Expr
    e
                substName Name
    _ Name
    _ Expr
    e = Expr
    e
            substNames' [] [] Expr
    e = Expr -> Maybe Expr
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Expr
    e
            substNames' [TypedBinding]
    _ [TypedBinding]
    _ Expr
    _ = Maybe Expr
    forall a. Maybe a
    Nothing

        tcDefineFun :: QName -> [R.Clause] -> UnquoteM Term
        tcDefineFun :: QName -> [Clause] -> UnquoteM Term
    tcDefineFun QName
    x [Clause]
    cs = UnquoteM Term -> UnquoteM Term
    forall a. UnquoteM a -> UnquoteM a
    inOriginalContext (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ (ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ()
    setDirty ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ()
    -> UnquoteM Term -> UnquoteM Term
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>) (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Term -> UnquoteM Term
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ do
          TCMT IO Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (Either SigError Definition -> Bool
    forall a b. Either a b -> Bool
    isLeft (Either SigError Definition -> Bool)
    -> TCMT IO (Either SigError Definition) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    x) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            UnquoteError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    UnquoteError -> m a
    unquoteError (UnquoteError -> TCMT IO ()) -> UnquoteError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> UnquoteError
    MissingDeclaration QName
    x
          cs <- (Clause -> TCMT IO Clause) -> [Clause] -> TCMT IO [Clause]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (QNamed Clause -> TCMT IO Clause
    QNamed Clause -> TCMT IO (AbsOfRef (QNamed Clause))
    forall r (m :: * -> *).
    (ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
     MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
     HasConstInfo m) =>
    r -> m (AbsOfRef r)
    toAbstract_ (QNamed Clause -> TCMT IO Clause)
    -> (Clause -> QNamed Clause) -> Clause -> TCMT IO Clause
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Clause -> QNamed Clause
    forall a. QName -> a -> QNamed a
    QNamed QName
    x) [Clause]
    cs
          alwaysReportSDoc "tc.unquote.def" 10 $ vcat $ map prettyA cs
          let accessDontCare = a
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- or ConcreteDef, value not looked at
          ac <- asksTC (^. lensIsAbstract)     -- Issue #4012, respect AbstractMode
          oc <- asksTC (^. lensIsOpaque)       -- Issue #6959, respect current opaque block
          let
            i' = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
    forall t.
    Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
    mkDefInfo (Name -> Name
    nameConcrete (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    x) Fixity'
    noFixity' Access
    forall {a}. a
    accessDontCare IsAbstract
    ac Range
    forall a. Range' a
    noRange
            i = DefInfo' Expr
    i' { Info.defOpaque = oc }
          locallyReduceAllDefs $ checkFunDef i x cs
          primUnitUnit

        tcPragmaForeign :: Text -> Text -> TCM Term
        tcPragmaForeign :: ExeName -> ExeName -> TCMT IO Term
    tcPragmaForeign ExeName
    backend ExeName
    code = do
          ExeName -> [Char] -> TCMT IO ()
    addForeignCode ExeName
    backend (ExeName -> [Char]
    T.unpack ExeName
    code)
          TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primUnitUnit

        tcPragmaCompile :: Text -> QName -> Text -> TCM Term
        tcPragmaCompile :: ExeName -> QName -> ExeName -> TCMT IO Term
    tcPragmaCompile ExeName
    backend QName
    name ExeName
    code = do
          (Signature -> Signature) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCMT IO ())
    -> (Signature -> Signature) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    name ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $
            ExeName -> CompilerPragma -> Definition -> Definition
    addCompilerPragma ExeName
    backend (CompilerPragma -> Definition -> Definition)
    -> CompilerPragma -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ Range -> [Char] -> CompilerPragma
    CompilerPragma Range
    forall a. Range' a
    noRange (ExeName -> [Char]
    T.unpack ExeName
    code)
          TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primUnitUnit

        tcRunSpeculative :: Term -> UnquoteM Term
        tcRunSpeculative :: Term -> UnquoteM Term
    tcRunSpeculative Term
    mu = do
          oldState <- ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
          u <- reduce =<< evalTCM mu
          case u of
            Con ConHead
    _ ConInfo
    _ [Apply (Arg { unArg :: forall e. Arg e -> e
    unArg = Term
    x }), Apply (Arg { unArg :: forall e. Arg e -> e
    unArg = Term
    b })] -> do
              UnquoteM Bool
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (Term -> UnquoteM Bool
    forall a. Unquote a => Term -> UnquoteM a
    unquote Term
    b) (ReaderT
       Context
       (StateT
          UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
       ()
     -> ReaderT
          Context
          (StateT
             UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
          ())
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall a b. (a -> b) -> a -> b
    $ TCState
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    oldState
              Term -> UnquoteM Term
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    x
            Term
    _ -> TCMT IO Term -> UnquoteM Term
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCMT IO Term
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO Term)
    -> (Doc -> TypeError) -> Doc -> TCMT IO Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCMT IO Term) -> TCMT IO Doc -> TCMT IO Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
              TCMT IO Doc
    "Should be a pair: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u

        tcGetInstances :: MetaId -> UnquoteM Term
        tcGetInstances :: MetaId -> UnquoteM Term
    tcGetInstances MetaId
    m = TCM (Either Blocker [Candidate])
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         (Either Blocker [Candidate])
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (MetaId -> TCM (Either Blocker [Candidate])
    getInstanceCandidates MetaId
    m) ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Either Blocker [Candidate])
    -> (Either Blocker [Candidate] -> UnquoteM Term) -> UnquoteM Term
    forall a b.
    ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      a
    -> (a
        -> ReaderT
             Context
             (StateT
                UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
             b)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Left Blocker
    unblock -> do
            s <- (UnquoteState -> TCState)
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         TCState
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets UnquoteState -> TCState
    forall a b. (a, b) -> b
    snd
            throwError (BlockedOnMeta s unblock)
          Right [Candidate]
    cands -> TCMT IO Term -> UnquoteM Term
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $
            TCM ([Term] -> Term)
    buildList TCM ([Term] -> Term) -> TCMT IO [Term] -> TCMT IO Term
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Candidate -> TCMT IO Term) -> [Candidate] -> TCMT IO [Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Term -> TCMT IO Term
    quoteTerm (Term -> TCMT IO Term)
    -> (Candidate -> Term) -> Candidate -> TCMT IO Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Candidate -> Term
    candidateTerm) [Candidate]
    cands

        tcSolveInstances :: UnquoteM Term
        tcSolveInstances :: UnquoteM Term
    tcSolveInstances = TCMT IO Term -> UnquoteM Term
    forall a.
    TCM a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
    forall a b. (a -> b) -> a -> b
    $ do
          Lens' TCState Bool -> (Bool -> Bool) -> TCMT IO () -> TCMT IO ()
    forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> m b -> m b
    locallyTCState (Bool -> f Bool) -> TCState -> f TCState
    Lens' TCState Bool
    stPostponeInstanceSearch (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    False) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
            -- Steal instance constraints (TODO: not all!)
            current <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Set ProblemId
    envActiveProblems
            topPid  <- fromMaybe __IMPOSSIBLE__ <$> asksTC envUnquoteProblem
            let steal pc :: ProblemConstraint
    pc@(PConstr Set ProblemId
    pids Blocker
    u Closure Constraint
    c)
                  | ProblemConstraint -> Bool
    isInstance ProblemConstraint
    pc
                  , ProblemId -> Set ProblemId -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member ProblemId
    topPid Set ProblemId
    pids = Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
    PConstr (Set ProblemId -> Set ProblemId -> Set ProblemId
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Set ProblemId
    current Set ProblemId
    pids) Blocker
    u Closure Constraint
    c
                  | Bool
    otherwise              = ProblemConstraint
    pc
                isInstance ProblemConstraint
    c | FindInstance{} <- Closure Constraint -> Constraint
    forall a. Closure a -> a
    clValue (ProblemConstraint -> Closure Constraint
    theConstraint ProblemConstraint
    c) = Bool
    True
                             | Bool
    otherwise                                   = Bool
    False
            modifyAwakeConstraints    $ map steal
            modifySleepingConstraints $ map steal
            wakeConstraints (wakeUpWhen_ isInstance)
            solveSomeAwakeConstraints isInstance True  -- Force solving them now!
          TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primUnitUnit

        splitPars :: Int -> A.Expr -> UnquoteM ([A.TypedBinding], A.Expr)
        splitPars :: Int -> Expr -> UnquoteM ([TypedBinding], Expr)
    splitPars Int
    0     = ([TypedBinding], Expr) -> UnquoteM ([TypedBinding], Expr)
    forall a.
    a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (([TypedBinding], Expr) -> UnquoteM ([TypedBinding], Expr))
    -> (Expr -> ([TypedBinding], Expr))
    -> Expr
    -> UnquoteM ([TypedBinding], Expr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([],)
        splitPars Int
    npars = \case
          A.Pi ExprInfo
    _ (TypedBinding
    n :| [TypedBinding]
    _) Expr
    e -> ([TypedBinding] -> [TypedBinding])
    -> ([TypedBinding], Expr) -> ([TypedBinding], Expr)
    forall b c d. (b -> c) -> (b, d) -> (c, d)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first (TypedBinding
    n TypedBinding -> [TypedBinding] -> [TypedBinding]
    forall a. a -> [a] -> [a]
    :) (([TypedBinding], Expr) -> ([TypedBinding], Expr))
    -> UnquoteM ([TypedBinding], Expr)
    -> UnquoteM ([TypedBinding], Expr)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> Expr -> UnquoteM ([TypedBinding], Expr)
    splitPars (Int
    npars Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Expr
    e
          A.Fun{}           -> UnquoteM ([TypedBinding], Expr)
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- trusting the original author of this function
          A.ScopedExpr{}    -> UnquoteM ([TypedBinding], Expr)
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- trusting the original author of this function
          Expr
    e                 -> UnquoteError -> UnquoteM ([TypedBinding], Expr)
    forall a.
    UnquoteError
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (UnquoteError -> UnquoteM ([TypedBinding], Expr))
    -> UnquoteError -> UnquoteM ([TypedBinding], Expr)
    forall a b. (a -> b) -> a -> b
    $ Int -> Expr -> UnquoteError
    TooManyParameters Int
    npars Expr
    e

    ------------------------------------------------------------------------
    -- * Trusted executables
    ------------------------------------------------------------------------

    type ExeArg  = Text
    type StdIn   = Text
    type StdOut  = Text
    type StdErr  = Text

    -- | Raise an error if the @--allow-exec@ option was not specified.
    --
    requireAllowExec :: TCM ()
    requireAllowExec :: TCMT IO ()
    requireAllowExec = do
      TCMT IO Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (PragmaOptions -> Bool
    optAllowExec (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError TypeError
    NeedOptionAllowExec

    -- | Convert an @ExitCode@ to an Agda natural number.
    --
    exitCodeToNat :: ExitCode -> Nat
    exitCodeToNat :: ExitCode -> Nat
    exitCodeToNat  ExitCode
    ExitSuccess    = Integer -> Nat
    Nat Integer
    0
    exitCodeToNat (ExitFailure Int
    n) = Integer -> Nat
    Nat (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    n)

    -- | Call a trusted executable with the given arguments and input.
    --
    --   Returns the exit code, stdout, and stderr.
    --
    tcExec :: ExeName -> [ExeArg] -> StdIn -> TCM Term
    tcExec :: ExeName -> [ExeName] -> ExeName -> TCMT IO Term
    tcExec ExeName
    exe [ExeName]
    args ExeName
    stdIn = do
      TCMT IO ()
    requireAllowExec
      exes <- CommandLineOptions -> Map ExeName [Char]
    optTrustedExecutables (CommandLineOptions -> Map ExeName [Char])
    -> TCMT IO CommandLineOptions -> TCMT IO (Map ExeName [Char])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      case Map.lookup exe exes of
        Maybe [Char]
    Nothing -> ExecError -> TCMT IO Term
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    ExecError -> m a
    execError (ExecError -> TCMT IO Term) -> ExecError -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ ExeName -> Map ExeName [Char] -> ExecError
    ExeNotTrusted ExeName
    exe Map ExeName [Char]
    exes
        Just [Char]
    fp -> do
          -- Check that the executable exists.
          TCMT IO Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (IO Bool -> TCMT IO Bool
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool -> TCMT IO Bool) -> IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO Bool
    doesFileExist [Char]
    fp) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ ExecError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    ExecError -> m a
    execError (ExecError -> TCMT IO ()) -> ExecError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ ExeName -> [Char] -> ExecError
    ExeNotFound ExeName
    exe [Char]
    fp
          -- Check that the executable is executable.
          TCMT IO Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (IO Bool -> TCMT IO Bool
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool -> TCMT IO Bool) -> IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ Permissions -> Bool
    executable (Permissions -> Bool) -> IO Permissions -> IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> IO Permissions
    getPermissions [Char]
    fp) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ ExecError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    ExecError -> m a
    execError (ExecError -> TCMT IO ()) -> ExecError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ ExeName -> [Char] -> ExecError
    ExeNotExecutable ExeName
    exe [Char]
    fp

          let strArgs :: [[Char]]
    strArgs    = ExeName -> [Char]
    T.unpack (ExeName -> [Char]) -> [ExeName] -> [[Char]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [ExeName]
    args
          (datExitCode, txtStdOut, txtStdErr) <- IO (ExitCode, ExeName, ExeName)
    -> TCMT IO (ExitCode, ExeName, ExeName)
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (ExitCode, ExeName, ExeName)
     -> TCMT IO (ExitCode, ExeName, ExeName))
    -> IO (ExitCode, ExeName, ExeName)
    -> TCMT IO (ExitCode, ExeName, ExeName)
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [[Char]] -> ExeName -> IO (ExitCode, ExeName, ExeName)
    readProcessWithExitCode [Char]
    fp [[Char]]
    strArgs ExeName
    stdIn
          let natExitCode = ExitCode -> Nat
    exitCodeToNat ExitCode
    datExitCode
          toR <- toTerm
          runReduceM $ toR (natExitCode, (txtStdOut, txtStdErr))