    {-# LANGUAGE NondecreasingIndentation #-}

    -- | Checking local or global confluence of rewrite rules.
    --
    -- For checking LOCAL CONFLUENCE of a given rewrite rule @f ps ↦ v@,
    -- we construct critical pairs involving this as the main rule by
    -- searching for:
    --
    -- 1. *Different* rules @f ps' ↦ ...@ where @ps@ and @ps'@ can be
    --    unified.
    --
    -- 2. Subpatterns @g qs@ of @ps@ and rewrite rules @g qs' ↦ ...@ where
    --    @qs@ and @qs'@ can be unified.
    --
    -- Each of these leads to a *critical pair* @v₁ <-- f us --> v₂@, which
    -- should satisfy @v₁ = v₂@.
    --
    -- For checking GLOBAL CONFLUENCE, we check the following two
    -- properties:
    --
    -- 1. For any two left-hand sides of the rewrite rules that overlap
    --    (either at the root position or at a subterm), the most general
    --    unifier of the two left-hand sides is again a left-hand side of
    --    a rewrite rule. For example, if there are two rules @suc m + n =
    --    suc (m + n)@ and @m + suc n = suc (m + n)@, then there should
    --    also be a rule @suc m + suc n = suc (suc (m + n))@.
    --
    -- 2. Each rewrite rule should satisfy the *triangle property*: For
    --    any rewrite rule @u ↦ w@ and any single-step parallel unfolding
    --    @u => v@, we should have another single-step parallel unfolding
    --    @v => w@.

    module Agda.TypeChecking.Rewriting.Confluence
      ( checkConfluenceOfRules
      , checkConfluenceOfClauses
      , sortRulesOfSymbol
      ) where

    import Control.Applicative
    import Control.Arrow ((***))
    import Control.Monad.Except ( MonadError(..) )
    import Control.Monad.Reader ( MonadReader(..), asks, runReaderT )

    import Data.Either
    import Data.Function ( on )
    import Data.Functor ( ($>) )
    import qualified Data.HashMap.Strict as HMap
    import Data.List ( elemIndex , tails )
    import Data.Set (Set)
    import qualified Data.Set as Set

    import Agda.Interaction.Options ( ConfluenceCheck(..) )

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

    import Agda.TypeChecking.Constraints
    import Agda.TypeChecking.Conversion
    import Agda.TypeChecking.Conversion.Pure
    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Irrelevance ( isIrrelevantOrPropM )
    import Agda.TypeChecking.Level
    import Agda.TypeChecking.MetaVars
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Pretty.Warning    ()
    import Agda.TypeChecking.Pretty.Constraint
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Rewriting.Clause
    import Agda.TypeChecking.Rewriting.NonLinMatch
    import Agda.TypeChecking.Rewriting.NonLinPattern
    import Agda.TypeChecking.Sort
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Warnings

    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.Impossible
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.ListT
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null (unlessNullM)
    import Agda.Utils.Permutation
    import Agda.Utils.Singleton
    import Agda.Utils.Size

    -- | Check confluence of the clauses of the given function wrt rewrite rules of the
    -- constructors they match against
    checkConfluenceOfClauses :: ConfluenceCheck -> QName -> TCM ()
    checkConfluenceOfClauses :: ConfluenceCheck -> QName -> TCM ()
    checkConfluenceOfClauses ConfluenceCheck
    confChk QName
    f = do
      rews <- QName -> TCMT IO [RewriteRule]
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getClausesAsRewriteRules QName
    f
      let noMetasInPats RewriteRule
    rew
            | PElims -> Bool
    forall a. AllMetas a => a -> Bool
    noMetas (RewriteRule -> PElims
    rewPats RewriteRule
    rew) = Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
            | Bool
    otherwise             = Bool
    False Bool -> TCM () -> TCMT IO Bool
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ do Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Warning
    ConfluenceCheckingIncompleteBecauseOfMeta QName
    f
      rews <- filterM noMetasInPats rews
      let matchables = (RewriteRule -> [QName]) -> [RewriteRule] -> [[QName]]
    forall a b. (a -> b) -> [a] -> [b]
    map RewriteRule -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables [RewriteRule]
    rews
      reportSDoc "rewriting.confluence" 30 $
        "Function" <+> prettyTCM f <+> "has matchable symbols" <+> prettyList_ (map prettyTCM matchables)
      modifySignature $ setMatchableSymbols f $ concat matchables
      let hasRules QName
    g = Bool -> Bool
    not (Bool -> Bool) -> ([RewriteRule] -> Bool) -> [RewriteRule] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [RewriteRule] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ([RewriteRule] -> Bool) -> f [RewriteRule] -> f Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> f [RewriteRule]
    forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
    getRewriteRulesFor QName
    g
      forM_ (zip rews matchables) $ \(RewriteRule
    rew,[QName]
    ms) ->
        TCMT IO [QName] -> ([QName] -> TCM ()) -> TCM ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    m a -> (a -> m ()) -> m ()
    unlessNullM ((QName -> TCMT IO Bool) -> [QName] -> TCMT IO [QName]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM QName -> TCMT IO Bool
    forall {f :: * -> *}. HasConstInfo f => QName -> f Bool
    hasRules [QName]
    ms) (([QName] -> TCM ()) -> TCM ()) -> ([QName] -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \[QName]
    _ -> do
          ConfluenceCheck -> [RewriteRule] -> TCM ()
    checkConfluenceOfRules ConfluenceCheck
    confChk [RewriteRule
    rew]

    -- | Check confluence of the given rewrite rules wrt all other rewrite
    --   rules (also amongst themselves).
    checkConfluenceOfRules :: ConfluenceCheck -> [RewriteRule] -> TCM ()
    checkConfluenceOfRules :: ConfluenceCheck -> [RewriteRule] -> TCM ()
    checkConfluenceOfRules ConfluenceCheck
    confChk [RewriteRule]
    rews = TCM () -> TCM ()
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    inAbstractMode (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

      -- Global confluence: we need to check the triangle property for each rewrite
      -- rule of each head symbol as well as rules that match on them
      Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (ConfluenceCheck
    confChk ConfluenceCheck -> ConfluenceCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConfluenceCheck
    GlobalConfluenceCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        let getSymbols :: RewriteRule -> f (Set QName)
    getSymbols RewriteRule
    rew = let f :: QName
    f = RewriteRule -> QName
    rewHead RewriteRule
    rew in
             (QName -> Set QName -> Set QName
    forall a. Ord a => a -> Set a -> Set a
    Set.insert QName
    f) (Set QName -> Set QName)
    -> (Definition -> Set QName) -> Definition -> Set QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Set QName
    defMatchable (Definition -> Set QName) -> f Definition -> f (Set QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> f Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
        allSymbols <- Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList (Set QName -> [QName])
    -> ([Set QName] -> Set QName) -> [Set QName] -> [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Set QName] -> Set QName
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set QName] -> [QName]) -> TCMT IO [Set QName] -> TCMT IO [QName]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (RewriteRule -> TCMT IO (Set QName))
    -> [RewriteRule] -> TCMT IO [Set QName]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse RewriteRule -> TCMT IO (Set QName)
    forall {f :: * -> *}.
    HasConstInfo f =>
    RewriteRule -> f (Set QName)
    getSymbols [RewriteRule]
    rews
        forM_ allSymbols $ \QName
    f -> do
          rewsf <- QName -> TCMT IO [RewriteRule]
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getAllRulesFor QName
    f
          forM_ rewsf $ \RewriteRule
    rew -> do
            VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.triangle" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              TCMT IO Doc
    "(re)checking triangle property for rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    rew)
            RewriteRule -> TCM ()
    checkTrianglePropertyForRule RewriteRule
    rew

      [[RewriteRule]] -> ([RewriteRule] -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ ([RewriteRule] -> [[RewriteRule]]
    forall a. [a] -> [[a]]
    tails [RewriteRule]
    rews) (([RewriteRule] -> TCM ()) -> TCM ())
    -> ([RewriteRule] -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM ()
    -> (RewriteRule -> [RewriteRule] -> TCM ())
    -> [RewriteRule]
    -> TCM ()
    forall b a. b -> (a -> [a] -> b) -> [a] -> b
    listCase (() -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) ((RewriteRule -> [RewriteRule] -> TCM ())
     -> [RewriteRule] -> TCM ())
    -> (RewriteRule -> [RewriteRule] -> TCM ())
    -> [RewriteRule]
    -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \RewriteRule
    rew [RewriteRule]
    rewsRest -> do

      VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "Checking confluence of rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    rew)
      VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "Checking confluence of rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> RewriteRule -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => RewriteRule -> m Doc
    prettyTCM RewriteRule
    rew

      let f :: QName
    f   = RewriteRule -> QName
    rewHead RewriteRule
    rew
          qs :: PElims
    qs  = RewriteRule -> PElims
    rewPats RewriteRule
    rew
          tel :: Telescope
    tel = RewriteRule -> Telescope
    rewContext RewriteRule
    rew
      def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
      (fa , hdf) <- addContext tel $ makeHead def (rewType rew)

      reportSDoc "rewriting.confluence" 30 $ addContext tel $
        "Head symbol" <+> prettyTCM (hdf []) <+> "of rewrite rule has type" <+> prettyTCM fa

      -- Step 1: check other rewrite rules that overlap at top position
      forMM_ (getAllRulesFor f) $ \ RewriteRule
    rew' -> do
        Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ((RewriteRule -> Bool) -> [RewriteRule] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (RewriteRule -> RewriteRule -> Bool
    sameRuleName RewriteRule
    rew') (RewriteRule
    rewRewriteRule -> [RewriteRule] -> [RewriteRule]
    forall a. a -> [a] -> [a]
    :[RewriteRule]
    rewsRest) Bool -> Bool -> Bool
    ||
                (RewriteRule -> Bool
    rewFromClause RewriteRule
    rew Bool -> Bool -> Bool
    && RewriteRule -> Bool
    rewFromClause RewriteRule
    rew')) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          (Elims -> Term) -> RewriteRule -> RewriteRule -> TCM ()
    checkConfluenceTop Elims -> Term
    hdf RewriteRule
    rew RewriteRule
    rew'
      reportSDoc "rewriting.confluence" 30 $ "Finished step 1 of confluence check of rule" <+> prettyTCM (rewName rew)

      -- Step 2: check other rewrite rules that overlap with a subpattern
      -- of this rewrite rule
      es <- nlPatToTerm qs
      forMM_ (addContext tel $ allHolesList (fa, hdf) es) $ \ OneHole Elims
    hole -> do
        let g :: QName
    g   = OneHole Elims -> QName
    forall a. OneHole a -> QName
    ohHeadName OneHole Elims
    hole
            hdg :: Elims -> Term
    hdg = OneHole Elims -> Elims -> Term
    forall a. OneHole a -> Elims -> Term
    ohHead OneHole Elims
    hole
        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO Doc
    "Found hole with head symbol" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    g
        rews' <- QName -> TCMT IO [RewriteRule]
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getAllRulesFor QName
    g
        forM_ rews' $ \RewriteRule
    rew' -> do
          Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ((RewriteRule -> Bool) -> [RewriteRule] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (RewriteRule -> RewriteRule -> Bool
    sameRuleName RewriteRule
    rew') [RewriteRule]
    rewsRest) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            (Elims -> Term)
    -> (Elims -> Term)
    -> RewriteRule
    -> RewriteRule
    -> OneHole Elims
    -> TCM ()
    checkConfluenceSub Elims -> Term
    hdf Elims -> Term
    hdg RewriteRule
    rew RewriteRule
    rew' OneHole Elims
    hole
      reportSDoc "rewriting.confluence" 30 $ "Finished step 2 of confluence check of rule" <+> prettyTCM (rewName rew)

      -- Step 3: check other rewrite rules that have a subpattern which
      -- overlaps with this rewrite rule
      forM_ (defMatchable def) $ \ QName
    g -> do
        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO Doc
    "Symbol" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    g TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "has rules that match on" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    f
        TCMT IO [RewriteRule] -> (RewriteRule -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, Monad m) =>
    m (t a) -> (a -> m ()) -> m ()
    forMM_ (QName -> TCMT IO [RewriteRule]
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getAllRulesFor QName
    g) ((RewriteRule -> TCM ()) -> TCM ())
    -> (RewriteRule -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ RewriteRule
    rew' -> do
          Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ((RewriteRule -> Bool) -> [RewriteRule] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (RewriteRule -> RewriteRule -> Bool
    sameRuleName RewriteRule
    rew') [RewriteRule]
    rewsRest) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            es' <- PElims -> TCMT IO Elims
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => PElims -> m Elims
    nlPatToTerm (RewriteRule -> PElims
    rewPats RewriteRule
    rew')
            let tel' = RewriteRule -> Telescope
    rewContext RewriteRule
    rew'
            def' <- getConstInfo g
            (ga , hdg) <- addContext tel' $ makeHead def' (rewType rew')
            forMM_ (addContext tel' $ allHolesList (ga , hdg) es') $ \ OneHole Elims
    hole -> do
              let f' :: QName
    f' = OneHole Elims -> QName
    forall a. OneHole a -> QName
    ohHeadName OneHole Elims
    hole
              Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when (QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f') (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Elims -> Term)
    -> (Elims -> Term)
    -> RewriteRule
    -> RewriteRule
    -> OneHole Elims
    -> TCM ()
    checkConfluenceSub Elims -> Term
    hdg Elims -> Term
    hdf RewriteRule
    rew' RewriteRule
    rew OneHole Elims
    hole
      reportSDoc "rewriting.confluence" 30 $ "Finished step 3 of confluence check of rule" <+> prettyTCM (rewName rew)

      where

        -- Check confluence of two rewrite rules that have the same head symbol,
        -- e.g. @f ps --> a@ and @f ps' --> b@.
        checkConfluenceTop :: (Elims -> Term) -> RewriteRule -> RewriteRule -> TCM ()
        checkConfluenceTop :: (Elims -> Term) -> RewriteRule -> RewriteRule -> TCM ()
    checkConfluenceTop Elims -> Term
    hd RewriteRule
    rew1 RewriteRule
    rew2 =
          Call -> TCM () -> TCM ()
    forall a. Call -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (QName -> QName -> Call
    CheckConfluence (RewriteRule -> QName
    rewName RewriteRule
    rew1) (RewriteRule -> QName
    rewName RewriteRule
    rew2)) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          TCM () -> TCM ()
    forall a. TCM a -> TCM a
    localTCStateSavingWarnings (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

            sub1 <- Telescope -> TCMT IO Substitution
    forall (m :: * -> *).
    MonadMetaSolver m =>
    Telescope -> m Substitution
    makeMetaSubst (Telescope -> TCMT IO Substitution)
    -> Telescope -> TCMT IO Substitution
    forall a b. (a -> b) -> a -> b
    $ RewriteRule -> Telescope
    rewContext RewriteRule
    rew1
            sub2 <- makeMetaSubst $ rewContext rew2

            let f    = RewriteRule -> QName
    rewHead RewriteRule
    rew1 -- == rewHead rew2
                a1   = Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Type)
    sub1 (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ RewriteRule -> Type
    rewType RewriteRule
    rew1
                a2   = Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Type)
    sub2 (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ RewriteRule -> Type
    rewType RewriteRule
    rew2

            es1 <- applySubst sub1 <$> nlPatToTerm (rewPats rew1)
            es2 <- applySubst sub2 <$> nlPatToTerm (rewPats rew2)

            reportSDoc "rewriting.confluence" 30 $ vcat
              [ "checkConfluenceTop" <+> prettyTCM (rewName rew1) <+> prettyTCM (rewName rew2)
              , "  f    = " <+> prettyTCM f
              , "  ctx1 = " <+> prettyTCM (rewContext rew1)
              , "  ctx2 = " <+> prettyTCM (rewContext rew2)
              , "  es1  = " <+> prettyTCM es1
              , "  es2  = " <+> prettyTCM es2
              ]

            -- Make sure we are comparing eliminations with the same arity
            -- (see #3810).
            let n = Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    min (Elims -> Int
    forall a. Sized a => a -> Int
    size Elims
    es1) (Elims -> Int
    forall a. Sized a => a -> Int
    size Elims
    es2)
                (es1' , es1r) = splitAt n es1
                (es2' , es2r) = splitAt n es2
                esr           = Elims
    es1r Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es2r

                lhs1 = Elims -> Term
    hd (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Elims
    es1' Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    esr
                lhs2 = Elims -> Term
    hd (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Elims
    es2' Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    esr

                -- Use type of rewrite rule with the most eliminations
                a | Elims -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Elims
    es1r = Type
    a2
                  | Bool
    otherwise = Type
    a1

            reportSDoc "rewriting.confluence" 20 $ sep
              [ "Considering potential critical pair at top-level: "
              , nest 2 $ prettyTCM $ lhs1, " =?= "
              , nest 2 $ prettyTCM $ lhs2 , " : " , nest 2 $ prettyTCM a
              ]

            maybeCriticalPair <- tryUnification lhs1 lhs2 $ do
              -- Unify the left-hand sides of both rewrite rules
              fa   <- defType <$> getConstInfo f
              fpol <- getPolarity' CmpEq f
              onlyReduceTypes $
                compareElims fpol [] fa (hd []) es1' es2'

              -- Get the rhs of both rewrite rules (after unification). In
              -- case of different arities, add additional arguments from
              -- one side to the other side.
              let rhs1 = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    sub1 (RewriteRule -> Term
    rewRHS RewriteRule
    rew1) Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es2r
                  rhs2 = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    sub2 (RewriteRule -> Term
    rewRHS RewriteRule
    rew2) Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es1r

              return (rhs1 , rhs2)

            whenJust maybeCriticalPair $ uncurry (checkCriticalPair a hd (es1' ++ esr))

        -- Check confluence between two rules that overlap at a subpattern,
        -- e.g. @f ps[g qs] --> a@ and @g qs' --> b@.
        checkConfluenceSub :: (Elims -> Term) -> (Elims -> Term) -> RewriteRule -> RewriteRule -> OneHole Elims -> TCM ()
        checkConfluenceSub :: (Elims -> Term)
    -> (Elims -> Term)
    -> RewriteRule
    -> RewriteRule
    -> OneHole Elims
    -> TCM ()
    checkConfluenceSub Elims -> Term
    hdf Elims -> Term
    hdg RewriteRule
    rew1 RewriteRule
    rew2 OneHole Elims
    hole0 = do
          VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Int
    100 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "foo 2" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    rew1) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    rew2)
          Call -> TCM () -> TCM ()
    forall a. Call -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (QName -> QName -> Call
    CheckConfluence (RewriteRule -> QName
    rewName RewriteRule
    rew1) (RewriteRule -> QName
    rewName RewriteRule
    rew2)) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    forall a. TCM a -> TCM a
    localTCStateSavingWarnings (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

            VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              TCMT IO Doc
    "Checking confluence of rules" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    rew1) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
              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
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    rew2) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "at subpattern position"

            sub1 <- Telescope -> TCMT IO Substitution
    forall (m :: * -> *).
    MonadMetaSolver m =>
    Telescope -> m Substitution
    makeMetaSubst (Telescope -> TCMT IO Substitution)
    -> Telescope -> TCMT IO Substitution
    forall a b. (a -> b) -> a -> b
    $ RewriteRule -> Telescope
    rewContext RewriteRule
    rew1

            let bvTel0     = OneHole Elims -> Telescope
    forall a. OneHole a -> Telescope
    ohBoundVars OneHole Elims
    hole0
                k          = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    bvTel0
                b0         = Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    k Substitution
    sub1) (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ OneHole Elims -> Type
    forall a. OneHole a -> Type
    ohType OneHole Elims
    hole0
                g          = OneHole Elims -> QName
    forall a. OneHole a -> QName
    ohHeadName OneHole Elims
    hole0
                es0        = Substitution' (SubstArg Elims) -> Elims -> Elims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS Int
    k Substitution
    sub1) (Elims -> Elims) -> Elims -> Elims
    forall a b. (a -> b) -> a -> b
    $ OneHole Elims -> Elims
    forall a. OneHole a -> Elims
    ohElims OneHole Elims
    hole0
                qs2        = RewriteRule -> PElims
    rewPats RewriteRule
    rew2

            -- TODO: support IApply in forceEtaExpansion
            let isIApply IApply{} = Bool
    True
                isIApply Elim' a
    _        = Bool
    False
            unless (any isIApply $ drop (size es0) qs2) $ do

            -- If the second rewrite rule has more eliminations than the
            -- subpattern of the first rule, the only chance of overlap is
            -- by eta-expanding the subpattern of the first rule.
            hole1 <- addContext bvTel0 $
              forceEtaExpansion b0 (hdg es0) $ drop (size es0) qs2

            verboseS "rewriting.confluence.eta" 30 $
              unless (size es0 == size qs2) $
              addContext bvTel0 $
              reportSDoc "rewriting.confluence.eta" 30 $ vcat
                [ "forceEtaExpansion result:"
                , nest 2 $ "bound vars: " <+> prettyTCM (ohBoundVars hole1)
                , nest 2 $ "hole contents: " <+> addContext (ohBoundVars hole1) (prettyTCM $ ohContents hole1)
                ]

            let hole      = OneHole Term
    hole1 OneHole Term -> OneHole Elims -> OneHole Elims
    forall a. OneHole Term -> OneHole a -> OneHole a
    `composeHole` OneHole Elims
    hole0
                g         = OneHole Elims -> QName
    forall a. OneHole a -> QName
    ohHeadName OneHole Elims
    hole -- == rewHead rew2
                es'       = OneHole Elims -> Elims
    forall a. OneHole a -> Elims
    ohElims OneHole Elims
    hole
                bvTel     = OneHole Elims -> Telescope
    forall a. OneHole a -> Telescope
    ohBoundVars OneHole Elims
    hole
                plug      = OneHole Elims -> Term -> Elims
    forall a. OneHole a -> Term -> a
    ohPlugHole OneHole Elims
    hole

            sub2 <- addContext bvTel $ makeMetaSubst $ rewContext rew2

            let es1 = Substitution' (SubstArg Elims) -> Elims -> Elims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    bvTel) Substitution
    sub1) Elims
    es'
            es2 <- applySubst sub2 <$> nlPatToTerm (rewPats rew2)

            -- Make sure we are comparing eliminations with the same arity
            -- (see #3810). Because we forced eta-expansion of es1, we
            -- know that it is at least as long as es2.
            when (size es1 < size es2) __IMPOSSIBLE__
            let n = Elims -> Int
    forall a. Sized a => a -> Int
    size Elims
    es2
                (es1' , es1r) = splitAt n es1

            let lhs1 = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    sub1 (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Elims -> Term
    hdf (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Elims
    plug (Term -> Elims) -> Term -> Elims
    forall a b. (a -> b) -> a -> b
    $ Elims -> Term
    hdg Elims
    es1
                lhs2 = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    sub1 (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Elims -> Term
    hdf (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Elims
    plug (Term -> Elims) -> Term -> Elims
    forall a b. (a -> b) -> a -> b
    $ Elims -> Term
    hdg (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Elims
    es2 Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    es1r
                a    = Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Type)
    sub1 (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ RewriteRule -> Type
    rewType RewriteRule
    rew1

            reportSDoc "rewriting.confluence" 20 $ sep
              [ "Considering potential critical pair at subpattern: "
              , nest 2 $ prettyTCM $ lhs1 , " =?= "
              , nest 2 $ prettyTCM $ lhs2 , " : " , nest 2 $ prettyTCM a
              ]

            maybeCriticalPair <- tryUnification lhs1 lhs2 $ do
              -- Unify the subpattern of the first rewrite rule with the lhs
              -- of the second one
              ga   <- defType <$> getConstInfo g
              gpol <- getPolarity' CmpEq g
              onlyReduceTypes $ addContext bvTel $
                compareElims gpol [] ga (hdg []) es1' es2

              -- Right-hand side of first rewrite rule (after unification)
              let rhs1 = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    sub1 (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ RewriteRule -> Term
    rewRHS RewriteRule
    rew1

              -- Left-hand side of first rewrite rule, with subpattern
              -- rewritten by the second rewrite rule
              let w = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    sub2 (RewriteRule -> Term
    rewRHS RewriteRule
    rew2) Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es1r
              reportSDoc "rewriting.confluence" 30 $ sep
                [ "Plugging hole with w = "
                , nest 2 $ addContext bvTel $ prettyTCM w
                ]
              let rhs2 = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    sub1 (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Elims -> Term
    hdf (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Elims
    plug Term
    w

              return (rhs1 , rhs2)

            whenJust maybeCriticalPair $ uncurry (checkCriticalPair a hdf (applySubst sub1 $ plug $ hdg es1))

        checkCriticalPair
          :: Type     -- Type of the critical pair
          -> (Elims -> Term)  -- Head of lhs
          -> Elims            -- Eliminations of lhs
          -> Term     -- First reduct
          -> Term     -- Second reduct
          -> TCM ()
        checkCriticalPair :: Type -> (Elims -> Term) -> Elims -> Term -> Term -> TCM ()
    checkCriticalPair Type
    a Elims -> Term
    hd Elims
    es Term
    rhs1 Term
    rhs2 = do

          (a,es,rhs1,rhs2) <- (Type, Elims, Term, Term) -> TCMT IO (Type, Elims, Term, Term)
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull (Type
    a,Elims
    es,Term
    rhs1,Term
    rhs2)

          let ms = Set MetaId -> [MetaId]
    forall a. Set a -> [a]
    Set.toList (Set MetaId -> [MetaId]) -> Set MetaId -> [MetaId]
    forall a b. (a -> b) -> a -> b
    $ (MetaId -> Set MetaId) -> (Type, Elims, Term, Term) -> Set MetaId
    forall m.
    Monoid m =>
    (MetaId -> m) -> (Type, Elims, Term, Term) -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas MetaId -> Set MetaId
    forall el coll. Singleton el coll => el -> coll
    singleton ((Type, Elims, Term, Term) -> Set MetaId)
    -> (Type, Elims, Term, Term) -> Set MetaId
    forall a b. (a -> b) -> a -> b
    $ (Type
    a,Elims
    es,Term
    rhs1,Term
    rhs2)

          reportSDoc "rewriting.confluence" 30 $ sep
            [ "Abstracting over metas: "
            , prettyList_ (map (text . show) ms)
            ]
          (gamma , (a,es,rhs1,rhs2)) <- fromMaybe __IMPOSSIBLE__ <$>
            abstractOverMetas ms (a,es,rhs1,rhs2)

          addContext gamma $ reportSDoc "rewriting.confluence" 10 $ sep
            [ "Found critical pair: "
            , nest 2 $ prettyTCM (hd es)
            , " ---> " , nest 2 $ prettyTCM rhs1
            , " =?= " , nest 2 $ prettyTCM rhs2
            , " : " , nest 2 $ prettyTCM a ]
          reportSDoc "rewriting.confluence" 30 $ do
            gamma <- instantiateFull gamma
            sep [ "Context of critical pair: "
                , nest 2 $ prettyTCM gamma ]

          addContext gamma $ case confChk of

            -- Local confluence check: check that critical pair has a
            -- common reduct.
            ConfluenceCheck
    LocalConfluenceCheck -> do
                TCM () -> TCM ()
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    dontAssignMetas (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    forall (m :: * -> *) a.
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m a -> m a
    noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Type -> Term -> Term -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    Type -> Term -> Term -> m ()
    equalTerm Type
    a Term
    rhs1 Term
    rhs2
              TCM () -> (TCErr -> TCM ()) -> TCM ()
    forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \case
                TypeError CallStack
    _ TCState
    s Closure TypeError
    err -> do
                  prettyErr <- (TCState -> TCState) -> TCMT IO Doc -> TCMT IO Doc
    forall a. (TCState -> TCState) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    ReadTCState m =>
    (TCState -> TCState) -> m a -> m a
    withTCState (TCState -> TCState -> TCState
    forall a b. a -> b -> a
    const TCState
    s) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Closure TypeError -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Closure TypeError -> m Doc
    prettyTCM Closure TypeError
    err
                  warning $ RewriteNonConfluent (hd es) rhs1 rhs2 prettyErr
                TCErr
    err           -> TCErr -> TCM ()
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err

            -- Global confluence check: enforce that MGU is again the LHS
            -- of a rewrite rule (actual global confluence then follows
            -- from the triangle property which was checked before).
            ConfluenceCheck
    GlobalConfluenceCheck -> do
              (f, t) <- (QName, Type) -> Maybe (QName, Type) -> (QName, Type)
    forall a. a -> Maybe a -> a
    fromMaybe (QName, Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (QName, Type) -> (QName, Type))
    -> TCMT IO (Maybe (QName, Type)) -> TCMT IO (QName, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> TCMT IO (Maybe (QName, Type))
    forall (m :: * -> *). PureTCM m => Term -> m (Maybe (QName, Type))
    getTypedHead (Elims -> Term
    hd [])

              let checkEqualLHS :: RewriteRule -> TCM Bool
                  checkEqualLHS (RewriteRule QName
    q Telescope
    delta QName
    _ PElims
    ps Term
    _ Type
    _ Bool
    _ TopLevelModuleName
    _) = do
                    TCMT IO (Either Blocked_ Substitution)
    -> TCMT IO (Either Blocked_ Substitution)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    onlyReduceTypes (Telescope
    -> TypeOf Elims
    -> PElims
    -> Elims
    -> TCMT IO (Either Blocked_ Substitution)
    forall (m :: * -> *) a b.
    (PureTCM m, Match a b) =>
    Telescope -> TypeOf b -> a -> b -> m (Either Blocked_ Substitution)
    nonLinMatch Telescope
    delta (Type
    t , Elims -> Term
    hd) PElims
    ps Elims
    es) TCMT IO (Either Blocked_ Substitution)
    -> (Either Blocked_ Substitution -> TCMT IO Bool) -> TCMT IO Bool
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                      Left Blocked_
    _    -> Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
                      Right Substitution
    sub -> do
                        let us :: [Term]
    us = Substitution' (SubstArg [Term]) -> [Term] -> [Term]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg [Term])
    sub ([Term] -> [Term]) -> [Term] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ (Int -> Term) -> [Int] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Term
    var ([Int] -> [Term]) -> [Int] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    delta
                            as :: [Dom Type]
    as = Substitution' (SubstArg [Dom Type]) -> [Dom Type] -> [Dom Type]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg [Dom Type])
    sub ([Dom Type] -> [Dom Type]) -> [Dom Type] -> [Dom Type]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Telescope
    delta
                        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.global" Int
    35 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                          Bool -> (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyUnless ([Term] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Term]
    us) (TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (TCMT IO Doc
    "with instantiation" 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Term -> TCMT IO Doc) -> [Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM [Term]
    us))) (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
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Elims -> Term
    hd Elims
    es) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "is an instance of the LHS of rule" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q
                        ok <- [(Term, Dom Type)] -> TCMT IO Bool
    allDistinctVars ([(Term, Dom Type)] -> TCMT IO Bool)
    -> [(Term, Dom Type)] -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ [Term] -> [Dom Type] -> [(Term, Dom Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Term]
    us [Dom Type]
    as
                        when ok $ reportSDoc "rewriting.confluence.global" 30 $
                          "It is equal to the LHS of rewrite rule" <+> prettyTCM q
                        return ok
                  allDistinctVars :: [(Term,Dom Type)] -> TCM Bool
                  allDistinctVars [(Term, Dom Type)]
    us = do
                    us' <- ((Term, Dom Type) -> TCMT IO Bool)
    -> [(Term, Dom Type)] -> TCMT IO [(Term, Dom Type)]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM (Bool -> Bool
    not (Bool -> Bool)
    -> ((Term, Dom Type) -> TCMT IO Bool)
    -> (Term, Dom Type)
    -> TCMT IO Bool
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> Dom Type -> TCMT IO Bool
    forall a (m :: * -> *).
    (LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
     MonadBlock m) =>
    a -> m Bool
    isIrrelevantOrPropM (Dom Type -> TCMT IO Bool)
    -> ((Term, Dom Type) -> Dom Type)
    -> (Term, Dom Type)
    -> TCMT IO Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term, Dom Type) -> Dom Type
    forall a b. (a, b) -> b
    snd) [(Term, Dom Type)]
    us
                    mis <- traverse (\(Term
    u,Dom Type
    a) -> Term -> Type -> TCMT IO (Maybe Int)
    forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
    isEtaVar Term
    u (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a)) $ us'
                    case sequence mis of
                      Just [Int]
    is -> Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ [Int] -> Bool
    forall a. Ord a => [a] -> Bool
    fastDistinct [Int]
    is
                      Maybe [Int]
    Nothing -> Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

              rews <- getAllRulesFor f
              let sameRHS = TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    onlyReduceTypes (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ Type -> Term -> Term -> TCMT IO Bool
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Type -> Term -> Term -> m Bool
    pureEqualTerm Type
    a Term
    rhs1 Term
    rhs2
              unlessM (sameRHS `or2M` anyM checkEqualLHS rews) $ addContext gamma $
                warning $ RewriteAmbiguousRules (hd es) rhs1 rhs2

        checkTrianglePropertyForRule :: RewriteRule -> TCM ()
        checkTrianglePropertyForRule :: RewriteRule -> TCM ()
    checkTrianglePropertyForRule (RewriteRule QName
    q Telescope
    gamma QName
    f PElims
    ps Term
    rhs Type
    b Bool
    c TopLevelModuleName
    _) = Telescope -> TCM () -> TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    gamma (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          u  <- NLPat -> TCMT IO Term
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    forall (m :: * -> *). PureTCM m => NLPat -> m Term
    nlPatToTerm (NLPat -> TCMT IO Term) -> NLPat -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ QName -> PElims -> NLPat
    PDef QName
    f PElims
    ps
          -- First element in the list is the "best reduct" @ρ(u)@
          (rhou,vs) <- fromMaybe __IMPOSSIBLE__ . uncons <$> allParallelReductions u
          reportSDoc "rewriting.confluence" 40 $ ("rho(" <> prettyTCM u <> ") =") <+> prettyTCM rhou
          reportSDoc "rewriting.confluence" 40 $ ("S(" <> prettyTCM u <> ") =") <+> prettyList_ (map prettyTCM vs)
          -- If present, last element is always equal to u
          caseMaybe (initLast vs) (return ()) $ \([Term]
    vs',Term
    u') -> do
            Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (Term
    u Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Term
    u') TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            [Term] -> (Term -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Term]
    vs' ((Term -> TCM ()) -> TCM ()) -> (Term -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \Term
    v -> TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (Type -> Term -> Term -> TCMT IO Bool
    checkParallelReductionStep Type
    b Term
    v Term
    rhou) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Term -> Term -> Term -> Warning
    RewriteMissingRule Term
    u Term
    v Term
    rhou

        checkParallelReductionStep :: Type -> Term -> Term -> TCM Bool
        checkParallelReductionStep :: Type -> Term -> Term -> TCMT IO Bool
    checkParallelReductionStep Type
    a Term
    u Term
    w = do
          VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.global" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
            [ TCMT IO Doc
    "Global confluence: checking if" , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u
            , TCMT IO Doc
    "reduces to" , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    w , TCMT IO Doc
    "in one parallel step." ]
          ListT (TCMT IO) Term -> (Term -> TCMT IO Bool) -> TCMT IO Bool
    forall (m :: * -> *) a.
    Monad m =>
    ListT m a -> (a -> m Bool) -> m Bool
    anyListT (Term -> ListT (TCMT IO) Term
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    Term -> m Term
    parReduce Term
    u) ((Term -> TCMT IO Bool) -> TCMT IO Bool)
    -> (Term -> TCMT IO Bool) -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ \Term
    v -> do
            VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.global" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
              [ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u , TCMT IO Doc
    " reduces to " , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
              ]
            eq <- TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    onlyReduceTypes (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ Type -> Term -> Term -> TCMT IO Bool
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Type -> Term -> Term -> m Bool
    pureEqualTerm Type
    a Term
    v Term
    w
            when eq $ reportSDoc "rewriting.confluence.global" 30 $ fsep
              [ "  which is equal to" , prettyTCM w
              ]
            return eq

    sortRulesOfSymbol :: QName -> TCM ()
    sortRulesOfSymbol :: QName -> TCM ()
    sortRulesOfSymbol QName
    f = do
        -- Andreas, 2025-06-28, PR #7934:
        -- By getting all rewrite rules regardless of scope,
        -- we replicate the old (unhygienic) approach to rewrite rule scoping
        -- here to avoid a regression.
        -- See also #7969 for a reason why the code below is questionable.
        rules <- [RewriteRule] -> TCMT IO [RewriteRule]
    forall (m :: * -> *). PureTCM m => [RewriteRule] -> m [RewriteRule]
    sortRules ([RewriteRule] -> TCMT IO [RewriteRule])
    -> TCMT IO [RewriteRule] -> TCMT IO [RewriteRule]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Bool -> QName -> TCMT IO [RewriteRule]
    forall (m :: * -> *).
    (ReadTCState m, MonadTCEnv m) =>
    Bool -> QName -> m [RewriteRule]
    getFilteredRewriteRulesFor Bool
    False QName
    f
        modifySignature $ over sigRewriteRules $ HMap.insert f rules
      where
        sortRules :: PureTCM m => [RewriteRule] -> m [RewriteRule]
        sortRules :: forall (m :: * -> *). PureTCM m => [RewriteRule] -> m [RewriteRule]
    sortRules [RewriteRule]
    rs = do
          ordPairs <- Set (QName, QName) -> Set (QName, QName)
    forall a. Ord a => Set (a, a) -> Set (a, a)
    deleteLoops (Set (QName, QName) -> Set (QName, QName))
    -> ([(RewriteRule, RewriteRule)] -> Set (QName, QName))
    -> [(RewriteRule, RewriteRule)]
    -> Set (QName, QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(QName, QName)] -> Set (QName, QName)
    forall a. Ord a => [a] -> Set a
    Set.fromList ([(QName, QName)] -> Set (QName, QName))
    -> ([(RewriteRule, RewriteRule)] -> [(QName, QName)])
    -> [(RewriteRule, RewriteRule)]
    -> Set (QName, QName)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((RewriteRule, RewriteRule) -> (QName, QName))
    -> [(RewriteRule, RewriteRule)] -> [(QName, QName)]
    forall a b. (a -> b) -> [a] -> [b]
    map (RewriteRule -> QName
    rewName (RewriteRule -> QName)
    -> (RewriteRule -> QName)
    -> (RewriteRule, RewriteRule)
    -> (QName, QName)
    forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** RewriteRule -> QName
    rewName) ([(RewriteRule, RewriteRule)] -> Set (QName, QName))
    -> m [(RewriteRule, RewriteRule)] -> m (Set (QName, QName))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
            ((RewriteRule, RewriteRule) -> m Bool)
    -> [(RewriteRule, RewriteRule)] -> m [(RewriteRule, RewriteRule)]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM ((RewriteRule -> RewriteRule -> m Bool)
    -> (RewriteRule, RewriteRule) -> m Bool
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ((RewriteRule -> RewriteRule -> m Bool)
     -> (RewriteRule, RewriteRule) -> m Bool)
    -> (RewriteRule -> RewriteRule -> m Bool)
    -> (RewriteRule, RewriteRule)
    -> m Bool
    forall a b. (a -> b) -> a -> b
    $ (RewriteRule -> RewriteRule -> m Bool)
    -> RewriteRule -> RewriteRule -> m Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip RewriteRule -> RewriteRule -> m Bool
    forall (m :: * -> *).
    PureTCM m =>
    RewriteRule -> RewriteRule -> m Bool
    moreGeneralLHS) [(RewriteRule
    r1,RewriteRule
    r2) | RewriteRule
    r1 <- [RewriteRule]
    rs, RewriteRule
    r2 <- [RewriteRule]
    rs]
          let perm = Permutation -> Maybe Permutation -> Permutation
    forall a. a -> Maybe a -> a
    fromMaybe Permutation
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Permutation -> Permutation)
    -> Maybe Permutation -> Permutation
    forall a b. (a -> b) -> a -> b
    $
                       (RewriteRule -> RewriteRule -> Bool)
    -> [RewriteRule] -> Maybe Permutation
    forall a. (a -> a -> Bool) -> [a] -> Maybe Permutation
    topoSort (\RewriteRule
    r1 RewriteRule
    r2 -> (RewriteRule -> QName
    rewName RewriteRule
    r1,RewriteRule -> QName
    rewName RewriteRule
    r2) (QName, QName) -> Set (QName, QName) -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set (QName, QName)
    ordPairs) [RewriteRule]
    rs
          reportSDoc "rewriting.confluence.sort" 50 $ "sorted rules: " <+>
            prettyList_ (map (prettyTCM . rewName) $ permute perm rs)
          return $ permute perm rs

        moreGeneralLHS :: PureTCM m => RewriteRule -> RewriteRule -> m Bool
        moreGeneralLHS :: forall (m :: * -> *).
    PureTCM m =>
    RewriteRule -> RewriteRule -> m Bool
    moreGeneralLHS RewriteRule
    r1 RewriteRule
    r2
          | RewriteRule -> RewriteRule -> Bool
    sameRuleName RewriteRule
    r1 RewriteRule
    r2       = Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          | RewriteRule -> QName
    rewHead RewriteRule
    r1 QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    /= RewriteRule -> QName
    rewHead RewriteRule
    r2 = Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          | Bool
    otherwise                = Telescope -> m Bool -> m Bool
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext (RewriteRule -> Telescope
    rewContext RewriteRule
    r2) (m Bool -> m Bool) -> m Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ do
              def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo (QName -> m Definition) -> QName -> m Definition
    forall a b. (a -> b) -> a -> b
    $ RewriteRule -> QName
    rewHead RewriteRule
    r1
              (t, hd) <- makeHead def (rewType r2)
              (vs :: Elims) <- nlPatToTerm $ rewPats r2
              res <- isRight <$> onlyReduceTypes (nonLinMatch (rewContext r1) (t, hd) (rewPats r1) vs)
              when res $ reportSDoc "rewriting.confluence.sort" 55 $
                "the lhs of " <+> prettyTCM (rewName r1) <+>
                "is more general than the lhs of" <+> prettyTCM (rewName r2)
              return res

        deleteLoops :: Ord a => Set (a,a) -> Set (a,a)
        deleteLoops :: forall a. Ord a => Set (a, a) -> Set (a, a)
    deleteLoops Set (a, a)
    xs = ((a, a) -> Bool) -> Set (a, a) -> Set (a, a)
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter (\(a
    x,a
    y) -> Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ (a
    y,a
    x) (a, a) -> Set (a, a) -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set (a, a)
    xs) Set (a, a)
    xs

    makeHead :: PureTCM m => Definition -> Type -> m (Type , Elims -> Term)
    makeHead :: forall (m :: * -> *).
    PureTCM m =>
    Definition -> Type -> m (Type, Elims -> Term)
    makeHead Definition
    def Type
    a = case Definition -> Defn
    theDef Definition
    def of
      Constructor{ conSrcCon :: Defn -> ConHead
    conSrcCon = ConHead
    ch } -> do
        ca <- ((QName, Type, Args), Type) -> Type
    forall a b. (a, b) -> b
    snd (((QName, Type, Args), Type) -> Type)
    -> (Maybe ((QName, Type, Args), Type)
        -> ((QName, Type, Args), Type))
    -> Maybe ((QName, Type, Args), Type)
    -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((QName, Type, Args), Type)
    -> Maybe ((QName, Type, Args), Type) -> ((QName, Type, Args), Type)
    forall a. a -> Maybe a -> a
    fromMaybe ((QName, Type, Args), Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe ((QName, Type, Args), Type) -> Type)
    -> m (Maybe ((QName, Type, Args), Type)) -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    getFullyAppliedConType ConHead
    ch Type
    a
        return (ca , Con ch ConOSystem)
      -- For record projections @f : R Δ → A@, we rely on the invariant
      -- that any clause is fully general in the parameters, i.e. it
      -- is quantified over the parameter telescope @Δ@
      Function { funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right Projection
    proj } -> do
        let f :: QName
    f          = Projection -> QName
    projOrig Projection
    proj
            r :: QName
    r          = Arg QName -> QName
    forall e. Arg e -> e
    unArg (Arg QName -> QName) -> Arg QName -> QName
    forall a b. (a -> b) -> a -> b
    $ Projection -> Arg QName
    projFromType Projection
    proj
        rtype <- 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
    r
        TelV ptel _ <- telView rtype
        n <- getContextSize
        let pars :: Args
            pars = Int -> Args -> Args
    forall a. Subst a => Int -> a -> a
    raise (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    ptel) (Args -> Args) -> Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Args
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Telescope
    ptel
        ftype <- defType def `piApplyM` pars
        return (ftype , Def f)
      Defn
    _ -> (Type, Elims -> Term) -> m (Type, Elims -> Term)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Definition -> Type
    defType Definition
    def , QName -> Elims -> Term
    Def (QName -> Elims -> Term) -> QName -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Definition -> QName
    defName Definition
    def)

    sameRuleName :: RewriteRule -> RewriteRule -> Bool
    sameRuleName :: RewriteRule -> RewriteRule -> Bool
    sameRuleName = QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (QName -> QName -> Bool)
    -> (RewriteRule -> QName) -> RewriteRule -> RewriteRule -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` RewriteRule -> QName
    rewName

    -- | Get both clauses and rewrite rules for the given symbol
    getAllRulesFor :: (HasConstInfo m, ReadTCState m, MonadFresh NameId m) => QName -> m [RewriteRule]
    getAllRulesFor :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getAllRulesFor QName
    f = [RewriteRule] -> [RewriteRule] -> [RewriteRule]
    forall a. [a] -> [a] -> [a]
    (++) ([RewriteRule] -> [RewriteRule] -> [RewriteRule])
    -> m [RewriteRule] -> m ([RewriteRule] -> [RewriteRule])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m [RewriteRule]
    forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
    getRewriteRulesFor QName
    f m ([RewriteRule] -> [RewriteRule])
    -> m [RewriteRule] -> m [RewriteRule]
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> QName -> m [RewriteRule]
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getClausesAsRewriteRules QName
    f

    -- | Build a substitution that replaces all variables in the given
    --   telescope by fresh metavariables.
    makeMetaSubst :: (MonadMetaSolver m) => Telescope -> m Substitution
    makeMetaSubst :: forall (m :: * -> *).
    MonadMetaSolver m =>
    Telescope -> m Substitution
    makeMetaSubst Telescope
    gamma = [Term] -> Substitution
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution)
    -> (Args -> [Term]) -> Args -> Substitution
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Term] -> [Term]
    forall a. [a] -> [a]
    reverse ([Term] -> [Term]) -> (Args -> [Term]) -> Args -> [Term]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Term) -> Args -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg (Args -> Substitution) -> m Args -> m Substitution
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope -> m Args
    forall (m :: * -> *). MonadMetaSolver m => Telescope -> m Args
    newTelMeta Telescope
    gamma

    computingOverlap :: (MonadTCEnv m) => m a -> m a
    computingOverlap :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    computingOverlap = Lens' TCEnv Bool -> (Bool -> Bool) -> m a -> m a
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    eConflComputingOverlap ((Bool -> Bool) -> m a -> m a) -> (Bool -> Bool) -> m a -> m a
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True

    -- | Try to run the TCM action, return @Just x@ if it succeeds with
    --   result @x@ or @Nothing@ if it throws a type error. Abort if there
    --   are any constraints.
    tryUnification :: Term -> Term -> TCM a -> TCM (Maybe a)
    tryUnification :: forall a. Term -> Term -> TCM a -> TCM (Maybe a)
    tryUnification Term
    lhs1 Term
    lhs2 TCM a
    f = TCMT IO (Maybe a) -> TCMT IO (Maybe a)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    computingOverlap (a -> Maybe a
    forall a. a -> Maybe a
    Just (a -> Maybe a) -> TCM a -> TCMT IO (Maybe a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCM a
    f)
      TCMT IO (Maybe a)
    -> (TCErr -> TCMT IO (Maybe a)) -> TCMT IO (Maybe a)
    forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \case
        err :: TCErr
    err@TypeError{} -> do
          VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "Unification failed with error: "
            , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCErr -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
    prettyTCM TCErr
    err
            ]
          Maybe a -> TCMT IO (Maybe a)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing
        TCErr
    err -> TCErr -> TCMT IO (Maybe a)
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err
      TCMT IO (Maybe a)
    -> (Maybe a -> TCMT IO (Maybe a))
    -> (ProblemId -> Maybe a -> TCMT IO (Maybe a))
    -> TCMT IO (Maybe a)
    forall a b.
    TCM a -> (a -> TCM b) -> (ProblemId -> a -> TCM b) -> TCM b
    `ifNoConstraints` Maybe a -> TCMT IO (Maybe a)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((ProblemId -> Maybe a -> TCMT IO (Maybe a)) -> TCMT IO (Maybe a))
    -> (ProblemId -> Maybe a -> TCMT IO (Maybe a)) -> TCMT IO (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ \ProblemId
    pid Maybe a
    _ -> do
        cs <- ProblemId -> TCMT IO Constraints
    forall (m :: * -> *). ReadTCState m => ProblemId -> m Constraints
    getConstraintsForProblem ProblemId
    pid
        prettyCs <- prettyInterestingConstraints cs
        warning $ RewriteMaybeNonConfluent lhs1 lhs2 prettyCs
        return Nothing

    type MonadParallelReduce m =
      ( PureTCM m
      , MonadFresh NameId m
      )

    -- | List all possible single-step parallel reductions of the given term.
    allParallelReductions :: (MonadParallelReduce m, ParallelReduce a) => a -> m [a]
    allParallelReductions :: forall (m :: * -> *) a.
    (MonadParallelReduce m, ParallelReduce a) =>
    a -> m [a]
    allParallelReductions = ListT m a -> m [a]
    forall (m :: * -> *) a. Monad m => ListT m a -> m [a]
    sequenceListT (ListT m a -> m [a]) -> (a -> ListT m a) -> a -> m [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> ListT m a
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    parReduce

    -- | Single-step parallel reduction of a given term.
    --   The monad 'm' can be instantiated in multiple ways:
    --   * Use 'MaybeT TCM' to get the "optimal reduct" obtained by
    --     applying rewrite rules eagerly.
    --   * Use 'ListT TCM' to obtain all possible one-step parallel
    --     reductions.
    class ParallelReduce a where
      parReduce :: (MonadParallelReduce m, MonadPlus m) => a -> m a

      default parReduce
        :: ( MonadParallelReduce m, MonadPlus m
           , Traversable f, a ~ f b, ParallelReduce b)
        => a -> m a
      parReduce = (b -> m b) -> f b -> m (f b)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> f a -> f (f b)
    traverse b -> m b
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    b -> m b
    parReduce

    -- | Compute possible one-step reductions by applying a rewrite rule
    --   at the top-level and reducing all subterms in the position of a
    --   variable of the rewrite rule in parallel.
    topLevelReductions :: (MonadParallelReduce m, MonadPlus m) => (Elims -> Term) -> Elims -> m Term
    topLevelReductions :: forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    (Elims -> Term) -> Elims -> m Term
    topLevelReductions Elims -> Term
    hd Elims
    es = do
      VerboseKey -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.parreduce" Int
    30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "topLevelReductions" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Elims -> Term
    hd Elims
    es)
      -- Get type of head symbol
      (f , t) <- (QName, Type) -> Maybe (QName, Type) -> (QName, Type)
    forall a. a -> Maybe a -> a
    fromMaybe (QName, Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (QName, Type) -> (QName, Type))
    -> m (Maybe (QName, Type)) -> m (QName, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m (Maybe (QName, Type))
    forall (m :: * -> *). PureTCM m => Term -> m (Maybe (QName, Type))
    getTypedHead (Elims -> Term
    hd [])
      reportSDoc "rewriting.parreduce" 60 $ "topLevelReductions: head symbol" <+> prettyTCM (hd []) <+> ":" <+> prettyTCM t
      RewriteRule q gamma _ ps rhs b c _ <- scatterMP (getAllRulesFor f)
      reportSDoc "rewriting.parreduce" 60 $ "topLevelReductions: trying rule" <+> prettyTCM q
      -- Don't reduce if underapplied
      guard $ length es >= length ps
      let (es0 , es1) = splitAt (length ps) es
      onlyReduceTypes (nonLinMatch gamma (t,hd) ps es0) >>= \case
        -- Matching failed: no reduction
        Left Blocked_
    block -> m Term
    forall a. m a
    forall (f :: * -> *) a. Alternative f => f a
    empty
        -- Matching succeeded
        Right Substitution
    sub -> do
          let vs :: [Term]
    vs = (Int -> Term) -> [Int] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Substitution -> Int -> Term
    forall a. EndoSubst a => Substitution' a -> Int -> a
    lookupS Substitution
    sub) ([Int] -> [Term]) -> [Int] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ [Int
    0..(Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    gammaInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1)]
          sub' <- [Term] -> Substitution
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution) -> m [Term] -> m Substitution
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Term] -> m [Term]
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    [Term] -> m [Term]
    parReduce [Term]
    vs
          es1' <- parReduce es1
          let w = (Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    sub' Term
    rhs) Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` Elims
    es1'
          reportSDoc "rewriting.parreduce" 50 $ "topLevelReductions: rewrote" <+> prettyTCM (hd es) <+> "to" <+> prettyTCM w
          return w

    instance ParallelReduce Term where
      parReduce :: forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    Term -> m Term
    parReduce = \case
        -- Interesting cases
        (Def QName
    f Elims
    es) -> ((Elims -> Term) -> Elims -> m Term
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    (Elims -> Term) -> Elims -> m Term
    topLevelReductions (QName -> Elims -> Term
    Def QName
    f) Elims
    es) m Term -> m Term -> m Term
    forall a. m a -> m a -> m a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (QName -> Elims -> Term
    Def QName
    f (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    Elims -> m Elims
    parReduce Elims
    es)
        (Con ConHead
    c ConInfo
    ci Elims
    es) -> ((Elims -> Term) -> Elims -> m Term
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    (Elims -> Term) -> Elims -> m Term
    topLevelReductions (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci) Elims
    es) m Term -> m Term -> m Term
    forall a. m a -> m a -> m a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    Elims -> m Elims
    parReduce Elims
    es)

        -- Congruence cases
        Lam ArgInfo
    i Abs Term
    u  -> ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    i (Abs Term -> Term) -> m (Abs Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Term -> m (Abs Term)
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    Abs Term -> m (Abs Term)
    parReduce Abs Term
    u
        Var Int
    x Elims
    es -> Int -> Elims -> Term
    Var Int
    x (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    Elims -> m Elims
    parReduce Elims
    es
        Pi Dom Type
    a Abs Type
    b   -> Dom Type -> Abs Type -> Term
    Pi    (Dom Type -> Abs Type -> Term)
    -> m (Dom Type) -> m (Abs Type -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type -> m (Dom Type)
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    Dom Type -> m (Dom Type)
    parReduce Dom Type
    a m (Abs Type -> Term) -> m (Abs Type) -> m Term
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Abs Type -> m (Abs Type)
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    Abs Type -> m (Abs Type)
    parReduce Abs Type
    b
        Sort Sort
    s   -> Sort -> Term
    Sort  (Sort -> Term) -> m Sort -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort -> m Sort
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    Sort -> m Sort
    parReduce Sort
    s

        -- Base cases
        u :: Term
    u@Lit{}      -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    u
        u :: Term
    u@Level{}    -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    u -- TODO: is this fine?
        u :: Term
    u@DontCare{} -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    u
        u :: Term
    u@Dummy{}    -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    u -- not __IMPOSSIBLE__ because of presence of Dummy
                                 -- parameters for rewrite rules on constructors.

        -- Impossible cases
        MetaV{}    -> m Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance ParallelReduce Sort where
      parReduce :: forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    Sort -> m Sort
    parReduce = Sort -> m Sort
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure -- TODO: is this fine?

    instance ParallelReduce a => ParallelReduce (Arg a) where
    instance ParallelReduce a => ParallelReduce (Dom a) where
    instance ParallelReduce a => ParallelReduce (Type' a) where
    instance ParallelReduce a => ParallelReduce [a] where

    instance ParallelReduce a => ParallelReduce (Elim' a) where
      parReduce :: forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    Elim' a -> m (Elim' a)
    parReduce (Apply Arg a
    u)  = Arg a -> Elim' a
    forall a. Arg a -> Elim' a
    Apply (Arg a -> Elim' a) -> m (Arg a) -> m (Elim' a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg a -> m (Arg a)
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    Arg a -> m (Arg a)
    parReduce Arg a
    u
      parReduce e :: Elim' a
    e@Proj{}   = Elim' a -> m (Elim' a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Elim' a
    e
      parReduce e :: Elim' a
    e@IApply{} = Elim' a -> m (Elim' a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Elim' a
    e -- TODO

    instance (Free a, Subst a, ParallelReduce a) => ParallelReduce (Abs a) where
      parReduce :: forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    Abs a -> m (Abs a)
    parReduce = Dom Type -> (a -> m a) -> Abs a -> m (Abs a)
    forall a b (m :: * -> *).
    (Subst a, Subst b, MonadAddContext m) =>
    Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
    mapAbstraction Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__ a -> m a
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    parReduce

    -- | Given metavariables ms and some x, construct a telescope Γ and
    --   replace all occurrences of the given metavariables in @x@ by
    --   normal variables from Γ. Returns @Nothing@ if metas have cyclic
    --   dependencies.
    abstractOverMetas :: (MetasToVars a) => [MetaId] -> a -> TCM (Maybe (Telescope, a))
    abstractOverMetas :: forall a.
    MetasToVars a =>
    [MetaId] -> a -> TCM (Maybe (Telescope, a))
    abstractOverMetas [MetaId]
    ms a
    x = do

      -- Sort metas in dependency order
      TCMT IO (Maybe [MetaId])
    -> ([MetaId] -> TCMT IO (Telescope, a))
    -> TCMT IO (Maybe (Telescope, a))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    m (t a) -> (a -> m b) -> m (t b)
    forMM ([MetaId] -> TCMT IO (Maybe [MetaId])
    dependencySortMetas [MetaId]
    ms) (([MetaId] -> TCMT IO (Telescope, a))
     -> TCMT IO (Maybe (Telescope, a)))
    -> ([MetaId] -> TCMT IO (Telescope, a))
    -> TCMT IO (Maybe (Telescope, a))
    forall a b. (a -> b) -> a -> b
    $ \[MetaId]
    ms' -> do

        -- Get types and suggested names of metas
        as <- [MetaId] -> (MetaId -> TCMT IO Type) -> TCMT IO [Type]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [MetaId]
    ms' MetaId -> TCMT IO Type
    forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    getMetaType
        ns <- forM ms' getMetaNameSuggestion

        -- Construct telescope (still containing the metas)
        let n     = [MetaId] -> Int
    forall a. Sized a => a -> Int
    size [MetaId]
    ms'
            gamma = Int -> [VerboseKey] -> [Dom Type] -> Telescope
    unflattenTel' Int
    n [VerboseKey]
    ns ([Dom Type] -> Telescope) -> [Dom Type] -> Telescope
    forall a b. (a -> b) -> a -> b
    $ (Type -> Dom Type) -> [Type] -> [Dom Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Dom Type
    forall a. a -> Dom a
    defaultDom [Type]
    as

        -- Replace metas by variables
        let metaIndex MetaId
    x = (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -) (Int -> Int) -> Maybe Int -> Maybe Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> [MetaId] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    elemIndex MetaId
    x [MetaId]
    ms'
        runReaderT (metasToVars (gamma, x)) metaIndex

    -- | A @OneHole p@ is a @p@ with a subpattern @f ps@ singled out.
    data OneHole a = OneHole
      { forall a. OneHole a -> Telescope
    ohBoundVars :: Telescope     -- Telescope of bound variables at the hole
      , forall a. OneHole a -> Type
    ohType      :: Type          -- Type of the term in the hole
      , forall a. OneHole a -> Term -> a
    ohPlugHole  :: Term -> a     -- Plug the hole with some term
      , forall a. OneHole a -> Elims -> Term
    ohHead      :: Elims -> Term -- The head symbol of the term in the hole
      , forall a. OneHole a -> Elims
    ohElims     :: Elims         -- The eliminations of the term in the hole
      } deriving ((forall a b. (a -> b) -> OneHole a -> OneHole b)
    -> (forall a b. a -> OneHole b -> OneHole a) -> Functor OneHole
    forall a b. a -> OneHole b -> OneHole a
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> OneHole a -> OneHole b
    fmap :: forall a b. (a -> b) -> OneHole a -> OneHole b
    $c<$ :: forall a b. a -> OneHole b -> OneHole a
    <$ :: forall a b. a -> OneHole b -> OneHole a
    Functor)

    ohHeadName :: OneHole a -> QName
    ohHeadName :: forall a. OneHole a -> QName
    ohHeadName OneHole a
    oh = case OneHole a -> Elims -> Term
    forall a. OneHole a -> Elims -> Term
    ohHead OneHole a
    oh [] of
      Def QName
    f Elims
    _   -> QName
    f
      Con ConHead
    c ConInfo
    _ Elims
    _ -> ConHead -> QName
    conName ConHead
    c
      Term
    _         -> QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    ohContents :: OneHole a -> Term
    ohContents :: forall a. OneHole a -> Term
    ohContents OneHole a
    oh = OneHole a -> Elims -> Term
    forall a. OneHole a -> Elims -> Term
    ohHead OneHole a
    oh (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ OneHole a -> Elims
    forall a. OneHole a -> Elims
    ohElims OneHole a
    oh

    -- | The trivial hole
    idHole :: Type -> Term -> OneHole Term
    idHole :: Type -> Term -> OneHole Term
    idHole Type
    a = \case
      Def QName
    f Elims
    es    -> Telescope
    -> Type
    -> (Term -> Term)
    -> (Elims -> Term)
    -> Elims
    -> OneHole Term
    forall a.
    Telescope
    -> Type -> (Term -> a) -> (Elims -> Term) -> Elims -> OneHole a
    OneHole Telescope
    forall a. Tele a
    EmptyTel Type
    a Term -> Term
    forall a. a -> a
    id (QName -> Elims -> Term
    Def QName
    f) Elims
    es
      Con ConHead
    c ConInfo
    ci Elims
    es -> Telescope
    -> Type
    -> (Term -> Term)
    -> (Elims -> Term)
    -> Elims
    -> OneHole Term
    forall a.
    Telescope
    -> Type -> (Term -> a) -> (Elims -> Term) -> Elims -> OneHole a
    OneHole Telescope
    forall a. Tele a
    EmptyTel Type
    a Term -> Term
    forall a. a -> a
    id (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci) Elims
    es
      Term
    _           -> OneHole Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Plug a hole with another hole
    composeHole :: OneHole Term -> OneHole a -> OneHole a
    composeHole :: forall a. OneHole Term -> OneHole a -> OneHole a
    composeHole OneHole Term
    inner OneHole a
    outer = OneHole
      { ohBoundVars :: Telescope
    ohBoundVars = OneHole a -> Telescope
    forall a. OneHole a -> Telescope
    ohBoundVars OneHole a
    outer Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` OneHole Term -> Telescope
    forall a. OneHole a -> Telescope
    ohBoundVars OneHole Term
    inner
      , ohType :: Type
    ohType      = OneHole Term -> Type
    forall a. OneHole a -> Type
    ohType OneHole Term
    inner
      , ohPlugHole :: Term -> a
    ohPlugHole  = OneHole a -> Term -> a
    forall a. OneHole a -> Term -> a
    ohPlugHole OneHole a
    outer (Term -> a) -> (Term -> Term) -> Term -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OneHole Term -> Term -> Term
    forall a. OneHole a -> Term -> a
    ohPlugHole OneHole Term
    inner
      , ohHead :: Elims -> Term
    ohHead      = OneHole Term -> Elims -> Term
    forall a. OneHole a -> Elims -> Term
    ohHead OneHole Term
    inner
      , ohElims :: Elims
    ohElims     = OneHole Term -> Elims
    forall a. OneHole a -> Elims
    ohElims OneHole Term
    inner
      }

    ohAddBV :: ArgName -> Dom Type -> OneHole a -> OneHole a
    ohAddBV :: forall a. VerboseKey -> Dom Type -> OneHole a -> OneHole a
    ohAddBV VerboseKey
    x Dom Type
    a OneHole a
    oh = OneHole a
    oh { ohBoundVars = ExtendTel a $ Abs x $ ohBoundVars oh }

    -- | Given a @p : a@, @allHoles p@ lists all the possible
    --   decompositions @p = p'[(f ps)/x]@.
    class (TermSubst p, Free p) => AllHoles p where
      allHoles :: (Alternative m, PureTCM m) => TypeOf p -> p -> m (OneHole p)

    allHoles_
      :: ( Alternative m , PureTCM m , AllHoles p , TypeOf p ~ () )
      => p -> m (OneHole p)
    allHoles_ :: forall (m :: * -> *) p.
    (Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ = TypeOf p -> p -> m (OneHole p)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    TypeOf p -> p -> m (OneHole p)
    forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf p -> p -> m (OneHole p)
    allHoles ()

    allHolesList
      :: ( PureTCM m , AllHoles p)
      => TypeOf p -> p -> m [OneHole p]
    allHolesList :: forall (m :: * -> *) p.
    (PureTCM m, AllHoles p) =>
    TypeOf p -> p -> m [OneHole p]
    allHolesList TypeOf p
    a = ListT m (OneHole p) -> m [OneHole p]
    forall (m :: * -> *) a. Monad m => ListT m a -> m [a]
    sequenceListT (ListT m (OneHole p) -> m [OneHole p])
    -> (p -> ListT m (OneHole p)) -> p -> m [OneHole p]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TypeOf p -> p -> ListT m (OneHole p)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    TypeOf p -> p -> m (OneHole p)
    forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf p -> p -> m (OneHole p)
    allHoles TypeOf p
    a

    -- | Given a term @v : a@ and eliminations @es@, force eta-expansion
    --   of @v@ to match the structure (Apply/Proj) of the eliminations.
    --
    --   Examples:
    --
    --   1. @v : _A@ and @es = [$ w]@: this will instantiate
    --      @_A := (x : _A1) → _A2@ and return the @OneHole Term@
    --      @λ x → [v x]@.
    --
    --   2. @v : _A@ and @es = [.fst]@: this will instantiate
    --      @_A := _A1 × _A2@ and return the @OneHole Term@
    --      @([v .fst]) , (v .snd)@.
    forceEtaExpansion :: Type -> Term -> [Elim' a] -> TCM (OneHole Term)
    forceEtaExpansion :: forall a. Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
    forceEtaExpansion Type
    a Term
    v [] = OneHole Term -> TCMT IO (OneHole Term)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (OneHole Term -> TCMT IO (OneHole Term))
    -> OneHole Term -> TCMT IO (OneHole Term)
    forall a b. (a -> b) -> a -> b
    $ Type -> Term -> OneHole Term
    idHole Type
    a Term
    v
    forceEtaExpansion Type
    a Term
    v (Elim' a
    e:[Elim' a]
    es) = case Elim' a
    e of

      Apply (Arg ArgInfo
    i a
    w) -> do

        -- Force a to be a pi type
        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.eta" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
          [ TCMT IO Doc
    "Forcing" , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v , TCMT IO Doc
    ":" , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a , TCMT IO Doc
    "to take one more argument" ]
        dom <- ArgInfo -> Type -> Dom Type
    forall a. ArgInfo -> a -> Dom a
    defaultArgDom ArgInfo
    i (Type -> Dom Type) -> TCMT IO Type -> TCMT IO (Dom Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Type
    newTypeMeta_
        cod <- addContext dom $ newTypeMeta_
        equalType a $ mkPi (("x",) <$> dom) cod

        -- Construct body of eta-expansion
        let body = Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    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 (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    0]

        -- Continue with remaining eliminations
        addContext dom $ ohAddBV "x" dom . fmap (Lam i . mkAbs "x") <$>
          forceEtaExpansion cod body es

      Proj ProjOrigin
    o QName
    f -> do

        -- Force a to be the right record type for projection by f
        VerboseKey -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.eta" Int
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
          [ TCMT IO Doc
    "Forcing" , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v , TCMT IO Doc
    ":" , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a , TCMT IO Doc
    "to be projectible by" , QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    f ]
        r <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> TCMT IO (Maybe QName) -> TCMT IO QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO (Maybe QName)
    getRecordOfField QName
    f
        Defn{ defType = ra, theDef = RecordDefn rdef } <- getConstInfo r
        pars <- newArgsMeta ra
        s <- ra `piApplyM` pars >>= \Type
    s -> Type -> (Sort -> TCMT IO Sort) -> TCMT IO Sort -> TCMT IO Sort
    forall (m :: * -> *) a.
    (MonadReduce m, MonadBlock m) =>
    Type -> (Sort -> m a) -> m a -> m a
    ifIsSort Type
    s Sort -> TCMT IO Sort
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TCMT IO Sort
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        equalType a $ El s (Def r $ map Apply pars)

        -- Eta-expand v at record type r, and get field corresponding to f
        (_ , c , ci , fields) <- etaExpandRecord_ r pars rdef v
        let fs        = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom QName -> Arg QName
    forall t a. Dom' t a -> Arg a
    argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
    forall a b. (a -> b) -> a -> b
    $ RecordData -> [Dom QName]
    _recFields RecordData
    rdef
            i         = Int -> Maybe Int -> Int
    forall a. a -> Maybe a -> a
    fromMaybe Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
    forall a b. (a -> b) -> a -> b
    $ QName -> [QName] -> Maybe Int
    forall a. Eq a => a -> [a] -> Maybe Int
    elemIndex QName
    f ([QName] -> Maybe Int) -> [QName] -> Maybe Int
    forall a b. (a -> b) -> a -> b
    $ (Arg QName -> QName) -> [Arg QName] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg QName -> QName
    forall e. Arg e -> e
    unArg [Arg QName]
    fs
            fContent  = Arg Term -> Term
    forall e. Arg e -> e
    unArg (Arg Term -> Term) -> Arg Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Maybe (Arg Term) -> Arg Term
    forall a. a -> Maybe a -> a
    fromMaybe Arg Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (Arg Term) -> Arg Term) -> Maybe (Arg Term) -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Args
    fields Args -> Int -> Maybe (Arg Term)
    forall a. [a] -> Int -> Maybe a
    !!! Int
    i
            fUpdate Term
    w = ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Args -> Elims) -> Args -> Elims
    forall a b. (a -> b) -> a -> b
    $ Int -> (Arg Term -> Arg Term) -> Args -> Args
    forall a. Int -> (a -> a) -> [a] -> [a]
    updateAt Int
    i (Term
    w Term -> Arg Term -> Arg Term
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) Args
    fields

        -- Get type of field corresponding to f
        ~(Just (El _ (Pi b c))) <- getDefType f =<< reduce a
        let fa = Abs Type
    c Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    v

        -- Continue with remaining eliminations
        fmap fUpdate <$> forceEtaExpansion fa fContent es

      IApply{} -> TCMT IO (OneHole Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- Not yet implemented

    -- Instances for @AllHoles@

    instance AllHoles p => AllHoles (Arg p) where
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf (Arg p) -> Arg p -> m (OneHole (Arg p))
    allHoles TypeOf (Arg p)
    a Arg p
    x = (p -> Arg p) -> OneHole p -> OneHole (Arg p)
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Arg p
    x Arg p -> p -> Arg p
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $>) (OneHole p -> OneHole (Arg p))
    -> m (OneHole p) -> m (OneHole (Arg p))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TypeOf p -> p -> m (OneHole p)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    TypeOf p -> p -> m (OneHole p)
    forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf p -> p -> m (OneHole p)
    allHoles (Dom' Term (TypeOf p) -> TypeOf p
    forall t e. Dom' t e -> e
    unDom TypeOf (Arg p)
    Dom' Term (TypeOf p)
    a) (Arg p -> p
    forall e. Arg e -> e
    unArg Arg p
    x)

    instance AllHoles p => AllHoles (Dom p) where
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf (Dom p) -> Dom p -> m (OneHole (Dom p))
    allHoles TypeOf (Dom p)
    a Dom p
    x = (p -> Dom p) -> OneHole p -> OneHole (Dom p)
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Dom p
    x Dom p -> p -> Dom p
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $>) (OneHole p -> OneHole (Dom p))
    -> m (OneHole p) -> m (OneHole (Dom p))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TypeOf p -> p -> m (OneHole p)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    TypeOf p -> p -> m (OneHole p)
    forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf p -> p -> m (OneHole p)
    allHoles TypeOf p
    TypeOf (Dom p)
    a (Dom p -> p
    forall t e. Dom' t e -> e
    unDom Dom p
    x)

    instance AllHoles (Abs Term) where
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf (Abs Term) -> Abs Term -> m (OneHole (Abs Term))
    allHoles (Dom Type
    dom , Abs Type
    a) Abs Term
    x = (VerboseKey, Dom Type)
    -> m (OneHole (Abs Term)) -> m (OneHole (Abs Term))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (VerboseKey, Dom Type) -> m a -> m a
    addContext (Abs Term -> VerboseKey
    forall a. Abs a -> VerboseKey
    absName Abs Term
    x , Dom Type
    dom) (m (OneHole (Abs Term)) -> m (OneHole (Abs Term)))
    -> m (OneHole (Abs Term)) -> m (OneHole (Abs Term))
    forall a b. (a -> b) -> a -> b
    $
        VerboseKey -> Dom Type -> OneHole (Abs Term) -> OneHole (Abs Term)
    forall a. VerboseKey -> Dom Type -> OneHole a -> OneHole a
    ohAddBV (Abs Type -> VerboseKey
    forall a. Abs a -> VerboseKey
    absName Abs Type
    a) Dom Type
    dom (OneHole (Abs Term) -> OneHole (Abs Term))
    -> (OneHole Term -> OneHole (Abs Term))
    -> OneHole Term
    -> OneHole (Abs Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> Abs Term) -> OneHole Term -> OneHole (Abs Term)
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (VerboseKey -> Term -> Abs Term
    forall a. (Subst a, Free a) => VerboseKey -> a -> Abs a
    mkAbs (VerboseKey -> Term -> Abs Term) -> VerboseKey -> Term -> Abs Term
    forall a b. (a -> b) -> a -> b
    $ Abs Term -> VerboseKey
    forall a. Abs a -> VerboseKey
    absName Abs Term
    x) (OneHole Term -> OneHole (Abs Term))
    -> m (OneHole Term) -> m (OneHole (Abs Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
          TypeOf Term -> Term -> m (OneHole Term)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    TypeOf p -> p -> m (OneHole p)
    forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf Term -> Term -> m (OneHole Term)
    allHoles (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    a) (Abs Term -> Term
    forall a. Subst a => Abs a -> a
    absBody Abs Term
    x)

    instance AllHoles (Abs Type) where
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf (Abs Type) -> Abs Type -> m (OneHole (Abs Type))
    allHoles TypeOf (Abs Type)
    dom Abs Type
    a = (VerboseKey, Dom Type)
    -> m (OneHole (Abs Type)) -> m (OneHole (Abs Type))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    (VerboseKey, Dom Type) -> m a -> m a
    addContext (Abs Type -> VerboseKey
    forall a. Abs a -> VerboseKey
    absName Abs Type
    a , TypeOf (Abs Type)
    Dom Type
    dom) (m (OneHole (Abs Type)) -> m (OneHole (Abs Type)))
    -> m (OneHole (Abs Type)) -> m (OneHole (Abs Type))
    forall a b. (a -> b) -> a -> b
    $
        VerboseKey -> Dom Type -> OneHole (Abs Type) -> OneHole (Abs Type)
    forall a. VerboseKey -> Dom Type -> OneHole a -> OneHole a
    ohAddBV (Abs Type -> VerboseKey
    forall a. Abs a -> VerboseKey
    absName Abs Type
    a) TypeOf (Abs Type)
    Dom Type
    dom (OneHole (Abs Type) -> OneHole (Abs Type))
    -> (OneHole Type -> OneHole (Abs Type))
    -> OneHole Type
    -> OneHole (Abs Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Type -> Abs Type) -> OneHole Type -> OneHole (Abs Type)
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (VerboseKey -> Type -> Abs Type
    forall a. (Subst a, Free a) => VerboseKey -> a -> Abs a
    mkAbs (VerboseKey -> Type -> Abs Type) -> VerboseKey -> Type -> Abs Type
    forall a b. (a -> b) -> a -> b
    $ Abs Type -> VerboseKey
    forall a. Abs a -> VerboseKey
    absName Abs Type
    a) (OneHole Type -> OneHole (Abs Type))
    -> m (OneHole Type) -> m (OneHole (Abs Type))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
          Type -> m (OneHole Type)
    forall (m :: * -> *) p.
    (Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    a)

    instance AllHoles Elims where
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf Elims -> Elims -> m (OneHole Elims)
    allHoles (Type
    a,Elims -> Term
    hd) [] = m (OneHole Elims)
    forall a. m a
    forall (f :: * -> *) a. Alternative f => f a
    empty
      allHoles (Type
    a,Elims -> Term
    hd) (Elim' Term
    e:Elims
    es) = do
        VerboseKey -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.hole" Int
    65 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
          [ TCMT IO Doc
    "Head symbol" , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Elims -> Term
    hd []) , TCMT IO Doc
    ":" , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a
          , TCMT IO Doc
    "is eliminated by" , Elim' Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Elim' Term -> m Doc
    prettyTCM Elim' Term
    e
          ]
        case Elim' Term
    e of
          Apply Arg Term
    x -> do
            ~(Pi b c) <- Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> m Type -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    a
            let a'  = Abs Type
    c Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    x
                hd' = Elims -> Term
    hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Elim' Term
    eElim' Term -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :)
            (fmap ((:es) . Apply) <$> allHoles b x)
             <|> (fmap (e:) <$> allHoles (a' , hd') es)
          Proj ProjOrigin
    o QName
    f -> do
            ~(Just (El _ (Pi b c))) <- QName -> Type -> m (Maybe Type)
    forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
    getDefType QName
    f (Type -> m (Maybe Type)) -> m Type -> m (Maybe Type)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    a
            let a' = Abs Type
    c Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Elims -> Term
    hd []
            hd' <- applyE <$> applyDef o f (argFromDom b $> hd [])
            fmap (e:) <$> allHoles (a' , hd') es
          IApply Term
    x Term
    y Term
    u -> m (OneHole Elims)
    forall a. m a
    forall (f :: * -> *) a. Alternative f => f a
    empty -- TODO: support --confluence-check + --cubical

    instance AllHoles Type where
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf Type -> Type -> m (OneHole Type)
    allHoles TypeOf Type
    _ (El Sort
    s Term
    a) = m (OneHole Type) -> m (OneHole Type)
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    workOnTypes (m (OneHole Type) -> m (OneHole Type))
    -> m (OneHole Type) -> m (OneHole Type)
    forall a b. (a -> b) -> a -> b
    $
        (Term -> Type) -> OneHole Term -> OneHole Type
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s) (OneHole Term -> OneHole Type)
    -> m (OneHole Term) -> m (OneHole Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TypeOf Term -> Term -> m (OneHole Term)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    TypeOf p -> p -> m (OneHole p)
    forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf Term -> Term -> m (OneHole Term)
    allHoles (Sort -> Type
    sort Sort
    s) Term
    a

    instance AllHoles Term where
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf Term -> Term -> m (OneHole Term)
    allHoles TypeOf Term
    a Term
    u = do
        VerboseKey -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Int -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.hole" Int
    60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep
          [ TCMT IO Doc
    "Getting holes of term" , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u , TCMT IO Doc
    ":" , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM TypeOf Term
    Type
    a ]
        case Term
    u of
          Var Int
    i Elims
    es       -> do
            ai <- Int -> m Type
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
    typeOfBV Int
    i
            fmap (Var i) <$> allHoles (ai , Var i) es
          Lam ArgInfo
    i Abs Term
    u        -> do
            ~(Pi b c) <- Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> m Type -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce TypeOf Term
    Type
    a
            fmap (Lam i) <$> allHoles (b,c) u
          Lit Literal
    l          -> m (OneHole Term)
    forall a. m a
    forall (f :: * -> *) a. Alternative f => f a
    empty
          v :: Term
    v@(Def QName
    f Elims
    es)   -> do
            fa <- 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
    f
            pure (idHole a v)
             <|> (fmap (Def f) <$> allHoles (fa , Def f) es)
          v :: Term
    v@(Con ConHead
    c ConInfo
    ci Elims
    es) -> do
            ca <- ((QName, Type, Args), Type) -> Type
    forall a b. (a, b) -> b
    snd (((QName, Type, Args), Type) -> Type)
    -> (Maybe ((QName, Type, Args), Type)
        -> ((QName, Type, Args), Type))
    -> Maybe ((QName, Type, Args), Type)
    -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((QName, Type, Args), Type)
    -> Maybe ((QName, Type, Args), Type) -> ((QName, Type, Args), Type)
    forall a. a -> Maybe a -> a
    fromMaybe ((QName, Type, Args), Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe ((QName, Type, Args), Type) -> Type)
    -> m (Maybe ((QName, Type, Args), Type)) -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
              ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    getFullyAppliedConType ConHead
    c (Type -> m (Maybe ((QName, Type, Args), Type)))
    -> m Type -> m (Maybe ((QName, Type, Args), Type))
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce TypeOf Term
    Type
    a
            pure (idHole a v)
             <|> (fmap (Con c ci) <$> allHoles (ca , Con c ci) es)
          Pi Dom Type
    a Abs Type
    b         ->
            ((Dom Type -> Term) -> OneHole (Dom Type) -> OneHole Term
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\Dom Type
    a -> Dom Type -> Abs Type -> Term
    Pi Dom Type
    a Abs Type
    b) (OneHole (Dom Type) -> OneHole Term)
    -> m (OneHole (Dom Type)) -> m (OneHole Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type -> m (OneHole (Dom Type))
    forall (m :: * -> *) p.
    (Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ Dom Type
    a) m (OneHole Term) -> m (OneHole Term) -> m (OneHole Term)
    forall a. m a -> m a -> m a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|>
            ((Abs Type -> Term) -> OneHole (Abs Type) -> OneHole Term
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\Abs Type
    b -> Dom Type -> Abs Type -> Term
    Pi Dom Type
    a Abs Type
    b) (OneHole (Abs Type) -> OneHole Term)
    -> m (OneHole (Abs Type)) -> m (OneHole Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TypeOf (Abs Type) -> Abs Type -> m (OneHole (Abs Type))
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    TypeOf p -> p -> m (OneHole p)
    forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf (Abs Type) -> Abs Type -> m (OneHole (Abs Type))
    allHoles TypeOf (Abs Type)
    Dom Type
    a Abs Type
    b)
          Sort Sort
    s         -> (Sort -> Term) -> OneHole Sort -> OneHole Term
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Sort -> Term
    Sort (OneHole Sort -> OneHole Term)
    -> m (OneHole Sort) -> m (OneHole Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort -> m (OneHole Sort)
    forall (m :: * -> *) p.
    (Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ Sort
    s
          Level Level
    l        -> (Level -> Term) -> OneHole Level -> OneHole Term
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Level -> Term
    Level (OneHole Level -> OneHole Term)
    -> m (OneHole Level) -> m (OneHole Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Level -> m (OneHole Level)
    forall (m :: * -> *) p.
    (Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ Level
    l
          MetaV{}        -> m (OneHole Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          DontCare{}     -> m (OneHole Term)
    forall a. m a
    forall (f :: * -> *) a. Alternative f => f a
    empty
          Dummy{}        -> m (OneHole Term)
    forall a. m a
    forall (f :: * -> *) a. Alternative f => f a
    empty

    instance AllHoles Sort where
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf Sort -> Sort -> m (OneHole Sort)
    allHoles TypeOf Sort
    _ = \case
        Univ Univ
    u Level
    l     -> (Level -> Sort) -> OneHole Level -> OneHole Sort
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Univ -> Level -> Sort
    forall t. Univ -> Level' t -> Sort' t
    Univ Univ
    u) (OneHole Level -> OneHole Sort)
    -> m (OneHole Level) -> m (OneHole Sort)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Level -> m (OneHole Level)
    forall (m :: * -> *) p.
    (Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ Level
    l
        Inf Univ
    _ Integer
    _      -> m (OneHole Sort)
    forall a. m a
    forall (f :: * -> *) a. Alternative f => f a
    empty
        Sort
    SizeUniv     -> m (OneHole Sort)
    forall a. m a
    forall (f :: * -> *) a. Alternative f => f a
    empty
        Sort
    LockUniv     -> m (OneHole Sort)
    forall a. m a
    forall (f :: * -> *) a. Alternative f => f a
    empty
        Sort
    LevelUniv    -> m (OneHole Sort)
    forall a. m a
    forall (f :: * -> *) a. Alternative f => f a
    empty
        Sort
    IntervalUniv -> m (OneHole Sort)
    forall a. m a
    forall (f :: * -> *) a. Alternative f => f a
    empty
        PiSort{}     -> m (OneHole Sort)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        FunSort{}    -> m (OneHole Sort)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        UnivSort{}   -> m (OneHole Sort)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        MetaS{}      -> m (OneHole Sort)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        DefS QName
    f Elims
    es    -> do
          fa <- 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
    f
          fmap (DefS f) <$> allHoles (fa , Def f) es
        DummyS{}     -> m (OneHole Sort)
    forall a. m a
    forall (f :: * -> *) a. Alternative f => f a
    empty

    instance AllHoles Level where
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf Level -> Level -> m (OneHole Level)
    allHoles TypeOf Level
    _ (Max Integer
    n [PlusLevel' Term]
    ls) = ([PlusLevel' Term] -> Level)
    -> OneHole [PlusLevel' Term] -> OneHole Level
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    n) (OneHole [PlusLevel' Term] -> OneHole Level)
    -> m (OneHole [PlusLevel' Term]) -> m (OneHole Level)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [PlusLevel' Term] -> m (OneHole [PlusLevel' Term])
    forall (m :: * -> *) p.
    (Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ [PlusLevel' Term]
    ls

    instance AllHoles [PlusLevel] where
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf [PlusLevel' Term]
    -> [PlusLevel' Term] -> m (OneHole [PlusLevel' Term])
    allHoles TypeOf [PlusLevel' Term]
    _ []     = m (OneHole [PlusLevel' Term])
    forall a. m a
    forall (f :: * -> *) a. Alternative f => f a
    empty
      allHoles TypeOf [PlusLevel' Term]
    _ (PlusLevel' Term
    l:[PlusLevel' Term]
    ls) =
        ((PlusLevel' Term -> [PlusLevel' Term])
    -> OneHole (PlusLevel' Term) -> OneHole [PlusLevel' Term]
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (PlusLevel' Term -> [PlusLevel' Term] -> [PlusLevel' Term]
    forall a. a -> [a] -> [a]
    :[PlusLevel' Term]
    ls) (OneHole (PlusLevel' Term) -> OneHole [PlusLevel' Term])
    -> m (OneHole (PlusLevel' Term)) -> m (OneHole [PlusLevel' Term])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PlusLevel' Term -> m (OneHole (PlusLevel' Term))
    forall (m :: * -> *) p.
    (Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ PlusLevel' Term
    l)
        m (OneHole [PlusLevel' Term])
    -> m (OneHole [PlusLevel' Term]) -> m (OneHole [PlusLevel' Term])
    forall a. m a -> m a -> m a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (([PlusLevel' Term] -> [PlusLevel' Term])
    -> OneHole [PlusLevel' Term] -> OneHole [PlusLevel' Term]
    forall a b. (a -> b) -> OneHole a -> OneHole b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (PlusLevel' Term
    lPlusLevel' Term -> [PlusLevel' Term] -> [PlusLevel' Term]
    forall a. a -> [a] -> [a]
    :) (OneHole [PlusLevel' Term] -> OneHole [PlusLevel' Term])
    -> m (OneHole [PlusLevel' Term]) -> m (OneHole [PlusLevel' Term])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [PlusLevel' Term] -> m (OneHole [PlusLevel' Term])
    forall (m :: * -> *) p.
    (Alternative m, PureTCM m, AllHoles p, TypeOf p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ [PlusLevel' Term]
    ls)

    instance AllHoles PlusLevel where
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    TypeOf (PlusLevel' Term)
    -> PlusLevel' Term -> m (OneHole (PlusLevel' Term))
    allHoles TypeOf (PlusLevel' Term)
    _ (Plus Integer
    n Term
    l) = do
        la <- m Type
    forall (m :: * -> *). HasBuiltins m => m Type
    levelType'
        fmap (Plus n) <$> allHoles la l

    -- | Convert metavariables to normal variables. Warning: doesn't
    --   convert sort metas.
    class MetasToVars a where
      metasToVars
        :: (MonadReader (MetaId -> Maybe Nat) m , HasBuiltins m)
        => a -> m a

      default metasToVars
        :: ( MetasToVars a', Traversable f, a ~ f a'
           , MonadReader (MetaId -> Maybe Nat) m , HasBuiltins m)
        => a -> m a
      metasToVars = (a' -> m a') -> f a' -> m (f a')
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> f a -> f (f b)
    traverse a' -> m a'
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    a' -> m a'
    metasToVars

    instance MetasToVars a => MetasToVars [a] where
    instance MetasToVars a => MetasToVars (Arg a) where
    instance MetasToVars a => MetasToVars (Dom a) where
    instance MetasToVars a => MetasToVars (Elim' a) where

    instance MetasToVars a => MetasToVars (Abs a) where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Abs a -> m (Abs a)
    metasToVars (Abs   VerboseKey
    i a
    x) = VerboseKey -> a -> Abs a
    forall a. VerboseKey -> a -> Abs a
    Abs VerboseKey
    i   (a -> Abs a) -> m a -> m (Abs a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((MetaId -> Maybe Int) -> MetaId -> Maybe Int) -> m a -> m a
    forall a.
    ((MetaId -> Maybe Int) -> MetaId -> Maybe Int) -> m a -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((Int -> Int) -> Maybe Int -> Maybe Int
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Int -> Int
    forall a. Enum a => a -> a
    succ (Maybe Int -> Maybe Int)
    -> (MetaId -> Maybe Int) -> MetaId -> Maybe Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .) (a -> m a
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    a -> m a
    metasToVars a
    x)
      metasToVars (NoAbs VerboseKey
    i a
    x) = VerboseKey -> a -> Abs a
    forall a. VerboseKey -> a -> Abs a
    NoAbs VerboseKey
    i (a -> Abs a) -> m a -> m (Abs a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m a
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    a -> m a
    metasToVars a
    x

    instance MetasToVars Term where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Term -> m Term
    metasToVars = \case
        Var Int
    i Elims
    es   -> Int -> Elims -> Term
    Var Int
    i    (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Elims -> m Elims
    metasToVars Elims
    es
        Lam ArgInfo
    i Abs Term
    u    -> ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    i    (Abs Term -> Term) -> m (Abs Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Abs Term -> m (Abs Term)
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Abs Term -> m (Abs Term)
    metasToVars Abs Term
    u
        Lit Literal
    l      -> Term -> m Term
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Literal -> Term
    Lit Literal
    l)
        Def QName
    f Elims
    es   -> QName -> Elims -> Term
    Def QName
    f    (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Elims -> m Elims
    metasToVars Elims
    es
        Con ConHead
    c ConInfo
    i Elims
    es -> ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    i  (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Elims -> m Elims
    metasToVars Elims
    es
        Pi Dom Type
    a Abs Type
    b     -> Dom Type -> Abs Type -> Term
    Pi       (Dom Type -> Abs Type -> Term)
    -> m (Dom Type) -> m (Abs Type -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type -> m (Dom Type)
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Dom Type -> m (Dom Type)
    metasToVars Dom Type
    a m (Abs Type -> Term) -> m (Abs Type) -> m Term
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Abs Type -> m (Abs Type)
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Abs Type -> m (Abs Type)
    metasToVars Abs Type
    b
        Sort Sort
    s     -> Sort -> Term
    Sort     (Sort -> Term) -> m Sort -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort -> m Sort
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Sort -> m Sort
    metasToVars Sort
    s
        Level Level
    l    -> Level -> Term
    Level    (Level -> Term) -> m Level -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Level -> m Level
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Level -> m Level
    metasToVars Level
    l
        MetaV MetaId
    x Elims
    es -> ((MetaId -> Maybe Int) -> Maybe Int) -> m (Maybe Int)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks ((MetaId -> Maybe Int) -> MetaId -> Maybe Int
    forall a b. (a -> b) -> a -> b
    $ MetaId
    x) m (Maybe Int) -> (Maybe Int -> m Term) -> m Term
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Just Int
    i   -> Int -> Elims -> Term
    Var Int
    i    (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Elims -> m Elims
    metasToVars Elims
    es
          Maybe Int
    Nothing  -> MetaId -> Elims -> Term
    MetaV MetaId
    x  (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Elims -> m Elims
    metasToVars Elims
    es
        DontCare Term
    u -> Term -> Term
    DontCare (Term -> Term) -> m Term -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m Term
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Term -> m Term
    metasToVars Term
    u
        Dummy VerboseKey
    s Elims
    es -> VerboseKey -> Elims -> Term
    Dummy VerboseKey
    s  (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Elims -> m Elims
    metasToVars Elims
    es

    instance MetasToVars Type where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Type -> m Type
    metasToVars (El Sort
    s Term
    t) = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Sort -> Term -> Type) -> m Sort -> m (Term -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort -> m Sort
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Sort -> m Sort
    metasToVars Sort
    s m (Term -> Type) -> m Term -> m Type
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m Term
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Term -> m Term
    metasToVars Term
    t

    instance MetasToVars Sort where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Sort -> m Sort
    metasToVars = \case
        Univ Univ
    u Level
    l   -> Univ -> Level -> Sort
    forall t. Univ -> Level' t -> Sort' t
    Univ Univ
    u (Level -> Sort) -> m Level -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Level -> m Level
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Level -> m Level
    metasToVars Level
    l
        Inf Univ
    u Integer
    n    -> Sort -> m Sort
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf Univ
    u Integer
    n
        Sort
    SizeUniv   -> Sort -> m Sort
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    forall t. Sort' t
    SizeUniv
        Sort
    LockUniv   -> Sort -> m Sort
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    forall t. Sort' t
    LockUniv
        Sort
    LevelUniv  -> Sort -> m Sort
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    forall t. Sort' t
    LevelUniv
        Sort
    IntervalUniv -> Sort -> m Sort
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    forall t. Sort' t
    IntervalUniv
        PiSort Dom' Term Term
    s Sort
    t Abs Sort
    u -> Dom' Term Term -> Sort -> Abs Sort -> Sort
    forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
    PiSort   (Dom' Term Term -> Sort -> Abs Sort -> Sort)
    -> m (Dom' Term Term) -> m (Sort -> Abs Sort -> Sort)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom' Term Term -> m (Dom' Term Term)
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Dom' Term Term -> m (Dom' Term Term)
    metasToVars Dom' Term Term
    s m (Sort -> Abs Sort -> Sort) -> m Sort -> m (Abs Sort -> Sort)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Sort -> m Sort
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Sort -> m Sort
    metasToVars Sort
    t m (Abs Sort -> Sort) -> m (Abs Sort) -> m Sort
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Abs Sort -> m (Abs Sort)
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Abs Sort -> m (Abs Sort)
    metasToVars Abs Sort
    u
        FunSort Sort
    s Sort
    t -> Sort -> Sort -> Sort
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort (Sort -> Sort -> Sort) -> m Sort -> m (Sort -> Sort)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort -> m Sort
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Sort -> m Sort
    metasToVars Sort
    s m (Sort -> Sort) -> m Sort -> m Sort
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Sort -> m Sort
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Sort -> m Sort
    metasToVars Sort
    t
        UnivSort Sort
    s -> Sort -> Sort
    forall t. Sort' t -> Sort' t
    UnivSort (Sort -> Sort) -> m Sort -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Sort -> m Sort
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Sort -> m Sort
    metasToVars Sort
    s
        MetaS MetaId
    x Elims
    es -> MetaId -> Elims -> Sort
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x  (Elims -> Sort) -> m Elims -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Elims -> m Elims
    metasToVars Elims
    es
        DefS QName
    f Elims
    es  -> QName -> Elims -> Sort
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    f   (Elims -> Sort) -> m Elims -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Elims -> m Elims
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Elims -> m Elims
    metasToVars Elims
    es
        DummyS VerboseKey
    s   -> Sort -> m Sort
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> Sort
    forall t. VerboseKey -> Sort' t
    DummyS VerboseKey
    s

    instance MetasToVars Level where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Level -> m Level
    metasToVars (Max Integer
    n [PlusLevel' Term]
    ls) = Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    n ([PlusLevel' Term] -> Level) -> m [PlusLevel' Term] -> m Level
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [PlusLevel' Term] -> m [PlusLevel' Term]
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    [PlusLevel' Term] -> m [PlusLevel' Term]
    metasToVars [PlusLevel' Term]
    ls

    instance MetasToVars PlusLevel where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    PlusLevel' Term -> m (PlusLevel' Term)
    metasToVars (Plus Integer
    n Term
    x) = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    n (Term -> PlusLevel' Term) -> m Term -> m (PlusLevel' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m Term
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Term -> m Term
    metasToVars Term
    x

    instance MetasToVars a => MetasToVars (Tele a) where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Tele a -> m (Tele a)
    metasToVars Tele a
    EmptyTel = Tele a -> m (Tele a)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Tele a
    forall a. Tele a
    EmptyTel
      metasToVars (ExtendTel a
    a Abs (Tele a)
    tel) = a -> Abs (Tele a) -> Tele a
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (a -> Abs (Tele a) -> Tele a) -> m a -> m (Abs (Tele a) -> Tele a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m a
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    a -> m a
    metasToVars a
    a m (Abs (Tele a) -> Tele a) -> m (Abs (Tele a)) -> m (Tele a)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Abs (Tele a) -> m (Abs (Tele a))
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    Abs (Tele a) -> m (Abs (Tele a))
    metasToVars Abs (Tele a)
    tel

    instance (MetasToVars a, MetasToVars b) => MetasToVars (a,b) where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    (a, b) -> m (a, b)
    metasToVars (a
    x,b
    y) = (,) (a -> b -> (a, b)) -> m a -> m (b -> (a, b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m a
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    a -> m a
    metasToVars a
    x m (b -> (a, b)) -> m b -> m (a, b)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> m b
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    b -> m b
    metasToVars b
    y

    instance (MetasToVars a, MetasToVars b, MetasToVars c) => MetasToVars (a,b,c) where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    (a, b, c) -> m (a, b, c)
    metasToVars (a
    x,b
    y,c
    z) = (,,) (a -> b -> c -> (a, b, c)) -> m a -> m (b -> c -> (a, b, c))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m a
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    a -> m a
    metasToVars a
    x m (b -> c -> (a, b, c)) -> m b -> m (c -> (a, b, c))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> m b
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    b -> m b
    metasToVars b
    y m (c -> (a, b, c)) -> m c -> m (a, b, c)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> c -> m c
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    c -> m c
    metasToVars c
    z

    instance (MetasToVars a, MetasToVars b, MetasToVars c, MetasToVars d) => MetasToVars (a,b,c,d) where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    (a, b, c, d) -> m (a, b, c, d)
    metasToVars (a
    x,b
    y,c
    z,d
    w) = (,,,) (a -> b -> c -> d -> (a, b, c, d))
    -> m a -> m (b -> c -> d -> (a, b, c, d))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> m a
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    a -> m a
    metasToVars a
    x m (b -> c -> d -> (a, b, c, d))
    -> m b -> m (c -> d -> (a, b, c, d))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> m b
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    b -> m b
    metasToVars b
    y m (c -> d -> (a, b, c, d)) -> m c -> m (d -> (a, b, c, d))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> c -> m c
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    c -> m c
    metasToVars c
    z m (d -> (a, b, c, d)) -> m d -> m (a, b, c, d)
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> d -> m d
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Int) m,
     HasBuiltins m) =>
    a -> m a
    forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Int) m, HasBuiltins m) =>
    d -> m d
    metasToVars d
    w