    {-# LANGUAGE ScopedTypeVariables #-}
    {-# 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' ↦ v'@ where @ps@ and @ps'@ can be
    --    unified@.
    --
    -- 2. Subpatterns @g qs@ of @ps@ and rewrite rules @g qs' ↦ w@ where
    --    @qs@ and @qs'@ can be unified.
    --
    -- Each of these leads to a *critical pair* @v₁ <-- u --> 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
    import Control.Monad.Except
    import Control.Monad.Reader

    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 ( workOnTypes , 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.Applicative
    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
      [RewriteRule]
    rews <- QName -> TCMT IO [RewriteRule]
    forall (m :: * -> *).
    (HasConstInfo m, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getClausesAsRewriteRules QName
    f
      let matchables :: [[QName]]
    matchables = (RewriteRule -> [QName]) -> [RewriteRule] -> [[QName]]
    forall a b. (a -> b) -> [a] -> [b]
    map RewriteRule -> [QName]
    forall a. GetMatchables a => a -> [QName]
    getMatchables [RewriteRule]
    rews
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "Function" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "has matchable symbols" 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_ (([QName] -> TCMT IO Doc) -> [[QName]] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map [QName] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [[QName]]
    matchables)
      (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> [QName] -> Signature -> Signature
    setMatchableSymbols QName
    f ([QName] -> Signature -> Signature)
    -> [QName] -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ [[QName]] -> [QName]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[QName]]
    matchables
      let hasRules :: QName -> f Bool
    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 (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
      [(RewriteRule, [QName])]
    -> ((RewriteRule, [QName]) -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ ([RewriteRule] -> [[QName]] -> [(RewriteRule, [QName])]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [RewriteRule]
    rews [[QName]]
    matchables) (((RewriteRule, [QName]) -> TCM ()) -> TCM ())
    -> ((RewriteRule, [QName]) -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \(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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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
        [QName]
    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)
    traverse RewriteRule -> TCMT IO (Set QName)
    forall {f :: * -> *}.
    HasConstInfo f =>
    RewriteRule -> f (Set QName)
    getSymbols [RewriteRule]
    rews
        [QName] -> (QName -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [QName]
    allSymbols ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \QName
    f -> do
          [RewriteRule]
    rewsf <- QName -> TCMT IO [RewriteRule]
    forall (m :: * -> *).
    (HasConstInfo m, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getAllRulesFor QName
    f
          [RewriteRule] -> (RewriteRule -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [RewriteRule]
    rewsf ((RewriteRule -> TCM ()) -> TCM ())
    -> (RewriteRule -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \RewriteRule
    rew -> do
            VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.triangle" Nat
    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
    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 (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 -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    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
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    rew)
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    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
    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
      Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
      (Type
    fa , Elims -> Term
    hdf) <- Telescope
    -> TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term))
    -> TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term)
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type -> TCMT IO (Type, Elims -> Term)
    forall (m :: * -> *).
    PureTCM m =>
    Definition -> Type -> m (Type, Elims -> Term)
    makeHead Definition
    def (RewriteRule -> Type
    rewType RewriteRule
    rew)

      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "Head symbol" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Elims -> Term
    hdf []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "of rewrite rule has type" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    fa

      -- Step 1: check other rewrite rules that overlap at top position
      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, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getAllRulesFor QName
    f) ((RewriteRule -> TCM ()) -> TCM ())
    -> (RewriteRule -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ RewriteRule
    rew' -> do
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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'
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Finished step 1 of confluence check 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
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    rew)

      -- Step 2: check other rewrite rules that overlap with a subpattern
      -- of this rewrite rule
      Elims
    es <- PElims -> TCMT IO Elims
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    nlPatToTerm PElims
    qs
      TCMT IO [OneHole Elims] -> (OneHole Elims -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, Monad m) =>
    m (t a) -> (a -> m ()) -> m ()
    forMM_ (Telescope -> TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims]
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims])
    -> TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims]
    forall a b. (a -> b) -> a -> b
    $ PType Elims -> Elims -> TCMT IO [OneHole Elims]
    forall (m :: * -> *) p.
    (PureTCM m, AllHoles p) =>
    PType p -> p -> m [OneHole p]
    allHolesList (Type
    fa, Elims -> Term
    hdf) Elims
    es) ((OneHole Elims -> TCM ()) -> TCM ())
    -> (OneHole Elims -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ 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 -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    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
    prettyTCM QName
    g
        [RewriteRule]
    rews' <- QName -> TCMT IO [RewriteRule]
    forall (m :: * -> *).
    (HasConstInfo m, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getAllRulesFor QName
    g
        [RewriteRule] -> (RewriteRule -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [RewriteRule]
    rews' ((RewriteRule -> TCM ()) -> TCM ())
    -> (RewriteRule -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \RewriteRule
    rew' -> do
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Finished step 2 of confluence check 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
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    rew)

      -- Step 3: check other rewrite rules that have a subpattern which
      -- overlaps with this rewrite rule
      Set QName -> (QName -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ (Definition -> Set QName
    defMatchable Definition
    def) ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    g -> do
        VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    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
    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
    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, 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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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
            Elims
    es' <- PElims -> TCMT IO Elims
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    nlPatToTerm (RewriteRule -> PElims
    rewPats RewriteRule
    rew')
            let tel' :: Telescope
    tel' = RewriteRule -> Telescope
    rewContext RewriteRule
    rew'
            Definition
    def' <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    g
            (Type
    ga , Elims -> Term
    hdg) <- Telescope
    -> TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel' (TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term))
    -> TCMT IO (Type, Elims -> Term) -> TCMT IO (Type, Elims -> Term)
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type -> TCMT IO (Type, Elims -> Term)
    forall (m :: * -> *).
    PureTCM m =>
    Definition -> Type -> m (Type, Elims -> Term)
    makeHead Definition
    def' (RewriteRule -> Type
    rewType RewriteRule
    rew')
            TCMT IO [OneHole Elims] -> (OneHole Elims -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, Monad m) =>
    m (t a) -> (a -> m ()) -> m ()
    forMM_ (Telescope -> TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims]
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel' (TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims])
    -> TCMT IO [OneHole Elims] -> TCMT IO [OneHole Elims]
    forall a b. (a -> b) -> a -> b
    $ PType Elims -> Elims -> TCMT IO [OneHole Elims]
    forall (m :: * -> *) p.
    (PureTCM m, AllHoles p) =>
    PType p -> p -> m [OneHole p]
    allHolesList (Type
    ga , Elims -> Term
    hdg) Elims
    es') ((OneHole Elims -> TCM ()) -> TCM ())
    -> (OneHole Elims -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ OneHole Elims
    hole -> do
              let f' :: QName
    f' = OneHole Elims -> QName
    forall a. OneHole a -> QName
    ohHeadName OneHole Elims
    hole
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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
      VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Finished step 3 of confluence check 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
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    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 (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

            Substitution
    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
            Substitution
    sub2 <- 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
    rew2

            let f :: QName
    f    = RewriteRule -> QName
    rewHead RewriteRule
    rew1 -- == rewHead rew2
                a1 :: Type
    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 :: Type
    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

            Elims
    es1 <- Substitution' (SubstArg Elims) -> Elims -> Elims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Elims)
    sub1 (Elims -> Elims) -> TCMT IO Elims -> TCMT IO Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PElims -> TCMT IO Elims
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    nlPatToTerm (RewriteRule -> PElims
    rewPats RewriteRule
    rew1)
            Elims
    es2 <- Substitution' (SubstArg Elims) -> Elims -> Elims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Elims)
    sub2 (Elims -> Elims) -> TCMT IO Elims -> TCMT IO Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PElims -> TCMT IO Elims
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    nlPatToTerm (RewriteRule -> PElims
    rewPats RewriteRule
    rew2)

            VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    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
    vcat
              [ TCMT IO Doc
    "checkConfluenceTop" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (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
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    rew2)
              , TCMT IO Doc
    "  f    = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f
              , TCMT IO Doc
    "  ctx1 = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (RewriteRule -> Telescope
    rewContext RewriteRule
    rew1)
              , TCMT IO Doc
    "  ctx2 = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (RewriteRule -> Telescope
    rewContext RewriteRule
    rew2)
              , TCMT IO Doc
    "  es1  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Elims -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Elims
    es1
              , TCMT IO Doc
    "  es2  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Elims -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Elims
    es2
              ]

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

                lhs1 :: Term
    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 :: Term
    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 :: Type
    a | Elims -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Elims
    es1r = Type
    a2
                  | Bool
    otherwise = Type
    a1

            VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    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
    sep
              [ TCMT IO Doc
    "Considering potential critical pair at top-level: "
              , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Term -> TCMT IO Doc) -> Term -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term
    lhs1, TCMT IO Doc
    " =?= "
              , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Term -> TCMT IO Doc) -> Term -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term
    lhs2 , TCMT IO Doc
    " : " , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a
              ]

            Maybe (Term, Term)
    maybeCriticalPair <- Term -> Term -> TCM (Term, Term) -> TCM (Maybe (Term, Term))
    forall a. Term -> Term -> TCM a -> TCM (Maybe a)
    tryUnification Term
    lhs1 Term
    lhs2 (TCM (Term, Term) -> TCM (Maybe (Term, Term)))
    -> TCM (Term, Term) -> TCM (Maybe (Term, Term))
    forall a b. (a -> b) -> a -> b
    $ do
              -- Unify the left-hand sides of both rewrite rules
              Type
    fa   <- Definition -> Type
    defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
              [Polarity]
    fpol <- Comparison -> QName -> TCMT IO [Polarity]
    forall (m :: * -> *).
    HasConstInfo m =>
    Comparison -> QName -> m [Polarity]
    getPolarity' Comparison
    CmpEq QName
    f
              TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    onlyReduceTypes (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                [Polarity]
    -> [IsForced] -> Type -> Term -> Elims -> Elims -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    [Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
    compareElims [Polarity]
    fpol [] Type
    fa (Elims -> Term
    hd []) Elims
    es1' Elims
    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 :: Term
    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 :: Term
    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

              (Term, Term) -> TCM (Term, Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term
    rhs1 , Term
    rhs2)

            Maybe (Term, Term) -> ((Term, Term) -> TCM ()) -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust Maybe (Term, Term)
    maybeCriticalPair (((Term, Term) -> TCM ()) -> TCM ())
    -> ((Term, Term) -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Term -> Term -> TCM ()) -> (Term, Term) -> TCM ()
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (Type -> (Elims -> Term) -> Elims -> Term -> Term -> TCM ()
    checkCriticalPair Type
    a Elims -> Term
    hd (Elims
    es1' Elims -> Elims -> Elims
    forall a. [a] -> [a] -> [a]
    ++ Elims
    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 -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    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
    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
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    rew2)
          Call -> TCM () -> TCM ()
    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 -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    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
    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
    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"

            Substitution
    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 :: Telescope
    bvTel0     = OneHole Elims -> Telescope
    forall a. OneHole a -> Telescope
    ohBoundVars OneHole Elims
    hole0
                k :: Nat
    k          = Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    bvTel0
                b0 :: Type
    b0         = Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Nat -> Substitution -> Substitution
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    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 :: QName
    g          = OneHole Elims -> QName
    forall a. OneHole a -> QName
    ohHeadName OneHole Elims
    hole0
                es0 :: Elims
    es0        = Substitution' (SubstArg Elims) -> Elims -> Elims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Nat -> Substitution -> Substitution
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    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 :: PElims
    qs2        = RewriteRule -> PElims
    rewPats RewriteRule
    rew2

            -- 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.
            OneHole Term
    hole1 <- Telescope -> TCMT IO (OneHole Term) -> TCMT IO (OneHole Term)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    bvTel0 (TCMT IO (OneHole Term) -> TCMT IO (OneHole Term))
    -> TCMT IO (OneHole Term) -> TCMT IO (OneHole Term)
    forall a b. (a -> b) -> a -> b
    $
              Type -> Term -> PElims -> TCMT IO (OneHole Term)
    forall a. Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
    forceEtaExpansion Type
    b0 (Elims -> Term
    hdg Elims
    es0) (PElims -> TCMT IO (OneHole Term))
    -> PElims -> TCMT IO (OneHole Term)
    forall a b. (a -> b) -> a -> b
    $ Nat -> PElims -> PElims
    forall a. Nat -> [a] -> [a]
    drop (Elims -> Nat
    forall a. Sized a => a -> Nat
    size Elims
    es0) PElims
    qs2

            VerboseKey -> Nat -> TCM () -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> m () -> m ()
    verboseS VerboseKey
    "rewriting.confluence.eta" Nat
    30 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Elims -> Nat
    forall a. Sized a => a -> Nat
    size Elims
    es0 Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == PElims -> Nat
    forall a. Sized a => a -> Nat
    size PElims
    qs2) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              Telescope -> TCM () -> TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    bvTel0 (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.eta" Nat
    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
    vcat
                [ TCMT IO Doc
    "forceEtaExpansion result:"
                , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "bound vars: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (OneHole Term -> Telescope
    forall a. OneHole a -> Telescope
    ohBoundVars OneHole Term
    hole1)
                , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "hole contents: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (OneHole Term -> Telescope
    forall a. OneHole a -> Telescope
    ohBoundVars OneHole Term
    hole1) (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Term -> TCMT IO Doc) -> Term -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ OneHole Term -> Term
    forall a. OneHole a -> Term
    ohContents OneHole Term
    hole1)
                ]

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

            Substitution
    sub2 <- Telescope -> TCMT IO Substitution -> TCMT IO Substitution
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    bvTel (TCMT IO Substitution -> TCMT IO Substitution)
    -> TCMT IO Substitution -> TCMT IO Substitution
    forall a b. (a -> b) -> a -> b
    $ 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
    rew2

            let es1 :: Elims
    es1 = Substitution' (SubstArg Elims) -> Elims -> Elims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Nat -> Substitution -> Substitution
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS (Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    bvTel) Substitution
    sub1) Elims
    es'
            Elims
    es2 <- Substitution' (SubstArg Elims) -> Elims -> Elims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Elims)
    sub2 (Elims -> Elims) -> TCMT IO Elims -> TCMT IO Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PElims -> TCMT IO Elims
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    nlPatToTerm (RewriteRule -> PElims
    rewPats RewriteRule
    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.
            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Elims -> Nat
    forall a. Sized a => a -> Nat
    size Elims
    es1 Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Elims -> Nat
    forall a. Sized a => a -> Nat
    size Elims
    es2) TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            let n :: Nat
    n = Elims -> Nat
    forall a. Sized a => a -> Nat
    size Elims
    es2
                (Elims
    es1' , Elims
    es1r) = Nat -> Elims -> (Elims, Elims)
    forall a. Nat -> [a] -> ([a], [a])
    splitAt Nat
    n Elims
    es1

            let lhs1 :: Term
    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 :: Term
    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 :: Type
    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

            VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    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
    sep
              [ TCMT IO Doc
    "Considering potential critical pair at subpattern: "
              , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Term -> TCMT IO Doc) -> Term -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term
    lhs1 , TCMT IO Doc
    " =?= "
              , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Term -> TCMT IO Doc) -> Term -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term
    lhs2 , TCMT IO Doc
    " : " , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a
              ]

            Maybe (Term, Term)
    maybeCriticalPair <- Term -> Term -> TCM (Term, Term) -> TCM (Maybe (Term, Term))
    forall a. Term -> Term -> TCM a -> TCM (Maybe a)
    tryUnification Term
    lhs1 Term
    lhs2 (TCM (Term, Term) -> TCM (Maybe (Term, Term)))
    -> TCM (Term, Term) -> TCM (Maybe (Term, Term))
    forall a b. (a -> b) -> a -> b
    $ do
              -- Unify the subpattern of the first rewrite rule with the lhs
              -- of the second one
              Type
    ga   <- Definition -> Type
    defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    g
              [Polarity]
    gpol <- Comparison -> QName -> TCMT IO [Polarity]
    forall (m :: * -> *).
    HasConstInfo m =>
    Comparison -> QName -> m [Polarity]
    getPolarity' Comparison
    CmpEq QName
    g
              TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    onlyReduceTypes (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCM () -> TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    bvTel (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                [Polarity]
    -> [IsForced] -> Type -> Term -> Elims -> Elims -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    [Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
    compareElims [Polarity]
    gpol [] Type
    ga (Elims -> Term
    hdg []) Elims
    es1' Elims
    es2

              -- Right-hand side of first rewrite rule (after unification)
              let rhs1 :: Term
    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 :: Term
    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
              VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    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
    sep
                [ TCMT IO Doc
    "Plugging hole with w = "
                , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    bvTel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    w
                ]
              let rhs2 :: Term
    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

              (Term, Term) -> TCM (Term, Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term
    rhs1 , Term
    rhs2)

            Maybe (Term, Term) -> ((Term, Term) -> TCM ()) -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust Maybe (Term, Term)
    maybeCriticalPair (((Term, Term) -> TCM ()) -> TCM ())
    -> ((Term, Term) -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (Term -> Term -> TCM ()) -> (Term, Term) -> TCM ()
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (Type -> (Elims -> Term) -> Elims -> Term -> Term -> TCM ()
    checkCriticalPair Type
    a Elims -> Term
    hdf (Substitution' (SubstArg Elims) -> Elims -> Elims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Elims)
    sub1 (Elims -> Elims) -> Elims -> Elims
    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))

        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

          (Type
    a,Elims
    es,Term
    rhs1,Term
    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 :: [MetaId]
    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 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)

          VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    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
    sep
            [ TCMT IO Doc
    "Abstracting over metas: "
            , [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((MetaId -> TCMT IO Doc) -> [MetaId] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (VerboseKey -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
    text (VerboseKey -> TCMT IO Doc)
    -> (MetaId -> VerboseKey) -> MetaId -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MetaId -> VerboseKey
    forall a. Show a => a -> VerboseKey
    show) [MetaId]
    ms)
            ]
          (Telescope
    gamma , (Type
    a,Elims
    es,Term
    rhs1,Term
    rhs2)) <- (Telescope, (Type, Elims, Term, Term))
    -> Maybe (Telescope, (Type, Elims, Term, Term))
    -> (Telescope, (Type, Elims, Term, Term))
    forall a. a -> Maybe a -> a
    fromMaybe (Telescope, (Type, Elims, Term, Term))
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (Telescope, (Type, Elims, Term, Term))
     -> (Telescope, (Type, Elims, Term, Term)))
    -> TCMT IO (Maybe (Telescope, (Type, Elims, Term, Term)))
    -> TCMT IO (Telescope, (Type, Elims, Term, Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
            [MetaId]
    -> (Type, Elims, Term, Term)
    -> TCMT IO (Maybe (Telescope, (Type, Elims, Term, Term)))
    forall a.
    MetasToVars a =>
    [MetaId] -> a -> TCM (Maybe (Telescope, a))
    abstractOverMetas [MetaId]
    ms (Type
    a,Elims
    es,Term
    rhs1,Term
    rhs2)

          Telescope -> TCM () -> TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    gamma (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    10 (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
    sep
            [ TCMT IO Doc
    "Found critical pair: "
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Elims -> Term
    hd Elims
    es)
            , TCMT IO Doc
    " ---> " , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    rhs1
            , TCMT IO Doc
    " =?= " , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    rhs2
            , TCMT IO Doc
    " : " , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a ]
          VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            Telescope
    gamma <- Telescope -> TCMT IO Telescope
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Telescope
    gamma
            [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "Context of critical pair: "
                , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    gamma ]

          Telescope -> TCM () -> TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    gamma (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ case ConfluenceCheck
    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 e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \case
                TypeError CallStack
    _ TCState
    s Closure TypeError
    err -> do
                  Doc
    prettyErr <- (TCState -> TCState) -> TCMT IO Doc -> TCMT IO Doc
    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
    prettyTCM Closure TypeError
    err
                  Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Term -> Term -> Term -> Doc -> Warning
    RewriteNonConfluent (Elims -> Term
    hd Elims
    es) Term
    rhs1 Term
    rhs2 Doc
    prettyErr
                TCErr
    err           -> TCErr -> TCM ()
    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
              (QName
    f, Type
    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 -> TCMT IO Bool
    checkEqualLHS (RewriteRule QName
    q Telescope
    delta QName
    _ PElims
    ps Term
    _ Type
    _ Bool
    _) = do
                    TCMT IO (Either Blocked_ Substitution)
    -> TCMT IO (Either Blocked_ Substitution)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    onlyReduceTypes (Telescope
    -> (Type, Elims -> Term)
    -> PElims
    -> Elims
    -> TCMT IO (Either Blocked_ Substitution)
    forall (m :: * -> *) t a b.
    (PureTCM m, Match t a b) =>
    Telescope -> t -> 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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                      Left Blocked_
    _    -> Bool -> TCMT IO Bool
    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
    $ (Nat -> Term) -> [Nat] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Nat -> Term
    var ([Nat] -> [Term]) -> [Nat] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom (Nat -> [Nat]) -> Nat -> [Nat]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Nat
    forall a. Sized a => a -> Nat
    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 -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.global" Nat
    35 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                          Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    prettyTCM QName
    q 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
    prettyTCM [Term]
    us)
                        Bool
    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
                        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    ok (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.global" Nat
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                          TCMT IO Doc
    "It is equal to the LHS of rewrite 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
    prettyTCM QName
    q
                        Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    ok
                  allDistinctVars :: [(Term,Dom Type)] -> TCM Bool
                  allDistinctVars :: [(Term, Dom Type)] -> TCMT IO Bool
    allDistinctVars [(Term, Dom Type)]
    us = do
                    [(Term, Dom Type)]
    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
                    [Maybe Nat]
    mis <- ((Term, Dom Type) -> TCMT IO (Maybe Nat))
    -> [(Term, Dom Type)] -> TCMT IO [Maybe Nat]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (\(Term
    u,Dom Type
    a) -> Term -> Type -> TCMT IO (Maybe Nat)
    forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Nat)
    isEtaVar Term
    u (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a)) ([(Term, Dom Type)] -> TCMT IO [Maybe Nat])
    -> [(Term, Dom Type)] -> TCMT IO [Maybe Nat]
    forall a b. (a -> b) -> a -> b
    $ [(Term, Dom Type)]
    us'
                    case [Maybe Nat] -> Maybe [Nat]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence [Maybe Nat]
    mis of
                      Just [Nat]
    is -> Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ [Nat] -> Bool
    forall a. Ord a => [a] -> Bool
    fastDistinct [Nat]
    is
                      Maybe [Nat]
    Nothing -> Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

              [RewriteRule]
    rews <- QName -> TCMT IO [RewriteRule]
    forall (m :: * -> *).
    (HasConstInfo m, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getAllRulesFor QName
    f
              let sameRHS :: TCMT IO Bool
    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
              TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (TCMT IO Bool
    sameRHS TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M` [RewriteRule] -> (RewriteRule -> TCMT IO Bool) -> TCMT IO Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Functor f, Foldable f, Monad m) =>
    f a -> (a -> m Bool) -> m Bool
    anyM [RewriteRule]
    rews RewriteRule -> TCMT IO Bool
    checkEqualLHS) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCM () -> TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    gamma (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
    RewriteAmbiguousRules (Elims -> Term
    hd Elims
    es) Term
    rhs1 Term
    rhs2

        checkTrianglePropertyForRule :: RewriteRule -> TCM ()
        checkTrianglePropertyForRule :: RewriteRule -> TCM ()
    checkTrianglePropertyForRule (RewriteRule QName
    q Telescope
    gamma QName
    f PElims
    ps Term
    rhs Type
    b Bool
    c) = Telescope -> TCM () -> TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    gamma (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          Term
    u  <- NLPat -> TCMT IO Term
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    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)@
          (Term
    rhou,[Term]
    vs) <- (Term, [Term]) -> Maybe (Term, [Term]) -> (Term, [Term])
    forall a. a -> Maybe a -> a
    fromMaybe (Term, [Term])
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (Term, [Term]) -> (Term, [Term]))
    -> ([Term] -> Maybe (Term, [Term])) -> [Term] -> (Term, [Term])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Term] -> Maybe (Term, [Term])
    forall a. [a] -> Maybe (a, [a])
    uncons ([Term] -> (Term, [Term]))
    -> TCMT IO [Term] -> TCMT IO (Term, [Term])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> TCMT IO [Term]
    forall (m :: * -> *) a.
    (MonadParallelReduce m, ParallelReduce a) =>
    a -> m [a]
    allParallelReductions Term
    u
          VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (TCMT IO Doc
    "rho(" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    u TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> TCMT IO Doc
    ") =") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    rhou
          VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (TCMT IO Doc
    "S(" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    u TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> TCMT IO Doc
    ") =") 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
    prettyTCM [Term]
    vs)
          -- If present, last element is always equal to u
          Maybe ([Term], Term)
    -> TCM () -> (([Term], Term) -> TCM ()) -> TCM ()
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe ([Term] -> Maybe ([Term], Term)
    forall a. [a] -> Maybe ([a], a)
    initLast [Term]
    vs) (() -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) ((([Term], Term) -> TCM ()) -> TCM ())
    -> (([Term], Term) -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \([Term]
    vs',Term
    u') -> do
            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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 -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.global" Nat
    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
    prettyTCM Term
    u
            , TCMT IO Doc
    "reduces to" , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    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 -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.global" Nat
    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
    prettyTCM Term
    u , TCMT IO Doc
    " reduces to " , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    v
              ]
            Bool
    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
            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    eq (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.global" Nat
    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
    "  which is equal to" , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    w
              ]
            Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    eq

    sortRulesOfSymbol :: QName -> TCM ()
    sortRulesOfSymbol :: QName -> TCM ()
    sortRulesOfSymbol QName
    f = do
        [RewriteRule]
    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
    =<< QName -> TCMT IO [RewriteRule]
    forall (m :: * -> *). HasConstInfo m => QName -> m [RewriteRule]
    getRewriteRulesFor QName
    f
        (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Lens' (HashMap QName [RewriteRule]) Signature
    -> LensMap (HashMap QName [RewriteRule]) Signature
    forall i o. Lens' i o -> LensMap i o
    over Lens' (HashMap QName [RewriteRule]) Signature
    sigRewriteRules LensMap (HashMap QName [RewriteRule]) Signature
    -> LensMap (HashMap QName [RewriteRule]) Signature
    forall a b. (a -> b) -> a -> b
    $ QName
    -> [RewriteRule]
    -> HashMap QName [RewriteRule]
    -> HashMap QName [RewriteRule]
    forall k v.
    (Eq k, Hashable k) =>
    k -> v -> HashMap k v -> HashMap k v
    HMap.insert QName
    f [RewriteRule]
    rules
      where
        sortRules :: PureTCM m => [RewriteRule] -> m [RewriteRule]
        sortRules :: forall (m :: * -> *). PureTCM m => [RewriteRule] -> m [RewriteRule]
    sortRules [RewriteRule]
    rs = do
          Set (QName, QName)
    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 (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
    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
          VerboseKey -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.sort" Nat
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "sorted rules: " 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_ ((RewriteRule -> TCMT IO Doc) -> [RewriteRule] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (QName -> TCMT IO Doc)
    -> (RewriteRule -> QName) -> RewriteRule -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RewriteRule -> QName
    rewName) ([RewriteRule] -> [TCMT IO Doc]) -> [RewriteRule] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ Permutation -> [RewriteRule] -> [RewriteRule]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    perm [RewriteRule]
    rs)
          [RewriteRule] -> m [RewriteRule]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([RewriteRule] -> m [RewriteRule])
    -> [RewriteRule] -> m [RewriteRule]
    forall a b. (a -> b) -> a -> b
    $ Permutation -> [RewriteRule] -> [RewriteRule]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    perm [RewriteRule]
    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 (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 (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
    addContext (RewriteRule -> Telescope
    rewContext RewriteRule
    r2) (m Bool -> m Bool) -> m Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ do
              Definition
    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
              (Type
    t, Elims -> Term
    hd) <- Definition -> Type -> m (Type, Elims -> Term)
    forall (m :: * -> *).
    PureTCM m =>
    Definition -> Type -> m (Type, Elims -> Term)
    makeHead Definition
    def (RewriteRule -> Type
    rewType RewriteRule
    r2)
              (Elims
    vs :: Elims) <- PElims -> m Elims
    forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
    nlPatToTerm (PElims -> m Elims) -> PElims -> m Elims
    forall a b. (a -> b) -> a -> b
    $ RewriteRule -> PElims
    rewPats RewriteRule
    r2
              Bool
    res <- Either Blocked_ Substitution -> Bool
    forall a b. Either a b -> Bool
    isRight (Either Blocked_ Substitution -> Bool)
    -> m (Either Blocked_ Substitution) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (Either Blocked_ Substitution)
    -> m (Either Blocked_ Substitution)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    onlyReduceTypes (Telescope
    -> (Type, Elims -> Term)
    -> PElims
    -> Elims
    -> m (Either Blocked_ Substitution)
    forall (m :: * -> *) t a b.
    (PureTCM m, Match t a b) =>
    Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
    nonLinMatch (RewriteRule -> Telescope
    rewContext RewriteRule
    r1) (Type
    t, Elims -> Term
    hd) (RewriteRule -> PElims
    rewPats RewriteRule
    r1) Elims
    vs)
              Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    res (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.sort" Nat
    55 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
                TCMT IO Doc
    "the lhs of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    r1) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                TCMT IO Doc
    "is more general than the lhs of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (RewriteRule -> QName
    rewName RewriteRule
    r2)
              Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    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
        Type
    ca <- ((QName, Type, [Arg Term]), Type) -> Type
    forall a b. (a, b) -> b
    snd (((QName, Type, [Arg Term]), Type) -> Type)
    -> (Maybe ((QName, Type, [Arg Term]), Type)
        -> ((QName, Type, [Arg Term]), Type))
    -> Maybe ((QName, Type, [Arg Term]), Type)
    -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((QName, Type, [Arg Term]), Type)
    -> Maybe ((QName, Type, [Arg Term]), Type)
    -> ((QName, Type, [Arg Term]), Type)
    forall a. a -> Maybe a -> a
    fromMaybe ((QName, Type, [Arg Term]), Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe ((QName, Type, [Arg Term]), Type) -> Type)
    -> m (Maybe ((QName, Type, [Arg Term]), Type)) -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ConHead -> Type -> m (Maybe ((QName, Type, [Arg Term]), Type))
    forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, [Arg Term]), Type))
    getFullyAppliedConType ConHead
    ch Type
    a
        (Type, Elims -> Term) -> m (Type, Elims -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type
    ca , ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    ch ConInfo
    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 -> Maybe Projection
    funProjection = Just 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
        Type
    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 Telescope
    ptel Type
    _ <- Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    rtype
        Nat
    n <- m Nat
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
    getContextSize
        let pars :: Args
            pars :: [Arg Term]
    pars = Nat -> [Arg Term] -> [Arg Term]
    forall a. Subst a => Nat -> a -> a
    raise (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    ptel) ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Telescope
    ptel
        Type
    ftype <- Definition -> Type
    defType Definition
    def Type -> [Arg Term] -> m Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    Type -> a -> m Type
    `piApplyM` [Arg Term]
    pars
        (Type, Elims -> Term) -> m (Type, Elims -> Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type
    ftype , QName -> Elims -> Term
    Def QName
    f)
      Defn
    _ -> (Type, Elims -> Term) -> m (Type, Elims -> Term)
    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, MonadFresh NameId m) => QName -> m [RewriteRule]
    getAllRulesFor :: forall (m :: * -> *).
    (HasConstInfo 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> QName -> m [RewriteRule]
    forall (m :: * -> *).
    (HasConstInfo 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)
    -> ([Arg Term] -> [Term]) -> [Arg Term] -> Substitution
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Term] -> [Term]
    forall a. [a] -> [a]
    reverse ([Term] -> [Term])
    -> ([Arg Term] -> [Term]) -> [Arg Term] -> [Term]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Term) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg ([Arg Term] -> Substitution) -> m [Arg Term] -> m Substitution
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope -> m [Arg Term]
    forall (m :: * -> *).
    MonadMetaSolver m =>
    Telescope -> m [Arg Term]
    newTelMeta Telescope
    gamma

    computingOverlap :: (MonadTCEnv m) => m a -> m a
    computingOverlap :: forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    computingOverlap = Lens' Bool TCEnv -> (Bool -> Bool) -> m a -> m a
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' Bool TCEnv
    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 e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \case
        err :: TCErr
    err@TypeError{} -> do
          VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence" Nat
    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: "
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    prettyTCM TCErr
    err
            ]
          Maybe a -> TCMT IO (Maybe 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 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 (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
        Constraints
    cs <- ProblemId -> TCMT IO Constraints
    forall (m :: * -> *). ReadTCState m => ProblemId -> m Constraints
    getConstraintsForProblem ProblemId
    pid
        [Doc]
    prettyCs <- Constraints -> TCMT IO [Doc]
    forall (m :: * -> *). MonadPretty m => Constraints -> m [Doc]
    prettyInterestingConstraints Constraints
    cs
        Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Term -> Term -> [Doc] -> Warning
    RewriteMaybeNonConfluent Term
    lhs1 Term
    lhs2 [Doc]
    prettyCs
        Maybe a -> TCMT IO (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    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
    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)
    traverse b -> m b
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    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 -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.parreduce" Nat
    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
    prettyTCM (Elims -> Term
    hd Elims
    es)
      -- Get type of head symbol
      (QName
    f , Type
    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 [])
      VerboseKey -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.parreduce" Nat
    60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "topLevelReductions: head symbol" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Elims -> Term
    hd []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
      RewriteRule QName
    q Telescope
    gamma QName
    _ PElims
    ps Term
    rhs Type
    b Bool
    c <- m [RewriteRule] -> m RewriteRule
    forall (m :: * -> *) (t :: * -> *) a.
    (MonadPlus m, Foldable t) =>
    m (t a) -> m a
    scatterMP (QName -> m [RewriteRule]
    forall (m :: * -> *).
    (HasConstInfo m, MonadFresh NameId m) =>
    QName -> m [RewriteRule]
    getAllRulesFor QName
    f)
      VerboseKey -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.parreduce" Nat
    60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "topLevelReductions: trying 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
    prettyTCM QName
    q
      -- Don't reduce if underapplied
      Bool -> m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> m ()) -> Bool -> m ()
    forall a b. (a -> b) -> a -> b
    $ Elims -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Elims
    es Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    >= PElims -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length PElims
    ps
      let (Elims
    es0 , Elims
    es1) = Nat -> Elims -> (Elims, Elims)
    forall a. Nat -> [a] -> ([a], [a])
    splitAt (PElims -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length PElims
    ps) Elims
    es
      m (Either Blocked_ Substitution)
    -> m (Either Blocked_ Substitution)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    onlyReduceTypes (Telescope
    -> (Type, Elims -> Term)
    -> PElims
    -> Elims
    -> m (Either Blocked_ Substitution)
    forall (m :: * -> *) t a b.
    (PureTCM m, Match t a b) =>
    Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
    nonLinMatch Telescope
    gamma (Type
    t,Elims -> Term
    hd) PElims
    ps Elims
    es0) m (Either Blocked_ Substitution)
    -> (Either Blocked_ Substitution -> m Term) -> m Term
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        -- Matching failed: no reduction
        Left Blocked_
    block -> m Term
    forall (f :: * -> *) a. Alternative f => f a
    empty
        -- Matching succeeded
        Right Substitution
    sub -> do
          let vs :: [Term]
    vs = (Nat -> Term) -> [Nat] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Substitution -> Nat -> Term
    forall a. EndoSubst a => Substitution' a -> Nat -> a
    lookupS Substitution
    sub) ([Nat] -> [Term]) -> [Nat] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ [Nat
    0..(Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    gammaNat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    1)]
          Substitution
    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
    parReduce [Term]
    vs
          Elims
    es1' <- Elims -> m Elims
    forall a (m :: * -> *).
    (ParallelReduce a, MonadParallelReduce m, MonadPlus m) =>
    a -> m a
    parReduce Elims
    es1
          let w :: Term
    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'
          VerboseKey -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.parreduce" Nat
    50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "topLevelReductions: rewrote" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (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
    "to" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    w
          Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    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 (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
    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 (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
    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
    parReduce Abs Term
    u
        Var Nat
    x Elims
    es -> Nat -> Elims -> Term
    Var Nat
    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
    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
    parReduce Dom Type
    a m (Abs Type -> Term) -> m (Abs Type) -> m Term
    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
    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
    parReduce Sort
    s

        -- Base cases
        u :: Term
    u@Lit{}      -> Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    u
        u :: Term
    u@Level{}    -> Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    u -- TODO: is this fine?
        u :: Term
    u@DontCare{} -> Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    u
        u :: Term
    u@Dummy{}    -> Term -> m Term
    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 (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
    parReduce Arg a
    u
      parReduce e :: Elim' a
    e@Proj{}   = Elim' a -> m (Elim' a)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Elim' a
    e
      parReduce IApply{}   = m (Elim' a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- not yet supported

    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
    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))
    -> TCM (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))
     -> TCM (Maybe (Telescope, a)))
    -> ([MetaId] -> TCMT IO (Telescope, a))
    -> TCM (Maybe (Telescope, a))
    forall a b. (a -> b) -> a -> b
    $ \[MetaId]
    ms' -> do

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

        -- Construct telescope (still containing the metas)
        let gamma :: Telescope
    gamma = [VerboseKey] -> [Dom Type] -> Telescope
    unflattenTel [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 n :: Nat
    n           = [MetaId] -> Nat
    forall a. Sized a => a -> Nat
    size [MetaId]
    ms'
            metaIndex :: MetaId -> Maybe Nat
    metaIndex MetaId
    x = (Nat
    nNat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    1Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -) (Nat -> Nat) -> Maybe Nat -> Maybe Nat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> [MetaId] -> Maybe Nat
    forall a. Eq a => a -> [a] -> Maybe Nat
    elemIndex MetaId
    x [MetaId]
    ms'
        ReaderT (MetaId -> Maybe Nat) (TCMT IO) (Telescope, a)
    -> (MetaId -> Maybe Nat) -> TCMT IO (Telescope, a)
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ((Telescope, a)
    -> ReaderT (MetaId -> Maybe Nat) (TCMT IO) (Telescope, a)
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars (Telescope
    gamma, a
    x)) MetaId -> Maybe Nat
    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
    <$ :: forall a b. a -> OneHole b -> OneHole a
    $c<$ :: forall a b. a -> OneHole b -> OneHole a
    fmap :: forall a b. (a -> b) -> OneHole a -> OneHole b
    $cfmap :: forall a b. (a -> b) -> OneHole a -> OneHole b
    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 :: forall a.
    Telescope
    -> Type -> (Term -> a) -> (Elims -> Term) -> Elims -> OneHole a
    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 :: Telescope
    ohBoundVars = Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    a (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> Telescope -> Abs Telescope
    forall a. VerboseKey -> a -> Abs a
    Abs VerboseKey
    x (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
    forall a b. (a -> b) -> a -> b
    $ OneHole a -> Telescope
    forall a. OneHole a -> Telescope
    ohBoundVars OneHole a
    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
      type PType p
      allHoles :: (Alternative m, PureTCM m) => PType p -> p -> m (OneHole p)

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

    allHolesList
      :: ( PureTCM m , AllHoles p)
      => PType p -> p -> m [OneHole p]
    allHolesList :: forall (m :: * -> *) p.
    (PureTCM m, AllHoles p) =>
    PType p -> p -> m [OneHole p]
    allHolesList PType 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
    . PType p -> p -> ListT m (OneHole p)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    PType p -> p -> m (OneHole p)
    allHoles PType 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 (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 -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.eta" Nat
    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
    prettyTCM Term
    v , TCMT IO Doc
    ":" , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a , TCMT IO Doc
    "to take one more argument" ]
        Dom Type
    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_
        Type
    cod <- Dom Type -> TCMT IO Type -> TCMT IO Type
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Dom Type
    dom (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Type
    newTypeMeta_
        Type -> Type -> TCM ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    equalType Type
    a (Type -> TCM ()) -> Type -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Dom (VerboseKey, Type) -> Type -> Type
    mkPi ((VerboseKey
    "x",) (Type -> (VerboseKey, Type)) -> Dom Type -> Dom (VerboseKey, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type
    dom) Type
    cod

        -- Construct body of eta-expansion
        let body :: Term
    body = Nat -> Term -> Term
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 Term
    v Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> 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
    $ Nat -> Term
    var Nat
    0]

        -- Continue with remaining eliminations
        Dom Type -> TCMT IO (OneHole Term) -> TCMT IO (OneHole Term)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Dom Type
    dom (TCMT IO (OneHole Term) -> TCMT IO (OneHole Term))
    -> TCMT IO (OneHole Term) -> TCMT IO (OneHole Term)
    forall a b. (a -> b) -> a -> b
    $ VerboseKey -> Dom Type -> OneHole Term -> OneHole Term
    forall a. VerboseKey -> Dom Type -> OneHole a -> OneHole a
    ohAddBV VerboseKey
    "x" Dom Type
    dom (OneHole Term -> OneHole Term)
    -> (OneHole Term -> OneHole Term) -> OneHole Term -> OneHole Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> Term) -> OneHole Term -> OneHole Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    i (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VerboseKey -> Term -> Abs Term
    forall a. (Subst a, Free a) => VerboseKey -> a -> Abs a
    mkAbs VerboseKey
    "x") (OneHole Term -> OneHole Term)
    -> TCMT IO (OneHole Term) -> TCMT IO (OneHole Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
          Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
    forall a. Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
    forceEtaExpansion Type
    cod Term
    body [Elim' a]
    es

      Proj ProjOrigin
    o QName
    f -> do

        -- Force a to be the right record type for projection by f
        VerboseKey -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.eta" Nat
    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
    prettyTCM Term
    v , TCMT IO Doc
    ":" , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    prettyTCM QName
    f ]
        QName
    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
        Definition
    rdef <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    r
        let ra :: Type
    ra = Definition -> Type
    defType Definition
    rdef
        [Arg Term]
    pars <- Type -> TCMT IO [Arg Term]
    forall (m :: * -> *). MonadMetaSolver m => Type -> m [Arg Term]
    newArgsMeta Type
    ra
        Sort
    s <- Type
    ra Type -> [Arg Term] -> TCMT IO Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    Type -> a -> m Type
    `piApplyM` [Arg Term]
    pars TCMT IO Type -> (Type -> TCMT IO Sort) -> TCMT IO Sort
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \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 (m :: * -> *) a. Monad m => a -> m a
    return TCMT IO Sort
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Type -> Type -> TCM ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    equalType Type
    a (Type -> TCM ()) -> Type -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (QName -> Elims -> Term
    Def QName
    r (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply [Arg Term]
    pars)

        -- Eta-expand v at record type r, and get field corresponding to f
        (Telescope
    _ , ConHead
    c , ConInfo
    ci , [Arg Term]
    fields) <- QName
    -> [Arg Term]
    -> Defn
    -> Term
    -> TCMT IO (Telescope, ConHead, ConInfo, [Arg Term])
    forall (m :: * -> *).
    HasConstInfo m =>
    QName
    -> [Arg Term]
    -> Defn
    -> Term
    -> m (Telescope, ConHead, ConInfo, [Arg Term])
    etaExpandRecord_ QName
    r [Arg Term]
    pars (Definition -> Defn
    theDef Definition
    rdef) Term
    v
        let fs :: [Arg QName]
    fs        = (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term QName -> Arg QName
    forall t a. Dom' t a -> Arg a
    argFromDom ([Dom' Term QName] -> [Arg QName])
    -> [Dom' Term QName] -> [Arg QName]
    forall a b. (a -> b) -> a -> b
    $ Defn -> [Dom' Term QName]
    recFields (Defn -> [Dom' Term QName]) -> Defn -> [Dom' Term QName]
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    rdef
            i :: Nat
    i         = Nat -> Maybe Nat -> Nat
    forall a. a -> Maybe a -> a
    fromMaybe Nat
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Nat -> Nat) -> Maybe Nat -> Nat
    forall a b. (a -> b) -> a -> b
    $ QName -> [QName] -> Maybe Nat
    forall a. Eq a => a -> [a] -> Maybe Nat
    elemIndex QName
    f ([QName] -> Maybe Nat) -> [QName] -> Maybe Nat
    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 :: Term
    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
    $ [Arg Term]
    fields [Arg Term] -> Nat -> Maybe (Arg Term)
    forall a. [a] -> Nat -> Maybe a
    !!! Nat
    i
            fUpdate :: Term -> Term
    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) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> a -> b
    $ Nat -> (Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
    forall a. Nat -> (a -> a) -> [a] -> [a]
    updateAt Nat
    i (Term
    w Term -> Arg Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) [Arg Term]
    fields

        -- Get type of field corresponding to f
        ~(Just (El Sort
    _ (Pi Dom Type
    b Abs Type
    c))) <- QName -> Type -> TCMT IO (Maybe Type)
    forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
    getDefType QName
    f (Type -> TCMT IO (Maybe Type))
    -> TCMT IO Type -> TCMT IO (Maybe Type)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    a
        let fa :: Type
    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
        (Term -> Term) -> OneHole Term -> OneHole Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Term -> Term
    fUpdate (OneHole Term -> OneHole Term)
    -> TCMT IO (OneHole Term) -> TCMT IO (OneHole Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
    forall a. Type -> Term -> [Elim' a] -> TCMT IO (OneHole Term)
    forceEtaExpansion Type
    fa Term
    fContent [Elim' a]
    es

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

    -- ^ Instances for @AllHoles@

    instance AllHoles p => AllHoles (Arg p) where
      type PType (Arg p) = Dom (PType p)
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    PType (Arg p) -> Arg p -> m (OneHole (Arg p))
    allHoles PType (Arg p)
    a Arg p
    x = (p -> Arg p) -> OneHole p -> OneHole (Arg p)
    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
    <$> PType p -> p -> m (OneHole p)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    PType p -> p -> m (OneHole p)
    allHoles (Dom' Term (PType p) -> PType p
    forall t e. Dom' t e -> e
    unDom Dom' Term (PType p)
    PType (Arg p)
    a) (Arg p -> p
    forall e. Arg e -> e
    unArg Arg p
    x)

    instance AllHoles p => AllHoles (Dom p) where
      type PType (Dom p) = PType p
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    PType (Dom p) -> Dom p -> m (OneHole (Dom p))
    allHoles PType (Dom p)
    a Dom p
    x = (p -> Dom p) -> OneHole p -> OneHole (Dom p)
    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
    <$> PType p -> p -> m (OneHole p)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    PType p -> p -> m (OneHole p)
    allHoles PType p
    PType (Dom p)
    a (Dom p -> p
    forall t e. Dom' t e -> e
    unDom Dom p
    x)

    instance AllHoles (Abs Term) where
      type PType (Abs Term) = (Dom Type , Abs Type)
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    PType (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
    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 (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
    <$>
          PType Term -> Term -> m (OneHole Term)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    PType p -> p -> m (OneHole p)
    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
      type PType (Abs Type) = Dom Type
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    PType (Abs Type) -> Abs Type -> m (OneHole (Abs Type))
    allHoles PType (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
    addContext (Abs Type -> VerboseKey
    forall a. Abs a -> VerboseKey
    absName Abs Type
    a , Dom Type
    PType (Abs 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) Dom Type
    PType (Abs 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 (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, PType p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    a)

    instance AllHoles Elims where
      type PType Elims = (Type , Elims -> Term)
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    PType Elims -> Elims -> m (OneHole Elims)
    allHoles (Type
    a,Elims -> Term
    hd) [] = m (OneHole Elims)
    forall (f :: * -> *) a. Alternative f => f a
    empty
      allHoles (Type
    a,Elims -> Term
    hd) (Elim' Term
    e:Elims
    es) = do
        VerboseKey -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    VerboseKey -> Nat -> TCMT IO Doc -> m ()
    reportSDoc VerboseKey
    "rewriting.confluence.hole" Nat
    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
    prettyTCM (Elims -> Term
    hd []) , TCMT IO Doc
    ":" , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    prettyTCM Elim' Term
    e
          ]
        case Elim' Term
    e of
          Apply Arg Term
    x -> do
            ~(Pi Dom Type
    b Abs Type
    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' :: Type
    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
    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]
    :)
            ((Arg Term -> Elims) -> OneHole (Arg Term) -> OneHole Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Elim' Term -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :Elims
    es) (Elim' Term -> Elims)
    -> (Arg Term -> Elim' Term) -> Arg Term -> Elims
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply) (OneHole (Arg Term) -> OneHole Elims)
    -> m (OneHole (Arg Term)) -> m (OneHole Elims)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PType (Arg Term) -> Arg Term -> m (OneHole (Arg Term))
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    PType p -> p -> m (OneHole p)
    allHoles Dom Type
    PType (Arg Term)
    b Arg Term
    x)
             m (OneHole Elims) -> m (OneHole Elims) -> m (OneHole Elims)
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> ((Elims -> Elims) -> OneHole Elims -> OneHole Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Elim' Term
    eElim' Term -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :) (OneHole Elims -> OneHole Elims)
    -> m (OneHole Elims) -> m (OneHole Elims)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PType Elims -> Elims -> m (OneHole Elims)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    PType p -> p -> m (OneHole p)
    allHoles (Type
    a' , Elims -> Term
    hd') Elims
    es)
          Proj ProjOrigin
    o QName
    f -> do
            ~(Just (El Sort
    _ (Pi Dom Type
    b Abs Type
    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' :: Type
    a' = Abs Type
    c Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Elims -> Term
    hd []
            Elims -> Term
    hd' <- Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    applyE (Term -> Elims -> Term) -> m Term -> m (Elims -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ProjOrigin -> QName -> Arg Term -> m Term
    forall (m :: * -> *).
    HasConstInfo m =>
    ProjOrigin -> QName -> Arg Term -> m Term
    applyDef ProjOrigin
    o QName
    f (Dom Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom Type
    b Arg Type -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Elims -> Term
    hd [])
            (Elims -> Elims) -> OneHole Elims -> OneHole Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Elim' Term
    eElim' Term -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :) (OneHole Elims -> OneHole Elims)
    -> m (OneHole Elims) -> m (OneHole Elims)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PType Elims -> Elims -> m (OneHole Elims)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    PType p -> p -> m (OneHole p)
    allHoles (Type
    a' , Elims -> Term
    hd') Elims
    es
          IApply Term
    x Term
    y Term
    u -> m (OneHole Elims)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- Not yet implemented

    instance AllHoles Type where
      type PType Type = ()
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    PType Type -> Type -> m (OneHole Type)
    allHoles PType 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 (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
    <$> PType Term -> Term -> m (OneHole Term)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    PType p -> p -> m (OneHole p)
    allHoles (Sort -> Type
    sort Sort
    s) Term
    a

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

    instance AllHoles Sort where
      type PType Sort = ()
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    PType Sort -> Sort -> m (OneHole Sort)
    allHoles PType Sort
    _ = \case
        Type Level
    l       -> (Level -> Sort) -> OneHole Level -> OneHole Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Level -> Sort
    forall t. Level' t -> Sort' t
    Type (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, PType p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ Level
    l
        Prop Level
    l       -> (Level -> Sort) -> OneHole Level -> OneHole Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Level -> Sort
    forall t. Level' t -> Sort' t
    Prop (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, PType p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ Level
    l
        Inf IsFibrant
    f Integer
    n      -> m (OneHole Sort)
    forall (f :: * -> *) a. Alternative f => f a
    empty
        SSet Level
    l       -> (Level -> Sort) -> OneHole Level -> OneHole Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Level -> Sort
    forall t. Level' t -> Sort' t
    SSet (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, PType p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ Level
    l
        Sort
    SizeUniv     -> m (OneHole Sort)
    forall (f :: * -> *) a. Alternative f => f a
    empty
        Sort
    LockUniv     -> m (OneHole Sort)
    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
          Type
    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
          (Elims -> Sort) -> OneHole Elims -> OneHole Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (QName -> Elims -> Sort
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    f) (OneHole Elims -> OneHole Sort)
    -> m (OneHole Elims) -> m (OneHole Sort)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PType Elims -> Elims -> m (OneHole Elims)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    PType p -> p -> m (OneHole p)
    allHoles (Type
    fa , QName -> Elims -> Term
    Def QName
    f) Elims
    es
        DummyS{}     -> m (OneHole Sort)
    forall (f :: * -> *) a. Alternative f => f a
    empty

    instance AllHoles Level where
      type PType Level = ()
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    PType Level -> Level -> m (OneHole Level)
    allHoles PType Level
    _ (Max Integer
    n [PlusLevel' Term]
    ls) = ([PlusLevel' Term] -> Level)
    -> OneHole [PlusLevel' Term] -> OneHole Level
    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, PType p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ [PlusLevel' Term]
    ls

    instance AllHoles [PlusLevel] where
      type PType [PlusLevel] = ()
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    PType [PlusLevel' Term]
    -> [PlusLevel' Term] -> m (OneHole [PlusLevel' Term])
    allHoles PType [PlusLevel' Term]
    _ []     = m (OneHole [PlusLevel' Term])
    forall (f :: * -> *) a. Alternative f => f a
    empty
      allHoles PType [PlusLevel' Term]
    _ (PlusLevel' Term
    l:[PlusLevel' Term]
    ls) =
        ((PlusLevel' Term -> [PlusLevel' Term])
    -> OneHole (PlusLevel' Term) -> OneHole [PlusLevel' Term]
    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, PType p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ PlusLevel' Term
    l)
        m (OneHole [PlusLevel' Term])
    -> m (OneHole [PlusLevel' Term]) -> m (OneHole [PlusLevel' Term])
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> (([PlusLevel' Term] -> [PlusLevel' Term])
    -> OneHole [PlusLevel' Term] -> OneHole [PlusLevel' Term]
    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, PType p ~ ()) =>
    p -> m (OneHole p)
    allHoles_ [PlusLevel' Term]
    ls)

    instance AllHoles PlusLevel where
      type PType PlusLevel = ()
      allHoles :: forall (m :: * -> *).
    (Alternative m, PureTCM m) =>
    PType (PlusLevel' Term)
    -> PlusLevel' Term -> m (OneHole (PlusLevel' Term))
    allHoles PType (PlusLevel' Term)
    _ (Plus Integer
    n Term
    l) = do
        Type
    la <- m Type
    forall (m :: * -> *). HasBuiltins m => m Type
    levelType
        (Term -> PlusLevel' Term)
    -> OneHole Term -> OneHole (PlusLevel' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    n) (OneHole Term -> OneHole (PlusLevel' Term))
    -> m (OneHole Term) -> m (OneHole (PlusLevel' Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PType Term -> Term -> m (OneHole Term)
    forall p (m :: * -> *).
    (AllHoles p, Alternative m, PureTCM m) =>
    PType p -> p -> m (OneHole p)
    allHoles Type
    PType Term
    la Term
    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)
    traverse a' -> m a'
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Nat) 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 Nat) 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 Nat) -> MetaId -> Maybe Nat) -> m a -> m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((Nat -> Nat) -> Maybe Nat -> Maybe Nat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Nat -> Nat
    forall a. Enum a => a -> a
    succ (Maybe Nat -> Maybe Nat)
    -> (MetaId -> Maybe Nat) -> MetaId -> Maybe Nat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .) (a -> m a
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Nat) 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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars a
    x

    instance MetasToVars Term where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Nat) m, HasBuiltins m) =>
    Term -> m Term
    metasToVars = \case
        Var Nat
    i Elims
    es   -> Nat -> Elims -> Term
    Var Nat
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Abs Term
    u
        Lit Literal
    l      -> Term -> m Term
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Dom Type
    a m (Abs Type -> Term) -> m (Abs Type) -> m Term
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Level
    l
        MetaV MetaId
    x Elims
    es -> ((MetaId -> Maybe Nat) -> Maybe Nat) -> m (Maybe Nat)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks ((MetaId -> Maybe Nat) -> MetaId -> Maybe Nat
    forall a b. (a -> b) -> a -> b
    $ MetaId
    x) m (Maybe Nat) -> (Maybe Nat -> m Term) -> m Term
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Just Nat
    i   -> Nat -> Elims -> Term
    Var Nat
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Elims
    es
          Maybe Nat
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Elims
    es

    instance MetasToVars Type where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Nat) 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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Sort
    s m (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m Term
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Term
    t

    instance MetasToVars Sort where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Nat) m, HasBuiltins m) =>
    Sort -> m Sort
    metasToVars = \case
        Type Level
    l     -> Level -> Sort
    forall t. Level' t -> Sort' t
    Type     (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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Level
    l
        Prop Level
    l     -> Level -> Sort
    forall t. Level' t -> Sort' t
    Prop     (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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Level
    l
        Inf IsFibrant
    f Integer
    n    -> Sort -> m Sort
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ IsFibrant -> Integer -> Sort
    forall t. IsFibrant -> Integer -> Sort' t
    Inf IsFibrant
    f Integer
    n
        SSet Level
    l     -> Level -> Sort
    forall t. Level' t -> Sort' t
    SSet     (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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Level
    l
        Sort
    SizeUniv   -> Sort -> m Sort
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    forall t. Sort' t
    SizeUniv
        Sort
    LockUniv   -> Sort -> m Sort
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    forall t. Sort' t
    LockUniv
        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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Dom' Term Term
    s m (Sort -> Abs Sort -> Sort) -> m Sort -> m (Abs Sort -> Sort)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Sort -> m Sort
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Sort
    t m (Abs Sort -> Sort) -> m (Abs Sort) -> m Sort
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Sort
    s m (Sort -> Sort) -> m Sort -> m Sort
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Sort -> m Sort
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
     HasBuiltins m) =>
    a -> m a
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Elims
    es
        DummyS VerboseKey
    s   -> Sort -> m Sort
    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 Nat) 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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars [PlusLevel' Term]
    ls

    instance MetasToVars PlusLevel where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Nat) 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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Term
    x

    instance MetasToVars a => MetasToVars (Tele a) where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Nat) m, HasBuiltins m) =>
    Tele a -> m (Tele a)
    metasToVars Tele a
    EmptyTel = Tele a -> m (Tele 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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars a
    a m (Abs (Tele a) -> Tele a) -> m (Abs (Tele a)) -> m (Tele a)
    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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars Abs (Tele a)
    tel

    instance (MetasToVars a, MetasToVars b) => MetasToVars (a,b) where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Nat) 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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars a
    x m (b -> (a, b)) -> m b -> m (a, 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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars b
    y

    instance (MetasToVars a, MetasToVars b, MetasToVars c) => MetasToVars (a,b,c) where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Nat) 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 Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars a
    x m (b -> c -> (a, b, c)) -> m b -> m (c -> (a, b, c))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> m b
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars b
    y m (c -> (a, b, c)) -> m c -> m (a, b, c)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> c -> m c
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars c
    z

    instance (MetasToVars a, MetasToVars b, MetasToVars c, MetasToVars d) => MetasToVars (a,b,c,d) where
      metasToVars :: forall (m :: * -> *).
    (MonadReader (MetaId -> Maybe Nat) 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 Nat) 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> b -> m b
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars b
    y m (c -> d -> (a, b, c, d)) -> m c -> m (d -> (a, b, c, d))
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> c -> m c
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars c
    z m (d -> (a, b, c, d)) -> m d -> m (a, b, c, d)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> d -> m d
    forall a (m :: * -> *).
    (MetasToVars a, MonadReader (MetaId -> Maybe Nat) m,
     HasBuiltins m) =>
    a -> m a
    metasToVars d
    w