    {-# LANGUAGE NondecreasingIndentation #-}

    {- |  Non-linear matching of the lhs of a rewrite rule against a
          neutral term.

    Given a lhs

      Δ ⊢ lhs : B

    and a candidate term

      Γ ⊢ t : A

    we seek a substitution Γ ⊢ σ : Δ such that

      Γ ⊢ B[σ] = A   and
      Γ ⊢ lhs[σ] = t : A

    -}

    module Agda.TypeChecking.Rewriting.NonLinMatch where

    import Prelude hiding (null, sequence)

    import Control.Applicative  ( Alternative )
    import Control.Monad        ( void )
    import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )
    import Control.Monad.State  ( MonadState, StateT, runStateT )

    import qualified Control.Monad.Fail as Fail

    import Data.Maybe
    import Data.IntMap (IntMap)
    import qualified Data.IntMap as IntMap
    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet
    import qualified Data.Set as Set

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

    import Agda.TypeChecking.Conversion.Pure
    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Free.Reduce
    import Agda.TypeChecking.Irrelevance (workOnTypes, isPropM)
    import Agda.TypeChecking.Level
    import Agda.TypeChecking.Monad hiding (constructorForm)
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Reduce.Monad
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Primitive.Cubical

    import Agda.Utils.Either
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Permutation
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    -- | Monad for non-linear matching.
    newtype NLM a = NLM { forall a. NLM a -> ExceptT Blocked_ (StateT NLMState ReduceM) a
    unNLM :: ExceptT Blocked_ (StateT NLMState ReduceM) a }
      deriving ( (forall a b. (a -> b) -> NLM a -> NLM b)
    -> (forall a b. a -> NLM b -> NLM a) -> Functor NLM
    forall a b. a -> NLM b -> NLM a
    forall a b. (a -> b) -> NLM a -> NLM 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 -> NLM b -> NLM a
    $c<$ :: forall a b. a -> NLM b -> NLM a
    fmap :: forall a b. (a -> b) -> NLM a -> NLM b
    $cfmap :: forall a b. (a -> b) -> NLM a -> NLM b
    Functor, Functor NLM
    Functor NLM
    -> (forall a. a -> NLM a)
    -> (forall a b. NLM (a -> b) -> NLM a -> NLM b)
    -> (forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c)
    -> (forall a b. NLM a -> NLM b -> NLM b)
    -> (forall a b. NLM a -> NLM b -> NLM a)
    -> Applicative NLM
    forall a. a -> NLM a
    forall a b. NLM a -> NLM b -> NLM a
    forall a b. NLM a -> NLM b -> NLM b
    forall a b. NLM (a -> b) -> NLM a -> NLM b
    forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM 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. NLM a -> NLM b -> NLM a
    $c<* :: forall a b. NLM a -> NLM b -> NLM a
    *> :: forall a b. NLM a -> NLM b -> NLM b
    $c*> :: forall a b. NLM a -> NLM b -> NLM b
    liftA2 :: forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c
    $cliftA2 :: forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c
    <*> :: forall a b. NLM (a -> b) -> NLM a -> NLM b
    $c<*> :: forall a b. NLM (a -> b) -> NLM a -> NLM b
    pure :: forall a. a -> NLM a
    $cpure :: forall a. a -> NLM a
    Applicative, Applicative NLM
    Applicative NLM
    -> (forall a b. NLM a -> (a -> NLM b) -> NLM b)
    -> (forall a b. NLM a -> NLM b -> NLM b)
    -> (forall a. a -> NLM a)
    -> Monad NLM
    forall a. a -> NLM a
    forall a b. NLM a -> NLM b -> NLM b
    forall a b. NLM a -> (a -> NLM b) -> NLM 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 -> NLM a
    $creturn :: forall a. a -> NLM a
    >> :: forall a b. NLM a -> NLM b -> NLM b
    $c>> :: forall a b. NLM a -> NLM b -> NLM b
    >>= :: forall a b. NLM a -> (a -> NLM b) -> NLM b
    $c>>= :: forall a b. NLM a -> (a -> NLM b) -> NLM b
    Monad, Monad NLM
    Monad NLM -> (forall a. String -> NLM a) -> MonadFail NLM
    forall a. String -> NLM a
    forall (m :: * -> *).
    Monad m -> (forall a. String -> m a) -> MonadFail m
    fail :: forall a. String -> NLM a
    $cfail :: forall a. String -> NLM a
    Fail.MonadFail
               , Applicative NLM
    Applicative NLM
    -> (forall a. NLM a)
    -> (forall a. NLM a -> NLM a -> NLM a)
    -> (forall a. NLM a -> NLM [a])
    -> (forall a. NLM a -> NLM [a])
    -> Alternative NLM
    forall a. NLM a
    forall a. NLM a -> NLM [a]
    forall a. NLM a -> NLM a -> NLM a
    forall (f :: * -> *).
    Applicative f
    -> (forall a. f a)
    -> (forall a. f a -> f a -> f a)
    -> (forall a. f a -> f [a])
    -> (forall a. f a -> f [a])
    -> Alternative f
    many :: forall a. NLM a -> NLM [a]
    $cmany :: forall a. NLM a -> NLM [a]
    some :: forall a. NLM a -> NLM [a]
    $csome :: forall a. NLM a -> NLM [a]
    <|> :: forall a. NLM a -> NLM a -> NLM a
    $c<|> :: forall a. NLM a -> NLM a -> NLM a
    empty :: forall a. NLM a
    $cempty :: forall a. NLM a
    Alternative, Monad NLM
    Alternative NLM
    Alternative NLM
    -> Monad NLM
    -> (forall a. NLM a)
    -> (forall a. NLM a -> NLM a -> NLM a)
    -> MonadPlus NLM
    forall a. NLM a
    forall a. NLM a -> NLM a -> NLM a
    forall (m :: * -> *).
    Alternative m
    -> Monad m
    -> (forall a. m a)
    -> (forall a. m a -> m a -> m a)
    -> MonadPlus m
    mplus :: forall a. NLM a -> NLM a -> NLM a
    $cmplus :: forall a. NLM a -> NLM a -> NLM a
    mzero :: forall a. NLM a
    $cmzero :: forall a. NLM a
    MonadPlus
               , MonadError Blocked_, MonadState NLMState
               , Functor NLM
    MonadFail NLM
    Applicative NLM
    Functor NLM
    -> Applicative NLM
    -> MonadFail NLM
    -> (String -> NLM (Maybe (Builtin PrimFun)))
    -> HasBuiltins NLM
    String -> NLM (Maybe (Builtin PrimFun))
    forall (m :: * -> *).
    Functor m
    -> Applicative m
    -> MonadFail m
    -> (String -> m (Maybe (Builtin PrimFun)))
    -> HasBuiltins m
    getBuiltinThing :: String -> NLM (Maybe (Builtin PrimFun))
    $cgetBuiltinThing :: String -> NLM (Maybe (Builtin PrimFun))
    HasBuiltins, Functor NLM
    MonadFail NLM
    Applicative NLM
    MonadDebug NLM
    HasOptions NLM
    MonadTCEnv NLM
    Functor NLM
    -> Applicative NLM
    -> MonadFail NLM
    -> HasOptions NLM
    -> MonadDebug NLM
    -> MonadTCEnv NLM
    -> (QName -> NLM Definition)
    -> (QName -> NLM (Either SigError Definition))
    -> (QName -> NLM RewriteRules)
    -> HasConstInfo NLM
    QName -> NLM RewriteRules
    QName -> NLM (Either SigError Definition)
    QName -> NLM Definition
    forall (m :: * -> *).
    Functor m
    -> Applicative m
    -> MonadFail m
    -> HasOptions m
    -> MonadDebug m
    -> MonadTCEnv m
    -> (QName -> m Definition)
    -> (QName -> m (Either SigError Definition))
    -> (QName -> m RewriteRules)
    -> HasConstInfo m
    getRewriteRulesFor :: QName -> NLM RewriteRules
    $cgetRewriteRulesFor :: QName -> NLM RewriteRules
    getConstInfo' :: QName -> NLM (Either SigError Definition)
    $cgetConstInfo' :: QName -> NLM (Either SigError Definition)
    getConstInfo :: QName -> NLM Definition
    $cgetConstInfo :: QName -> NLM Definition
    HasConstInfo, Monad NLM
    Functor NLM
    Applicative NLM
    NLM PragmaOptions
    NLM CommandLineOptions
    Functor NLM
    -> Applicative NLM
    -> Monad NLM
    -> NLM PragmaOptions
    -> NLM CommandLineOptions
    -> HasOptions NLM
    forall (m :: * -> *).
    Functor m
    -> Applicative m
    -> Monad m
    -> m PragmaOptions
    -> m CommandLineOptions
    -> HasOptions m
    commandLineOptions :: NLM CommandLineOptions
    $ccommandLineOptions :: NLM CommandLineOptions
    pragmaOptions :: NLM PragmaOptions
    $cpragmaOptions :: NLM PragmaOptions
    HasOptions, Monad NLM
    NLM TCState
    Monad NLM
    -> NLM TCState
    -> (forall a b. Lens' a TCState -> (a -> a) -> NLM b -> NLM b)
    -> (forall a. (TCState -> TCState) -> NLM a -> NLM a)
    -> ReadTCState NLM
    forall a. (TCState -> TCState) -> NLM a -> NLM a
    forall a b. Lens' a TCState -> (a -> a) -> NLM b -> NLM b
    forall (m :: * -> *).
    Monad m
    -> m TCState
    -> (forall a b. Lens' a TCState -> (a -> a) -> m b -> m b)
    -> (forall a. (TCState -> TCState) -> m a -> m a)
    -> ReadTCState m
    withTCState :: forall a. (TCState -> TCState) -> NLM a -> NLM a
    $cwithTCState :: forall a. (TCState -> TCState) -> NLM a -> NLM a
    locallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> NLM b -> NLM b
    $clocallyTCState :: forall a b. Lens' a TCState -> (a -> a) -> NLM b -> NLM b
    getTCState :: NLM TCState
    $cgetTCState :: NLM TCState
    ReadTCState
               , Monad NLM
    NLM TCEnv
    Monad NLM
    -> NLM TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a)
    -> MonadTCEnv NLM
    forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
    forall (m :: * -> *).
    Monad m
    -> m TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
    -> MonadTCEnv m
    localTC :: forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
    $clocalTC :: forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
    askTC :: NLM TCEnv
    $caskTC :: NLM TCEnv
    MonadTCEnv, Applicative NLM
    HasOptions NLM
    MonadTCEnv NLM
    ReadTCState NLM
    Applicative NLM
    -> MonadTCEnv NLM
    -> ReadTCState NLM
    -> HasOptions NLM
    -> (forall a. ReduceM a -> NLM a)
    -> MonadReduce NLM
    forall a. ReduceM a -> NLM a
    forall (m :: * -> *).
    Applicative m
    -> MonadTCEnv m
    -> ReadTCState m
    -> HasOptions m
    -> (forall a. ReduceM a -> m a)
    -> MonadReduce m
    liftReduce :: forall a. ReduceM a -> NLM a
    $cliftReduce :: forall a. ReduceM a -> NLM a
    MonadReduce, MonadTCEnv NLM
    MonadTCEnv NLM
    -> (forall a. Name -> Dom Type -> NLM a -> NLM a)
    -> (forall a. Name -> Term -> Dom Type -> NLM a -> NLM a)
    -> (forall a.
        Substitution -> (Context -> Context) -> NLM a -> NLM a)
    -> (forall a. Range -> String -> (Name -> NLM a) -> NLM a)
    -> MonadAddContext NLM
    forall a. Range -> String -> (Name -> NLM a) -> NLM a
    forall a. Name -> Term -> Dom Type -> NLM a -> NLM a
    forall a. Name -> Dom Type -> NLM a -> NLM a
    forall a. Substitution -> (Context -> Context) -> NLM a -> NLM a
    forall (m :: * -> *).
    MonadTCEnv m
    -> (forall a. Name -> Dom Type -> m a -> m a)
    -> (forall a. Name -> Term -> Dom Type -> m a -> m a)
    -> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
    -> (forall a. Range -> String -> (Name -> m a) -> m a)
    -> MonadAddContext m
    withFreshName :: forall a. Range -> String -> (Name -> NLM a) -> NLM a
    $cwithFreshName :: forall a. Range -> String -> (Name -> NLM a) -> NLM a
    updateContext :: forall a. Substitution -> (Context -> Context) -> NLM a -> NLM a
    $cupdateContext :: forall a. Substitution -> (Context -> Context) -> NLM a -> NLM a
    addLetBinding' :: forall a. Name -> Term -> Dom Type -> NLM a -> NLM a
    $caddLetBinding' :: forall a. Name -> Term -> Dom Type -> NLM a -> NLM a
    addCtx :: forall a. Name -> Dom Type -> NLM a -> NLM a
    $caddCtx :: forall a. Name -> Dom Type -> NLM a -> NLM a
    MonadAddContext, Monad NLM
    Functor NLM
    Applicative NLM
    NLM Bool
    NLM Verbosity
    Functor NLM
    -> Applicative NLM
    -> Monad NLM
    -> (String -> Key -> TCMT IO Doc -> NLM String)
    -> (forall a. String -> Key -> String -> NLM a -> NLM a)
    -> (forall a. String -> Key -> String -> NLM a -> NLM a)
    -> NLM Verbosity
    -> NLM Bool
    -> (forall a. NLM a -> NLM a)
    -> MonadDebug NLM
    String -> Key -> TCMT IO Doc -> NLM String
    forall a. String -> Key -> String -> NLM a -> NLM a
    forall a. NLM a -> NLM a
    forall (m :: * -> *).
    Functor m
    -> Applicative m
    -> Monad m
    -> (String -> Key -> TCMT IO Doc -> m String)
    -> (forall a. String -> Key -> String -> m a -> m a)
    -> (forall a. String -> Key -> String -> m a -> m a)
    -> m Verbosity
    -> m Bool
    -> (forall a. m a -> m a)
    -> MonadDebug m
    nowDebugPrinting :: forall a. NLM a -> NLM a
    $cnowDebugPrinting :: forall a. NLM a -> NLM a
    isDebugPrinting :: NLM Bool
    $cisDebugPrinting :: NLM Bool
    getVerbosity :: NLM Verbosity
    $cgetVerbosity :: NLM Verbosity
    verboseBracket :: forall a. String -> Key -> String -> NLM a -> NLM a
    $cverboseBracket :: forall a. String -> Key -> String -> NLM a -> NLM a
    traceDebugMessage :: forall a. String -> Key -> String -> NLM a -> NLM a
    $ctraceDebugMessage :: forall a. String -> Key -> String -> NLM a -> NLM a
    formatDebugMessage :: String -> Key -> TCMT IO Doc -> NLM String
    $cformatDebugMessage :: String -> Key -> TCMT IO Doc -> NLM String
    MonadDebug
               , MonadDebug NLM
    MonadTCEnv NLM
    MonadReduce NLM
    ReadTCState NLM
    MonadAddContext NLM
    HasBuiltins NLM
    HasConstInfo NLM
    HasBuiltins NLM
    -> HasConstInfo NLM
    -> MonadAddContext NLM
    -> MonadDebug NLM
    -> MonadReduce NLM
    -> MonadTCEnv NLM
    -> ReadTCState NLM
    -> PureTCM NLM
    forall (m :: * -> *).
    HasBuiltins m
    -> HasConstInfo m
    -> MonadAddContext m
    -> MonadDebug m
    -> MonadReduce m
    -> MonadTCEnv m
    -> ReadTCState m
    -> PureTCM m
    PureTCM
               )

    instance MonadBlock NLM where
      patternViolation :: forall a. Blocker -> NLM a
    patternViolation Blocker
    b = Blocked_ -> NLM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (Blocked_ -> NLM a) -> Blocked_ -> NLM a
    forall a b. (a -> b) -> a -> b
    $ Blocker -> () -> Blocked_
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    b ()
      catchPatternErr :: forall a. (Blocker -> NLM a) -> NLM a -> NLM a
    catchPatternErr Blocker -> NLM a
    h NLM a
    f = NLM a -> (Blocked_ -> NLM a) -> NLM a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    catchError NLM a
    f ((Blocked_ -> NLM a) -> NLM a) -> (Blocked_ -> NLM a) -> NLM a
    forall a b. (a -> b) -> a -> b
    $ \case
        Blocked Blocker
    b ()
    _      -> Blocker -> NLM a
    h Blocker
    b
        err :: Blocked_
    err@NotBlocked{} -> Blocked_ -> NLM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError Blocked_
    err

    data NLMState = NLMState
      { NLMState -> Sub
    _nlmSub   :: Sub
      , NLMState -> PostponedEquations
    _nlmEqs   :: PostponedEquations
      }

    instance Null NLMState where
      empty :: NLMState
    empty  = NLMState :: Sub -> PostponedEquations -> NLMState
    NLMState { _nlmSub :: Sub
    _nlmSub = Sub
    forall a. Null a => a
    empty , _nlmEqs :: PostponedEquations
    _nlmEqs = PostponedEquations
    forall a. Null a => a
    empty }
      null :: NLMState -> Bool
    null NLMState
    s = Sub -> Bool
    forall a. Null a => a -> Bool
    null (NLMState
    sNLMState -> Lens' Sub NLMState -> Sub
    forall o i. o -> Lens' i o -> i
    ^.Lens' Sub NLMState
    nlmSub) Bool -> Bool -> Bool
    && PostponedEquations -> Bool
    forall a. Null a => a -> Bool
    null (NLMState
    sNLMState -> Lens' PostponedEquations NLMState -> PostponedEquations
    forall o i. o -> Lens' i o -> i
    ^.Lens' PostponedEquations NLMState
    nlmEqs)

    nlmSub :: Lens' Sub NLMState
    nlmSub :: Lens' Sub NLMState
    nlmSub Sub -> f Sub
    f NLMState
    s = Sub -> f Sub
    f (NLMState -> Sub
    _nlmSub NLMState
    s) f Sub -> (Sub -> NLMState) -> f NLMState
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \Sub
    x -> NLMState
    s {_nlmSub :: Sub
    _nlmSub = Sub
    x}

    nlmEqs :: Lens' PostponedEquations NLMState
    nlmEqs :: Lens' PostponedEquations NLMState
    nlmEqs PostponedEquations -> f PostponedEquations
    f NLMState
    s = PostponedEquations -> f PostponedEquations
    f (NLMState -> PostponedEquations
    _nlmEqs NLMState
    s) f PostponedEquations
    -> (PostponedEquations -> NLMState) -> f NLMState
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \PostponedEquations
    x -> NLMState
    s {_nlmEqs :: PostponedEquations
    _nlmEqs = PostponedEquations
    x}

    runNLM :: (MonadReduce m) => NLM () -> m (Either Blocked_ NLMState)
    runNLM :: forall (m :: * -> *).
    MonadReduce m =>
    NLM () -> m (Either Blocked_ NLMState)
    runNLM NLM ()
    nlm = do
      (Either Blocked_ ()
    ok,NLMState
    out) <- ReduceM (Either Blocked_ (), NLMState)
    -> m (Either Blocked_ (), NLMState)
    forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
    liftReduce (ReduceM (Either Blocked_ (), NLMState)
     -> m (Either Blocked_ (), NLMState))
    -> ReduceM (Either Blocked_ (), NLMState)
    -> m (Either Blocked_ (), NLMState)
    forall a b. (a -> b) -> a -> b
    $ StateT NLMState ReduceM (Either Blocked_ ())
    -> NLMState -> ReduceM (Either Blocked_ (), NLMState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (ExceptT Blocked_ (StateT NLMState ReduceM) ()
    -> StateT NLMState ReduceM (Either Blocked_ ())
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT Blocked_ (StateT NLMState ReduceM) ()
     -> StateT NLMState ReduceM (Either Blocked_ ()))
    -> ExceptT Blocked_ (StateT NLMState ReduceM) ()
    -> StateT NLMState ReduceM (Either Blocked_ ())
    forall a b. (a -> b) -> a -> b
    $ NLM () -> ExceptT Blocked_ (StateT NLMState ReduceM) ()
    forall a. NLM a -> ExceptT Blocked_ (StateT NLMState ReduceM) a
    unNLM NLM ()
    nlm) NLMState
    forall a. Null a => a
    empty
      case Either Blocked_ ()
    ok of
        Left Blocked_
    block -> Either Blocked_ NLMState -> m (Either Blocked_ NLMState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocked_ NLMState -> m (Either Blocked_ NLMState))
    -> Either Blocked_ NLMState -> m (Either Blocked_ NLMState)
    forall a b. (a -> b) -> a -> b
    $ Blocked_ -> Either Blocked_ NLMState
    forall a b. a -> Either a b
    Left Blocked_
    block
        Right ()
    _    -> Either Blocked_ NLMState -> m (Either Blocked_ NLMState)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocked_ NLMState -> m (Either Blocked_ NLMState))
    -> Either Blocked_ NLMState -> m (Either Blocked_ NLMState)
    forall a b. (a -> b) -> a -> b
    $ NLMState -> Either Blocked_ NLMState
    forall a b. b -> Either a b
    Right NLMState
    out

    matchingBlocked :: Blocked_ -> NLM ()
    matchingBlocked :: Blocked_ -> NLM ()
    matchingBlocked = Blocked_ -> NLM ()
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError

    -- | Add substitution @i |-> v : a@ to result of matching.
    tellSub :: Relevance -> Int -> Type -> Term -> NLM ()
    tellSub :: Relevance -> Key -> Type -> Term -> NLM ()
    tellSub Relevance
    r Key
    i Type
    a Term
    v = do
      Maybe (Relevance, Term)
    old <- Key -> Sub -> Maybe (Relevance, Term)
    forall a. Key -> IntMap a -> Maybe a
    IntMap.lookup Key
    i (Sub -> Maybe (Relevance, Term))
    -> NLM Sub -> NLM (Maybe (Relevance, Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' Sub NLMState -> NLM Sub
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
    use Lens' Sub NLMState
    nlmSub
      case Maybe (Relevance, Term)
    old of
        Maybe (Relevance, Term)
    Nothing -> Lens' Sub NLMState
    nlmSub Lens' Sub NLMState -> (Sub -> Sub) -> NLM ()
    forall o (m :: * -> *) i.
    MonadState o m =>
    Lens' i o -> (i -> i) -> m ()
    %= Key -> (Relevance, Term) -> Sub -> Sub
    forall a. Key -> a -> IntMap a -> IntMap a
    IntMap.insert Key
    i (Relevance
    r,Term
    v)
        Just (Relevance
    r',Term
    v')
          | Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    r  -> () -> NLM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          | Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    r' -> Lens' Sub NLMState
    nlmSub Lens' Sub NLMState -> (Sub -> Sub) -> NLM ()
    forall o (m :: * -> *) i.
    MonadState o m =>
    Lens' i o -> (i -> i) -> m ()
    %= Key -> (Relevance, Term) -> Sub -> Sub
    forall a. Key -> a -> IntMap a -> IntMap a
    IntMap.insert Key
    i (Relevance
    r,Term
    v)
          | Bool
    otherwise       -> NLM (Maybe Blocked_) -> (Blocked_ -> NLM ()) -> NLM ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM (Type -> Term -> Term -> NLM (Maybe Blocked_)
    forall (m :: * -> *).
    PureTCM m =>
    Type -> Term -> Term -> m (Maybe Blocked_)
    equal Type
    a Term
    v Term
    v') Blocked_ -> NLM ()
    matchingBlocked

    tellEq :: Telescope -> Telescope -> Type -> Term -> Term -> NLM ()
    tellEq :: Telescope -> Telescope -> Type -> Term -> Term -> NLM ()
    tellEq Telescope
    gamma Telescope
    k Type
    a Term
    u Term
    v = do
      String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    30 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                   [ TCMT IO Doc
    "adding equality between" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Telescope
    gamma Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    k) (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    u)
                   , TCMT IO Doc
    " and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
      Lens' PostponedEquations NLMState
    nlmEqs Lens' PostponedEquations NLMState
    -> (PostponedEquations -> PostponedEquations) -> NLM ()
    forall o (m :: * -> *) i.
    MonadState o m =>
    Lens' i o -> (i -> i) -> m ()
    %= (Telescope -> Type -> Term -> Term -> PostponedEquation
    PostponedEquation Telescope
    k Type
    a Term
    u Term
    vPostponedEquation -> PostponedEquations -> PostponedEquations
    forall a. a -> [a] -> [a]
    :)

    type Sub = IntMap (Relevance, Term)

    -- | Matching against a term produces a constraint
    --   which we have to verify after applying
    --   the substitution computed by matching.
    data PostponedEquation = PostponedEquation
      { PostponedEquation -> Telescope
    eqFreeVars :: Telescope -- ^ Telescope of free variables in the equation
      , PostponedEquation -> Type
    eqType :: Type    -- ^ Type of the equation, living in same context as the rhs.
      , PostponedEquation -> Term
    eqLhs :: Term     -- ^ Term from pattern, living in pattern context.
      , PostponedEquation -> Term
    eqRhs :: Term     -- ^ Term from scrutinee, living in context where matching was invoked.
      }
    type PostponedEquations = [PostponedEquation]

    -- | Match a non-linear pattern against a neutral term,
    --   returning a substitution.

    class Match t a b where
      match :: Relevance  -- ^ Are we currently matching in an irrelevant context?
            -> Telescope  -- ^ The telescope of pattern variables
            -> Telescope  -- ^ The telescope of lambda-bound variables
            -> t          -- ^ The type of the pattern
            -> a          -- ^ The pattern to match
            -> b          -- ^ The term to be matched against the pattern
            -> NLM ()

    instance Match t a b => Match (Dom t) (Arg a) (Arg b) where
      match :: Relevance
    -> Telescope -> Telescope -> Dom t -> Arg a -> Arg b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k Dom t
    t Arg a
    p Arg b
    v = let r' :: Relevance
    r' = Relevance
    r Relevance -> Relevance -> Relevance
    `composeRelevance` Arg a -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Arg a
    p
                              in  Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r' Telescope
    gamma Telescope
    k (Dom t -> t
    forall t e. Dom' t e -> e
    unDom Dom t
    t) (Arg a -> a
    forall e. Arg e -> e
    unArg Arg a
    p) (Arg b -> b
    forall e. Arg e -> e
    unArg Arg b
    v)

    instance Match (Type, Elims -> Term) [Elim' NLPat] Elims where
      match :: Relevance
    -> Telescope
    -> Telescope
    -> (Type, Elims -> Term)
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k (Type
    t, Elims -> Term
    hd) [] [] = () -> NLM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      match Relevance
    r Telescope
    gamma Telescope
    k (Type
    t, Elims -> Term
    hd) [] Elims
    _  = Blocked_ -> NLM ()
    matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked ()
      match Relevance
    r Telescope
    gamma Telescope
    k (Type
    t, Elims -> Term
    hd) [Elim' NLPat]
    _  [] = Blocked_ -> NLM ()
    matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked ()
      match Relevance
    r Telescope
    gamma Telescope
    k (Type
    t, Elims -> Term
    hd) (Elim' NLPat
    p:[Elim' NLPat]
    ps) (Elim
    v:Elims
    vs) =
       String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    50 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
         [ TCMT IO Doc
    "matching elimination " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Telescope
    gamma Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    k) (Elim' NLPat -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Elim' NLPat
    p)
         , TCMT IO Doc
    "  with               " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (Elim -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Elim
    v)
         , TCMT IO Doc
    "  eliminating head   " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Term -> TCMT IO Doc) -> Term -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Elims -> Term
    hd []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t)]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
       case (Elim' NLPat
    p,Elim
    v) of
        (Apply Arg NLPat
    p, Apply Arg Term
    v) -> (Telescope -> NLM Term -> NLM Term
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM Term -> NLM Term) -> NLM Term -> NLM Term
    forall a b. (a -> b) -> a -> b
    $ Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> NLM Type -> NLM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> NLM Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t) NLM Term -> (Term -> NLM ()) -> NLM ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Pi Dom Type
    a Abs Type
    b -> do
            Relevance
    -> Telescope
    -> Telescope
    -> Dom Type
    -> Arg NLPat
    -> Arg Term
    -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k Dom Type
    a Arg NLPat
    p Arg Term
    v
            let t' :: Type
    t'  = Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp Abs Type
    b (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    v)
                hd' :: Elims -> Term
    hd' = Elims -> Term
    hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Arg Term
    vElim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :)
            Relevance
    -> Telescope
    -> Telescope
    -> (Type, Elims -> Term)
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k (Type
    t',Elims -> Term
    hd') [Elim' NLPat]
    ps Elims
    vs
          Term
    t -> String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    20
            (TCMT IO Doc
    "application at non-pi type (possible non-confluence?) " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    t) NLM ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

        (IApply NLPat
    x NLPat
    y NLPat
    p , IApply Term
    u Term
    v Term
    i) -> (Telescope -> NLM PathView -> NLM PathView
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM PathView -> NLM PathView) -> NLM PathView -> NLM PathView
    forall a b. (a -> b) -> a -> b
    $ Type -> NLM PathView
    forall (m :: * -> *). HasBuiltins m => Type -> m PathView
    pathView (Type -> NLM PathView) -> NLM Type -> NLM PathView
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> NLM Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t) NLM PathView -> (PathView -> NLM ()) -> NLM ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          PathType Sort
    s QName
    q Arg Term
    l Arg Term
    b Arg Term
    _u Arg Term
    _v -> do
            Right Type
    interval <- ExceptT TCErr NLM Type -> NLM (Either TCErr Type)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT ExceptT TCErr NLM Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType
            Relevance
    -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k Type
    interval NLPat
    p Term
    i
            let t' :: Type
    t' = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    b Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    i ]
            let hd' :: Elims -> Term
    hd' = Elims -> Term
    hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> Term -> Term -> Elim
    forall a. a -> a -> a -> Elim' a
    IApply Term
    u Term
    v Term
    iElim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :)
            Relevance
    -> Telescope
    -> Telescope
    -> (Type, Elims -> Term)
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k (Type
    t',Elims -> Term
    hd') [Elim' NLPat]
    ps Elims
    vs
          PathView
    t -> String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    20
            (TCMT IO Doc
    "interval application at non-pi type (possible non-confluence?) " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (PathView -> Type
    pathUnview PathView
    t)) NLM ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

        (Proj ProjOrigin
    o QName
    f, Proj ProjOrigin
    o' QName
    f') | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f' -> do
          ~(Just (El Sort
    _ (Pi Dom Type
    a Abs Type
    b))) <- Telescope -> NLM (Maybe Type) -> NLM (Maybe Type)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM (Maybe Type) -> NLM (Maybe Type))
    -> NLM (Maybe Type) -> NLM (Maybe Type)
    forall a b. (a -> b) -> a -> b
    $ QName -> Type -> NLM (Maybe Type)
    forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
    getDefType QName
    f (Type -> NLM (Maybe Type)) -> NLM Type -> NLM (Maybe Type)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> NLM Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t
          let u :: Term
    u = Elims -> Term
    hd []
              t' :: Type
    t' = Abs Type
    b Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    u
          Elims -> Term
    hd' <- Telescope -> NLM (Elims -> Term) -> NLM (Elims -> Term)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM (Elims -> Term) -> NLM (Elims -> Term))
    -> NLM (Elims -> Term) -> NLM (Elims -> Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    applyE (Term -> Elims -> Term) -> NLM Term -> NLM (Elims -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ProjOrigin -> QName -> Arg Term -> NLM Term
    forall (m :: * -> *).
    HasConstInfo m =>
    ProjOrigin -> QName -> Arg Term -> m Term
    applyDef ProjOrigin
    o QName
    f (Dom Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom Type
    a Arg Type -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Term
    u)
          Relevance
    -> Telescope
    -> Telescope
    -> (Type, Elims -> Term)
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k (Type
    t',Elims -> Term
    hd') [Elim' NLPat]
    ps Elims
    vs

        (Proj ProjOrigin
    _ QName
    f, Proj ProjOrigin
    _ QName
    f') | Bool
    otherwise -> do
          String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    20 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "mismatch between projections " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f
            , TCMT IO Doc
    " and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f' ]) NLM ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

        (Apply{}, Proj{} ) -> NLM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (Proj{} , Apply{}) -> NLM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        (IApply{} , Elim
    _    ) -> NLM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- TODO
        (Elim' NLPat
    _ , IApply{}    ) -> NLM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- TODO

    instance Match t a b => Match t (Dom a) (Dom b) where
      match :: Relevance
    -> Telescope -> Telescope -> t -> Dom a -> Dom b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k t
    t Dom a
    p Dom b
    v = Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k t
    t (Dom a -> a
    forall t e. Dom' t e -> e
    unDom Dom a
    p) (Dom b -> b
    forall t e. Dom' t e -> e
    unDom Dom b
    v)

    instance Match () NLPType Type where
      match :: Relevance
    -> Telescope -> Telescope -> () -> NLPType -> Type -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k ()
    _ (NLPType NLPSort
    sp NLPat
    p) (El Sort
    s Term
    a) = NLM () -> NLM ()
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    workOnTypes (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
        Relevance
    -> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k () NLPSort
    sp Sort
    s
        Relevance
    -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k (Sort -> Type
    sort Sort
    s) NLPat
    p Term
    a

    instance Match () NLPSort Sort where
      match :: Relevance
    -> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k ()
    _ NLPSort
    p Sort
    s = do
        Blocked Sort
    bs <- Telescope -> NLM (Blocked Sort) -> NLM (Blocked Sort)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM (Blocked Sort) -> NLM (Blocked Sort))
    -> NLM (Blocked Sort) -> NLM (Blocked Sort)
    forall a b. (a -> b) -> a -> b
    $ Sort -> NLM (Blocked Sort)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Sort
    s
        let b :: Blocked_
    b = Blocked Sort -> Blocked_
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void Blocked Sort
    bs
            s :: Sort
    s = Blocked Sort -> Sort
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Sort
    bs
            yes :: NLM ()
    yes = () -> NLM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            no :: NLM ()
    no  = Blocked_ -> NLM ()
    matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked ()
        String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    30 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
          [ TCMT IO Doc
    "matching pattern " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Telescope
    gamma Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    k) (NLPSort -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM NLPSort
    p)
          , TCMT IO Doc
    "  with sort      " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (Sort -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Sort
    s) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
        case (NLPSort
    p , Sort
    s) of
          (PType NLPat
    lp  , Type Level' Term
    l  ) -> Relevance
    -> Telescope -> Telescope -> () -> NLPat -> Level' Term -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k () NLPat
    lp Level' Term
    l
          (PProp NLPat
    lp  , Prop Level' Term
    l  ) -> Relevance
    -> Telescope -> Telescope -> () -> NLPat -> Level' Term -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k () NLPat
    lp Level' Term
    l
          (PInf IsFibrant
    fp Integer
    np , Inf IsFibrant
    f Integer
    n)
            | IsFibrant
    fp IsFibrant -> IsFibrant -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsFibrant
    f, Integer
    np Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    n   -> NLM ()
    yes
          (NLPSort
    PSizeUniv , Sort
    SizeUniv) -> NLM ()
    yes
          (NLPSort
    PLockUniv , Sort
    LockUniv) -> NLM ()
    yes

          -- blocked cases
          (NLPSort
    _ , UnivSort{}) -> Blocked_ -> NLM ()
    matchingBlocked Blocked_
    b
          (NLPSort
    _ , PiSort{}  ) -> Blocked_ -> NLM ()
    matchingBlocked Blocked_
    b
          (NLPSort
    _ , FunSort{} ) -> Blocked_ -> NLM ()
    matchingBlocked Blocked_
    b
          (NLPSort
    _ , MetaS MetaId
    m Elims
    _ ) -> Blocked_ -> NLM ()
    matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Blocked_
    forall t. MetaId -> Blocked' t ()
    blocked_ MetaId
    m

          -- all other cases do not match
          (NLPSort
    _ , Sort
    _) -> NLM ()
    no

    instance Match () NLPat Level where
      match :: Relevance
    -> Telescope -> Telescope -> () -> NLPat -> Level' Term -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k ()
    _ NLPat
    p Level' Term
    l = do
        Type
    t <- Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Integer -> Sort
    mkType Integer
    0) (Term -> Type) -> (Maybe Term -> Term) -> Maybe Term -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Type) -> NLM (Maybe Term) -> NLM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> NLM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    builtinLevel
        Term
    v <- Level' Term -> NLM Term
    forall (m :: * -> *). HasBuiltins m => Level' Term -> m Term
    reallyUnLevelView Level' Term
    l
        Relevance
    -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k Type
    t NLPat
    p Term
    v

    instance Match Type NLPat Term where
      match :: Relevance
    -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
    match Relevance
    r0 Telescope
    gamma Telescope
    k Type
    t NLPat
    p Term
    v = do
        Blocked (Term, Type)
    vbt <- Telescope
    -> NLM (Blocked (Term, Type)) -> NLM (Blocked (Term, Type))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM (Blocked (Term, Type)) -> NLM (Blocked (Term, Type)))
    -> NLM (Blocked (Term, Type)) -> NLM (Blocked (Term, Type))
    forall a b. (a -> b) -> a -> b
    $ (Term, Type) -> NLM (Blocked (Term, Type))
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB (Term
    v,Type
    t)
        let n :: Key
    n = Telescope -> Key
    forall a. Sized a => a -> Key
    size Telescope
    k
            b :: Blocked_
    b = Blocked (Term, Type) -> Blocked_
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void Blocked (Term, Type)
    vbt
            (Term
    v,Type
    t) = Blocked (Term, Type) -> (Term, Type)
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked (Term, Type)
    vbt
            prettyPat :: TCMT IO Doc
    prettyPat  = TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a. ReadTCState m => m a -> m a
    withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Telescope
    gamma Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    k) (NLPat -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM NLPat
    p)
            prettyTerm :: TCMT IO Doc
    prettyTerm = TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a. ReadTCState m => m a -> m a
    withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v
            prettyType :: TCMT IO Doc
    prettyType = TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a. ReadTCState m => m a -> m a
    withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
        Maybe (QName, Args)
    etaRecord <- Telescope -> NLM (Maybe (QName, Args)) -> NLM (Maybe (QName, Args))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM (Maybe (QName, Args)) -> NLM (Maybe (QName, Args)))
    -> NLM (Maybe (QName, Args)) -> NLM (Maybe (QName, Args))
    forall a b. (a -> b) -> a -> b
    $ Type -> NLM (Maybe (QName, Args))
    forall (m :: * -> *).
    HasConstInfo m =>
    Type -> m (Maybe (QName, Args))
    isEtaRecordType Type
    t
        Bool
    prop <- (Blocker -> Bool) -> Either Blocker Bool -> Bool
    forall a b. (a -> b) -> Either a b -> b
    fromRight Blocker -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Either Blocker Bool -> Bool)
    -> (BlockT NLM Bool -> NLM (Either Blocker Bool))
    -> BlockT NLM Bool
    -> NLM Bool
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> BlockT NLM Bool -> NLM (Either Blocker Bool)
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked (BlockT NLM Bool -> NLM (Either Blocker Bool))
    -> (BlockT NLM Bool -> BlockT NLM Bool)
    -> BlockT NLM Bool
    -> NLM (Either Blocker Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> BlockT NLM Bool -> BlockT NLM Bool
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (BlockT NLM Bool -> NLM Bool) -> BlockT NLM Bool -> NLM Bool
    forall a b. (a -> b) -> a -> b
    $ Type -> BlockT NLM Bool
    forall a (m :: * -> *).
    (LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
    a -> m Bool
    isPropM Type
    t
        let r :: Relevance
    r = if Bool
    prop then Relevance
    Irrelevant else Relevance
    r0
        String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    30 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
          [ TCMT IO Doc
    "matching pattern " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    prettyPat
          , TCMT IO Doc
    "  with term      " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    prettyTerm
          , TCMT IO Doc
    "  of type        " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    prettyType ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
        String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    80 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "  raw pattern:  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (NLPat -> String
    forall a. Show a => a -> String
    show NLPat
    p)
          , TCMT IO Doc
    "  raw term:     " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Term -> String
    forall a. Show a => a -> String
    show Term
    v)
          , TCMT IO Doc
    "  raw type:     " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Type -> String
    forall a. Show a => a -> String
    show Type
    t) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
        String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    70 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "pattern vars:   " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    gamma
          , TCMT IO Doc
    "bound vars:     " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    k ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
        let yes :: NLM ()
    yes = () -> NLM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            no :: TCMT IO Doc -> NLM ()
    no TCMT IO Doc
    msg = if Relevance
    r Relevance -> Relevance -> Bool
    forall a. Eq a => a -> a -> Bool
    == Relevance
    Irrelevant then NLM ()
    yes else do
              String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    10 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                [ TCMT IO Doc
    "mismatch between" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    prettyPat
                , TCMT IO Doc
    " and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    prettyTerm
                , TCMT IO Doc
    " of type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    prettyType
                , TCMT IO Doc
    msg ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
              String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    30 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                [ TCMT IO Doc
    "blocking tag from reduction: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Blocked_ -> String
    forall a. Show a => a -> String
    show Blocked_
    b) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
              Blocked_ -> NLM ()
    matchingBlocked Blocked_
    b
            block :: Blocked_ -> NLM ()
    block Blocked_
    b' = if Relevance
    r Relevance -> Relevance -> Bool
    forall a. Eq a => a -> a -> Bool
    == Relevance
    Irrelevant then NLM ()
    yes else do
              String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    10 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                [ TCMT IO Doc
    "matching blocked on meta"
                , String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Blocked_ -> String
    forall a. Show a => a -> String
    show Blocked_
    b') ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
              String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    30 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                [ TCMT IO Doc
    "blocking tag from reduction: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Blocked_ -> String
    forall a. Show a => a -> String
    show Blocked_
    b') ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
              Blocked_ -> NLM ()
    matchingBlocked (Blocked_
    b Blocked_ -> Blocked_ -> Blocked_
    forall a. Monoid a => a -> a -> a
    `mappend` Blocked_
    b')
            maybeBlock :: Term -> NLM ()
    maybeBlock = \case
              MetaV MetaId
    m Elims
    es -> Blocked_ -> NLM ()
    matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Blocked_
    forall t. MetaId -> Blocked' t ()
    blocked_ MetaId
    m
              Term
    _          -> TCMT IO Doc -> NLM ()
    no TCMT IO Doc
    ""
        case NLPat
    p of
          PVar Key
    i [Arg Key]
    bvs -> String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    60 (TCMT IO Doc
    "matching a PVar: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Key -> String
    forall a. Show a => a -> String
    show Key
    i)) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
            let allowedVars :: IntSet
                allowedVars :: IntSet
    allowedVars = [Key] -> IntSet
    IntSet.fromList ((Arg Key -> Key) -> [Arg Key] -> [Key]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Key -> Key
    forall e. Arg e -> e
    unArg [Arg Key]
    bvs)
                badVars :: IntSet
                badVars :: IntSet
    badVars = IntSet -> IntSet -> IntSet
    IntSet.difference ([Key] -> IntSet
    IntSet.fromList (Key -> [Key]
    forall a. Integral a => a -> [a]
    downFrom Key
    n)) IntSet
    allowedVars
                perm :: Permutation
                perm :: Permutation
    perm = Key -> [Key] -> Permutation
    Perm Key
    n ([Key] -> Permutation) -> [Key] -> Permutation
    forall a b. (a -> b) -> a -> b
    $ [Key] -> [Key]
    forall a. [a] -> [a]
    reverse ([Key] -> [Key]) -> [Key] -> [Key]
    forall a b. (a -> b) -> a -> b
    $ (Arg Key -> Key) -> [Arg Key] -> [Key]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Key -> Key
    forall e. Arg e -> e
    unArg ([Arg Key] -> [Key]) -> [Arg Key] -> [Key]
    forall a b. (a -> b) -> a -> b
    $ [Arg Key]
    bvs
                tel :: Telescope
                tel :: Telescope
    tel = Permutation -> Telescope -> Telescope
    permuteTel Permutation
    perm Telescope
    k
            Either Blocked_ (Maybe Term)
    ok <- Telescope
    -> NLM (Either Blocked_ (Maybe Term))
    -> NLM (Either Blocked_ (Maybe Term))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM (Either Blocked_ (Maybe Term))
     -> NLM (Either Blocked_ (Maybe Term)))
    -> NLM (Either Blocked_ (Maybe Term))
    -> NLM (Either Blocked_ (Maybe Term))
    forall a b. (a -> b) -> a -> b
    $ IntSet -> Term -> NLM (Either Blocked_ (Maybe Term))
    forall (m :: * -> *) a.
    (MonadReduce m, Reduce a, ForceNotFree a) =>
    IntSet -> a -> m (Either Blocked_ (Maybe a))
    reallyFree IntSet
    badVars Term
    v
            case Either Blocked_ (Maybe Term)
    ok of
              Left Blocked_
    b         -> Blocked_ -> NLM ()
    block Blocked_
    b
              Right Maybe Term
    Nothing  -> TCMT IO Doc -> NLM ()
    no TCMT IO Doc
    ""
              Right (Just Term
    v) ->
                let t' :: Type
    t' = Telescope -> Type -> Type
    telePi  Telescope
    tel (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Impossible -> Permutation -> Type -> Type
    forall a. Subst a => Impossible -> Permutation -> a -> a
    renameP Impossible
    HasCallStack => Impossible
    impossible Permutation
    perm Type
    t
                    v' :: Term
    v' = Telescope -> Term -> Term
    teleLam Telescope
    tel (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Impossible -> Permutation -> Term -> Term
    forall a. Subst a => Impossible -> Permutation -> a -> a
    renameP Impossible
    HasCallStack => Impossible
    impossible Permutation
    perm Term
    v
                in Relevance -> Key -> Type -> Term -> NLM ()
    tellSub Relevance
    r (Key
    iKey -> Key -> Key
    forall a. Num a => a -> a -> a
    -Key
    n) Type
    t' Term
    v'

          PDef QName
    f [Elim' NLPat]
    ps -> String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    60 (TCMT IO Doc
    "matching a PDef: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
            Term
    v <- Telescope -> NLM Term -> NLM Term
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM Term -> NLM Term) -> NLM Term -> NLM Term
    forall a b. (a -> b) -> a -> b
    $ Term -> NLM Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm (Term -> NLM Term) -> NLM Term -> NLM Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> NLM Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    unLevel Term
    v
            case Term
    v of
              Def QName
    f' Elims
    es
                | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f'   -> do
                    Type
    ft <- Telescope -> NLM Type -> NLM Type
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM Type -> NLM Type) -> NLM Type -> NLM Type
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type
    defType (Definition -> Type) -> NLM Definition -> NLM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> NLM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
                    Relevance
    -> Telescope
    -> Telescope
    -> (Type, Elims -> Term)
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k (Type
    ft , QName -> Elims -> Term
    Def QName
    f) [Elim' NLPat]
    ps Elims
    es
              Con ConHead
    c ConInfo
    ci Elims
    vs
                | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead -> QName
    conName ConHead
    c -> do
                    ~(Just ((QName, Type, Args)
    _ , Type
    ct)) <- Telescope
    -> NLM (Maybe ((QName, Type, Args), Type))
    -> NLM (Maybe ((QName, Type, Args), Type))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM (Maybe ((QName, Type, Args), Type))
     -> NLM (Maybe ((QName, Type, Args), Type)))
    -> NLM (Maybe ((QName, Type, Args), Type))
    -> NLM (Maybe ((QName, Type, Args), Type))
    forall a b. (a -> b) -> a -> b
    $ ConHead -> Type -> NLM (Maybe ((QName, Type, Args), Type))
    forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    getFullyAppliedConType ConHead
    c Type
    t
                    Relevance
    -> Telescope
    -> Telescope
    -> (Type, Elims -> Term)
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k (Type
    ct , ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci) [Elim' NLPat]
    ps Elims
    vs
              Term
    _ | Pi Dom Type
    a Abs Type
    b <- Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t -> do
                let ai :: ArgInfo
    ai    = Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    a
                    pbody :: NLPat
    pbody = QName -> [Elim' NLPat] -> NLPat
    PDef QName
    f ([Elim' NLPat] -> NLPat) -> [Elim' NLPat] -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Key -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. Subst a => Key -> a -> a
    raise Key
    1 [Elim' NLPat]
    ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. [a] -> [a] -> [a]
    ++ [ Arg NLPat -> Elim' NLPat
    forall a. Arg a -> Elim' a
    Apply (Arg NLPat -> Elim' NLPat) -> Arg NLPat -> Elim' NLPat
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> NLPat -> Arg NLPat
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (NLPat -> Arg NLPat) -> NLPat -> Arg NLPat
    forall a b. (a -> b) -> a -> b
    $ Term -> NLPat
    PTerm (Term -> NLPat) -> Term -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Key -> Term
    var Key
    0 ]
                    body :: Term
    body  = Key -> Term -> Term
    forall a. Subst a => Key -> a -> a
    raise Key
    1 Term
    v Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg (Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    a) (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Key -> Term
    var Key
    0 ]
                    k' :: Telescope
    k'    = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    a (String -> Telescope -> Abs Telescope
    forall a. String -> a -> Abs a
    Abs (Abs Type -> String
    forall a. Abs a -> String
    absName Abs Type
    b) Telescope
    k)
                Relevance
    -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k' (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b) NLPat
    pbody Term
    body
              Term
    _ | Just (QName
    d, Args
    pars) <- Maybe (QName, Args)
    etaRecord -> do
              -- If v is not of record constructor form but we are matching at record
              -- type, e.g., we eta-expand both v to (c vs) and
              -- the pattern (p = PDef f ps) to @c (p .f1) ... (p .fn)@.
                Defn
    def <- Telescope -> NLM Defn -> NLM Defn
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM Defn -> NLM Defn) -> NLM Defn -> NLM Defn
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef (Definition -> Defn) -> NLM Definition -> NLM Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> NLM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
                (Telescope
    tel, ConHead
    c, ConInfo
    ci, Args
    vs) <- Telescope
    -> NLM (Telescope, ConHead, ConInfo, Args)
    -> NLM (Telescope, ConHead, ConInfo, Args)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM (Telescope, ConHead, ConInfo, Args)
     -> NLM (Telescope, ConHead, ConInfo, Args))
    -> NLM (Telescope, ConHead, ConInfo, Args)
    -> NLM (Telescope, ConHead, ConInfo, Args)
    forall a b. (a -> b) -> a -> b
    $ QName
    -> Args -> Defn -> Term -> NLM (Telescope, ConHead, ConInfo, Args)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName
    -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
    etaExpandRecord_ QName
    d Args
    pars Defn
    def Term
    v
                ~(Just ((QName, Type, Args)
    _ , Type
    ct)) <- Telescope
    -> NLM (Maybe ((QName, Type, Args), Type))
    -> NLM (Maybe ((QName, Type, Args), Type))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM (Maybe ((QName, Type, Args), Type))
     -> NLM (Maybe ((QName, Type, Args), Type)))
    -> NLM (Maybe ((QName, Type, Args), Type))
    -> NLM (Maybe ((QName, Type, Args), Type))
    forall a b. (a -> b) -> a -> b
    $ ConHead -> Type -> NLM (Maybe ((QName, Type, Args), Type))
    forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    getFullyAppliedConType ConHead
    c Type
    t
                let flds :: [Arg QName]
    flds = (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term QName -> Arg QName
    forall t a. Dom' t a -> Arg a
    argFromDom ([Dom' Term QName] -> [Arg QName])
    -> [Dom' Term QName] -> [Arg QName]
    forall a b. (a -> b) -> a -> b
    $ Defn -> [Dom' Term QName]
    recFields Defn
    def
                    mkField :: QName -> NLPat
    mkField QName
    fld = QName -> [Elim' NLPat] -> NLPat
    PDef QName
    f ([Elim' NLPat]
    ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. [a] -> [a] -> [a]
    ++ [ProjOrigin -> QName -> Elim' NLPat
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    fld])
                    -- Issue #3335: when matching against the record constructor,
                    -- don't add projections but take record field directly.
                    ps' :: [Elim' NLPat]
    ps'
                      | ConHead -> QName
    conName ConHead
    c QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f = [Elim' NLPat]
    ps
                      | Bool
    otherwise      = (Arg QName -> Elim' NLPat) -> [Arg QName] -> [Elim' NLPat]
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg NLPat -> Elim' NLPat
    forall a. Arg a -> Elim' a
    Apply (Arg NLPat -> Elim' NLPat)
    -> (Arg QName -> Arg NLPat) -> Arg QName -> Elim' NLPat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QName -> NLPat) -> Arg QName -> Arg NLPat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap QName -> NLPat
    mkField) [Arg QName]
    flds
                Relevance
    -> Telescope
    -> Telescope
    -> (Type, Elims -> Term)
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k (Type
    ct, ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci) [Elim' NLPat]
    ps' ((Arg Term -> Elim) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Args
    vs)
              Term
    v -> Term -> NLM ()
    maybeBlock Term
    v
          PLam ArgInfo
    i Abs NLPat
    p' -> case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
            Pi Dom Type
    a Abs Type
    b -> do
              let body :: Term
    body = Key -> Term -> Term
    forall a. Subst a => Key -> a -> a
    raise Key
    1 Term
    v Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i (Key -> Term
    var Key
    0)]
                  k' :: Telescope
    k'   = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    a (String -> Telescope -> Abs Telescope
    forall a. String -> a -> Abs a
    Abs (Abs Type -> String
    forall a. Abs a -> String
    absName Abs Type
    b) Telescope
    k)
              Relevance
    -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k' (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b) (Abs NLPat -> NLPat
    forall a. Subst a => Abs a -> a
    absBody Abs NLPat
    p') Term
    body
            Term
    v -> Term -> NLM ()
    maybeBlock Term
    v
          PPi Dom NLPType
    pa Abs NLPType
    pb -> case Term
    v of
            Pi Dom Type
    a Abs Type
    b -> do
              Relevance
    -> Telescope
    -> Telescope
    -> ()
    -> Dom NLPType
    -> Dom Type
    -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k () Dom NLPType
    pa Dom Type
    a
              let k' :: Telescope
    k' = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    a (String -> Telescope -> Abs Telescope
    forall a. String -> a -> Abs a
    Abs (Abs Type -> String
    forall a. Abs a -> String
    absName Abs Type
    b) Telescope
    k)
              Relevance
    -> Telescope -> Telescope -> () -> NLPType -> Type -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k' () (Abs NLPType -> NLPType
    forall a. Subst a => Abs a -> a
    absBody Abs NLPType
    pb) (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b)
            Term
    v -> Term -> NLM ()
    maybeBlock Term
    v
          PSort NLPSort
    ps -> case Term
    v of
            Sort Sort
    s -> Relevance
    -> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k () NLPSort
    ps Sort
    s
            Term
    v -> Term -> NLM ()
    maybeBlock Term
    v
          PBoundVar Key
    i [Elim' NLPat]
    ps -> case Term
    v of
            Var Key
    i' Elims
    es | Key
    i Key -> Key -> Bool
    forall a. Eq a => a -> a -> Bool
    == Key
    i' -> do
              let ti :: Type
    ti = Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom (Dom Type -> Type) -> Dom Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> [Dom Type] -> Key -> Dom Type
    forall a. a -> [a] -> Key -> a
    indexWithDefault Dom Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Telescope -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Telescope
    k) Key
    i
              Relevance
    -> Telescope
    -> Telescope
    -> (Type, Elims -> Term)
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k (Type
    ti , Key -> Elims -> Term
    Var Key
    i) [Elim' NLPat]
    ps Elims
    es
            Term
    _ | Pi Dom Type
    a Abs Type
    b <- Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t -> do
              let ai :: ArgInfo
    ai    = Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    a
                  pbody :: NLPat
    pbody = Key -> [Elim' NLPat] -> NLPat
    PBoundVar (Key
    1Key -> Key -> Key
    forall a. Num a => a -> a -> a
    +Key
    i) ([Elim' NLPat] -> NLPat) -> [Elim' NLPat] -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Key -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. Subst a => Key -> a -> a
    raise Key
    1 [Elim' NLPat]
    ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. [a] -> [a] -> [a]
    ++ [ Arg NLPat -> Elim' NLPat
    forall a. Arg a -> Elim' a
    Apply (Arg NLPat -> Elim' NLPat) -> Arg NLPat -> Elim' NLPat
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> NLPat -> Arg NLPat
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (NLPat -> Arg NLPat) -> NLPat -> Arg NLPat
    forall a b. (a -> b) -> a -> b
    $ Term -> NLPat
    PTerm (Term -> NLPat) -> Term -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Key -> Term
    var Key
    0 ]
                  body :: Term
    body  = Key -> Term -> Term
    forall a. Subst a => Key -> a -> a
    raise Key
    1 Term
    v Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Key -> Term
    var Key
    0 ]
                  k' :: Telescope
    k'    = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    a (String -> Telescope -> Abs Telescope
    forall a. String -> a -> Abs a
    Abs (Abs Type -> String
    forall a. Abs a -> String
    absName Abs Type
    b) Telescope
    k)
              Relevance
    -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k' (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b) NLPat
    pbody Term
    body
            Term
    _ | Just (QName
    d, Args
    pars) <- Maybe (QName, Args)
    etaRecord -> do
              Defn
    def <- Telescope -> NLM Defn -> NLM Defn
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM Defn -> NLM Defn) -> NLM Defn -> NLM Defn
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef (Definition -> Defn) -> NLM Definition -> NLM Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> NLM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
              (Telescope
    tel, ConHead
    c, ConInfo
    ci, Args
    vs) <- Telescope
    -> NLM (Telescope, ConHead, ConInfo, Args)
    -> NLM (Telescope, ConHead, ConInfo, Args)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM (Telescope, ConHead, ConInfo, Args)
     -> NLM (Telescope, ConHead, ConInfo, Args))
    -> NLM (Telescope, ConHead, ConInfo, Args)
    -> NLM (Telescope, ConHead, ConInfo, Args)
    forall a b. (a -> b) -> a -> b
    $ QName
    -> Args -> Defn -> Term -> NLM (Telescope, ConHead, ConInfo, Args)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName
    -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
    etaExpandRecord_ QName
    d Args
    pars Defn
    def Term
    v
              ~(Just ((QName, Type, Args)
    _ , Type
    ct)) <- Telescope
    -> NLM (Maybe ((QName, Type, Args), Type))
    -> NLM (Maybe ((QName, Type, Args), Type))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (NLM (Maybe ((QName, Type, Args), Type))
     -> NLM (Maybe ((QName, Type, Args), Type)))
    -> NLM (Maybe ((QName, Type, Args), Type))
    -> NLM (Maybe ((QName, Type, Args), Type))
    forall a b. (a -> b) -> a -> b
    $ ConHead -> Type -> NLM (Maybe ((QName, Type, Args), Type))
    forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    getFullyAppliedConType ConHead
    c Type
    t
              let flds :: [Arg QName]
    flds = (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term QName -> Arg QName
    forall t a. Dom' t a -> Arg a
    argFromDom ([Dom' Term QName] -> [Arg QName])
    -> [Dom' Term QName] -> [Arg QName]
    forall a b. (a -> b) -> a -> b
    $ Defn -> [Dom' Term QName]
    recFields Defn
    def
                  ps' :: [Arg NLPat]
    ps'  = (Arg QName -> Arg NLPat) -> [Arg QName] -> [Arg NLPat]
    forall a b. (a -> b) -> [a] -> [b]
    map ((QName -> NLPat) -> Arg QName -> Arg NLPat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((QName -> NLPat) -> Arg QName -> Arg NLPat)
    -> (QName -> NLPat) -> Arg QName -> Arg NLPat
    forall a b. (a -> b) -> a -> b
    $ \QName
    fld -> Key -> [Elim' NLPat] -> NLPat
    PBoundVar Key
    i ([Elim' NLPat]
    ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. [a] -> [a] -> [a]
    ++ [ProjOrigin -> QName -> Elim' NLPat
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    fld])) [Arg QName]
    flds
              Relevance
    -> Telescope
    -> Telescope
    -> (Type, Elims -> Term)
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Telescope
    k (Type
    ct, ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci) ((Arg NLPat -> Elim' NLPat) -> [Arg NLPat] -> [Elim' NLPat]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg NLPat -> Elim' NLPat
    forall a. Arg a -> Elim' a
    Apply [Arg NLPat]
    ps') ((Arg Term -> Elim) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Args
    vs)
            Term
    v -> Term -> NLM ()
    maybeBlock Term
    v
          PTerm Term
    u -> String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    60 (TCMT IO Doc
    "matching a PTerm" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Telescope
    gamma Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    k) (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    u)) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $
            Telescope -> Telescope -> Type -> Term -> Term -> NLM ()
    tellEq Telescope
    gamma Telescope
    k Type
    t Term
    u Term
    v

    -- Checks if the given term contains any free variables that satisfy the
    -- given condition on their DBI, possibly reducing the term in the process.
    -- Returns `Right Nothing` if there are such variables, `Right (Just v')`
    -- if there are none (where v' is the possibly reduced version of the given
    -- term) or `Left b` if the problem is blocked on a meta.
    reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a)
               => IntSet -> a -> m (Either Blocked_ (Maybe a))
    reallyFree :: forall (m :: * -> *) a.
    (MonadReduce m, Reduce a, ForceNotFree a) =>
    IntSet -> a -> m (Either Blocked_ (Maybe a))
    reallyFree IntSet
    xs a
    v = do
      (IntMap IsFree
    mxs , a
    v') <- IntSet -> a -> m (IntMap IsFree, a)
    forall a (m :: * -> *).
    (ForceNotFree a, Reduce a, MonadReduce m) =>
    IntSet -> a -> m (IntMap IsFree, a)
    forceNotFree IntSet
    xs a
    v
      case (IsFree -> IsFree -> IsFree) -> IsFree -> IntMap IsFree -> IsFree
    forall a b. (a -> b -> b) -> b -> IntMap a -> b
    IntMap.foldr IsFree -> IsFree -> IsFree
    pickFree IsFree
    NotFree IntMap IsFree
    mxs of
        MaybeFree MetaSet
    ms
          | MetaSet -> Bool
    forall a. Null a => a -> Bool
    null MetaSet
    ms   -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a)))
    -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ Maybe a -> Either Blocked_ (Maybe a)
    forall a b. b -> Either a b
    Right Maybe a
    forall a. Maybe a
    Nothing
          | Bool
    otherwise -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a)))
    -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ Blocked_ -> Either Blocked_ (Maybe a)
    forall a b. a -> Either a b
    Left (Blocked_ -> Either Blocked_ (Maybe a))
    -> Blocked_ -> Either Blocked_ (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ Blocker -> () -> Blocked_
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    blocker ()
          where blocker :: Blocker
    blocker = Set Blocker -> Blocker
    unblockOnAll (Set Blocker -> Blocker) -> Set Blocker -> Blocker
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Set Blocker -> Set Blocker)
    -> Set Blocker -> MetaSet -> Set Blocker
    forall a. (MetaId -> a -> a) -> a -> MetaSet -> a
    foldrMetaSet (Blocker -> Set Blocker -> Set Blocker
    forall a. Ord a => a -> Set a -> Set a
    Set.insert (Blocker -> Set Blocker -> Set Blocker)
    -> (MetaId -> Blocker) -> MetaId -> Set Blocker -> Set Blocker
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> Blocker
    unblockOnMeta) Set Blocker
    forall a. Set a
    Set.empty MetaSet
    ms
        IsFree
    NotFree -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a)))
    -> Either Blocked_ (Maybe a) -> m (Either Blocked_ (Maybe a))
    forall a b. (a -> b) -> a -> b
    $ Maybe a -> Either Blocked_ (Maybe a)
    forall a b. b -> Either a b
    Right (a -> Maybe a
    forall a. a -> Maybe a
    Just a
    v')

      where
        -- Check if any of the variables occur freely.
        -- Prefer occurrences that do not depend on any metas.
        pickFree :: IsFree -> IsFree -> IsFree
        pickFree :: IsFree -> IsFree -> IsFree
    pickFree f1 :: IsFree
    f1@(MaybeFree MetaSet
    ms1) IsFree
    f2
          | MetaSet -> Bool
    forall a. Null a => a -> Bool
    null MetaSet
    ms1  = IsFree
    f1
        pickFree f1 :: IsFree
    f1@(MaybeFree MetaSet
    ms1) f2 :: IsFree
    f2@(MaybeFree MetaSet
    ms2)
          | MetaSet -> Bool
    forall a. Null a => a -> Bool
    null MetaSet
    ms2  = IsFree
    f2
          | Bool
    otherwise = IsFree
    f1
        pickFree f1 :: IsFree
    f1@(MaybeFree MetaSet
    ms1) IsFree
    NotFree = IsFree
    f1
        pickFree IsFree
    NotFree IsFree
    f2 = IsFree
    f2

    makeSubstitution :: Telescope -> Sub -> Substitution
    makeSubstitution :: Telescope -> Sub -> Substitution
    makeSubstitution Telescope
    gamma Sub
    sub =
      [Term] -> Substitution
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution) -> [Term] -> Substitution
    forall a b. (a -> b) -> a -> b
    $ (Key -> Term) -> [Key] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    HasCallStack => Term
    __DUMMY_TERM__ (Maybe Term -> Term) -> (Key -> Maybe Term) -> Key -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Key -> Maybe Term
    val) [Key
    0 .. Telescope -> Key
    forall a. Sized a => a -> Key
    size Telescope
    gammaKey -> Key -> Key
    forall a. Num a => a -> a -> a
    -Key
    1]
        where
          val :: Key -> Maybe Term
    val Key
    i = case Key -> Sub -> Maybe (Relevance, Term)
    forall a. Key -> IntMap a -> Maybe a
    IntMap.lookup Key
    i Sub
    sub of
                    Just (Relevance
    Irrelevant, Term
    v) -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Term -> Maybe Term) -> Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Term
    dontCare Term
    v
                    Just (Relevance
    _         , Term
    v) -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    v
                    Maybe (Relevance, Term)
    Nothing              -> Maybe Term
    forall a. Maybe a
    Nothing

    checkPostponedEquations :: PureTCM m
                            => Substitution -> PostponedEquations -> m (Maybe Blocked_)
    checkPostponedEquations :: forall (m :: * -> *).
    PureTCM m =>
    Substitution -> PostponedEquations -> m (Maybe Blocked_)
    checkPostponedEquations Substitution
    sub PostponedEquations
    eqs = PostponedEquations
    -> (PostponedEquation -> m (Maybe Blocked_)) -> m (Maybe Blocked_)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Applicative m, Monoid b) =>
    t a -> (a -> m b) -> m b
    forM' PostponedEquations
    eqs ((PostponedEquation -> m (Maybe Blocked_)) -> m (Maybe Blocked_))
    -> (PostponedEquation -> m (Maybe Blocked_)) -> m (Maybe Blocked_)
    forall a b. (a -> b) -> a -> b
    $
      \ (PostponedEquation Telescope
    k Type
    a Term
    lhs Term
    rhs) -> do
          let lhs' :: Term
    lhs' = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Key -> Substitution -> Substitution
    forall a. Key -> Substitution' a -> Substitution' a
    liftS (Telescope -> Key
    forall a. Sized a => a -> Key
    size Telescope
    k) Substitution
    sub) Term
    lhs
          String
    -> Key -> TCMT IO Doc -> m (Maybe Blocked_) -> m (Maybe Blocked_)
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    30 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "checking postponed equality between" , Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    lhs')
            , TCMT IO Doc
    " and " , Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    rhs) ]) (m (Maybe Blocked_) -> m (Maybe Blocked_))
    -> m (Maybe Blocked_) -> m (Maybe Blocked_)
    forall a b. (a -> b) -> a -> b
    $ do
          Telescope -> m (Maybe Blocked_) -> m (Maybe Blocked_)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    k (m (Maybe Blocked_) -> m (Maybe Blocked_))
    -> m (Maybe Blocked_) -> m (Maybe Blocked_)
    forall a b. (a -> b) -> a -> b
    $ Type -> Term -> Term -> m (Maybe Blocked_)
    forall (m :: * -> *).
    PureTCM m =>
    Type -> Term -> Term -> m (Maybe Blocked_)
    equal Type
    a Term
    lhs' Term
    rhs

    -- main function
    nonLinMatch :: (PureTCM m, Match t a b)
                => Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
    nonLinMatch :: forall (m :: * -> *) t a b.
    (PureTCM m, Match t a b) =>
    Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
    nonLinMatch Telescope
    gamma t
    t a
    p b
    v = do
      let no :: String -> a -> m (Either a b)
    no String
    msg a
    b = String -> Key -> TCMT IO Doc -> m (Either a b) -> m (Either a b)
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    10 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                       [ TCMT IO Doc
    "matching failed during" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    msg
                       , TCMT IO Doc
    "blocking: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (a -> String
    forall a. Show a => a -> String
    show a
    b) ]) (m (Either a b) -> m (Either a b))
    -> m (Either a b) -> m (Either a b)
    forall a b. (a -> b) -> a -> b
    $ Either a b -> m (Either a b)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> Either a b
    forall a b. a -> Either a b
    Left a
    b)
      m (Either Blocked_ NLMState)
    -> (Blocked_ -> m (Either Blocked_ Substitution))
    -> (NLMState -> m (Either Blocked_ Substitution))
    -> m (Either Blocked_ Substitution)
    forall (m :: * -> *) a b c.
    Monad m =>
    m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
    caseEitherM (NLM () -> m (Either Blocked_ NLMState)
    forall (m :: * -> *).
    MonadReduce m =>
    NLM () -> m (Either Blocked_ NLMState)
    runNLM (NLM () -> m (Either Blocked_ NLMState))
    -> NLM () -> m (Either Blocked_ NLMState)
    forall a b. (a -> b) -> a -> b
    $ Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    forall t a b.
    Match t a b =>
    Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
    match Relevance
    Relevant Telescope
    gamma Telescope
    forall a. Tele a
    EmptyTel t
    t a
    p b
    v) (String -> Blocked_ -> m (Either Blocked_ Substitution)
    forall {m :: * -> *} {a} {b}.
    (MonadDebug m, Show a) =>
    String -> a -> m (Either a b)
    no String
    "matching") ((NLMState -> m (Either Blocked_ Substitution))
     -> m (Either Blocked_ Substitution))
    -> (NLMState -> m (Either Blocked_ Substitution))
    -> m (Either Blocked_ Substitution)
    forall a b. (a -> b) -> a -> b
    $ \ NLMState
    s -> do
        let sub :: Substitution
    sub = Telescope -> Sub -> Substitution
    makeSubstitution Telescope
    gamma (Sub -> Substitution) -> Sub -> Substitution
    forall a b. (a -> b) -> a -> b
    $ NLMState
    sNLMState -> Lens' Sub NLMState -> Sub
    forall o i. o -> Lens' i o -> i
    ^.Lens' Sub NLMState
    nlmSub
            eqs :: PostponedEquations
    eqs = NLMState
    sNLMState -> Lens' PostponedEquations NLMState -> PostponedEquations
    forall o i. o -> Lens' i o -> i
    ^.Lens' PostponedEquations NLMState
    nlmEqs
        String
    -> Key
    -> TCMT IO Doc
    -> m (Either Blocked_ Substitution)
    -> m (Either Blocked_ Substitution)
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    90 (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "sub = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Substitution -> String
    forall a. Show a => a -> String
    show Substitution
    sub) (m (Either Blocked_ Substitution)
     -> m (Either Blocked_ Substitution))
    -> m (Either Blocked_ Substitution)
    -> m (Either Blocked_ Substitution)
    forall a b. (a -> b) -> a -> b
    $ do
        Maybe Blocked_
    ok <- Substitution -> PostponedEquations -> m (Maybe Blocked_)
    forall (m :: * -> *).
    PureTCM m =>
    Substitution -> PostponedEquations -> m (Maybe Blocked_)
    checkPostponedEquations Substitution
    sub PostponedEquations
    eqs
        case Maybe Blocked_
    ok of
          Maybe Blocked_
    Nothing -> Either Blocked_ Substitution -> m (Either Blocked_ Substitution)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocked_ Substitution -> m (Either Blocked_ Substitution))
    -> Either Blocked_ Substitution -> m (Either Blocked_ Substitution)
    forall a b. (a -> b) -> a -> b
    $ Substitution -> Either Blocked_ Substitution
    forall a b. b -> Either a b
    Right Substitution
    sub
          Just Blocked_
    b  -> String -> Blocked_ -> m (Either Blocked_ Substitution)
    forall {m :: * -> *} {a} {b}.
    (MonadDebug m, Show a) =>
    String -> a -> m (Either a b)
    no String
    "checking of postponed equations" Blocked_
    b

    -- | Typed βη-equality, also handles empty record types.
    --   Returns `Nothing` if the terms are equal, or `Just b` if the terms are not
    --   (where b contains information about possible metas blocking the comparison)
    equal :: PureTCM m => Type -> Term -> Term -> m (Maybe Blocked_)
    equal :: forall (m :: * -> *).
    PureTCM m =>
    Type -> Term -> Term -> m (Maybe Blocked_)
    equal Type
    a Term
    u Term
    v = BlockT m Bool -> m (Either Blocker Bool)
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked (Type -> Term -> Term -> BlockT m Bool
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Type -> Term -> Term -> m Bool
    pureEqualTerm Type
    a Term
    u Term
    v) m (Either Blocker Bool)
    -> (Either Blocker Bool -> m (Maybe Blocked_))
    -> m (Maybe Blocked_)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Left Blocker
    b      -> Maybe Blocked_ -> m (Maybe Blocked_)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Blocked_ -> m (Maybe Blocked_))
    -> Maybe Blocked_ -> m (Maybe Blocked_)
    forall a b. (a -> b) -> a -> b
    $ Blocked_ -> Maybe Blocked_
    forall a. a -> Maybe a
    Just (Blocked_ -> Maybe Blocked_) -> Blocked_ -> Maybe Blocked_
    forall a b. (a -> b) -> a -> b
    $ Blocker -> () -> Blocked_
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    b ()
      Right Bool
    True  -> Maybe Blocked_ -> m (Maybe Blocked_)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Blocked_
    forall a. Maybe a
    Nothing
      Right Bool
    False -> String
    -> Key -> TCMT IO Doc -> m (Maybe Blocked_) -> m (Maybe Blocked_)
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    10 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
          [ TCMT IO Doc
    "mismatch between " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    u
          , TCMT IO Doc
    " and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v
          ]) (m (Maybe Blocked_) -> m (Maybe Blocked_))
    -> m (Maybe Blocked_) -> m (Maybe Blocked_)
    forall a b. (a -> b) -> a -> b
    $ do
        Maybe Blocked_ -> m (Maybe Blocked_)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Blocked_ -> m (Maybe Blocked_))
    -> Maybe Blocked_ -> m (Maybe Blocked_)
    forall a b. (a -> b) -> a -> b
    $ Blocked_ -> Maybe Blocked_
    forall a. a -> Maybe a
    Just (Blocked_ -> Maybe Blocked_) -> Blocked_ -> Maybe Blocked_
    forall a b. (a -> b) -> a -> b
    $ NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked ()

    -- | Utility function for getting the name and type of a head term (i.e. a
    --   `Def` or `Con` with no arguments)
    getTypedHead :: PureTCM m => Term -> m (Maybe (QName, Type))
    getTypedHead :: forall (m :: * -> *). PureTCM m => Term -> m (Maybe (QName, Type))
    getTypedHead = \case
      Def QName
    f []   -> (QName, Type) -> Maybe (QName, Type)
    forall a. a -> Maybe a
    Just ((QName, Type) -> Maybe (QName, Type))
    -> (Definition -> (QName, Type))
    -> Definition
    -> Maybe (QName, Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QName
    f,) (Type -> (QName, Type))
    -> (Definition -> Type) -> Definition -> (QName, Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Type
    defType (Definition -> Maybe (QName, Type))
    -> m Definition -> m (Maybe (QName, Type))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
      Con (ConHead { conName :: ConHead -> QName
    conName = QName
    c }) ConInfo
    _ [] -> do
        -- Andreas, 2018-09-08, issue #3211:
        -- discount module parameters for constructor heads
        Args
    vs <- QName -> m Args
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    QName -> m Args
    freeVarsToApply QName
    c
        -- Jesper, 2020-06-17, issue #4755: add dummy arguments in
        -- case we don't have enough parameters
        Key
    npars <- Key -> Maybe Key -> Key
    forall a. a -> Maybe a -> a
    fromMaybe Key
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Key -> Key) -> m (Maybe Key) -> m Key
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe Key)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Key)
    getNumberOfParameters QName
    c
        let ws :: Args
    ws = Key -> Arg Term -> Args
    forall a. Key -> a -> [a]
    replicate (Key
    npars Key -> Key -> Key
    forall a. Num a => a -> a -> a
    - Args -> Key
    forall a. Sized a => a -> Key
    size Args
    vs) (Arg Term -> Args) -> Arg Term -> Args
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    HasCallStack => Term
    __DUMMY_TERM__
        Type
    t0 <- Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    c
        Type
    t <- Type
    t0 Type -> Args -> m Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    Type -> a -> m Type
    `piApplyM` (Args
    vs Args -> Args -> Args
    forall a. [a] -> [a] -> [a]
    ++ Args
    ws)
        Maybe (QName, Type) -> m (Maybe (QName, Type))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (QName, Type) -> m (Maybe (QName, Type)))
    -> Maybe (QName, Type) -> m (Maybe (QName, Type))
    forall a b. (a -> b) -> a -> b
    $ (QName, Type) -> Maybe (QName, Type)
    forall a. a -> Maybe a
    Just (QName
    c , Type
    t)
      Term
    _ -> Maybe (QName, Type) -> m (Maybe (QName, Type))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Type)
    forall a. Maybe a
    Nothing