    module Agda.TypeChecking.Conversion.Pure where

    import Control.Monad.Except
    import Control.Monad.State

    import Data.String

    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    import {-# SOURCE #-} Agda.TypeChecking.Conversion
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Reduce (isBlocked)
    import Agda.TypeChecking.Warnings

    import Agda.Utils.Maybe
    import Agda.Utils.Null

    import Agda.Utils.Impossible

    data FreshThings = FreshThings
      { FreshThings -> Int
    freshInt       :: Int
      , FreshThings -> ProblemId
    freshProblemId :: ProblemId
      , FreshThings -> NameId
    freshNameId    :: NameId
      }

    newtype PureConversionT m a = PureConversionT
      { forall (m :: * -> *) a.
    PureConversionT m a -> ExceptT TCErr (StateT FreshThings m) a
    unPureConversionT :: ExceptT TCErr (StateT FreshThings m) a }
      deriving ((forall a b.
     (a -> b) -> PureConversionT m a -> PureConversionT m b)
    -> (forall a b. a -> PureConversionT m b -> PureConversionT m a)
    -> Functor (PureConversionT m)
    forall a b. a -> PureConversionT m b -> PureConversionT m a
    forall a b. (a -> b) -> PureConversionT m a -> PureConversionT m b
    forall (m :: * -> *) a b.
    Functor m =>
    a -> PureConversionT m b -> PureConversionT m a
    forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> PureConversionT m a -> PureConversionT m b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> PureConversionT m a -> PureConversionT m b
    fmap :: forall a b. (a -> b) -> PureConversionT m a -> PureConversionT m b
    $c<$ :: forall (m :: * -> *) a b.
    Functor m =>
    a -> PureConversionT m b -> PureConversionT m a
    <$ :: forall a b. a -> PureConversionT m b -> PureConversionT m a
    Functor, Functor (PureConversionT m)
    Functor (PureConversionT m) =>
    (forall a. a -> PureConversionT m a)
    -> (forall a b.
        PureConversionT m (a -> b)
        -> PureConversionT m a -> PureConversionT m b)
    -> (forall a b c.
        (a -> b -> c)
        -> PureConversionT m a
        -> PureConversionT m b
        -> PureConversionT m c)
    -> (forall a b.
        PureConversionT m a -> PureConversionT m b -> PureConversionT m b)
    -> (forall a b.
        PureConversionT m a -> PureConversionT m b -> PureConversionT m a)
    -> Applicative (PureConversionT m)
    forall a. a -> PureConversionT m a
    forall a b.
    PureConversionT m a -> PureConversionT m b -> PureConversionT m a
    forall a b.
    PureConversionT m a -> PureConversionT m b -> PureConversionT m b
    forall a b.
    PureConversionT m (a -> b)
    -> PureConversionT m a -> PureConversionT m b
    forall a b c.
    (a -> b -> c)
    -> PureConversionT m a
    -> PureConversionT m b
    -> PureConversionT m c
    forall (m :: * -> *). Monad m => Functor (PureConversionT m)
    forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
    forall (m :: * -> *) a b.
    Monad m =>
    PureConversionT m a -> PureConversionT m b -> PureConversionT m a
    forall (m :: * -> *) a b.
    Monad m =>
    PureConversionT m a -> PureConversionT m b -> PureConversionT m b
    forall (m :: * -> *) a b.
    Monad m =>
    PureConversionT m (a -> b)
    -> PureConversionT m a -> PureConversionT m b
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> b -> c)
    -> PureConversionT m a
    -> PureConversionT m b
    -> PureConversionT m c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    $cpure :: forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
    pure :: forall a. a -> PureConversionT m a
    $c<*> :: forall (m :: * -> *) a b.
    Monad m =>
    PureConversionT m (a -> b)
    -> PureConversionT m a -> PureConversionT m b
    <*> :: forall a b.
    PureConversionT m (a -> b)
    -> PureConversionT m a -> PureConversionT m b
    $cliftA2 :: forall (m :: * -> *) a b c.
    Monad m =>
    (a -> b -> c)
    -> PureConversionT m a
    -> PureConversionT m b
    -> PureConversionT m c
    liftA2 :: forall a b c.
    (a -> b -> c)
    -> PureConversionT m a
    -> PureConversionT m b
    -> PureConversionT m c
    $c*> :: forall (m :: * -> *) a b.
    Monad m =>
    PureConversionT m a -> PureConversionT m b -> PureConversionT m b
    *> :: forall a b.
    PureConversionT m a -> PureConversionT m b -> PureConversionT m b
    $c<* :: forall (m :: * -> *) a b.
    Monad m =>
    PureConversionT m a -> PureConversionT m b -> PureConversionT m a
    <* :: forall a b.
    PureConversionT m a -> PureConversionT m b -> PureConversionT m a
    Applicative, Applicative (PureConversionT m)
    Applicative (PureConversionT m) =>
    (forall a b.
     PureConversionT m a
     -> (a -> PureConversionT m b) -> PureConversionT m b)
    -> (forall a b.
        PureConversionT m a -> PureConversionT m b -> PureConversionT m b)
    -> (forall a. a -> PureConversionT m a)
    -> Monad (PureConversionT m)
    forall a. a -> PureConversionT m a
    forall a b.
    PureConversionT m a -> PureConversionT m b -> PureConversionT m b
    forall a b.
    PureConversionT m a
    -> (a -> PureConversionT m b) -> PureConversionT m b
    forall (m :: * -> *). Monad m => Applicative (PureConversionT m)
    forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
    forall (m :: * -> *) a b.
    Monad m =>
    PureConversionT m a -> PureConversionT m b -> PureConversionT m b
    forall (m :: * -> *) a b.
    Monad m =>
    PureConversionT m a
    -> (a -> PureConversionT m b) -> PureConversionT m b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    $c>>= :: forall (m :: * -> *) a b.
    Monad m =>
    PureConversionT m a
    -> (a -> PureConversionT m b) -> PureConversionT m b
    >>= :: forall a b.
    PureConversionT m a
    -> (a -> PureConversionT m b) -> PureConversionT m b
    $c>> :: forall (m :: * -> *) a b.
    Monad m =>
    PureConversionT m a -> PureConversionT m b -> PureConversionT m b
    >> :: forall a b.
    PureConversionT m a -> PureConversionT m b -> PureConversionT m b
    $creturn :: forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
    return :: forall a. a -> PureConversionT m a
    Monad, MonadError TCErr, MonadState FreshThings, MonadTCEnv (PureConversionT m)
    MonadReduce (PureConversionT m)
    ReadTCState (PureConversionT m)
    HasBuiltins (PureConversionT m)
    MonadAddContext (PureConversionT m)
    MonadDebug (PureConversionT m)
    HasConstInfo (PureConversionT m)
    (HasBuiltins (PureConversionT m), HasConstInfo (PureConversionT m),
     MonadAddContext (PureConversionT m),
     MonadDebug (PureConversionT m), MonadReduce (PureConversionT m),
     MonadTCEnv (PureConversionT m), ReadTCState (PureConversionT m)) =>
    PureTCM (PureConversionT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    MonadTCEnv (PureConversionT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    MonadReduce (PureConversionT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    ReadTCState (PureConversionT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    HasBuiltins (PureConversionT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    MonadAddContext (PureConversionT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    MonadDebug (PureConversionT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    HasConstInfo (PureConversionT m)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadDebug m,
     MonadReduce m, MonadTCEnv m, ReadTCState m) =>
    PureTCM m
    PureTCM)

    {-# SPECIALIZE pureEqualTerm :: Type -> Term -> Term -> TCM Bool #-}
    pureEqualTerm
      :: (PureTCM m, MonadBlock m)
      => Type -> Term -> Term -> m Bool
    pureEqualTerm :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Type -> Term -> Term -> m Bool
    pureEqualTerm Type
    a Term
    u Term
    v =
      Maybe () -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe () -> Bool) -> m (Maybe ()) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PureConversionT m () -> m (Maybe ())
    forall (m :: * -> *) a.
    (MonadBlock m, PureTCM m) =>
    PureConversionT m a -> m (Maybe a)
    runPureConversion (Type -> Term -> Term -> PureConversionT m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Type -> Term -> Term -> m ()
    equalTerm Type
    a Term
    u Term
    v)

    {-# SPECIALIZE pureEqualTermB :: Type -> Term -> Term -> TCM (Either Blocker Bool) #-}
    -- | Return the blocker instead of throwing a `patternViolation`.
    pureEqualTermB :: PureTCM m => Type -> Term -> Term -> m (Either Blocker Bool)
    pureEqualTermB :: forall (m :: * -> *).
    PureTCM m =>
    Type -> Term -> Term -> m (Either Blocker Bool)
    pureEqualTermB Type
    a Term
    u Term
    v =
      (Maybe () -> Bool)
    -> Either Blocker (Maybe ()) -> Either Blocker Bool
    forall a b. (a -> b) -> Either Blocker a -> Either Blocker b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Maybe () -> Bool
    forall a. Maybe a -> Bool
    isJust (Either Blocker (Maybe ()) -> Either Blocker Bool)
    -> m (Either Blocker (Maybe ())) -> m (Either Blocker Bool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PureConversionT m () -> m (Either Blocker (Maybe ()))
    forall (m :: * -> *) a.
    PureTCM m =>
    PureConversionT m a -> m (Either Blocker (Maybe a))
    runPureConversionB (Type -> Term -> Term -> PureConversionT m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Type -> Term -> Term -> m ()
    equalTerm Type
    a Term
    u Term
    v)

    {-# SPECIALIZE pureEqualType :: Type -> Type -> TCM Bool #-}
    pureEqualType
      :: (PureTCM m, MonadBlock m)
      => Type -> Type -> m Bool
    pureEqualType :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Type -> Type -> m Bool
    pureEqualType Type
    a Type
    b =
      Maybe () -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe () -> Bool) -> m (Maybe ()) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PureConversionT m () -> m (Maybe ())
    forall (m :: * -> *) a.
    (MonadBlock m, PureTCM m) =>
    PureConversionT m a -> m (Maybe a)
    runPureConversion (Type -> Type -> PureConversionT m ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    equalType Type
    a Type
    b)

    {-# SPECIALIZE pureEqualType :: Type -> Type -> TCM Bool #-}
    -- | Return the blocker instead of throwing a `patternViolation`.
    pureEqualTypeB :: PureTCM m => Type -> Type -> m (Either Blocker Bool)
    pureEqualTypeB :: forall (m :: * -> *).
    PureTCM m =>
    Type -> Type -> m (Either Blocker Bool)
    pureEqualTypeB Type
    a Type
    b =
      (Maybe () -> Bool)
    -> Either Blocker (Maybe ()) -> Either Blocker Bool
    forall a b. (a -> b) -> Either Blocker a -> Either Blocker b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Maybe () -> Bool
    forall a. Maybe a -> Bool
    isJust (Either Blocker (Maybe ()) -> Either Blocker Bool)
    -> m (Either Blocker (Maybe ())) -> m (Either Blocker Bool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PureConversionT m () -> m (Either Blocker (Maybe ()))
    forall (m :: * -> *) a.
    PureTCM m =>
    PureConversionT m a -> m (Either Blocker (Maybe a))
    runPureConversionB (Type -> Type -> PureConversionT m ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    equalType Type
    a Type
    b)

    {-# SPECIALIZE pureCompareAs :: Comparison -> CompareAs -> Term -> Term -> TCM Bool #-}
    pureCompareAs
      :: (PureTCM m, MonadBlock m)
      => Comparison -> CompareAs -> Term -> Term -> m Bool
    pureCompareAs :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Comparison -> CompareAs -> Term -> Term -> m Bool
    pureCompareAs Comparison
    cmp CompareAs
    a Term
    u Term
    v =
      Maybe () -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe () -> Bool) -> m (Maybe ()) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PureConversionT m () -> m (Maybe ())
    forall (m :: * -> *) a.
    (MonadBlock m, PureTCM m) =>
    PureConversionT m a -> m (Maybe a)
    runPureConversion (Comparison -> CompareAs -> Term -> Term -> PureConversionT m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> CompareAs -> Term -> Term -> m ()
    compareAs Comparison
    cmp CompareAs
    a Term
    u Term
    v)

    {-# SPECIALIZE runPureConversion :: PureConversionT TCM a -> TCM (Maybe a) #-}
    runPureConversion
      :: (MonadBlock m, PureTCM m)
      => PureConversionT m a -> m (Maybe a)
    runPureConversion :: forall (m :: * -> *) a.
    (MonadBlock m, PureTCM m) =>
    PureConversionT m a -> m (Maybe a)
    runPureConversion PureConversionT m a
    m = (Blocker -> m (Maybe a))
    -> (Maybe a -> m (Maybe a))
    -> Either Blocker (Maybe a)
    -> m (Maybe a)
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either Blocker -> m (Maybe a)
    forall a. Blocker -> m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Maybe a -> m (Maybe a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Either Blocker (Maybe a) -> m (Maybe a))
    -> m (Either Blocker (Maybe a)) -> m (Maybe a)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< PureConversionT m a -> m (Either Blocker (Maybe a))
    forall (m :: * -> *) a.
    PureTCM m =>
    PureConversionT m a -> m (Either Blocker (Maybe a))
    runPureConversionB PureConversionT m a
    m

    {-# SPECIALIZE runPureConversionB :: PureConversionT TCM a -> TCM (Either Blocker (Maybe a)) #-}
    runPureConversionB :: PureTCM m => PureConversionT m a -> m (Either Blocker (Maybe a))
    runPureConversionB :: forall (m :: * -> *) a.
    PureTCM m =>
    PureConversionT m a -> m (Either Blocker (Maybe a))
    runPureConversionB (PureConversionT ExceptT TCErr (StateT FreshThings m) a
    m) = Lens' TCEnv Bool
    -> (Bool -> Bool)
    -> m (Either Blocker (Maybe a))
    -> m (Either Blocker (Maybe a))
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eCompareBlocked (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (m (Either Blocker (Maybe a)) -> m (Either Blocker (Maybe a)))
    -> m (Either Blocker (Maybe a)) -> m (Either Blocker (Maybe a))
    forall a b. (a -> b) -> a -> b
    $
      VerboseKey
    -> Int
    -> VerboseKey
    -> m (Either Blocker (Maybe a))
    -> m (Either Blocker (Maybe a))
    forall a. VerboseKey -> Int -> VerboseKey -> m a -> m a
    forall (m :: * -> *) a.
    MonadDebug m =>
    VerboseKey -> Int -> VerboseKey -> m a -> m a
    verboseBracket VerboseKey
    "tc.conv.pure" Int
    40 VerboseKey
    "runPureConversion" (m (Either Blocker (Maybe a)) -> m (Either Blocker (Maybe a)))
    -> m (Either Blocker (Maybe a)) -> m (Either Blocker (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ do
      i <- Lens' TCState Int -> m Int
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (Int -> f Int) -> TCState -> f TCState
    Lens' TCState Int
    stFreshInt
      pid <- useR stFreshProblemId
      nid <- useR stFreshNameId
      let frsh = Int -> ProblemId -> NameId -> FreshThings
    FreshThings Int
    i ProblemId
    pid NameId
    nid
      result <- fst <$> runStateT (runExceptT m) frsh
      case result of
        Left (PatternErr Blocker
    block)
         | Blocker
    block Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    == Blocker
    neverUnblock -> do
             TCMT IO Doc -> m ()
    forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
    debugResult TCMT IO Doc
    "stuck"
             Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocker (Maybe a) -> m (Either Blocker (Maybe a)))
    -> Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ Maybe a -> Either Blocker (Maybe a)
    forall a b. b -> Either a b
    Right Maybe a
    forall a. Maybe a
    Nothing
         | Bool
    otherwise             -> do
             TCMT IO Doc -> m ()
    forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
    debugResult (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "blocked on" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Blocker -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
    prettyTCM Blocker
    block
             Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocker (Maybe a) -> m (Either Blocker (Maybe a)))
    -> Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Either Blocker (Maybe a)
    forall a b. a -> Either a b
    Left Blocker
    block
        Left TypeError{}         -> do
          TCMT IO Doc -> m ()
    forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
    debugResult TCMT IO Doc
    "type error"
          Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocker (Maybe a) -> m (Either Blocker (Maybe a)))
    -> Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ Maybe a -> Either Blocker (Maybe a)
    forall a b. b -> Either a b
    Right Maybe a
    forall a. Maybe a
    Nothing
        Left GenericException{}  -> m (Either Blocker (Maybe a))
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Left IOException{}       -> m (Either Blocker (Maybe a))
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Left ParserError{}       -> m (Either Blocker (Maybe a))
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Right a
    x                  -> do
          TCMT IO Doc -> m ()
    forall {m :: * -> *}. MonadDebug m => TCMT IO Doc -> m ()
    debugResult TCMT IO Doc
    "success"
          Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocker (Maybe a) -> m (Either Blocker (Maybe a)))
    -> Either Blocker (Maybe a) -> m (Either Blocker (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ Maybe a -> Either Blocker (Maybe a)
    forall a b. b -> Either a b
    Right (Maybe a -> Either Blocker (Maybe a))
    -> Maybe a -> Either Blocker (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ a -> Maybe a
    forall a. a -> Maybe a
    Just a
    x
      where
        debugResult :: TCMT IO Doc -> m ()
    debugResult TCMT IO Doc
    msg = VerboseKey -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "tc.conv.pure" Int
    40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "runPureConversion result: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    msg

    instance MonadTrans PureConversionT where
      lift :: forall (m :: * -> *) a. Monad m => m a -> PureConversionT m a
    lift = ExceptT TCErr (StateT FreshThings m) a -> PureConversionT m a
    forall (m :: * -> *) a.
    ExceptT TCErr (StateT FreshThings m) a -> PureConversionT m a
    PureConversionT (ExceptT TCErr (StateT FreshThings m) a -> PureConversionT m a)
    -> (m a -> ExceptT TCErr (StateT FreshThings m) a)
    -> m a
    -> PureConversionT m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . StateT FreshThings m a -> ExceptT TCErr (StateT FreshThings m) a
    forall (m :: * -> *) a. Monad m => m a -> ExceptT TCErr m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (StateT FreshThings m a -> ExceptT TCErr (StateT FreshThings m) a)
    -> (m a -> StateT FreshThings m a)
    -> m a
    -> ExceptT TCErr (StateT FreshThings m) a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m a -> StateT FreshThings m a
    forall (m :: * -> *) a. Monad m => m a -> StateT FreshThings m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift

    deriving instance MonadFail       m => MonadFail       (PureConversionT m)
    deriving instance HasBuiltins     m => HasBuiltins     (PureConversionT m)
    deriving instance HasConstInfo    m => HasConstInfo    (PureConversionT m)
    deriving instance HasOptions      m => HasOptions      (PureConversionT m)
    deriving instance MonadTCEnv      m => MonadTCEnv      (PureConversionT m)
    deriving instance ReadTCState     m => ReadTCState     (PureConversionT m)
    deriving instance MonadReduce     m => MonadReduce     (PureConversionT m)
    deriving instance MonadAddContext m => MonadAddContext (PureConversionT m)
    deriving instance MonadDebug      m => MonadDebug      (PureConversionT m)

    instance (Monad m, Semigroup a) => Semigroup (PureConversionT m a) where
      PureConversionT m a
    d1 <> :: PureConversionT m a -> PureConversionT m a -> PureConversionT m a
    <> PureConversionT m a
    d2 = a -> a -> a
    forall a. Semigroup a => a -> a -> a
    (<>) (a -> a -> a) -> PureConversionT m a -> PureConversionT m (a -> a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PureConversionT m a
    d1 PureConversionT m (a -> a)
    -> PureConversionT m a -> PureConversionT m a
    forall a b.
    PureConversionT m (a -> b)
    -> PureConversionT m a -> PureConversionT m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> PureConversionT m a
    d2

    instance (IsString a, Monad m) => IsString (PureConversionT m a) where
      fromString :: VerboseKey -> PureConversionT m a
    fromString VerboseKey
    s = a -> PureConversionT m a
    forall a. a -> PureConversionT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (VerboseKey -> a
    forall a. IsString a => VerboseKey -> a
    fromString VerboseKey
    s)

    instance Monad m => Null (PureConversionT m Doc) where
      empty :: PureConversionT m Doc
    empty = Doc -> PureConversionT m Doc
    forall a. a -> PureConversionT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Doc
    forall a. Null a => a
    empty
      null :: PureConversionT m Doc -> Bool
    null = PureConversionT m Doc -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance Monad m => MonadBlock (PureConversionT m) where
      patternViolation :: forall a. Blocker -> PureConversionT m a
    patternViolation = TCErr -> PureConversionT m a
    forall a. TCErr -> PureConversionT m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (TCErr -> PureConversionT m a)
    -> (Blocker -> TCErr) -> Blocker -> PureConversionT m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Blocker -> TCErr
    PatternErr
      catchPatternErr :: forall a.
    (Blocker -> PureConversionT m a)
    -> PureConversionT m a -> PureConversionT m a
    catchPatternErr Blocker -> PureConversionT m a
    handle PureConversionT m a
    m = PureConversionT m a
    m PureConversionT m a
    -> (TCErr -> PureConversionT m a) -> PureConversionT m a
    forall a.
    PureConversionT m a
    -> (TCErr -> PureConversionT m a) -> PureConversionT m a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \case
        PatternErr Blocker
    b -> Blocker -> PureConversionT m a
    handle Blocker
    b
        TCErr
    err          -> TCErr -> PureConversionT m a
    forall a. TCErr -> PureConversionT m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err

    instance PureTCM m => MonadConstraint (PureConversionT m) where
      addConstraint :: Blocker -> Constraint -> PureConversionT m ()
    addConstraint Blocker
    u Constraint
    _ = Blocker -> PureConversionT m ()
    forall a. Blocker -> PureConversionT m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    u
      addAwakeConstraint :: Blocker -> Constraint -> PureConversionT m ()
    addAwakeConstraint Blocker
    u Constraint
    _ = Blocker -> PureConversionT m ()
    forall a. Blocker -> PureConversionT m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    u
      solveConstraint :: Constraint -> PureConversionT m ()
    solveConstraint Constraint
    c = Blocker -> PureConversionT m ()
    forall a. Blocker -> PureConversionT m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    alwaysUnblock  -- TODO: does this happen?
      solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> PureConversionT m ()
    solveSomeAwakeConstraints ProblemConstraint -> Bool
    _ Bool
    _ = () -> PureConversionT m ()
    forall a. a -> PureConversionT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      wakeConstraints :: (ProblemConstraint -> WakeUp) -> PureConversionT m ()
    wakeConstraints ProblemConstraint -> WakeUp
    _ = () -> PureConversionT m ()
    forall a. a -> PureConversionT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      stealConstraints :: ProblemId -> PureConversionT m ()
    stealConstraints ProblemId
    _ = () -> PureConversionT m ()
    forall a. a -> PureConversionT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      modifyAwakeConstraints :: (Constraints -> Constraints) -> PureConversionT m ()
    modifyAwakeConstraints Constraints -> Constraints
    _ = Blocker -> PureConversionT m ()
    forall a. Blocker -> PureConversionT m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    alwaysUnblock  -- TODO: does this happen?
      modifySleepingConstraints :: (Constraints -> Constraints) -> PureConversionT m ()
    modifySleepingConstraints Constraints -> Constraints
    _ = Blocker -> PureConversionT m ()
    forall a. Blocker -> PureConversionT m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    alwaysUnblock  -- TODO: does this happen?

    instance PureTCM m => MonadMetaSolver (PureConversionT m) where
      newMeta' :: forall a.
    MetaInstantiation
    -> Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> PureConversionT m MetaId
    newMeta' MetaInstantiation
    _ Frozen
    _ MetaInfo
    _ MetaPriority
    _ Permutation
    _ Judgement a
    _ = Blocker -> PureConversionT m MetaId
    forall a. Blocker -> PureConversionT m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    alwaysUnblock  -- TODO: does this happen?
      assignV :: CompareDirection
    -> MetaId -> Args -> Term -> CompareAs -> PureConversionT m ()
    assignV CompareDirection
    _ MetaId
    m Args
    _ Term
    v CompareAs
    _ = do
        bv <- Term -> PureConversionT m (Maybe Blocker)
    forall t (m :: * -> *).
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> m (Maybe Blocker)
    isBlocked Term
    v
        let blocker = Maybe Blocker
    -> (Blocker -> Blocker)
    -> (Blocker -> Blocker -> Blocker)
    -> Blocker
    -> Blocker
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe Blocker
    bv Blocker -> Blocker
    forall a. a -> a
    id Blocker -> Blocker -> Blocker
    unblockOnEither (Blocker -> Blocker) -> Blocker -> Blocker
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Blocker
    unblockOnMeta MetaId
    m
        patternViolation blocker
      assignTerm' :: MonadMetaSolver (PureConversionT m) =>
    MetaId -> [Arg VerboseKey] -> Term -> PureConversionT m ()
    assignTerm' MetaId
    m [Arg VerboseKey]
    _ Term
    v = do
        bv <- Term -> PureConversionT m (Maybe Blocker)
    forall t (m :: * -> *).
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> m (Maybe Blocker)
    isBlocked Term
    v
        let blocker = Maybe Blocker
    -> (Blocker -> Blocker)
    -> (Blocker -> Blocker -> Blocker)
    -> Blocker
    -> Blocker
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe Blocker
    bv Blocker -> Blocker
    forall a. a -> a
    id Blocker -> Blocker -> Blocker
    unblockOnEither (Blocker -> Blocker) -> Blocker -> Blocker
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Blocker
    unblockOnMeta MetaId
    m
        patternViolation blocker
      etaExpandMeta :: [MetaClass] -> MetaId -> PureConversionT m ()
    etaExpandMeta [MetaClass]
    _ MetaId
    _ = () -> PureConversionT m ()
    forall a. a -> PureConversionT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> PureConversionT m ()
    updateMetaVar MetaId
    _ MetaVariable -> MetaVariable
    _ = Blocker -> PureConversionT m ()
    forall a. Blocker -> PureConversionT m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    alwaysUnblock  -- TODO: does this happen?
      speculateMetas :: PureConversionT m ()
    -> PureConversionT m KeepMetas -> PureConversionT m ()
    speculateMetas PureConversionT m ()
    fallback PureConversionT m KeepMetas
    m = PureConversionT m KeepMetas
    m PureConversionT m KeepMetas
    -> (KeepMetas -> PureConversionT m ()) -> PureConversionT m ()
    forall a b.
    PureConversionT m a
    -> (a -> PureConversionT m b) -> PureConversionT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        KeepMetas
    KeepMetas     -> () -> PureConversionT m ()
    forall a. a -> PureConversionT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        KeepMetas
    RollBackMetas -> PureConversionT m ()
    fallback

    instance PureTCM m => MonadInteractionPoints (PureConversionT m) where
      freshInteractionId :: PureConversionT m InteractionId
    freshInteractionId = Blocker -> PureConversionT m InteractionId
    forall a. Blocker -> PureConversionT m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    alwaysUnblock  -- TODO: does this happen?
      modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> PureConversionT m ()
    modifyInteractionPoints InteractionPoints -> InteractionPoints
    _ = Blocker -> PureConversionT m ()
    forall a. Blocker -> PureConversionT m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    alwaysUnblock  -- TODO: does this happen?

    -- This is a bogus instance that promptly forgets all concrete names,
    -- but we don't really care
    instance ReadTCState m => MonadStConcreteNames (PureConversionT m) where
      runStConcreteNames :: forall a.
    StateT ConcreteNames (PureConversionT m) a -> PureConversionT m a
    runStConcreteNames StateT ConcreteNames (PureConversionT m) a
    m = do
        concNames <- Lens' TCState ConcreteNames -> PureConversionT m ConcreteNames
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useR (ConcreteNames -> f ConcreteNames) -> TCState -> f TCState
    Lens' TCState ConcreteNames
    stConcreteNames
        fst <$> runStateT m concNames

    instance PureTCM m => MonadWarning (PureConversionT m) where
      addWarning :: Bool -> TCWarning -> PureConversionT m ()
    addWarning Bool
    _enabled TCWarning
    w = case Warning -> WhichWarnings
    classifyWarning (TCWarning -> Warning
    tcWarning TCWarning
    w) of
        WhichWarnings
    ErrorWarnings -> Blocker -> PureConversionT m ()
    forall a. Blocker -> PureConversionT m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    neverUnblock
        WhichWarnings
    AllWarnings   -> () -> PureConversionT m ()
    forall a. a -> PureConversionT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    instance ReadTCState m => MonadStatistics (PureConversionT m) where
      modifyCounter :: VerboseKey -> (Integer -> Integer) -> PureConversionT m ()
    modifyCounter VerboseKey
    _ Integer -> Integer
    _ = () -> PureConversionT m ()
    forall a. a -> PureConversionT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    instance Monad m => MonadFresh ProblemId (PureConversionT m) where
      fresh :: PureConversionT m ProblemId
    fresh = do
        i <- (FreshThings -> ProblemId) -> PureConversionT m ProblemId
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets FreshThings -> ProblemId
    freshProblemId
        modify $ \FreshThings
    f -> FreshThings
    f { freshProblemId = i + 1 }
        return i

    instance Monad m => MonadFresh NameId (PureConversionT m) where
      fresh :: PureConversionT m NameId
    fresh = do
        i <- (FreshThings -> NameId) -> PureConversionT m NameId
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets FreshThings -> NameId
    freshNameId
        modify $ \FreshThings
    f -> FreshThings
    f { freshNameId = succ i }
        return i

    instance Monad m => MonadFresh Int (PureConversionT m) where
      fresh :: PureConversionT m Int
    fresh = do
        i <- (FreshThings -> Int) -> PureConversionT m Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets FreshThings -> Int
    freshInt
        modify $ \FreshThings
    f -> FreshThings
    f { freshInt = i + 1 }
        return i