    module Agda.TypeChecking.Conversion.Pure where

    -- Control.Monad.Fail import is redundant since GHC 8.8.1
    import Control.Monad.Fail (MonadFail)

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

    import Data.String

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.MetaVars (unblockOnAnyMetaIn)

    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.Either
    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
    <$ :: forall a b. a -> PureConversionT m b -> PureConversionT m a
    $c<$ :: forall (m :: * -> *) a b.
    Functor m =>
    a -> PureConversionT m b -> PureConversionT m a
    fmap :: forall a b. (a -> b) -> PureConversionT m a -> PureConversionT m b
    $cfmap :: forall (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> PureConversionT m a -> PureConversionT m b
    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
    <* :: forall a b.
    PureConversionT m a -> PureConversionT m b -> PureConversionT m a
    $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 b
    $c*> :: forall (m :: * -> *) a b.
    Monad m =>
    PureConversionT m a -> PureConversionT m b -> PureConversionT m b
    liftA2 :: forall a b c.
    (a -> b -> c)
    -> PureConversionT m a
    -> PureConversionT m b
    -> PureConversionT m c
    $cliftA2 :: forall (m :: * -> *) a b c.
    Monad m =>
    (a -> b -> c)
    -> PureConversionT m a
    -> PureConversionT m b
    -> PureConversionT m c
    <*> :: forall a b.
    PureConversionT m (a -> b)
    -> PureConversionT m a -> PureConversionT m b
    $c<*> :: forall (m :: * -> *) a b.
    Monad m =>
    PureConversionT m (a -> b)
    -> PureConversionT m a -> PureConversionT m b
    pure :: forall a. a -> PureConversionT m a
    $cpure :: forall (m :: * -> *) a. Monad m => a -> 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
    return :: forall a. a -> PureConversionT m a
    $creturn :: forall (m :: * -> *) a. Monad m => a -> PureConversionT m a
    >> :: 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 b
    >>= :: forall a b.
    PureConversionT m a
    -> (a -> PureConversionT m b) -> PureConversionT m b
    $c>>= :: forall (m :: * -> *) a b.
    Monad m =>
    PureConversionT m a
    -> (a -> PureConversionT m b) -> PureConversionT m b
    Monad, MonadError TCErr, MonadState FreshThings, MonadDebug (PureConversionT m)
    MonadTCEnv (PureConversionT m)
    MonadReduce (PureConversionT m)
    ReadTCState (PureConversionT m)
    MonadAddContext (PureConversionT m)
    HasBuiltins (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
    -> MonadDebug m
    -> MonadReduce m
    -> MonadTCEnv m
    -> ReadTCState m
    -> PureTCM m
    forall {m :: * -> *}.
    (HasBuiltins m, HasConstInfo m, MonadAddContext m,
     MonadReduce m) =>
    MonadDebug (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) =>
    MonadAddContext (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) =>
    HasConstInfo (PureConversionT m)
    PureTCM)

    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, Show a) =>
    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)

    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, Show a) =>
    PureConversionT m a -> m (Maybe a)
    runPureConversion (Type -> Type -> PureConversionT m ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    equalType Type
    a Type
    b)

    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, Show a) =>
    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)

    runPureConversion
      :: (MonadBlock m, PureTCM m, Show a)
      => PureConversionT m a -> m (Maybe a)
    runPureConversion :: forall (m :: * -> *) a.
    (MonadBlock m, PureTCM m, Show a) =>
    PureConversionT m a -> m (Maybe a)
    runPureConversion (PureConversionT ExceptT TCErr (StateT FreshThings m) a
    m) = Lens' Bool TCEnv -> (Bool -> Bool) -> m (Maybe a) -> m (Maybe a)
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' Bool TCEnv
    eCompareBlocked (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (m (Maybe a) -> m (Maybe a)) -> m (Maybe a) -> m (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ do
      Int
    i <- Lens' Int TCState -> m Int
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' Int TCState
    stFreshInt
      ProblemId
    pid <- Lens' ProblemId TCState -> m ProblemId
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' ProblemId TCState
    stFreshProblemId
      NameId
    nid <- Lens' NameId TCState -> m NameId
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' NameId TCState
    stFreshNameId
      let frsh :: FreshThings
    frsh = Int -> ProblemId -> NameId -> FreshThings
    FreshThings Int
    i ProblemId
    pid NameId
    nid
      Either TCErr a
    result <- (Either TCErr a, FreshThings) -> Either TCErr a
    forall a b. (a, b) -> a
    fst ((Either TCErr a, FreshThings) -> Either TCErr a)
    -> m (Either TCErr a, FreshThings) -> m (Either TCErr a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> StateT FreshThings m (Either TCErr a)
    -> FreshThings -> m (Either TCErr a, FreshThings)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (ExceptT TCErr (StateT FreshThings m) a
    -> StateT FreshThings m (Either TCErr a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT ExceptT TCErr (StateT FreshThings m) a
    m) FreshThings
    frsh
      [Char] -> Int -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.conv.pure" Int
    40 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "runPureConversion result: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Either TCErr a -> [Char]
    forall a. Show a => a -> [Char]
    show Either TCErr a
    result
      case Either TCErr a
    result of
        Left (PatternErr Blocker
    block)
         | Blocker
    block Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    == Blocker
    neverUnblock -> Maybe a -> m (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing
         | Bool
    otherwise             -> Blocker -> m (Maybe a)
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    block
        Left TypeError{}   -> Maybe a -> m (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing
        Left Exception{}   -> m (Maybe a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Left IOException{} -> m (Maybe a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Right a
    x            -> Maybe a -> m (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ a -> Maybe a
    forall a. a -> Maybe a
    Just a
    x

    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 (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 (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 (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 :: [Char] -> PureConversionT m a
    fromString [Char]
    s = a -> PureConversionT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char] -> a
    forall a. IsString a => [Char] -> a
    fromString [Char]
    s)

    instance Monad m => Null (PureConversionT m Doc) where
      empty :: PureConversionT m Doc
    empty = Doc -> PureConversionT m Doc
    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 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 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 e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err

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

    instance (PureTCM m, MonadBlock 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 (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
        Maybe Blocker
    bv <- Term -> PureConversionT m (Maybe Blocker)
    forall t (m :: * -> *).
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> m (Maybe Blocker)
    isBlocked Term
    v
        let blocker :: Blocker
    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
        Blocker -> PureConversionT m ()
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    blocker
      assignTerm' :: MonadMetaSolver (PureConversionT m) =>
    MetaId -> [Arg [Char]] -> Term -> PureConversionT m ()
    assignTerm' MetaId
    m [Arg [Char]]
    _ Term
    v = do
        Maybe Blocker
    bv <- Term -> PureConversionT m (Maybe Blocker)
    forall t (m :: * -> *).
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> m (Maybe Blocker)
    isBlocked Term
    v
        let blocker :: Blocker
    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
        Blocker -> PureConversionT m ()
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    blocker
      etaExpandMeta :: [MetaKind] -> MetaId -> PureConversionT m ()
    etaExpandMeta [MetaKind]
    _ MetaId
    _ = () -> PureConversionT m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> PureConversionT m ()
    updateMetaVar MetaId
    _ MetaVariable -> MetaVariable
    _ = Blocker -> PureConversionT m ()
    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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        KeepMetas
    KeepMetas     -> () -> PureConversionT m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        KeepMetas
    RollBackMetas -> PureConversionT m ()
    fallback

    instance (PureTCM m, MonadBlock m) => MonadInteractionPoints (PureConversionT m) where
      freshInteractionId :: PureConversionT m InteractionId
    freshInteractionId = Blocker -> PureConversionT m InteractionId
    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 (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
        ConcreteNames
    concNames <- Lens' ConcreteNames TCState -> PureConversionT m ConcreteNames
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' ConcreteNames TCState
    stConcreteNames
        (a, ConcreteNames) -> a
    forall a b. (a, b) -> a
    fst ((a, ConcreteNames) -> a)
    -> PureConversionT m (a, ConcreteNames) -> PureConversionT m a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> StateT ConcreteNames (PureConversionT m) a
    -> ConcreteNames -> PureConversionT m (a, ConcreteNames)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT StateT ConcreteNames (PureConversionT m) a
    m ConcreteNames
    concNames

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

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

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

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

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