    -- | Lenses for 'TCState' and more.

    module Agda.TypeChecking.Monad.State where

    import qualified Control.Exception as E

    import Control.Monad       (void)
    import Control.Monad.Trans (MonadIO, liftIO)

    import Data.Maybe

    import qualified Data.Map as Map

    import qualified Data.List.NonEmpty as NonEmpty
    import Data.Set (Set)
    import qualified Data.Set as Set
    import qualified Data.HashMap.Strict as HMap

    import Agda.Benchmarking

    import Agda.Interaction.Response
      (InteractionOutputCallback, Response)

    import Agda.Syntax.Common
    import Agda.Syntax.Scope.Base
    import qualified Agda.Syntax.Concrete.Name as C
    import Agda.Syntax.Abstract (PatternSynDefn, PatternSynDefns)
    import Agda.Syntax.Abstract.PatternSynonyms
    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Warnings

    import Agda.TypeChecking.Monad.Debug (reportSDoc, reportSLn, verboseS)
    import Agda.TypeChecking.Positivity.Occurrence
    import Agda.TypeChecking.CompiledClause

    import Agda.Utils.Hash
    import Agda.Utils.Lens
    import Agda.Utils.Monad (bracket_)
    import Agda.Utils.Pretty
    import Agda.Utils.Tuple

    import Agda.Utils.Impossible

    -- | Resets the non-persistent part of the type checking state.

    resetState :: TCM ()
    resetState :: TCM ()
    resetState = do
        PersistentTCState
    pers <- (TCState -> PersistentTCState) -> TCMT IO PersistentTCState
    forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
    getsTC TCState -> PersistentTCState
    stPersistentState
        TCState -> TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC (TCState -> TCM ()) -> TCState -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCState
    initState { stPersistentState :: PersistentTCState
    stPersistentState = PersistentTCState
    pers }

    -- | Resets all of the type checking state.
    --
    --   Keep only 'Benchmark' and backend information.

    resetAllState :: TCM ()
    resetAllState :: TCM ()
    resetAllState = do
        Benchmark
    b <- TCM Benchmark
    getBenchmark
        [Backend]
    backends <- Lens' [Backend] TCState -> TCMT IO [Backend]
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' [Backend] TCState
    stBackends
        TCState -> TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC (TCState -> TCM ()) -> TCState -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (PersistentTCState -> PersistentTCState) -> TCState -> TCState
    updatePersistentState (\ PersistentTCState
    s -> PersistentTCState
    s { stBenchmark :: Benchmark
    stBenchmark = Benchmark
    b }) TCState
    initState
        Lens' [Backend] TCState
    stBackends Lens' [Backend] TCState -> [Backend] -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` [Backend]
    backends
    -- resetAllState = putTC initState

    -- | Restore 'TCState' after performing subcomputation.
    --
    --   In contrast to 'Agda.Utils.Monad.localState', the 'Benchmark'
    --   info from the subcomputation is saved.
    localTCState :: TCM a -> TCM a
    localTCState :: forall a. TCM a -> TCM a
    localTCState = TCMT IO TCState -> (TCState -> TCM ()) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a b.
    Monad m =>
    m a -> (a -> m ()) -> m b -> m b
    bracket_ TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC (\ TCState
    s -> do
       Benchmark
    b <- TCM Benchmark
    getBenchmark
       TCState -> TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    s
       (Benchmark -> Benchmark) -> TCM ()
    modifyBenchmark ((Benchmark -> Benchmark) -> TCM ())
    -> (Benchmark -> Benchmark) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Benchmark -> Benchmark -> Benchmark
    forall a b. a -> b -> a
    const Benchmark
    b)

    -- | Same as 'localTCState' but also returns the state in which we were just
    --   before reverting it.
    localTCStateSaving :: TCM a -> TCM (a, TCState)
    localTCStateSaving :: forall a. TCM a -> TCM (a, TCState)
    localTCStateSaving TCM a
    compute = do
      TCState
    oldState <- TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
      a
    result <- TCM a
    compute
      TCState
    newState <- TCMT IO TCState
    forall (m :: * -> *). MonadTCState m => m TCState
    getTC
      do
        Benchmark
    b <- TCM Benchmark
    getBenchmark
        TCState -> TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    oldState
        (Benchmark -> Benchmark) -> TCM ()
    modifyBenchmark ((Benchmark -> Benchmark) -> TCM ())
    -> (Benchmark -> Benchmark) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Benchmark -> Benchmark -> Benchmark
    forall a b. a -> b -> a
    const Benchmark
    b
      (a, TCState) -> TCM (a, TCState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    result, TCState
    newState)

    -- | Same as 'localTCState' but keep all warnings.
    localTCStateSavingWarnings :: TCM a -> TCM a
    localTCStateSavingWarnings :: forall a. TCM a -> TCM a
    localTCStateSavingWarnings TCM a
    compute = do
      (a
    result, TCState
    newState) <- TCM a -> TCM (a, TCState)
    forall a. TCM a -> TCM (a, TCState)
    localTCStateSaving TCM a
    compute
      (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Lens' [TCWarning] TCState -> LensMap [TCWarning] TCState
    forall i o. Lens' i o -> LensMap i o
    over Lens' [TCWarning] TCState
    stTCWarnings LensMap [TCWarning] TCState -> LensMap [TCWarning] TCState
    forall a b. (a -> b) -> a -> b
    $ [TCWarning] -> [TCWarning] -> [TCWarning]
    forall a b. a -> b -> a
    const ([TCWarning] -> [TCWarning] -> [TCWarning])
    -> [TCWarning] -> [TCWarning] -> [TCWarning]
    forall a b. (a -> b) -> a -> b
    $ TCState
    newState TCState -> Lens' [TCWarning] TCState -> [TCWarning]
    forall o i. o -> Lens' i o -> i
    ^. Lens' [TCWarning] TCState
    stTCWarnings
      a -> TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    result

    data SpeculateResult = SpeculateAbort | SpeculateCommit

    -- | Allow rolling back the state changes of a TCM computation.
    speculateTCState :: TCM (a, SpeculateResult) -> TCM a
    speculateTCState :: forall a. TCM (a, SpeculateResult) -> TCM a
    speculateTCState TCM (a, SpeculateResult)
    m = do
      ((a
    x, SpeculateResult
    res), TCState
    newState) <- TCM (a, SpeculateResult) -> TCM ((a, SpeculateResult), TCState)
    forall a. TCM a -> TCM (a, TCState)
    localTCStateSaving TCM (a, SpeculateResult)
    m
      case SpeculateResult
    res of
        SpeculateResult
    SpeculateAbort  -> a -> TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x
        SpeculateResult
    SpeculateCommit -> a
    x a -> TCM () -> TCM a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ TCState -> TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    newState

    speculateTCState_ :: TCM SpeculateResult -> TCM ()
    speculateTCState_ :: TCM SpeculateResult -> TCM ()
    speculateTCState_ TCM SpeculateResult
    m = TCM () -> TCM ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM ((), SpeculateResult) -> TCM ()
    forall a. TCM (a, SpeculateResult) -> TCM a
    speculateTCState (TCM ((), SpeculateResult) -> TCM ())
    -> TCM ((), SpeculateResult) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ((),) (SpeculateResult -> ((), SpeculateResult))
    -> TCM SpeculateResult -> TCM ((), SpeculateResult)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM SpeculateResult
    m

    -- | A fresh TCM instance.
    --
    -- The computation is run in a fresh state, with the exception that
    -- the persistent state is preserved. If the computation changes the
    -- state, then these changes are ignored, except for changes to the
    -- persistent state. (Changes to the persistent state are also ignored
    -- if errors other than type errors or IO exceptions are encountered.)

    freshTCM :: TCM a -> TCM (Either TCErr a)
    freshTCM :: forall a. TCM a -> TCM (Either TCErr a)
    freshTCM TCM a
    m = do
      PersistentTCState
    ps <- Lens' PersistentTCState TCState -> TCMT IO PersistentTCState
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' PersistentTCState TCState
    lensPersistentState
      let s :: TCState
    s = Lens' PersistentTCState TCState
    -> LensSet PersistentTCState TCState
    forall i o. Lens' i o -> LensSet i o
    set Lens' PersistentTCState TCState
    lensPersistentState PersistentTCState
    ps TCState
    initState
      Either TCErr (a, TCState)
    r <- IO (Either TCErr (a, TCState))
    -> TCMT IO (Either TCErr (a, TCState))
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Either TCErr (a, TCState))
     -> TCMT IO (Either TCErr (a, TCState)))
    -> IO (Either TCErr (a, TCState))
    -> TCMT IO (Either TCErr (a, TCState))
    forall a b. (a -> b) -> a -> b
    $ ((a, TCState) -> Either TCErr (a, TCState)
    forall a b. b -> Either a b
    Right ((a, TCState) -> Either TCErr (a, TCState))
    -> IO (a, TCState) -> IO (Either TCErr (a, TCState))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCEnv -> TCState -> TCM a -> IO (a, TCState)
    forall (m :: * -> *) a.
    MonadIO m =>
    TCEnv -> TCState -> TCMT m a -> m (a, TCState)
    runTCM TCEnv
    initEnv TCState
    s TCM a
    m) IO (Either TCErr (a, TCState))
    -> (TCErr -> IO (Either TCErr (a, TCState)))
    -> IO (Either TCErr (a, TCState))
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `E.catch` (Either TCErr (a, TCState) -> IO (Either TCErr (a, TCState))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either TCErr (a, TCState) -> IO (Either TCErr (a, TCState)))
    -> (TCErr -> Either TCErr (a, TCState))
    -> TCErr
    -> IO (Either TCErr (a, TCState))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCErr -> Either TCErr (a, TCState)
    forall a b. a -> Either a b
    Left)
      case Either TCErr (a, TCState)
    r of
        Right (a
    a, TCState
    s) -> do
          Lens' PersistentTCState TCState -> PersistentTCState -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    setTCLens Lens' PersistentTCState TCState
    lensPersistentState (PersistentTCState -> TCM ()) -> PersistentTCState -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCState
    s TCState -> Lens' PersistentTCState TCState -> PersistentTCState
    forall o i. o -> Lens' i o -> i
    ^. Lens' PersistentTCState TCState
    lensPersistentState
          Either TCErr a -> TCM (Either TCErr a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either TCErr a -> TCM (Either TCErr a))
    -> Either TCErr a -> TCM (Either TCErr a)
    forall a b. (a -> b) -> a -> b
    $ a -> Either TCErr a
    forall a b. b -> Either a b
    Right a
    a
        Left TCErr
    err -> do
          case TCErr
    err of
            TypeError { tcErrState :: TCErr -> TCState
    tcErrState = TCState
    s } ->
              Lens' PersistentTCState TCState -> PersistentTCState -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    setTCLens Lens' PersistentTCState TCState
    lensPersistentState (PersistentTCState -> TCM ()) -> PersistentTCState -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCState
    s TCState -> Lens' PersistentTCState TCState -> PersistentTCState
    forall o i. o -> Lens' i o -> i
    ^. Lens' PersistentTCState TCState
    lensPersistentState
            IOException TCState
    s Range
    _ IOException
    _ ->
              Lens' PersistentTCState TCState -> PersistentTCState -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    setTCLens Lens' PersistentTCState TCState
    lensPersistentState (PersistentTCState -> TCM ()) -> PersistentTCState -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCState
    s TCState -> Lens' PersistentTCState TCState -> PersistentTCState
    forall o i. o -> Lens' i o -> i
    ^. Lens' PersistentTCState TCState
    lensPersistentState
            TCErr
    _ -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          Either TCErr a -> TCM (Either TCErr a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either TCErr a -> TCM (Either TCErr a))
    -> Either TCErr a -> TCM (Either TCErr a)
    forall a b. (a -> b) -> a -> b
    $ TCErr -> Either TCErr a
    forall a b. a -> Either a b
    Left TCErr
    err

    ---------------------------------------------------------------------------
    -- * Lens for persistent states and its fields
    ---------------------------------------------------------------------------

    lensPersistentState :: Lens' PersistentTCState TCState
    lensPersistentState :: Lens' PersistentTCState TCState
    lensPersistentState PersistentTCState -> f PersistentTCState
    f TCState
    s =
      PersistentTCState -> f PersistentTCState
    f (TCState -> PersistentTCState
    stPersistentState TCState
    s) f PersistentTCState -> (PersistentTCState -> TCState) -> f TCState
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ PersistentTCState
    p -> TCState
    s { stPersistentState :: PersistentTCState
    stPersistentState = PersistentTCState
    p }

    updatePersistentState
      :: (PersistentTCState -> PersistentTCState) -> (TCState -> TCState)
    updatePersistentState :: (PersistentTCState -> PersistentTCState) -> TCState -> TCState
    updatePersistentState PersistentTCState -> PersistentTCState
    f TCState
    s = TCState
    s { stPersistentState :: PersistentTCState
    stPersistentState = PersistentTCState -> PersistentTCState
    f (TCState -> PersistentTCState
    stPersistentState TCState
    s) }

    modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
    modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
    modifyPersistentState = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ())
    -> ((PersistentTCState -> PersistentTCState) -> TCState -> TCState)
    -> (PersistentTCState -> PersistentTCState)
    -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (PersistentTCState -> PersistentTCState) -> TCState -> TCState
    updatePersistentState

    -- | Lens for 'stAccumStatistics'.

    lensAccumStatisticsP :: Lens' Statistics PersistentTCState
    lensAccumStatisticsP :: Lens' Statistics PersistentTCState
    lensAccumStatisticsP Statistics -> f Statistics
    f PersistentTCState
    s = Statistics -> f Statistics
    f (PersistentTCState -> Statistics
    stAccumStatistics PersistentTCState
    s) f Statistics
    -> (Statistics -> PersistentTCState) -> f PersistentTCState
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ Statistics
    a ->
      PersistentTCState
    s { stAccumStatistics :: Statistics
    stAccumStatistics = Statistics
    a }

    lensAccumStatistics :: Lens' Statistics TCState
    lensAccumStatistics :: Lens' Statistics TCState
    lensAccumStatistics =  (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
    Lens' PersistentTCState TCState
    lensPersistentState ((PersistentTCState -> f PersistentTCState)
     -> TCState -> f TCState)
    -> ((Statistics -> f Statistics)
        -> PersistentTCState -> f PersistentTCState)
    -> (Statistics -> f Statistics)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Statistics -> f Statistics)
    -> PersistentTCState -> f PersistentTCState
    Lens' Statistics PersistentTCState
    lensAccumStatisticsP

    ---------------------------------------------------------------------------
    -- * Scope
    ---------------------------------------------------------------------------

    -- | Get the current scope.
    getScope :: ReadTCState m => m ScopeInfo
    getScope :: forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope = Lens' ScopeInfo TCState -> m ScopeInfo
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' ScopeInfo TCState
    stScope

    -- | Set the current scope.
    setScope :: ScopeInfo -> TCM ()
    setScope :: ScopeInfo -> TCM ()
    setScope ScopeInfo
    scope = (ScopeInfo -> ScopeInfo) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope (ScopeInfo -> ScopeInfo -> ScopeInfo
    forall a b. a -> b -> a
    const ScopeInfo
    scope)

    -- | Modify the current scope without updating the inverse maps.
    modifyScope_ :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope_ :: forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope_ ScopeInfo -> ScopeInfo
    f = Lens' ScopeInfo TCState
    stScope Lens' ScopeInfo TCState -> (ScopeInfo -> ScopeInfo) -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` ScopeInfo -> ScopeInfo
    f

    -- | Modify the current scope.
    modifyScope :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope :: forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope ScopeInfo -> ScopeInfo
    f = (ScopeInfo -> ScopeInfo) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (ScopeInfo -> ScopeInfo) -> m ()
    modifyScope_ (ScopeInfo -> ScopeInfo
    recomputeInverseScopeMaps (ScopeInfo -> ScopeInfo)
    -> (ScopeInfo -> ScopeInfo) -> ScopeInfo -> ScopeInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ScopeInfo -> ScopeInfo
    f)

    -- | Get a part of the current scope.
    useScope :: ReadTCState m => Lens' a ScopeInfo -> m a
    useScope :: forall (m :: * -> *) a. ReadTCState m => Lens' a ScopeInfo -> m a
    useScope Lens' a ScopeInfo
    l = Lens' a TCState -> m a
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR (Lens' a TCState -> m a) -> Lens' a TCState -> m a
    forall a b. (a -> b) -> a -> b
    $ (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
    Lens' ScopeInfo TCState
    stScope ((ScopeInfo -> f ScopeInfo) -> TCState -> f TCState)
    -> ((a -> f a) -> ScopeInfo -> f ScopeInfo)
    -> (a -> f a)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> f a) -> ScopeInfo -> f ScopeInfo
    Lens' a ScopeInfo
    l

    -- | Run a computation in a modified scope.
    locallyScope :: ReadTCState m => Lens' a ScopeInfo -> (a -> a) -> m b -> m b
    locallyScope :: forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a ScopeInfo -> (a -> a) -> m b -> m b
    locallyScope Lens' a ScopeInfo
    l = Lens' a TCState -> (a -> a) -> m b -> m b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a TCState -> (a -> a) -> m b -> m b
    locallyTCState (Lens' a TCState -> (a -> a) -> m b -> m b)
    -> Lens' a TCState -> (a -> a) -> m b -> m b
    forall a b. (a -> b) -> a -> b
    $ (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
    Lens' ScopeInfo TCState
    stScope ((ScopeInfo -> f ScopeInfo) -> TCState -> f TCState)
    -> ((a -> f a) -> ScopeInfo -> f ScopeInfo)
    -> (a -> f a)
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> f a) -> ScopeInfo -> f ScopeInfo
    Lens' a ScopeInfo
    l

    -- | Run a computation in a local scope.
    withScope :: ReadTCState m => ScopeInfo -> m a -> m (a, ScopeInfo)
    withScope :: forall (m :: * -> *) a.
    ReadTCState m =>
    ScopeInfo -> m a -> m (a, ScopeInfo)
    withScope ScopeInfo
    s m a
    m = Lens' ScopeInfo TCState
    -> (ScopeInfo -> ScopeInfo) -> m (a, ScopeInfo) -> m (a, ScopeInfo)
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' a TCState -> (a -> a) -> m b -> m b
    locallyTCState Lens' ScopeInfo TCState
    stScope (ScopeInfo -> ScopeInfo
    recomputeInverseScopeMaps (ScopeInfo -> ScopeInfo)
    -> (ScopeInfo -> ScopeInfo) -> ScopeInfo -> ScopeInfo
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ScopeInfo -> ScopeInfo -> ScopeInfo
    forall a b. a -> b -> a
    const ScopeInfo
    s) (m (a, ScopeInfo) -> m (a, ScopeInfo))
    -> m (a, ScopeInfo) -> m (a, ScopeInfo)
    forall a b. (a -> b) -> a -> b
    $ (,) (a -> ScopeInfo -> (a, ScopeInfo))
    -> m a -> m (ScopeInfo -> (a, ScopeInfo))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m a
    m m (ScopeInfo -> (a, ScopeInfo)) -> m ScopeInfo -> m (a, ScopeInfo)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope

    -- | Same as 'withScope', but discard the scope from the computation.
    withScope_ :: ReadTCState m => ScopeInfo -> m a -> m a
    withScope_ :: forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
    withScope_ ScopeInfo
    s m a
    m = (a, ScopeInfo) -> a
    forall a b. (a, b) -> a
    fst ((a, ScopeInfo) -> a) -> m (a, ScopeInfo) -> m a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ScopeInfo -> m a -> m (a, ScopeInfo)
    forall (m :: * -> *) a.
    ReadTCState m =>
    ScopeInfo -> m a -> m (a, ScopeInfo)
    withScope ScopeInfo
    s m a
    m

    -- | Discard any changes to the scope by a computation.
    localScope :: TCM a -> TCM a
    localScope :: forall a. TCM a -> TCM a
    localScope TCM a
    m = do
      ScopeInfo
    scope <- TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      a
    x <- TCM a
    m
      ScopeInfo -> TCM ()
    setScope ScopeInfo
    scope
      a -> TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x

    -- | Scope error.
    notInScopeError :: C.QName -> TCM a
    notInScopeError :: forall a. QName -> TCM a
    notInScopeError QName
    x = do
      [Char] -> Int -> [Char] -> TCM ()
    printScope [Char]
    "unbound" Int
    5 [Char]
    ""
      TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> TypeError -> TCM a
    forall a b. (a -> b) -> a -> b
    $ [QName] -> TypeError
    NotInScope [QName
    x]

    notInScopeWarning :: C.QName -> TCM ()
    notInScopeWarning :: QName -> TCM ()
    notInScopeWarning QName
    x = do
      [Char] -> Int -> [Char] -> TCM ()
    printScope [Char]
    "unbound" Int
    5 [Char]
    ""
      Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [QName] -> Warning
    NotInScopeW [QName
    x]

    -- | Debug print the scope.
    printScope :: String -> Int -> String -> TCM ()
    printScope :: [Char] -> Int -> [Char] -> TCM ()
    printScope [Char]
    tag Int
    v [Char]
    s = [Char] -> Int -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
    verboseS ([Char]
    "scope." [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    tag) Int
    v (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      ScopeInfo
    scope <- TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      [Char] -> Int -> TCM Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCM Doc -> m ()
    reportSDoc ([Char]
    "scope." [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    tag) Int
    v (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCM Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCM Doc) -> Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat [ [Char] -> Doc
    text [Char]
    s, ScopeInfo -> Doc
    forall a. Pretty a => a -> Doc
    pretty ScopeInfo
    scope ]

    ---------------------------------------------------------------------------
    -- * Signature
    ---------------------------------------------------------------------------

    -- ** Lens for 'stSignature' and 'stImports'

    modifySignature :: MonadTCState m => (Signature -> Signature) -> m ()
    modifySignature :: forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature Signature -> Signature
    f = Lens' Signature TCState
    stSignature Lens' Signature TCState -> (Signature -> Signature) -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` Signature -> Signature
    f

    modifyImportedSignature :: MonadTCState m => (Signature -> Signature) -> m ()
    modifyImportedSignature :: forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifyImportedSignature Signature -> Signature
    f = Lens' Signature TCState
    stImports Lens' Signature TCState -> (Signature -> Signature) -> m ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` Signature -> Signature
    f

    getSignature :: ReadTCState m => m Signature
    getSignature :: forall (m :: * -> *). ReadTCState m => m Signature
    getSignature = Lens' Signature TCState -> m Signature
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' Signature TCState
    stSignature

    -- | Update a possibly imported definition. Warning: changes made to imported
    --   definitions (during type checking) will not persist outside the current
    --   module. This function is currently used to update the compiled
    --   representation of a function during compilation.
    modifyGlobalDefinition :: MonadTCState m => QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition :: forall (m :: * -> *).
    MonadTCState m =>
    QName -> (Definition -> Definition) -> m ()
    modifyGlobalDefinition QName
    q Definition -> Definition
    f = do
      (Signature -> Signature) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature         ((Signature -> Signature) -> m ())
    -> (Signature -> Signature) -> m ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q Definition -> Definition
    f
      (Signature -> Signature) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifyImportedSignature ((Signature -> Signature) -> m ())
    -> (Signature -> Signature) -> m ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q Definition -> Definition
    f

    setSignature :: MonadTCState m => Signature -> m ()
    setSignature :: forall (m :: * -> *). MonadTCState m => Signature -> m ()
    setSignature Signature
    sig = (Signature -> Signature) -> m ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> m ())
    -> (Signature -> Signature) -> m ()
    forall a b. (a -> b) -> a -> b
    $ Signature -> Signature -> Signature
    forall a b. a -> b -> a
    const Signature
    sig

    -- | Run some computation in a different signature, restore original signature.
    withSignature :: (ReadTCState m, MonadTCState m) => Signature -> m a -> m a
    withSignature :: forall (m :: * -> *) a.
    (ReadTCState m, MonadTCState m) =>
    Signature -> m a -> m a
    withSignature Signature
    sig m a
    m = do
      Signature
    sig0 <- m Signature
    forall (m :: * -> *). ReadTCState m => m Signature
    getSignature
      Signature -> m ()
    forall (m :: * -> *). MonadTCState m => Signature -> m ()
    setSignature Signature
    sig
      a
    r <- m a
    m
      Signature -> m ()
    forall (m :: * -> *). MonadTCState m => Signature -> m ()
    setSignature Signature
    sig0
      a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    r

    -- ** Modifiers for rewrite rules
    addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
    addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
    addRewriteRulesFor QName
    f RewriteRules
    rews [QName]
    matchables =
        Lens' (HashMap QName RewriteRules) Signature
    -> LensMap (HashMap QName RewriteRules) Signature
    forall i o. Lens' i o -> LensMap i o
    over Lens' (HashMap QName RewriteRules) Signature
    sigRewriteRules ((RewriteRules -> RewriteRules -> RewriteRules)
    -> QName
    -> RewriteRules
    -> HashMap QName RewriteRules
    -> HashMap QName RewriteRules
    forall k v.
    (Eq k, Hashable k) =>
    (v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
    HMap.insertWith RewriteRules -> RewriteRules -> RewriteRules
    forall a. Monoid a => a -> a -> a
    mappend QName
    f RewriteRules
    rews)
      (Signature -> Signature)
    -> (Signature -> Signature) -> Signature -> Signature
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    f ((Defn -> Defn) -> Definition -> Definition
    updateTheDef Defn -> Defn
    setNotInjective (Definition -> Definition)
    -> (Definition -> Definition) -> Definition -> Definition
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Definition
    setCopatternLHS)
      (Signature -> Signature)
    -> (Signature -> Signature) -> Signature -> Signature
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QName -> [QName] -> Signature -> Signature
    setMatchableSymbols QName
    f [QName]
    matchables)
        where
          setNotInjective :: Defn -> Defn
    setNotInjective def :: Defn
    def@Function{} = Defn
    def { funInv :: FunctionInverse
    funInv = FunctionInverse
    forall c. FunctionInverse' c
    NotInjective }
          setNotInjective Defn
    def            = Defn
    def

          setCopatternLHS :: Definition -> Definition
    setCopatternLHS =
            (Bool -> Bool) -> Definition -> Definition
    updateDefCopatternLHS (Bool -> Bool -> Bool
    || (RewriteRule -> Bool) -> RewriteRules -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any RewriteRule -> Bool
    hasProjectionPattern RewriteRules
    rews)

          hasProjectionPattern :: RewriteRule -> Bool
    hasProjectionPattern RewriteRule
    rew = (Elim' NLPat -> Bool) -> [Elim' NLPat] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Maybe (ProjOrigin, QName) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (ProjOrigin, QName) -> Bool)
    -> (Elim' NLPat -> Maybe (ProjOrigin, QName))
    -> Elim' NLPat
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Elim' NLPat -> Maybe (ProjOrigin, QName)
    forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
    isProjElim) ([Elim' NLPat] -> Bool) -> [Elim' NLPat] -> Bool
    forall a b. (a -> b) -> a -> b
    $ RewriteRule -> [Elim' NLPat]
    rewPats RewriteRule
    rew

    setMatchableSymbols :: QName -> [QName] -> Signature -> Signature
    setMatchableSymbols :: QName -> [QName] -> Signature -> Signature
    setMatchableSymbols QName
    f [QName]
    matchables =
      (QName -> (Signature -> Signature) -> Signature -> Signature)
    -> (Signature -> Signature) -> [QName] -> Signature -> Signature
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((Signature -> Signature)
    -> (Signature -> Signature) -> Signature -> Signature
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    (.) ((Signature -> Signature)
     -> (Signature -> Signature) -> Signature -> Signature)
    -> (QName -> Signature -> Signature)
    -> QName
    -> (Signature -> Signature)
    -> Signature
    -> Signature
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (\QName
    g -> QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    g Definition -> Definition
    setMatchable)) Signature -> Signature
    forall a. a -> a
    id [QName]
    matchables
        where
          setMatchable :: Definition -> Definition
    setMatchable Definition
    def = Definition
    def { defMatchable :: Set QName
    defMatchable = QName -> Set QName -> Set QName
    forall a. Ord a => a -> Set a -> Set a
    Set.insert QName
    f (Set QName -> Set QName) -> Set QName -> Set QName
    forall a b. (a -> b) -> a -> b
    $ Definition -> Set QName
    defMatchable Definition
    def }

    -- ** Modifiers for parts of the signature

    lookupDefinition :: QName -> Signature -> Maybe Definition
    lookupDefinition :: QName -> Signature -> Maybe Definition
    lookupDefinition QName
    q Signature
    sig = QName -> HashMap QName Definition -> Maybe Definition
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
    HMap.lookup QName
    q (HashMap QName Definition -> Maybe Definition)
    -> HashMap QName Definition -> Maybe Definition
    forall a b. (a -> b) -> a -> b
    $ Signature
    sig Signature
    -> Lens' (HashMap QName Definition) Signature
    -> HashMap QName Definition
    forall o i. o -> Lens' i o -> i
    ^. Lens' (HashMap QName Definition) Signature
    sigDefinitions

    updateDefinitions :: (Definitions -> Definitions) -> Signature -> Signature
    updateDefinitions :: (HashMap QName Definition -> HashMap QName Definition)
    -> Signature -> Signature
    updateDefinitions = Lens' (HashMap QName Definition) Signature
    -> (HashMap QName Definition -> HashMap QName Definition)
    -> Signature
    -> Signature
    forall i o. Lens' i o -> LensMap i o
    over Lens' (HashMap QName Definition) Signature
    sigDefinitions

    updateDefinition :: QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition :: QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q Definition -> Definition
    f = (HashMap QName Definition -> HashMap QName Definition)
    -> Signature -> Signature
    updateDefinitions ((HashMap QName Definition -> HashMap QName Definition)
     -> Signature -> Signature)
    -> (HashMap QName Definition -> HashMap QName Definition)
    -> Signature
    -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Definition -> Definition)
    -> QName -> HashMap QName Definition -> HashMap QName Definition
    forall k v.
    (Eq k, Hashable k) =>
    (v -> v) -> k -> HashMap k v -> HashMap k v
    HMap.adjust Definition -> Definition
    f QName
    q

    updateTheDef :: (Defn -> Defn) -> (Definition -> Definition)
    updateTheDef :: (Defn -> Defn) -> Definition -> Definition
    updateTheDef Defn -> Defn
    f Definition
    def = Definition
    def { theDef :: Defn
    theDef = Defn -> Defn
    f (Definition -> Defn
    theDef Definition
    def) }

    updateDefType :: (Type -> Type) -> (Definition -> Definition)
    updateDefType :: (Type -> Type) -> Definition -> Definition
    updateDefType Type -> Type
    f Definition
    def = Definition
    def { defType :: Type
    defType = Type -> Type
    f (Definition -> Type
    defType Definition
    def) }

    updateDefArgOccurrences :: ([Occurrence] -> [Occurrence]) -> (Definition -> Definition)
    updateDefArgOccurrences :: ([Occurrence] -> [Occurrence]) -> Definition -> Definition
    updateDefArgOccurrences [Occurrence] -> [Occurrence]
    f Definition
    def = Definition
    def { defArgOccurrences :: [Occurrence]
    defArgOccurrences = [Occurrence] -> [Occurrence]
    f (Definition -> [Occurrence]
    defArgOccurrences Definition
    def) }

    updateDefPolarity :: ([Polarity] -> [Polarity]) -> (Definition -> Definition)
    updateDefPolarity :: ([Polarity] -> [Polarity]) -> Definition -> Definition
    updateDefPolarity [Polarity] -> [Polarity]
    f Definition
    def = Definition
    def { defPolarity :: [Polarity]
    defPolarity = [Polarity] -> [Polarity]
    f (Definition -> [Polarity]
    defPolarity Definition
    def) }

    updateDefCompiledRep :: (CompiledRepresentation -> CompiledRepresentation) -> (Definition -> Definition)
    updateDefCompiledRep :: (CompiledRepresentation -> CompiledRepresentation)
    -> Definition -> Definition
    updateDefCompiledRep CompiledRepresentation -> CompiledRepresentation
    f Definition
    def = Definition
    def { defCompiledRep :: CompiledRepresentation
    defCompiledRep = CompiledRepresentation -> CompiledRepresentation
    f (Definition -> CompiledRepresentation
    defCompiledRep Definition
    def) }

    addCompilerPragma :: BackendName -> CompilerPragma -> Definition -> Definition
    addCompilerPragma :: [Char] -> CompilerPragma -> Definition -> Definition
    addCompilerPragma [Char]
    backend CompilerPragma
    pragma = (CompiledRepresentation -> CompiledRepresentation)
    -> Definition -> Definition
    updateDefCompiledRep ((CompiledRepresentation -> CompiledRepresentation)
     -> Definition -> Definition)
    -> (CompiledRepresentation -> CompiledRepresentation)
    -> Definition
    -> Definition
    forall a b. (a -> b) -> a -> b
    $ ([CompilerPragma] -> [CompilerPragma] -> [CompilerPragma])
    -> [Char]
    -> [CompilerPragma]
    -> CompiledRepresentation
    -> CompiledRepresentation
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith [CompilerPragma] -> [CompilerPragma] -> [CompilerPragma]
    forall a. [a] -> [a] -> [a]
    (++) [Char]
    backend [CompilerPragma
    pragma]

    updateFunClauses :: ([Clause] -> [Clause]) -> (Defn -> Defn)
    updateFunClauses :: ([Clause] -> [Clause]) -> Defn -> Defn
    updateFunClauses [Clause] -> [Clause]
    f def :: Defn
    def@Function{ funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs} = Defn
    def { funClauses :: [Clause]
    funClauses = [Clause] -> [Clause]
    f [Clause]
    cs }
    updateFunClauses [Clause] -> [Clause]
    f Defn
    _                              = Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    updateCovering :: ([Clause] -> [Clause]) -> (Defn -> Defn)
    updateCovering :: ([Clause] -> [Clause]) -> Defn -> Defn
    updateCovering [Clause] -> [Clause]
    f def :: Defn
    def@Function{ funCovering :: Defn -> [Clause]
    funCovering = [Clause]
    cs} = Defn
    def { funCovering :: [Clause]
    funCovering = [Clause] -> [Clause]
    f [Clause]
    cs }
    updateCovering [Clause] -> [Clause]
    f Defn
    _                               = Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> (Defn -> Defn)
    updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn
    updateCompiledClauses Maybe CompiledClauses -> Maybe CompiledClauses
    f def :: Defn
    def@Function{ funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Maybe CompiledClauses
    cc} = Defn
    def { funCompiled :: Maybe CompiledClauses
    funCompiled = Maybe CompiledClauses -> Maybe CompiledClauses
    f Maybe CompiledClauses
    cc }
    updateCompiledClauses Maybe CompiledClauses -> Maybe CompiledClauses
    f Defn
    _                              = Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    updateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition
    updateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition
    updateDefCopatternLHS Bool -> Bool
    f def :: Definition
    def@Defn{ defCopatternLHS :: Definition -> Bool
    defCopatternLHS = Bool
    b } = Definition
    def { defCopatternLHS :: Bool
    defCopatternLHS = Bool -> Bool
    f Bool
    b }

    updateDefBlocked :: (Blocked_ -> Blocked_) -> Definition -> Definition
    updateDefBlocked :: (Blocked_ -> Blocked_) -> Definition -> Definition
    updateDefBlocked Blocked_ -> Blocked_
    f def :: Definition
    def@Defn{ defBlocked :: Definition -> Blocked_
    defBlocked = Blocked_
    b } = Definition
    def { defBlocked :: Blocked_
    defBlocked = Blocked_ -> Blocked_
    f Blocked_
    b }

    ---------------------------------------------------------------------------
    -- * Top level module
    ---------------------------------------------------------------------------

    -- | Set the top-level module. This affects the global module id of freshly
    --   generated names.

    -- TODO: Is the hash-function collision-free? If not, then the
    -- implementation of 'setTopLevelModule' should be changed.

    setTopLevelModule :: C.QName -> TCM ()
    setTopLevelModule :: QName -> TCM ()
    setTopLevelModule QName
    x = Lens' NameId TCState
    stFreshNameId Lens' NameId TCState -> NameId -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` Word64 -> ModuleNameHash -> NameId
    NameId Word64
    0 (Word64 -> ModuleNameHash
    ModuleNameHash (Word64 -> ModuleNameHash) -> Word64 -> ModuleNameHash
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Word64
    hashString ([Char] -> Word64) -> [Char] -> Word64
    forall a b. (a -> b) -> a -> b
    $ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    x)

    -- | Use a different top-level module for a computation. Used when generating
    --   names for imported modules.
    withTopLevelModule :: C.QName -> TCM a -> TCM a
    withTopLevelModule :: forall a. QName -> TCM a -> TCM a
    withTopLevelModule QName
    x TCM a
    m = do
      NameId
    next <- Lens' NameId TCState -> TCMT IO NameId
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' NameId TCState
    stFreshNameId
      QName -> TCM ()
    setTopLevelModule QName
    x
      a
    y <- TCM a
    m
      Lens' NameId TCState
    stFreshNameId Lens' NameId TCState -> NameId -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` NameId
    next
      a -> TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    y

    currentModuleNameHash :: ReadTCState m => m ModuleNameHash
    currentModuleNameHash :: forall (m :: * -> *). ReadTCState m => m ModuleNameHash
    currentModuleNameHash = do
      NameId Word64
    _ ModuleNameHash
    h <- Lens' NameId TCState -> m NameId
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' NameId TCState
    stFreshNameId
      ModuleNameHash -> m ModuleNameHash
    forall (m :: * -> *) a. Monad m => a -> m a
    return ModuleNameHash
    h

    ---------------------------------------------------------------------------
    -- * Foreign code
    ---------------------------------------------------------------------------

    addForeignCode :: BackendName -> String -> TCM ()
    addForeignCode :: [Char] -> [Char] -> TCM ()
    addForeignCode [Char]
    backend [Char]
    code = do
      Range
    r <- (TCEnv -> Range) -> TCMT IO Range
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Range
    envRange  -- can't use TypeChecking.Monad.Trace.getCurrentRange without cycle
      Lens' (Maybe [ForeignCode]) TCState
    -> (Maybe [ForeignCode] -> Maybe [ForeignCode]) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    modifyTCLens ((Map [Char] [ForeignCode] -> f (Map [Char] [ForeignCode]))
    -> TCState -> f TCState
    Lens' (Map [Char] [ForeignCode]) TCState
    stForeignCode ((Map [Char] [ForeignCode] -> f (Map [Char] [ForeignCode]))
     -> TCState -> f TCState)
    -> ((Maybe [ForeignCode] -> f (Maybe [ForeignCode]))
        -> Map [Char] [ForeignCode] -> f (Map [Char] [ForeignCode]))
    -> (Maybe [ForeignCode] -> f (Maybe [ForeignCode]))
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Lens' (Maybe [ForeignCode]) (Map [Char] [ForeignCode])
    forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
    key [Char]
    backend) ((Maybe [ForeignCode] -> Maybe [ForeignCode]) -> TCM ())
    -> (Maybe [ForeignCode] -> Maybe [ForeignCode]) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [ForeignCode] -> Maybe [ForeignCode]
    forall a. a -> Maybe a
    Just ([ForeignCode] -> Maybe [ForeignCode])
    -> (Maybe [ForeignCode] -> [ForeignCode])
    -> Maybe [ForeignCode]
    -> Maybe [ForeignCode]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Range -> [Char] -> ForeignCode
    ForeignCode Range
    r [Char]
    code ForeignCode -> [ForeignCode] -> [ForeignCode]
    forall a. a -> [a] -> [a]
    :) ([ForeignCode] -> [ForeignCode])
    -> (Maybe [ForeignCode] -> [ForeignCode])
    -> Maybe [ForeignCode]
    -> [ForeignCode]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ForeignCode] -> Maybe [ForeignCode] -> [ForeignCode]
    forall a. a -> Maybe a -> a
    fromMaybe []

    ---------------------------------------------------------------------------
    -- * Interaction output callback
    ---------------------------------------------------------------------------

    getInteractionOutputCallback :: ReadTCState m => m InteractionOutputCallback
    getInteractionOutputCallback :: forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
    getInteractionOutputCallback
      = (TCState -> InteractionOutputCallback)
    -> m InteractionOutputCallback
    forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
    getsTC ((TCState -> InteractionOutputCallback)
     -> m InteractionOutputCallback)
    -> (TCState -> InteractionOutputCallback)
    -> m InteractionOutputCallback
    forall a b. (a -> b) -> a -> b
    $ PersistentTCState -> InteractionOutputCallback
    stInteractionOutputCallback (PersistentTCState -> InteractionOutputCallback)
    -> (TCState -> PersistentTCState)
    -> TCState
    -> InteractionOutputCallback
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> PersistentTCState
    stPersistentState

    appInteractionOutputCallback :: Response -> TCM ()
    appInteractionOutputCallback :: InteractionOutputCallback
    appInteractionOutputCallback Response
    r
      = TCMT IO InteractionOutputCallback
    forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
    getInteractionOutputCallback TCMT IO InteractionOutputCallback
    -> (InteractionOutputCallback -> TCM ()) -> TCM ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ InteractionOutputCallback
    cb -> InteractionOutputCallback
    cb Response
    r

    setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
    setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
    setInteractionOutputCallback InteractionOutputCallback
    cb
      = (PersistentTCState -> PersistentTCState) -> TCM ()
    modifyPersistentState ((PersistentTCState -> PersistentTCState) -> TCM ())
    -> (PersistentTCState -> PersistentTCState) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ PersistentTCState
    s -> PersistentTCState
    s { stInteractionOutputCallback :: InteractionOutputCallback
    stInteractionOutputCallback = InteractionOutputCallback
    cb }

    ---------------------------------------------------------------------------
    -- * Pattern synonyms
    ---------------------------------------------------------------------------

    getPatternSyns :: ReadTCState m => m PatternSynDefns
    getPatternSyns :: forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSyns = Lens' PatternSynDefns TCState -> m PatternSynDefns
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' PatternSynDefns TCState
    stPatternSyns

    setPatternSyns :: PatternSynDefns -> TCM ()
    setPatternSyns :: PatternSynDefns -> TCM ()
    setPatternSyns PatternSynDefns
    m = (PatternSynDefns -> PatternSynDefns) -> TCM ()
    modifyPatternSyns (PatternSynDefns -> PatternSynDefns -> PatternSynDefns
    forall a b. a -> b -> a
    const PatternSynDefns
    m)

    -- | Lens for 'stPatternSyns'.
    modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
    modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
    modifyPatternSyns PatternSynDefns -> PatternSynDefns
    f = Lens' PatternSynDefns TCState
    stPatternSyns Lens' PatternSynDefns TCState
    -> (PatternSynDefns -> PatternSynDefns) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` PatternSynDefns -> PatternSynDefns
    f

    getPatternSynImports :: ReadTCState m => m PatternSynDefns
    getPatternSynImports :: forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSynImports = Lens' PatternSynDefns TCState -> m PatternSynDefns
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' PatternSynDefns TCState
    stPatternSynImports

    -- | Get both local and imported pattern synonyms
    getAllPatternSyns :: ReadTCState m => m PatternSynDefns
    getAllPatternSyns :: forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getAllPatternSyns = PatternSynDefns -> PatternSynDefns -> PatternSynDefns
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (PatternSynDefns -> PatternSynDefns -> PatternSynDefns)
    -> m PatternSynDefns -> m (PatternSynDefns -> PatternSynDefns)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m PatternSynDefns
    forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSyns m (PatternSynDefns -> PatternSynDefns)
    -> m PatternSynDefns -> m PatternSynDefns
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m PatternSynDefns
    forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSynImports

    lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn
    lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn
    lookupPatternSyn (AmbQ List1 QName
    xs) = do
      NonEmpty PatternSynDefn
    defs <- (QName -> TCM PatternSynDefn)
    -> List1 QName -> TCMT IO (NonEmpty PatternSynDefn)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse QName -> TCM PatternSynDefn
    lookupSinglePatternSyn List1 QName
    xs
      case NonEmpty PatternSynDefn -> Maybe PatternSynDefn
    mergePatternSynDefs NonEmpty PatternSynDefn
    defs of
        Just PatternSynDefn
    def   -> PatternSynDefn -> TCM PatternSynDefn
    forall (m :: * -> *) a. Monad m => a -> m a
    return PatternSynDefn
    def
        Maybe PatternSynDefn
    Nothing    -> TypeError -> TCM PatternSynDefn
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM PatternSynDefn)
    -> TypeError -> TCM PatternSynDefn
    forall a b. (a -> b) -> a -> b
    $ List1 (QName, PatternSynDefn) -> TypeError
    CannotResolveAmbiguousPatternSynonym (List1 QName
    -> NonEmpty PatternSynDefn -> List1 (QName, PatternSynDefn)
    forall a b. NonEmpty a -> NonEmpty b -> NonEmpty (a, b)
    NonEmpty.zip List1 QName
    xs NonEmpty PatternSynDefn
    defs)

    lookupSinglePatternSyn :: QName -> TCM PatternSynDefn
    lookupSinglePatternSyn :: QName -> TCM PatternSynDefn
    lookupSinglePatternSyn QName
    x = do
        PatternSynDefns
    s <- TCMT IO PatternSynDefns
    forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSyns
        case QName -> PatternSynDefns -> Maybe PatternSynDefn
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    x PatternSynDefns
    s of
            Just PatternSynDefn
    d  -> PatternSynDefn -> TCM PatternSynDefn
    forall (m :: * -> *) a. Monad m => a -> m a
    return PatternSynDefn
    d
            Maybe PatternSynDefn
    Nothing -> do
                PatternSynDefns
    si <- TCMT IO PatternSynDefns
    forall (m :: * -> *). ReadTCState m => m PatternSynDefns
    getPatternSynImports
                case QName -> PatternSynDefns -> Maybe PatternSynDefn
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup QName
    x PatternSynDefns
    si of
                    Just PatternSynDefn
    d  -> PatternSynDefn -> TCM PatternSynDefn
    forall (m :: * -> *) a. Monad m => a -> m a
    return PatternSynDefn
    d
                    Maybe PatternSynDefn
    Nothing -> QName -> TCM PatternSynDefn
    forall a. QName -> TCM a
    notInScopeError (QName -> TCM PatternSynDefn) -> QName -> TCM PatternSynDefn
    forall a b. (a -> b) -> a -> b
    $ QName -> QName
    qnameToConcrete QName
    x

    ---------------------------------------------------------------------------
    -- * Benchmark
    ---------------------------------------------------------------------------

    -- | Lens getter for 'Benchmark' from 'TCState'.
    theBenchmark :: TCState -> Benchmark
    theBenchmark :: TCState -> Benchmark
    theBenchmark = PersistentTCState -> Benchmark
    stBenchmark (PersistentTCState -> Benchmark)
    -> (TCState -> PersistentTCState) -> TCState -> Benchmark
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TCState -> PersistentTCState
    stPersistentState

    -- | Lens map for 'Benchmark'.
    updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState
    updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState
    updateBenchmark Benchmark -> Benchmark
    f = (PersistentTCState -> PersistentTCState) -> TCState -> TCState
    updatePersistentState ((PersistentTCState -> PersistentTCState) -> TCState -> TCState)
    -> (PersistentTCState -> PersistentTCState) -> TCState -> TCState
    forall a b. (a -> b) -> a -> b
    $ \ PersistentTCState
    s -> PersistentTCState
    s { stBenchmark :: Benchmark
    stBenchmark = Benchmark -> Benchmark
    f (PersistentTCState -> Benchmark
    stBenchmark PersistentTCState
    s) }

    -- | Lens getter for 'Benchmark' from 'TCM'.
    getBenchmark :: TCM Benchmark
    getBenchmark :: TCM Benchmark
    getBenchmark = (TCState -> Benchmark) -> TCM Benchmark
    forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
    getsTC ((TCState -> Benchmark) -> TCM Benchmark)
    -> (TCState -> Benchmark) -> TCM Benchmark
    forall a b. (a -> b) -> a -> b
    $ TCState -> Benchmark
    theBenchmark

    -- | Lens modify for 'Benchmark'.
    modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()
    modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()
    modifyBenchmark = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC' ((TCState -> TCState) -> TCM ())
    -> ((Benchmark -> Benchmark) -> TCState -> TCState)
    -> (Benchmark -> Benchmark)
    -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Benchmark -> Benchmark) -> TCState -> TCState
    updateBenchmark

    ---------------------------------------------------------------------------
    -- * Instance definitions
    ---------------------------------------------------------------------------

    -- | Look through the signature and reconstruct the instance table.
    addImportedInstances :: Signature -> TCM ()
    addImportedInstances :: Signature -> TCM ()
    addImportedInstances Signature
    sig = do
      let itable :: Map QName (Set QName)
    itable = (Set QName -> Set QName -> Set QName)
    -> [(QName, Set QName)] -> Map QName (Set QName)
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith Set QName -> Set QName -> Set QName
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union
                   [ (QName
    c, QName -> Set QName
    forall a. a -> Set a
    Set.singleton QName
    i)
                   | (QName
    i, Defn{ defInstance :: Definition -> Maybe QName
    defInstance = Just QName
    c }) <- HashMap QName Definition -> [(QName, Definition)]
    forall k v. HashMap k v -> [(k, v)]
    HMap.toList (HashMap QName Definition -> [(QName, Definition)])
    -> HashMap QName Definition -> [(QName, Definition)]
    forall a b. (a -> b) -> a -> b
    $ Signature
    sig Signature
    -> Lens' (HashMap QName Definition) Signature
    -> HashMap QName Definition
    forall o i. o -> Lens' i o -> i
    ^. Lens' (HashMap QName Definition) Signature
    sigDefinitions ]
      Lens' (Map QName (Set QName)) TCState
    stImportedInstanceDefs Lens' (Map QName (Set QName)) TCState
    -> (Map QName (Set QName) -> Map QName (Set QName)) -> TCM ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> (a -> a) -> m ()
    `modifyTCLens` (Set QName -> Set QName -> Set QName)
    -> Map QName (Set QName)
    -> Map QName (Set QName)
    -> Map QName (Set QName)
    forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
    Map.unionWith Set QName -> Set QName -> Set QName
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Map QName (Set QName)
    itable

    -- | Lens for 'stInstanceDefs'.
    updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> (TCState -> TCState)
    updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
    updateInstanceDefs = Lens' TempInstanceTable TCState
    -> (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
    forall i o. Lens' i o -> LensMap i o
    over Lens' TempInstanceTable TCState
    stInstanceDefs

    modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
    modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
    modifyInstanceDefs = (TCState -> TCState) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (TCState -> TCState) -> m ()
    modifyTC ((TCState -> TCState) -> TCM ())
    -> ((TempInstanceTable -> TempInstanceTable) -> TCState -> TCState)
    -> (TempInstanceTable -> TempInstanceTable)
    -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
    updateInstanceDefs

    getAllInstanceDefs :: TCM TempInstanceTable
    getAllInstanceDefs :: TCM TempInstanceTable
    getAllInstanceDefs = do
      (Map QName (Set QName)
    table,Set QName
    xs) <- Lens' TempInstanceTable TCState -> TCM TempInstanceTable
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' TempInstanceTable TCState
    stInstanceDefs
      Map QName (Set QName)
    itable <- Lens' (Map QName (Set QName)) TCState
    -> TCMT IO (Map QName (Set QName))
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map QName (Set QName)) TCState
    stImportedInstanceDefs
      let !table' :: Map QName (Set QName)
    table' = (Set QName -> Set QName -> Set QName)
    -> Map QName (Set QName)
    -> Map QName (Set QName)
    -> Map QName (Set QName)
    forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
    Map.unionWith Set QName -> Set QName -> Set QName
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union Map QName (Set QName)
    itable Map QName (Set QName)
    table
      TempInstanceTable -> TCM TempInstanceTable
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Map QName (Set QName)
    table', Set QName
    xs)

    getAnonInstanceDefs :: TCM (Set QName)
    getAnonInstanceDefs :: TCM (Set QName)
    getAnonInstanceDefs = TempInstanceTable -> Set QName
    forall a b. (a, b) -> b
    snd (TempInstanceTable -> Set QName)
    -> TCM TempInstanceTable -> TCM (Set QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM TempInstanceTable
    getAllInstanceDefs

    -- | Remove all instances whose type is still unresolved.
    clearAnonInstanceDefs :: TCM ()
    clearAnonInstanceDefs :: TCM ()
    clearAnonInstanceDefs = (TempInstanceTable -> TempInstanceTable) -> TCM ()
    modifyInstanceDefs ((TempInstanceTable -> TempInstanceTable) -> TCM ())
    -> (TempInstanceTable -> TempInstanceTable) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Set QName -> Set QName) -> TempInstanceTable -> TempInstanceTable
    forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd ((Set QName -> Set QName)
     -> TempInstanceTable -> TempInstanceTable)
    -> (Set QName -> Set QName)
    -> TempInstanceTable
    -> TempInstanceTable
    forall a b. (a -> b) -> a -> b
    $ Set QName -> Set QName -> Set QName
    forall a b. a -> b -> a
    const Set QName
    forall a. Set a
    Set.empty

    -- | Add an instance whose type is still unresolved.
    addUnknownInstance :: QName -> TCM ()
    addUnknownInstance :: QName -> TCM ()
    addUnknownInstance QName
    x = do
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl.instance" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        [Char]
    "adding definition " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++
        [Char]
    " to the instance table (the type is not yet known)"
      (TempInstanceTable -> TempInstanceTable) -> TCM ()
    modifyInstanceDefs ((TempInstanceTable -> TempInstanceTable) -> TCM ())
    -> (TempInstanceTable -> TempInstanceTable) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Set QName -> Set QName) -> TempInstanceTable -> TempInstanceTable
    forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd ((Set QName -> Set QName)
     -> TempInstanceTable -> TempInstanceTable)
    -> (Set QName -> Set QName)
    -> TempInstanceTable
    -> TempInstanceTable
    forall a b. (a -> b) -> a -> b
    $ QName -> Set QName -> Set QName
    forall a. Ord a => a -> Set a -> Set a
    Set.insert QName
    x

    -- | Add instance to some ``class''.
    addNamedInstance
      :: QName  -- ^ Name of the instance.
      -> QName  -- ^ Name of the class.
      -> TCM ()
    addNamedInstance :: QName -> QName -> TCM ()
    addNamedInstance QName
    x QName
    n = do
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.decl.instance" Int
    10 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        [Char]
    "adding definition " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " to instance table for " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    n
      -- Mark x as instance for n.
      (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    x ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ \ Definition
    d -> Definition
    d { defInstance :: Maybe QName
    defInstance = QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    n }
      -- Add x to n's instances.
      (TempInstanceTable -> TempInstanceTable) -> TCM ()
    modifyInstanceDefs ((TempInstanceTable -> TempInstanceTable) -> TCM ())
    -> (TempInstanceTable -> TempInstanceTable) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Map QName (Set QName) -> Map QName (Set QName))
    -> TempInstanceTable -> TempInstanceTable
    forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst ((Map QName (Set QName) -> Map QName (Set QName))
     -> TempInstanceTable -> TempInstanceTable)
    -> (Map QName (Set QName) -> Map QName (Set QName))
    -> TempInstanceTable
    -> TempInstanceTable
    forall a b. (a -> b) -> a -> b
    $ (Set QName -> Set QName -> Set QName)
    -> QName
    -> Set QName
    -> Map QName (Set QName)
    -> Map QName (Set QName)
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith Set QName -> Set QName -> Set QName
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union QName
    n (Set QName -> Map QName (Set QName) -> Map QName (Set QName))
    -> Set QName -> Map QName (Set QName) -> Map QName (Set QName)
    forall a b. (a -> b) -> a -> b
    $ QName -> Set QName
    forall a. a -> Set a
    Set.singleton QName
    x