    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.MetaVars where

    import Prelude hiding (null)

    import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )
    import Control.Monad.Trans.Maybe

    import qualified Data.IntSet as IntSet
    import qualified Data.IntMap as IntMap
    import qualified Data.List as List
    import qualified Data.Map.Strict as MapS
    import qualified Data.Set as Set
    import qualified Data.Foldable as Fold
    import qualified Data.Traversable as Trav

    import Agda.Interaction.Options

    import Agda.Syntax.Abstract.Name as A
    import Agda.Syntax.Common
    import Agda.Syntax.Info ( MetaKind( InstanceMeta, UnificationMeta ), MetaNameSuggestion)
    import qualified Agda.Syntax.Info as A
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Generic
    import Agda.Syntax.Internal.MetaVars
    import Agda.Syntax.Position (getRange, killRange)

    import Agda.TypeChecking.Monad
    -- import Agda.TypeChecking.Monad.Builtin
    -- import Agda.TypeChecking.Monad.Context
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Sort
    import Agda.TypeChecking.Substitute
    import qualified Agda.TypeChecking.SyntacticEquality as SynEq
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Constraints
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Lock
    import Agda.TypeChecking.Level (levelType)
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.EtaContract
    import Agda.TypeChecking.SizedTypes (boundedSizeMetaHook, isSizeProblem)
    import {-# SOURCE #-} Agda.TypeChecking.CheckInternal
    import {-# SOURCE #-} Agda.TypeChecking.Conversion

    -- import Agda.TypeChecking.CheckInternal
    -- import {-# SOURCE #-} Agda.TypeChecking.CheckInternal (checkInternal)
    import Agda.TypeChecking.MetaVars.Occurs

    import qualified Agda.Utils.BiMap as BiMap
    import Agda.Utils.Function
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Size
    import Agda.Utils.Tuple
    import Agda.Utils.Permutation
    import Agda.Syntax.Common.Pretty (Pretty, prettyShow, render)
    import qualified Agda.Utils.ProfileOptions as Profile
    import Agda.Utils.Singleton
    import qualified Agda.Utils.Graph.TopSort as Graph
    import Agda.Utils.VarSet (VarSet)
    import qualified Agda.Utils.VarSet as VarSet

    import Agda.Utils.Impossible

    instance MonadMetaSolver TCM where
      newMeta' :: forall a.
    MetaInstantiation
    -> Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> TCM MetaId
    newMeta' = MetaInstantiation
    -> Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> TCM MetaId
    forall a.
    MetaInstantiation
    -> Frozen
    -> MetaInfo
    -> MetaPriority
    -> Permutation
    -> Judgement a
    -> TCM MetaId
    newMetaTCM'
      assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
    assignV CompareDirection
    dir MetaId
    x Args
    args Term
    v CompareAs
    t = CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM ()
    forall (m :: * -> *).
    (MonadMetaSolver m, MonadConstraint m, MonadError TCErr m,
     MonadDebug m, HasOptions m) =>
    CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
    assignWrapper CompareDirection
    dir MetaId
    x ((Arg Term -> Elim) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Args
    args) Term
    v (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
    assign CompareDirection
    dir MetaId
    x Args
    args Term
    v CompareAs
    t
      assignTerm' :: MonadMetaSolver (TCMT IO) =>
    MetaId -> [Arg [Char]] -> Term -> TCM ()
    assignTerm' = MetaId -> [Arg [Char]] -> Term -> TCM ()
    assignTermTCM'
      etaExpandMeta :: [MetaClass] -> MetaId -> TCM ()
    etaExpandMeta = [MetaClass] -> MetaId -> TCM ()
    etaExpandMetaTCM
      updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
    updateMetaVar = HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
    MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
    updateMetaVarTCM

      -- Right now we roll back the full state when aborting.
      -- TODO: only roll back the metavariables
      speculateMetas :: TCM () -> TCM KeepMetas -> TCM ()
    speculateMetas TCM ()
    fallback TCM KeepMetas
    m = do
        (a, s) <- TCM KeepMetas -> TCM (KeepMetas, TCState)
    forall a. TCM a -> TCM (a, TCState)
    localTCStateSaving TCM KeepMetas
    m
        case a of
          KeepMetas
    KeepMetas     -> TCState -> TCM ()
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
    putTC TCState
    s
          KeepMetas
    RollBackMetas -> TCM ()
    fallback

    -- | Find position of a value in a list.
    --   Used to change metavar argument indices during assignment.
    --
    --   @reverse@ is necessary because we are directly abstracting over the list.
    --
    findIdx :: Eq a => [a] -> a -> Maybe Int
    findIdx :: forall a. Eq a => [a] -> a -> Maybe Nat
    findIdx [a]
    vs a
    v = a -> [a] -> Maybe Nat
    forall a. Eq a => a -> [a] -> Maybe Nat
    List.elemIndex a
    v ([a] -> [a]
    forall a. [a] -> [a]
    reverse [a]
    vs)

    -- | Does the given local meta-variable have a twin meta-variable?

    hasTwinMeta :: MetaId -> TCM Bool
    hasTwinMeta :: MetaId -> TCM Bool
    hasTwinMeta MetaId
    x = do
        m <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    x
        return $ isJust $ mvTwin m

    -- | Check whether a meta variable is a place holder for a blocked term.
    isBlockedTerm :: MetaId -> TCM Bool
    isBlockedTerm :: MetaId -> TCM Bool
    isBlockedTerm MetaId
    x = do
        [Char] -> Nat -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.blocked" Nat
    12 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "is " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " a blocked term? "
        i <- MetaId -> TCMT IO MetaInstantiation
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m MetaInstantiation
    lookupMetaInstantiation MetaId
    x
        let r = case MetaInstantiation
    i of
                BlockedConst{}                 -> Bool
    True
                PostponedTypeCheckingProblem{} -> Bool
    True
                InstV{}                        -> Bool
    False
                OpenMeta{}                     -> Bool
    False
        reportSLn "tc.meta.blocked" 12 $
          if r then "  yes, because " ++ prettyShow i else "  no"
        return r

    isEtaExpandable :: [MetaClass] -> MetaId -> TCM Bool
    isEtaExpandable :: [MetaClass] -> MetaId -> TCM Bool
    isEtaExpandable [MetaClass]
    classes MetaId
    x = do
        i <- MetaId -> TCMT IO MetaInstantiation
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m MetaInstantiation
    lookupMetaInstantiation MetaId
    x
        return $ case i of
          OpenMeta MetaKind
    UnificationMeta       -> Bool
    True
          OpenMeta MetaKind
    InstanceMeta          -> MetaClass
    Records MetaClass -> [MetaClass] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [MetaClass]
    classes
          InstV{}                        -> Bool
    False
          BlockedConst{}                 -> Bool
    False
          PostponedTypeCheckingProblem{} -> Bool
    False

    -- * Performing the assignment

    -- | Performing the meta variable assignment.
    --
    --   The instantiation should not be an 'InstV' and the 'MetaId'
    --   should point to something 'Open' or a 'BlockedConst'.
    --   Further, the meta variable may not be 'Frozen'.
    assignTerm :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m ()
    assignTerm :: forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> [Arg [Char]] -> Term -> m ()
    assignTerm MetaId
    x [Arg [Char]]
    tel Term
    v = do
         -- verify (new) invariants
        m Bool -> m () -> m ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (MetaId -> m Bool
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    x) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        MetaId -> [Arg [Char]] -> Term -> m ()
    forall (m :: * -> *).
    (MonadMetaSolver m, MonadMetaSolver m) =>
    MetaId -> [Arg [Char]] -> Term -> m ()
    assignTerm' MetaId
    x [Arg [Char]]
    tel Term
    v

    -- | Skip frozen check.  Used for eta expanding frozen metas.
    assignTermTCM' :: MetaId -> [Arg ArgName] -> Term -> TCM ()
    assignTermTCM' :: MetaId -> [Arg [Char]] -> Term -> TCM ()
    assignTermTCM' MetaId
    x [Arg [Char]]
    tel Term
    v = do
        [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign" Nat
    70 (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
    "assignTerm" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    x 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
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
          , 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
    "tel =" 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_ ((Arg [Char] -> TCMT IO Doc) -> [Arg [Char]] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (Arg [Char] -> [Char]) -> Arg [Char] -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg [Char] -> [Char]
    forall e. Arg e -> e
    unArg) [Arg [Char]]
    tel)
          ]
         -- verify (new) invariants
        TCM Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (Bool -> Bool
    not (Bool -> Bool) -> TCM Bool -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCEnv -> Bool) -> TCM Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envAssignMetas) TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        ProfileOption -> TCM () -> TCM ()
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    Profile.Metas (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    forall a. TCM a -> TCM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return () {-tickMax "max-open-metas" . (fromIntegral . size) =<< getOpenMetas-}
        HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
    MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
    updateMetaVarTCM MetaId
    x ((MetaVariable -> MetaVariable) -> TCM ())
    -> (MetaVariable -> MetaVariable) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ MetaVariable
    mv ->
          MetaVariable
    mv { mvInstantiation = InstV $ Instantiation
                 { instTel = tel
                 , instBody = v
                 -- Andreas, 2022-04-28, issue #5875:
                 -- Can't killRange the meta-solution, since this will destroy
                 -- ranges of termination errors (and potentially other passes
                 -- that run on internal syntax)!
                 -- , instBody = killRange v
                 }
             }
        MetaId -> TCM ()
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
    etaExpandListeners MetaId
    x
        MetaId -> TCM ()
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
    wakeupConstraints MetaId
    x
        [Char] -> Nat -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.assign" Nat
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "completed assignment of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    x

    -- * Creating meta variables.

    -- | Create a sort meta that cannot be instantiated with 'Inf' (Setω).
    newSortMetaBelowInf :: TCM Sort
    newSortMetaBelowInf :: TCM Sort
    newSortMetaBelowInf = do
      x <- TCM Sort
    forall (m :: * -> *). MonadMetaSolver m => m Sort
    newSortMeta
      hasBiggerSort x
      return x

    {-# SPECIALIZE newSortMeta :: TCM Sort #-}
    -- | Create a sort meta that may be instantiated with 'Inf' (Setω).
    newSortMeta :: MonadMetaSolver m => m Sort
    newSortMeta :: forall (m :: * -> *). MonadMetaSolver m => m Sort
    newSortMeta =
      m Bool -> m Sort -> m Sort -> m Sort
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM m Bool
    forall (m :: * -> *). HasOptions m => m Bool
    hasUniversePolymorphism (Args -> m Sort
    forall (m :: * -> *). MonadMetaSolver m => Args -> m Sort
    newSortMetaCtx (Args -> m Sort) -> m Args -> m Sort
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs)
      -- else (no universe polymorphism)
      (m Sort -> m Sort) -> m Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ do i   <- m MetaInfo
    forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
    createMetaInfo
           let j = () -> Type -> Judgement ()
    forall a. a -> Type -> Judgement a
    IsSort () Type
    HasCallStack => Type
    __DUMMY_TYPE__
           x   <- newMeta Instantiable i normalMetaPriority (idP 0) j
           reportSDoc "tc.meta.new" 50 $
             "new sort meta" <+> prettyTCM x
           return $ MetaS x []

    -- | Create a sort meta that may be instantiated with 'Inf' (Setω).
    newSortMetaCtx :: MonadMetaSolver m => Args -> m Sort
    newSortMetaCtx :: forall (m :: * -> *). MonadMetaSolver m => Args -> m Sort
    newSortMetaCtx Args
    vs = do
        i   <- m MetaInfo
    forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
    createMetaInfo
        tel <- getContextTelescope
        let t = Tele (Dom Type) -> Type -> Type
    telePi_ Tele (Dom Type)
    tel Type
    HasCallStack => Type
    __DUMMY_TYPE__
        x   <- newMeta Instantiable i normalMetaPriority (idP $ size tel) $ IsSort () t
        reportSDoc "tc.meta.new" 50 $
          "new sort meta" <+> prettyTCM x <+> ":" <+> prettyTCM t
        return $ MetaS x $ map Apply vs

    newTypeMeta' :: Comparison -> Sort -> TCM Type
    newTypeMeta' :: Comparison -> Sort -> TCM Type
    newTypeMeta' Comparison
    cmp Sort
    s = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type)
    -> ((MetaId, Term) -> Term) -> (MetaId, Term) -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (MetaId, Term) -> Term
    forall a b. (a, b) -> b
    snd ((MetaId, Term) -> Type) -> TCMT IO (MetaId, Term) -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    newValueMeta RunMetaOccursCheck
    RunMetaOccursCheck Comparison
    cmp (Sort -> Type
    sort Sort
    s)

    newTypeMeta :: Sort -> TCM Type
    newTypeMeta :: Sort -> TCM Type
    newTypeMeta = Comparison -> Sort -> TCM Type
    newTypeMeta' Comparison
    CmpLeq

    newTypeMeta_ ::  TCM Type
    newTypeMeta_ :: TCM Type
    newTypeMeta_  = Comparison -> Sort -> TCM Type
    newTypeMeta' Comparison
    CmpEq (Sort -> TCM Type) -> TCM Sort -> TCM Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (TCM Sort -> TCM Sort
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    workOnTypes (TCM Sort -> TCM Sort) -> TCM Sort -> TCM Sort
    forall a b. (a -> b) -> a -> b
    $ TCM Sort
    forall (m :: * -> *). MonadMetaSolver m => m Sort
    newSortMeta)
    -- TODO: (this could be made work with new uni-poly)
    -- Andreas, 2011-04-27: If a type meta gets solved, than we do not have to check
    -- that it has a sort.  The sort comes from the solution.
    -- newTypeMeta_  = newTypeMeta Inf

    {-# SPECIALIZE newLevelMeta :: TCM Level #-}
    newLevelMeta :: MonadMetaSolver m => m Level
    newLevelMeta :: forall (m :: * -> *). MonadMetaSolver m => m Level
    newLevelMeta = do
      (x, v) <- RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    newValueMeta RunMetaOccursCheck
    RunMetaOccursCheck Comparison
    CmpEq (Type -> m (MetaId, Term)) -> m Type -> m (MetaId, Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m Type
    forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
    levelType
      return $ case v of
        Level Level
    l    -> Level
    l
        Term
    _          -> Term -> Level
    forall t. t -> Level' t
    atomicLevel Term
    v

    {-# SPECIALIZE newInstanceMeta :: MetaNameSuggestion -> Type -> TCM (MetaId, Term) #-}
    -- | @newInstanceMeta s t cands@ creates a new instance metavariable
    --   of type the output type of @t@ with name suggestion @s@.
    newInstanceMeta
      :: MonadMetaSolver m
      => MetaNameSuggestion -> Type -> m (MetaId, Term)
    newInstanceMeta :: forall (m :: * -> *).
    MonadMetaSolver m =>
    [Char] -> Type -> m (MetaId, Term)
    newInstanceMeta [Char]
    s Type
    t = do
      vs  <- m Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
      ctx <- getContextTelescope
      newInstanceMetaCtx s (telePi_ ctx t) vs

    newInstanceMetaCtx
      :: MonadMetaSolver m
      => MetaNameSuggestion -> Type -> Args -> m (MetaId, Term)
    newInstanceMetaCtx :: forall (m :: * -> *).
    MonadMetaSolver m =>
    [Char] -> Type -> Args -> m (MetaId, Term)
    newInstanceMetaCtx [Char]
    s Type
    t Args
    vs = do
      [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.new" Nat
    50 (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
    "new instance meta:"
        , 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
    $ Args -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Args -> m Doc
    prettyTCM Args
    vs TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "|-"
        ]
      -- Andreas, 2017-10-04, issue #2753: no metaOccurs check for instance metas
      i0 <- RunMetaOccursCheck -> m MetaInfo
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    RunMetaOccursCheck -> m MetaInfo
    createMetaInfo' RunMetaOccursCheck
    DontRunMetaOccursCheck
      let i = MetaInfo
    i0 { miNameSuggestion = s }
      TelV tel _ <- telView t
      let perm = Nat -> Permutation
    idP (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel)
      x <- newMeta' (OpenMeta InstanceMeta) Instantiable i normalMetaPriority perm (HasType () CmpLeq t)
      reportSDoc "tc.meta.new" 50 $ fsep
        [ nest 2 $ pretty x <+> ":" <+> prettyTCM t
        ]
      r <- getMetaRange x
      let c = Range -> MetaId -> Maybe [Candidate] -> Constraint
    FindInstance Range
    r MetaId
    x Maybe [Candidate]
    forall a. Maybe a
    Nothing
      addAwakeConstraint alwaysUnblock c
      etaExpandMetaSafe x
      return (x, MetaV x $ map Apply vs)

    -- | Create a new value meta with specific dependencies, possibly η-expanding in the process.
    newNamedValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term)
    newNamedValueMeta :: forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck
    -> [Char] -> Comparison -> Type -> m (MetaId, Term)
    newNamedValueMeta RunMetaOccursCheck
    b [Char]
    s Comparison
    cmp Type
    t = do
      (x, v) <- RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    newValueMeta RunMetaOccursCheck
    b Comparison
    cmp Type
    t
      setMetaNameSuggestion x s
      return (x, v)

    -- | Create a new value meta with specific dependencies without η-expanding.
    newNamedValueMeta' :: MonadMetaSolver m => RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> m (MetaId, Term)
    newNamedValueMeta' :: forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck
    -> [Char] -> Comparison -> Type -> m (MetaId, Term)
    newNamedValueMeta' RunMetaOccursCheck
    b [Char]
    s Comparison
    cmp Type
    t = do
      (x, v) <- RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    newValueMeta' RunMetaOccursCheck
    b Comparison
    cmp Type
    t
      setMetaNameSuggestion x s
      return (x, v)

    {-# SPECIALIZE newValueMetaOfKind :: A.MetaInfo -> RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term) #-}
    newValueMetaOfKind :: MonadMetaSolver m
      => A.MetaInfo
      -> RunMetaOccursCheck  -- ^ Ignored for instance metas.
      -> Comparison          -- ^ Ignored for instance metas.
      -> Type
      -> m (MetaId, Term)
    newValueMetaOfKind :: forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaInfo
    -> RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    newValueMetaOfKind MetaInfo
    info = case MetaInfo -> MetaKind
    A.metaKind MetaInfo
    info of
      MetaKind
    UnificationMeta -> RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    newValueMeta
      MetaKind
    InstanceMeta -> \ RunMetaOccursCheck
    _run Comparison
    _cmp -> [Char] -> Type -> m (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    [Char] -> Type -> m (MetaId, Term)
    newInstanceMeta (MetaInfo -> [Char]
    A.metaNameSuggestion MetaInfo
    info)

    {-# SPECIALIZE newValueMeta :: RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term) #-}
    -- | Create a new metavariable, possibly η-expanding in the process.
    newValueMeta :: MonadMetaSolver m => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    newValueMeta :: forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    newValueMeta RunMetaOccursCheck
    b Comparison
    cmp Type
    t = do
      vs  <- m Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
      tel <- getContextTelescope
      newValueMetaCtx Instantiable b cmp t tel (idP $ size tel) vs

    newValueMetaCtx
      :: MonadMetaSolver m
      => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term)
    newValueMetaCtx :: forall (m :: * -> *).
    MonadMetaSolver m =>
    Frozen
    -> RunMetaOccursCheck
    -> Comparison
    -> Type
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> m (MetaId, Term)
    newValueMetaCtx Frozen
    frozen RunMetaOccursCheck
    b Comparison
    cmp Type
    t Tele (Dom Type)
    tel Permutation
    perm Args
    ctx =
      (Term -> m Term) -> (MetaId, Term) -> m (MetaId, Term)
    forall (m :: * -> *) b d a.
    Functor m =>
    (b -> m d) -> (a, b) -> m (a, d)
    mapSndM Term -> m Term
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull ((MetaId, Term) -> m (MetaId, Term))
    -> m (MetaId, Term) -> m (MetaId, Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Frozen
    -> RunMetaOccursCheck
    -> Comparison
    -> Type
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> m (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    Frozen
    -> RunMetaOccursCheck
    -> Comparison
    -> Type
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> m (MetaId, Term)
    newValueMetaCtx' Frozen
    frozen RunMetaOccursCheck
    b Comparison
    cmp Type
    t Tele (Dom Type)
    tel Permutation
    perm Args
    ctx

    {-# SPECIALIZE newValueMeta' :: RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term) #-}
    -- | Create a new value meta without η-expanding.
    newValueMeta'
      :: MonadMetaSolver m
      => RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    newValueMeta' :: forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    newValueMeta' RunMetaOccursCheck
    b Comparison
    cmp Type
    t = do
      vs  <- m Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
      tel <- getContextTelescope
      newValueMetaCtx' Instantiable b cmp t tel (idP $ size tel) vs

    newValueMetaCtx'
      :: MonadMetaSolver m
      => Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> m (MetaId, Term)
    newValueMetaCtx' :: forall (m :: * -> *).
    MonadMetaSolver m =>
    Frozen
    -> RunMetaOccursCheck
    -> Comparison
    -> Type
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> m (MetaId, Term)
    newValueMetaCtx' Frozen
    frozen RunMetaOccursCheck
    b Comparison
    cmp Type
    a Tele (Dom Type)
    tel Permutation
    perm Args
    vs = do
      i <- RunMetaOccursCheck -> m MetaInfo
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    RunMetaOccursCheck -> m MetaInfo
    createMetaInfo' RunMetaOccursCheck
    b
      let t     = Tele (Dom Type) -> Type -> Type
    telePi_ Tele (Dom Type)
    tel Type
    a
      x <- newMeta frozen i normalMetaPriority perm (HasType () cmp t)
      modality <- currentModality
      reportSDoc "tc.meta.new" 50 $ fsep
        [ text $ "new meta (" ++ show (i ^. lensIsAbstract) ++ "):"
        , nest 2 $ prettyTCM vs <+> "|-"
        , nest 2 $ pretty x <+> ":" <+> pretty modality <+> prettyTCM t
        ]
      etaExpandMetaSafe x
      -- Andreas, 2012-09-24: for Metas X : Size< u add constraint X+1 <= u
      let u = MetaId -> Elims -> Term
    MetaV MetaId
    x (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Args
    vs
      boundedSizeMetaHook u tel a
      return (x, u)

    newTelMeta :: MonadMetaSolver m => Telescope -> m Args
    newTelMeta :: forall (m :: * -> *).
    MonadMetaSolver m =>
    Tele (Dom Type) -> m Args
    newTelMeta Tele (Dom Type)
    tel = Type -> m Args
    forall (m :: * -> *). MonadMetaSolver m => Type -> m Args
    newArgsMeta (Tele (Dom Type) -> Type -> Type
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Type
    HasCallStack => Type
    __DUMMY_TYPE__)

    type Condition = Dom Type -> Abs Type -> Bool

    trueCondition :: Condition
    trueCondition :: Condition
    trueCondition Dom Type
    _ Abs Type
    _ = Bool
    True

    {-# SPECIALIZE newArgsMeta :: Type -> TCM Args #-}
    newArgsMeta :: MonadMetaSolver m => Type -> m Args
    newArgsMeta :: forall (m :: * -> *). MonadMetaSolver m => Type -> m Args
    newArgsMeta = Condition -> Type -> m Args
    forall (m :: * -> *).
    MonadMetaSolver m =>
    Condition -> Type -> m Args
    newArgsMeta' Condition
    trueCondition

    {-# SPECIALIZE newArgsMeta' :: Condition -> Type -> TCM Args #-}
    newArgsMeta' :: MonadMetaSolver m => Condition -> Type -> m Args
    newArgsMeta' :: forall (m :: * -> *).
    MonadMetaSolver m =>
    Condition -> Type -> m Args
    newArgsMeta' Condition
    condition Type
    t = do
      args <- m Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
      tel  <- getContextTelescope
      newArgsMetaCtx' Instantiable condition t tel (idP $ size tel) args

    newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args
    newArgsMetaCtx :: Type -> Tele (Dom Type) -> Permutation -> Args -> TCM Args
    newArgsMetaCtx = Frozen
    -> Condition
    -> Type
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> TCM Args
    forall (m :: * -> *).
    MonadMetaSolver m =>
    Frozen
    -> Condition
    -> Type
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> m Args
    newArgsMetaCtx' Frozen
    Instantiable Condition
    trueCondition

    newArgsMetaCtx''
      :: MonadMetaSolver m
      => MetaNameSuggestion -> Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
    newArgsMetaCtx'' :: forall (m :: * -> *).
    MonadMetaSolver m =>
    [Char]
    -> Frozen
    -> Condition
    -> Type
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> m Args
    newArgsMetaCtx'' [Char]
    pref Frozen
    frozen Condition
    condition (El Sort
    s Term
    tm) Tele (Dom Type)
    tel Permutation
    perm Args
    ctx = do
      tm <- Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    tm
      case tm of
        Pi dom :: Dom Type
    dom@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    info, unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a}) Abs Type
    codom | Condition
    condition Dom Type
    dom Abs Type
    codom -> do
          let mod :: Modality
    mod  = ArgInfo -> Modality
    forall a. LensModality a => a -> Modality
    getModality ArgInfo
    info
              -- Issue #3031: It's not enough to applyModalityToContext, since most (all?)
              -- of the context lives in tel. Don't forget the arguments in ctx.
              tel' :: Tele (Dom Type)
    tel' = ListTel -> Tele (Dom Type)
    telFromList (ListTel -> Tele (Dom Type)) -> ListTel -> Tele (Dom Type)
    forall a b. (a -> b) -> a -> b
    $
                     (Dom ([Char], Type) -> Dom ([Char], Type)) -> ListTel -> ListTel
    forall a b. (a -> b) -> [a] -> [b]
    map (Modality
    mod Modality -> Dom ([Char], Type) -> Dom ([Char], Type)
    forall a. LensModality a => Modality -> a -> a
    `inverseApplyModalityButNotQuantity`) (ListTel -> ListTel) -> ListTel -> ListTel
    forall a b. (a -> b) -> a -> b
    $
                     Tele (Dom Type) -> ListTel
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Tele (Dom Type)
    tel
              ctx' :: Args
    ctx' = (Arg Term -> Arg Term) -> Args -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map (Modality
    mod Modality -> Arg Term -> Arg Term
    forall a. LensModality a => Modality -> a -> a
    `inverseApplyModalityButNotQuantity`) Args
    ctx
          (m, u) <- ArgInfo -> m (MetaId, Term) -> m (MetaId, Term)
    forall (tcm :: * -> *) m a.
    (MonadTCEnv tcm, LensModality m) =>
    m -> tcm a -> tcm a
    applyModalityToContext ArgInfo
    info (m (MetaId, Term) -> m (MetaId, Term))
    -> m (MetaId, Term) -> m (MetaId, Term)
    forall a b. (a -> b) -> a -> b
    $
                     Frozen
    -> RunMetaOccursCheck
    -> Comparison
    -> Type
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> m (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    Frozen
    -> RunMetaOccursCheck
    -> Comparison
    -> Type
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> m (MetaId, Term)
    newValueMetaCtx Frozen
    frozen RunMetaOccursCheck
    RunMetaOccursCheck Comparison
    CmpLeq Type
    a Tele (Dom Type)
    tel' Permutation
    perm Args
    ctx'
          -- Jesper, 2021-05-05: When creating a metavariable from a
          -- generalizable variable, we must set the modality at which it
          -- will be generalized.  Don't do this for other metavariables,
          -- as they should keep the defaul modality (see #5363).
          whenM ((== YesGeneralizeVar) <$> viewTC eGeneralizeMetas) $
            setMetaGeneralizableArgInfo m $ hideOrKeepInstance info
          setMetaNameSuggestion m (suffixNameSuggestion pref (absName codom))
          args <- newArgsMetaCtx'' pref frozen condition (codom `absApp` u) tel perm ctx
          return $ Arg info u : args
        Term
    _  -> Args -> m Args
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

    newArgsMetaCtx'
      :: MonadMetaSolver m
      => Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> m Args
    newArgsMetaCtx' :: forall (m :: * -> *).
    MonadMetaSolver m =>
    Frozen
    -> Condition
    -> Type
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> m Args
    newArgsMetaCtx' = [Char]
    -> Frozen
    -> Condition
    -> Type
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> m Args
    forall (m :: * -> *).
    MonadMetaSolver m =>
    [Char]
    -> Frozen
    -> Condition
    -> Type
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> m Args
    newArgsMetaCtx'' [Char]
    forall a. Monoid a => a
    mempty

    -- | Create a metavariable of record type. This is actually one metavariable
    --   for each field.
    newRecordMeta :: QName -> Args -> TCM Term
    newRecordMeta :: QName -> Args -> TCM Term
    newRecordMeta QName
    r Args
    pars = do
      args <- TCM Args
    forall (m :: * -> *). MonadTCEnv m => m Args
    getContextArgs
      tel  <- getContextTelescope
      newRecordMetaCtx mempty Instantiable r pars tel (idP $ size tel) args

    newRecordMetaCtx
      :: MetaNameSuggestion
      -- ^ Name suggestion to be used as a /prefix/ of the name suggestions
      -- for the metas that represent each field
      -> Frozen  -- ^ Should the meta be created frozen?
      -> QName   -- ^ Name of record type
      -> Args    -- ^ Parameters of record type.
      -> Telescope -> Permutation -> Args -> TCM Term
    newRecordMetaCtx :: [Char]
    -> Frozen
    -> QName
    -> Args
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> TCM Term
    newRecordMetaCtx [Char]
    pref Frozen
    frozen QName
    r Args
    pars Tele (Dom Type)
    tel Permutation
    perm Args
    ctx = do
      rdef   <- QName -> TCMT IO RecordData
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
    QName -> m RecordData
    getRecordDef QName
    r
      let con = KillRangeT ConHead
    forall a. KillRange a => KillRangeT a
    killRange KillRangeT ConHead -> KillRangeT ConHead
    forall a b. (a -> b) -> a -> b
    $ RecordData -> ConHead
    _recConHead RecordData
    rdef
      -- Get the record field types as telescope.
      let ftel = Tele (Dom Type) -> Args -> Tele (Dom Type)
    forall t. Apply t => t -> Args -> t
    apply (RecordData -> Tele (Dom Type)
    _recTel RecordData
    rdef) Args
    pars
      fields <- newArgsMetaCtx'' pref frozen trueCondition
                  (telePi_ ftel __DUMMY_TYPE__) tel perm ctx
      return $ Con con ConOSystem (map Apply fields)

    newQuestionMark :: InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
    newQuestionMark :: InteractionId -> Comparison -> Type -> TCMT IO (MetaId, Term)
    newQuestionMark InteractionId
    ii Comparison
    cmp = (Comparison -> Type -> TCMT IO (MetaId, Term))
    -> InteractionId -> Comparison -> Type -> TCMT IO (MetaId, Term)
    newQuestionMark' (RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
    forall (m :: * -> *).
    MonadMetaSolver m =>
    RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
    newValueMeta' RunMetaOccursCheck
    RunMetaOccursCheck) InteractionId
    ii Comparison
    cmp

    -- Since we are type-checking some code twice, e.g., record declarations
    -- for the sake of the record constructor type and then again for the sake
    -- of the record module (issue #434), we may encounter an interaction point
    -- for which we already have a meta.  In this case, we want to reuse the meta.
    -- Otherwise we get two meta for one interaction point which are not connected,
    -- and e.g. Agda might solve one in some way
    -- and the user the other in some other way...
    --
    -- New reference: Andreas, 2021-07-21, issues #5478 and #5463
    -- Old reference: Andreas, 2016-07-29, issue 1720-2
    -- See also: issue #2257
    newQuestionMark'
      :: (Comparison -> Type -> TCM (MetaId, Term))
      -> InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
    newQuestionMark' :: (Comparison -> Type -> TCMT IO (MetaId, Term))
    -> InteractionId -> Comparison -> Type -> TCMT IO (MetaId, Term)
    newQuestionMark' Comparison -> Type -> TCMT IO (MetaId, Term)
    new InteractionId
    ii Comparison
    cmp Type
    t = InteractionId -> TCMT IO (Maybe MetaId)
    forall (m :: * -> *).
    ReadTCState m =>
    InteractionId -> m (Maybe MetaId)
    lookupInteractionMeta InteractionId
    ii TCMT IO (Maybe MetaId)
    -> (Maybe MetaId -> TCMT IO (MetaId, Term))
    -> TCMT IO (MetaId, Term)
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case

      -- Case: new meta.
      Maybe MetaId
    Nothing -> do
        -- Do not run check for recursive occurrence of meta in definitions,
        -- because we want to give the recursive solution interactively (Issue 589)
        (x, m) <- Comparison -> Type -> TCMT IO (MetaId, Term)
    new Comparison
    cmp Type
    t
        connectInteractionPoint ii x
        return (x, m)

      -- Case: existing meta.
      Just MetaId
    x -> do
        -- Get the context Γ in which the meta was created.
        MetaVar
          { mvInfo = MetaInfo{ miClosRange = Closure{ clEnv = TCEnv{ envContext = gamma }}}
          , mvPermutation = p
          } <- MetaVariable -> Maybe MetaVariable -> MetaVariable
    forall a. a -> Maybe a -> a
    fromMaybe MetaVariable
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe MetaVariable -> MetaVariable)
    -> TCMT IO (Maybe MetaVariable) -> TCMT IO MetaVariable
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO (Maybe MetaVariable)
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe MetaVariable)
    lookupLocalMeta' MetaId
    x
        -- Get the current context Δ.
        delta <- getContext
        -- A bit hazardous:
        -- we base our decisions on the names of the context entries.
        -- Ideally, Agda would organize contexts in ancestry trees
        -- with substitutions to move between parent and child.
        let gxs  = Context -> [Name]
    contextNames' Context
    gamma
        let dxs  = Context -> [Name]
    contextNames' Context
    delta
        let gys  = (Name -> Name) -> [Name] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Name
    nameCanonical [Name]
    gxs
        let dys  = (Name -> Name) -> [Name] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Name
    nameCanonical [Name]
    dxs
        let glen = [Name] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Name]
    gxs
        let dlen = [Name] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Name]
    dxs
        reportSDoc "tc.interaction" 20 $ vcat
          [ "reusing meta"
          , nest 2 $ "creation context:" <+> pretty gxs
          , nest 2 $ "reusage  context:" <+> pretty dxs
          ]

        -- When checking a record declaration (e.g. Σ), creation context Γ
        -- might be of the forms Γ₀,Γ₁ or Γ₀,fst,Γ₁ or Γ₀,fst,snd,Γ₁ whereas
        -- Δ is of the form Γ₀,r,Γ₁,{Δ₂} for record variable r.
        -- So first find the record variable in Δ.
        rev_args <- case List.findIndex nameIsRecordName dxs of

          -- Case: no record variable in the context.
          -- Test whether Δ is an extension of Γ.
          Maybe Nat
    Nothing -> do
            Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ([Name]
    gys [Name] -> [Name] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `List.isSuffixOf` [Name]
    dys) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "impossible" 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
    vcat
                [ TCMT IO Doc
    "expecting meta-creation context"
                , 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
    $ [Name] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Name]
    gxs
                , TCMT IO Doc
    "to be a suffix of the meta-reuse context"
                , 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
    $ [Name] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Name]
    dxs
                ]
              [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "impossible" Nat
    70 (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
    "expecting meta-creation context"
                , 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
    $ ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> ([Name] -> [Char]) -> [Name] -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Name] -> [Char]
    forall a. Show a => a -> [Char]
    show) [Name]
    gxs
                , TCMT IO Doc
    "to be a suffix of the meta-reuse context"
                , 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
    $ ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> ([Name] -> [Char]) -> [Name] -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Name] -> [Char]
    forall a. Show a => a -> [Char]
    show) [Name]
    dxs
                ]
              TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            -- Apply the meta to |Γ| arguments from Δ.
            [Term] -> TCMT IO [Term]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Term] -> TCMT IO [Term]) -> [Term] -> TCMT IO [Term]
    forall a b. (a -> b) -> a -> b
    $ (Nat -> Term) -> [Nat] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Nat -> Term
    var [Nat
    dlen Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    glen .. Nat
    dlen Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1]

          -- Case: record variable in the context.
          Just Nat
    k -> do
            -- Verify that the contexts relate as expected.
            let g0len :: Nat
    g0len = [Name] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Name]
    dxs Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    k Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1
            -- Find out the Δ₂ and Γ₁ parts.
            -- However, as they do not share common ancestry, the @nameId@s differ,
            -- so we consider only the original concrete names in gys and dys.
            -- This is a bit risky... blame goes to #434.
            let (Nat
    d2len, Nat
    g1len) = [Name] -> [Name] -> (Nat, Nat)
    forall a. Eq a => [a] -> [a] -> (Nat, Nat)
    findOverlap (Nat -> [Name] -> [Name]
    forall a. Nat -> [a] -> [a]
    take Nat
    k [Name]
    dys) [Name]
    gys
            [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.interaction" 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] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (TCMT IO Doc -> TCMT IO Doc) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2)
              [ TCMT IO Doc
    "glen  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Nat -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Nat
    glen
              , TCMT IO Doc
    "g0len =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Nat -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Nat
    g0len
              , TCMT IO Doc
    "g1len =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Nat -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Nat
    g1len
              , TCMT IO Doc
    "d2len =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Nat -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Nat
    d2len
              ]
            -- The Γ₀ part should match.
            Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (Nat -> [Name] -> [Name]
    forall a. Nat -> [a] -> [a]
    drop (Nat
    glen Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    g0len) [Name]
    gxs [Name] -> [Name] -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat -> [Name] -> [Name]
    forall a. Nat -> [a] -> [a]
    drop (Nat
    k Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) [Name]
    dxs) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "impossible" 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
    vcat
                [ TCMT IO Doc
    "expecting meta-creation context (with fields instead of record var)"
                , 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
    $ [Name] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Name]
    gxs
                , TCMT IO Doc
    "to share ancestry (suffix) with the meta-reuse context (with record var)"
                , 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
    $ [Name] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Name]
    dxs
                ]
              TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            -- The Γ₁ part should match.
            Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ( ([Name] -> [Name] -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) ([Name] -> [Name] -> Bool)
    -> ([Name] -> [Name]) -> [Name] -> [Name] -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` Nat -> [Name] -> [Name]
    forall a. Nat -> [a] -> [a]
    take Nat
    g1len) [Name]
    gys (Nat -> [Name] -> [Name]
    forall a. Nat -> [a] -> [a]
    drop Nat
    d2len [Name]
    dys) ) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "impossible" 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
    vcat
                [ TCMT IO Doc
    "expecting meta-creation context (with fields instead of record var)"
                , 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
    $ [Name] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Name]
    gxs
                , TCMT IO Doc
    "to be an expansion of the meta-reuse context (with record var)"
                , 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
    $ [Name] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Name]
    dxs
                ]
              TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            let ([Term]
    vs1, Term
    v : [Term]
    vs0) = Nat -> [Term] -> ([Term], [Term])
    forall a. Nat -> [a] -> ([a], [a])
    splitAt Nat
    g1len ([Term] -> ([Term], [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
    d2len..Nat
    dlenNat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    -Nat
    1]
            -- We need to expand the record var @v@ into the correct number of fields.
            let numFields :: Nat
    numFields = Nat
    glen Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    g1len Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    g0len
            if Nat
    numFields Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Nat
    0 then [Term] -> TCMT IO [Term]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Term] -> TCMT IO [Term]) -> [Term] -> TCMT IO [Term]
    forall a b. (a -> b) -> a -> b
    $ [Term]
    vs1 [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term]
    vs0 else do
              -- Get the record type.
              let t :: Type
    t = (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom (Dom Type -> Type)
    -> (ContextEntry -> Dom Type) -> ContextEntry -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ContextEntry -> Dom Type
    ctxEntryDom) (ContextEntry -> Type) -> ContextEntry -> Type
    forall a b. (a -> b) -> a -> b
    $ ContextEntry -> Maybe ContextEntry -> ContextEntry
    forall a. a -> Maybe a -> a
    fromMaybe ContextEntry
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe ContextEntry -> ContextEntry)
    -> Maybe ContextEntry -> ContextEntry
    forall a b. (a -> b) -> a -> b
    $ Context
    delta Context -> Nat -> Maybe ContextEntry
    forall a. [a] -> Nat -> Maybe a
    !!! Nat
    k
              -- Get the record field names.
              fs <- Type -> TCM [Dom QName]
    getRecordTypeFields Type
    t
              -- Field arguments to the original meta are projections from the record var.
              let vfs = (Dom QName -> Term) -> [Dom QName] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map ((\ QName
    x -> Term
    v Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [ProjOrigin -> QName -> Elim
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    x]) (QName -> Term) -> (Dom QName -> QName) -> Dom QName -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom QName -> QName
    forall t e. Dom' t e -> e
    unDom) [Dom QName]
    fs
              -- These are the final args to the original meta:
              return $ vs1 ++ reverse (take numFields vfs) ++ vs0

        -- Use ArgInfo from Γ.
        let args = (Term -> Arg Term -> Arg Term) -> [Term] -> Args -> Args
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Term -> Arg Term -> Arg Term
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    (<$) ([Term] -> [Term]
    forall a. [a] -> [a]
    reverse [Term]
    rev_args) (Args -> Args) -> Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Context -> Args
    contextArgs Context
    gamma
        -- Take the permutation into account (see TC.Monad.MetaVars.getMetaContextArgs).
        let vs = Permutation -> Args -> Args
    forall a. Permutation -> [a] -> [a]
    permute (Nat -> Permutation -> Permutation
    takeP (Args -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Args
    args) Permutation
    p) Args
    args
        reportSDoc "tc.interaction" 20 $ vcat
          [ "meta reuse arguments:" <+> prettyTCM vs ]
        return (x, MetaV x $ map Apply vs)

    {-# SPECIALIZE blockTerm :: Type -> TCM Term -> TCM Term #-}
    -- | Construct a blocked constant if there are constraints.
    blockTerm
      :: (MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m, MonadFresh ProblemId m)
      => Type -> m Term -> m Term
    blockTerm :: forall (m :: * -> *).
    (MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m,
     MonadFresh ProblemId m) =>
    Type -> m Term -> m Term
    blockTerm Type
    t m Term
    blocker = do
      (pid, v) <- m Term -> m (ProblemId, Term)
    forall (m :: * -> *) a.
    (MonadFresh ProblemId m, MonadConstraint m) =>
    m a -> m (ProblemId, a)
    newProblem m Term
    blocker
      blockTermOnProblem t v pid

    {-# SPECIALIZE blockTermOnProblem :: Type -> Term -> ProblemId -> TCM Term #-}
    blockTermOnProblem
      :: (MonadMetaSolver m, MonadFresh Nat m)
      => Type -> Term -> ProblemId -> m Term
    blockTermOnProblem :: forall (m :: * -> *).
    (MonadMetaSolver m, MonadFresh Nat m) =>
    Type -> Term -> ProblemId -> m Term
    blockTermOnProblem Type
    t Term
    v ProblemId
    pid = do
      -- Andreas, 2012-09-27 do not block on unsolved size constraints
      solved <- ProblemId -> m Bool
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    ProblemId -> m Bool
    isProblemSolved ProblemId
    pid
      ifM (return solved `or2M` isSizeProblem pid)
          (v <$ reportSLn "tc.meta.blocked" 20 ("Not blocking because " ++ show pid ++ " is " ++
                                                if solved then "solved" else "a size problem")) $ do
        i   <- createMetaInfo
        es  <- map Apply <$> getContextArgs
        tel <- getContextTelescope
        x   <- newMeta' (BlockedConst $ abstract tel v)
                        Instantiable
                        i
                        lowMetaPriority
                        (idP $ size tel)
                        (HasType () CmpLeq $ telePi_ tel t)
                        -- we don't instantiate blocked terms
        inTopContext $ addConstraint (unblockOnProblem pid) (UnBlock x)
        reportSDoc "tc.meta.blocked" 20 $ vcat
          [ "blocked" <+> prettyTCM x <+> ":=" <+> inTopContext
            (prettyTCM $ abstract tel v)
          , "     by" <+> (prettyTCM =<< getConstraintsForProblem pid)
          ]
        inst <- isInstantiatedMeta x
        if inst
          then instantiate (MetaV x es)
          else do
            -- We don't return the blocked term instead create a fresh metavariable
            -- that we compare against the blocked term once it's unblocked. This way
            -- blocked terms can be instantiated before they are unblocked, thus making
            -- constraint solving a bit more robust against instantiation order.
            -- Andreas, 2015-05-22: DontRunMetaOccursCheck to avoid Issue585-17.
            (m', v) <- newValueMeta DontRunMetaOccursCheck CmpLeq t
            reportSDoc "tc.meta.blocked" 30
              $   "setting twin of"
              <+> prettyTCM m'
              <+> "to be"
              <+> prettyTCM x
            updateMetaVar m' (\MetaVariable
    mv -> MetaVariable
    mv { mvTwin = Just x })
            i   <- fresh
            -- This constraint is woken up when unblocking, so it doesn't need a problem id.
            cmp <- buildProblemConstraint_ (unblockOnMeta x) (ValueCmp CmpEq (AsTermsOf t) v (MetaV x es))
            reportSDoc "tc.constr.add" 20 $ "adding constraint" <+> prettyTCM cmp
            listenToMeta (CheckConstraint i cmp) x
            return v

    {-# SPECIALIZE blockTypeOnProblem :: Type -> ProblemId -> TCM Type #-}
    blockTypeOnProblem
      :: (MonadMetaSolver m, MonadFresh Nat m)
      => Type -> ProblemId -> m Type
    blockTypeOnProblem :: forall (m :: * -> *).
    (MonadMetaSolver m, MonadFresh Nat m) =>
    Type -> ProblemId -> m Type
    blockTypeOnProblem (El Sort
    s Term
    a) ProblemId
    pid = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Term -> ProblemId -> m Term
    forall (m :: * -> *).
    (MonadMetaSolver m, MonadFresh Nat m) =>
    Type -> Term -> ProblemId -> m Term
    blockTermOnProblem (Sort -> Type
    sort Sort
    s) Term
    a ProblemId
    pid

    -- | @unblockedTester t@ returns a 'Blocker' for @t@.
    --
    --   Auxiliary function used when creating a postponed type checking problem.
    unblockedTester :: Type -> TCM Blocker
    unblockedTester :: Type -> TCM Blocker
    unblockedTester Type
    t = Type
    -> (Blocker -> Type -> TCM Blocker)
    -> (NotBlocked -> Type -> TCM Blocker)
    -> TCM Blocker
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked Type
    t (\ Blocker
    b Type
    _ -> Blocker -> TCM Blocker
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Blocker
    b) (\ NotBlocked
    _ Type
    _ -> Blocker -> TCM Blocker
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Blocker
    alwaysUnblock)

    -- | Create a postponed type checking problem @e : t@ that waits for type @t@
    --   to unblock (become instantiated or its constraints resolved).
    postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
    postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
    postponeTypeCheckingProblem_ TypeCheckingProblem
    p = do
      TypeCheckingProblem -> Blocker -> TCM Term
    postponeTypeCheckingProblem TypeCheckingProblem
    p (Blocker -> TCM Term) -> TCM Blocker -> TCM Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TypeCheckingProblem -> TCM Blocker
    unblock TypeCheckingProblem
    p
      where
        unblock :: TypeCheckingProblem -> TCM Blocker
    unblock (CheckExpr Comparison
    _ Expr
    _ Type
    t)         = Type -> TCM Blocker
    unblockedTester Type
    t
        unblock (CheckArgs Comparison
    _ ExpandHidden
    _ Expr
    _ [NamedArg Expr]
    _ Type
    t Type
    _ ArgsCheckState CheckedTarget -> TCM Term
    _) = Type -> TCM Blocker
    unblockedTester Type
    t  -- The type of the head of the application.
        unblock (CheckProjAppToKnownPrincipalArg Comparison
    _ Expr
    _ ProjOrigin
    _ List1 QName
    _ Expr
    _ [NamedArg Expr]
    _ Type
    _ Nat
    _ Term
    _ Type
    t PrincipalArgTypeMetas
    _) = Type -> TCM Blocker
    unblockedTester Type
    t -- The type of the principal argument
        unblock (CheckLambda Comparison
    _ Arg (List1 (WithHiding Name), Maybe Type)
    _ Expr
    _ Type
    t)     = Type -> TCM Blocker
    unblockedTester Type
    t
        unblock (DoQuoteTerm Comparison
    _ Term
    _ Type
    _)       = TCM Blocker
    forall a. HasCallStack => a
    __IMPOSSIBLE__     -- also quoteTerm problems
        unblock (DisambiguateConstructor ConstructorDisambiguationData
    _ ConHead -> TCM Term
    _) = TCM Blocker
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- Used with explicit blocker only.

    -- | Create a postponed type checking problem @e : t@ that waits for conditon
    --   @unblock@.  A new meta is created in the current context that has as
    --   instantiation the postponed type checking problem.  An 'UnBlock' constraint
    --   is added for this meta, which links to this meta.
    postponeTypeCheckingProblem :: TypeCheckingProblem -> Blocker -> TCM Term
    postponeTypeCheckingProblem :: TypeCheckingProblem -> Blocker -> TCM Term
    postponeTypeCheckingProblem TypeCheckingProblem
    p Blocker
    unblock | Blocker
    unblock Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    == Blocker
    alwaysUnblock = do
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "impossible" Nat
    2 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Postponed without blocker:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> TypeCheckingProblem -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => TypeCheckingProblem -> m Doc
    prettyTCM TypeCheckingProblem
    p
      TCM Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    postponeTypeCheckingProblem TypeCheckingProblem
    p Blocker
    unblock = do
      i   <- RunMetaOccursCheck -> TCMT IO MetaInfo
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    RunMetaOccursCheck -> m MetaInfo
    createMetaInfo' RunMetaOccursCheck
    DontRunMetaOccursCheck
      tel <- getContextTelescope
      cl  <- buildClosure p
      let t = TypeCheckingProblem -> Type
    problemType TypeCheckingProblem
    p
      m   <- newMeta' (PostponedTypeCheckingProblem cl)
                      Instantiable i normalMetaPriority (idP (size tel))
             $ HasType () CmpLeq $ telePi_ tel t
      inTopContext $ reportSDoc "tc.meta.postponed" 20 $ vcat
        [ "new meta" <+> prettyTCM m <+> ":" <+> prettyTCM (telePi_ tel t)
        , "for postponed typechecking problem" <+> prettyTCM p
        ]

      -- Create the meta that we actually return
      -- Andreas, 2012-03-15
      -- This is an alias to the pptc meta, in order to allow pruning (issue 468)
      -- and instantiation.
      -- Since this meta's solution comes from user code, we do not need
      -- to run the extended occurs check (metaOccurs) to exclude
      -- non-terminating solutions.
      es  <- map Apply <$> getContextArgs
      (_, v) <- newValueMeta DontRunMetaOccursCheck CmpLeq t
      cmp <- buildProblemConstraint_ (unblockOnMeta m) (ValueCmp CmpEq (AsTermsOf t) v (MetaV m es))
      reportSDoc "tc.constr.add" 20 $ "adding constraint" <+> prettyTCM cmp
      i   <- liftTCM fresh
      listenToMeta (CheckConstraint i cmp) m
      addConstraint unblock (UnBlock m)
      return v

    -- | Type of the term that is produced by solving the 'TypeCheckingProblem'.
    problemType :: TypeCheckingProblem -> Type
    problemType :: TypeCheckingProblem -> Type
    problemType (CheckExpr Comparison
    _ Expr
    _ Type
    t         ) = Type
    t
    problemType (CheckArgs Comparison
    _ ExpandHidden
    _ Expr
    _ [NamedArg Expr]
    _ Type
    _ Type
    t ArgsCheckState CheckedTarget -> TCM Term
    _ ) = Type
    t  -- The target type of the application.
    problemType (CheckProjAppToKnownPrincipalArg Comparison
    _ Expr
    _ ProjOrigin
    _ List1 QName
    _ Expr
    _ [NamedArg Expr]
    _ Type
    t Nat
    _ Term
    _ Type
    _ PrincipalArgTypeMetas
    _) = Type
    t -- The target type of the application
    problemType (CheckLambda Comparison
    _ Arg (List1 (WithHiding Name), Maybe Type)
    _ Expr
    _ Type
    t     ) = Type
    t
    problemType (DoQuoteTerm Comparison
    _ Term
    _ Type
    t)        = Type
    t
    problemType (DisambiguateConstructor (ConstructorDisambiguationData QName
    _ List1 (QName, Type, ConHead)
    _ [NamedArg Expr]
    _ Type
    t) ConHead -> TCM Term
    _) = Type
    t

    -- | Eta-expand a local meta-variable, if it is of the specified kind.
    --   Don't do anything if the meta-variable is a blocked term.
    etaExpandMetaTCM :: [MetaClass] -> MetaId -> TCM ()
    etaExpandMetaTCM :: [MetaClass] -> MetaId -> TCM ()
    etaExpandMetaTCM [MetaClass]
    kinds MetaId
    m = TCM Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM ((Bool -> Bool
    not (Bool -> Bool) -> TCM Bool -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCM Bool
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m Bool
    isFrozen MetaId
    m) TCM Bool -> TCM Bool -> TCM Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` (TCEnv -> Bool) -> TCM Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envAssignMetas TCM Bool -> TCM Bool -> TCM Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` [MetaClass] -> MetaId -> TCM Bool
    isEtaExpandable [MetaClass]
    kinds MetaId
    m) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Nat -> [Char] -> TCM () -> TCM ()
    forall a. [Char] -> Nat -> [Char] -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m a -> m a
    verboseBracket [Char]
    "tc.meta.eta" Nat
    20 ([Char]
    "etaExpandMeta " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ MetaId -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow MetaId
    m) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        let waitFor :: Blocker -> TCM ()
    waitFor Blocker
    b = do
              [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.eta" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
                TCMT IO Doc
    "postponing eta-expansion of meta variable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                  MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                  TCMT IO Doc
    "which is blocked by" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Blocker -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
    prettyTCM Blocker
    b
              (MetaId -> TCM ()) -> Set MetaId -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Listener -> MetaId -> TCM ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    Listener -> MetaId -> m ()
    listenToMeta (MetaId -> Listener
    EtaExpand MetaId
    m)) (Set MetaId -> TCM ()) -> Set MetaId -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Set MetaId
    allBlockingMetas Blocker
    b
            dontExpand :: TCM ()
    dontExpand = do
              [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.eta" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
                TCMT IO Doc
    "we do not expand meta variable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
                  [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    "(requested was expansion of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [MetaClass] -> [Char]
    forall a. Show a => a -> [Char]
    show [MetaClass]
    kinds [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ")")
        meta <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    m
        case mvJudgement meta of
          IsSort{} -> TCM ()
    dontExpand
          HasType MetaId
    _ Comparison
    cmp Type
    a -> do

            [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.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
    sep
              [ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "considering eta-expansion at type "
              , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a
              , [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    " raw: "
              , Type -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Type
    a
              ]

            TelV tel b <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    a
            reportSDoc "tc.meta.eta" 40 $ sep
              [ text "considering eta-expansion at type"
              , addContext tel (prettyTCM b)
              , text "under telescope"
              , prettyTCM tel
              ]

            -- Eta expanding metas with a domFinite will just make sure
            -- they go unsolved: conversion will compare them at the
            -- different cases for the domain, so it will not find the
            -- solution for the whole meta.
            if any domIsFinite (flattenTel tel) then dontExpand else do

            -- Issue #3774: continue with the right context for b
            addContext tel $ do

            -- if the target type @b@ of @m@ is a meta variable @x@ itself
            -- (@NonBlocked (MetaV{})@),
            -- or it is blocked by a meta-variable @x@ (@Blocked@), we cannot
            -- eta expand now, we have to postpone this.  Once @x@ is
            -- instantiated, we can continue eta-expanding m.  This is realized
            -- by adding @m@ to the listeners of @x@.
            ifBlocked (unEl b) (\ Blocker
    x Term
    _ -> Blocker -> TCM ()
    waitFor Blocker
    x) $ \ NotBlocked
    _ Term
    t -> case Term
    t of
              lvl :: Term
    lvl@(Def QName
    r Elims
    es) ->
                TCM Bool -> TCM () -> TCM () -> TCM ()
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> TCM Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isEtaRecord QName
    r) {- then -} (do
                  let ps :: Args
    ps = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
                  let expand :: TCM ()
    expand = do
                        u <- MetaVariable -> TCM Term -> TCM Term
    forall (m :: * -> *) a.
    (MonadTCEnv m, ReadTCState m, MonadTrace m) =>
    MetaVariable -> m a -> m a
    withMetaInfo' MetaVariable
    meta (TCM Term -> TCM Term) -> TCM Term -> TCM Term
    forall a b. (a -> b) -> a -> b
    $
                          [Char]
    -> Frozen
    -> QName
    -> Args
    -> Tele (Dom Type)
    -> Permutation
    -> Args
    -> TCM Term
    newRecordMetaCtx (MetaInfo -> [Char]
    miNameSuggestion (MetaVariable -> MetaInfo
    mvInfo MetaVariable
    meta))
                            (MetaVariable -> Frozen
    mvFrozen MetaVariable
    meta) QName
    r Args
    ps Tele (Dom Type)
    tel (Nat -> Permutation
    idP (Nat -> Permutation) -> Nat -> Permutation
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel) (Args -> TCM Term) -> Args -> TCM Term
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Args
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    tel
                        -- Andreas, 2019-03-18, AIM XXIX, issue #3597
                        -- When meta is frozen instantiate it with in-turn frozen metas.
                        inTopContext $ do
                          reportSDoc "tc.meta.eta" 15 $ sep
                              [ "eta expanding: " <+> pretty m <+> " --> "
                              , nest 2 $ prettyTCM u
                              ]
                          -- Andreas, 2012-03-29: No need for occurrence check etc.
                          -- we directly assign the solution for the meta
                          -- 2012-05-23: We also bypass the check for frozen.
                          noConstraints $ assignTerm' m (telToArgs tel) u  -- should never produce any constraints
                  if MetaClass
    Records MetaClass -> [MetaClass] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [MetaClass]
    kinds then
                    TCM ()
    expand
                   else if (MetaClass
    SingletonRecords MetaClass -> [MetaClass] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [MetaClass]
    kinds) then
                    (Blocker -> TCM ()) -> TCM () -> TCM ()
    forall a. (Blocker -> TCMT IO a) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadBlock m =>
    (Blocker -> m a) -> m a -> m a
    catchPatternErr (\Blocker
    x -> Blocker -> TCM ()
    waitFor Blocker
    x) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
                     TCM Bool -> TCM () -> TCM () -> TCM ()
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> Args -> TCM Bool
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    QName -> Args -> m Bool
    isSingletonRecord QName
    r Args
    ps) TCM ()
    expand TCM ()
    dontExpand
                    else TCM ()
    dontExpand
                ) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ {- else -} TCM Bool -> TCM () -> TCM () -> TCM ()
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ([TCM Bool] -> TCM Bool
    forall (f :: * -> *) (m :: * -> *).
    (Foldable f, Monad m) =>
    f (m Bool) -> m Bool
    andM [ Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> TCM Bool) -> Bool -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ MetaClass
    Levels MetaClass -> [MetaClass] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [MetaClass]
    kinds
                                , TCM Bool
    forall (m :: * -> *). HasOptions m => m Bool
    typeInType
                                , (Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    lvl Maybe Term -> Maybe Term -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Maybe Term -> Bool) -> TCMT IO (Maybe Term) -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> TCMT IO (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinLevel
                                ]) (do
                  [Char] -> Nat -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.eta" Nat
    20 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Expanding level meta to 0 (type-in-type)"
                  -- Andreas, 2012-03-30: No need for occurrence check etc.
                  -- we directly assign the solution for the meta
                  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
    $ MetaId -> [Arg [Char]] -> Term -> TCM ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    MetaId -> [Arg [Char]] -> Term -> m ()
    assignTerm MetaId
    m (Tele (Dom Type) -> [Arg [Char]]
    forall a. TelToArgs a => a -> [Arg [Char]]
    telToArgs Tele (Dom Type)
    tel) (Term -> TCM ()) -> Term -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Level -> Term
    Level (Level -> Term) -> Level -> Term
    forall a b. (a -> b) -> a -> b
    $ Integer -> Level
    ClosedLevel Integer
    0
               ) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ {- else -} TCM ()
    dontExpand
              Term
    _ -> TCM ()
    dontExpand

    -- | Eta expand blocking metavariables of record type, and reduce the
    -- blocked thing.

    etaExpandBlocked :: (MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t)
                     => Blocked t -> m (Blocked t)
    etaExpandBlocked :: forall (m :: * -> *) t.
    (MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t) =>
    Blocked t -> m (Blocked t)
    etaExpandBlocked t :: Blocked t
    t@NotBlocked{} = Blocked t -> m (Blocked t)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Blocked t
    t
    etaExpandBlocked t :: Blocked t
    t@(Blocked Blocker
    _ t
    v) | Just{} <- t -> Maybe MetaId
    forall a. IsMeta a => a -> Maybe MetaId
    isMeta t
    v = Blocked t -> m (Blocked t)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Blocked t
    t
    etaExpandBlocked (Blocked Blocker
    b t
    t)  = do
      [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.eta" Nat
    30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Eta expanding blockers" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Blocker -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Blocker
    b
      (MetaId -> m ()) -> Set MetaId -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ ([MetaClass] -> MetaId -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    [MetaClass] -> MetaId -> m ()
    etaExpandMeta [MetaClass
    Records]) (Set MetaId -> m ()) -> Set MetaId -> m ()
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Set MetaId
    allBlockingMetas Blocker
    b
      t <- t -> m (Blocked t)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB t
    t
      case t of
        Blocked Blocker
    b' t
    _ | Blocker
    b Blocker -> Blocker -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Blocker
    b' -> Blocked t -> m (Blocked t)
    forall (m :: * -> *) t.
    (MonadReduce m, MonadMetaSolver m, IsMeta t, Reduce t) =>
    Blocked t -> m (Blocked t)
    etaExpandBlocked Blocked t
    t
        Blocked t
    _                      -> Blocked t -> m (Blocked t)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Blocked t
    t

    {-# SPECIALIZE assignWrapper :: CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM () #-}
    assignWrapper :: (MonadMetaSolver m, MonadConstraint m, MonadError TCErr m, MonadDebug m, HasOptions m)
                  => CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
    assignWrapper :: forall (m :: * -> *).
    (MonadMetaSolver m, MonadConstraint m, MonadError TCErr m,
     MonadDebug m, HasOptions m) =>
    CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
    assignWrapper CompareDirection
    dir MetaId
    x Elims
    es Term
    v m ()
    doAssign = do
      m Bool -> m () -> m () -> m ()
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM ((TCEnv -> Bool) -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Bool
    envAssignMetas) m ()
    forall {b}. m b
    dontAssign (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ {- else -} do
        [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign" Nat
    10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
          TCMT IO Doc
    "term" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (MetaId -> Elims -> Term
    MetaV MetaId
    x Elims
    es) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char]
    ":" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ CompareDirection -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow CompareDirection
    dir) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
        m () -> m ()
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    nowSolvingConstraints m ()
    doAssign m () -> m () -> m ()
    forall e (m :: * -> *) a. MonadError e m => m a -> m () -> m a
    `finally` m ()
    forall (m :: * -> *). MonadConstraint m => m ()
    solveAwakeConstraints

      where dontAssign :: m b
    dontAssign = do
              [Char] -> Nat -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.meta.assign" Nat
    10 [Char]
    "don't assign metas"
              Blocker -> m b
    forall a. Blocker -> m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    alwaysUnblock  -- retry again when we are allowed to instantiate metas

    -- | Miller pattern unification:
    --
    --   @assign dir x vs v a@ solves problem @x vs <=(dir) v : a@ for meta @x@
    --   if @vs@ are distinct variables (linearity check)
    --   and @v@ depends only on these variables
    --   and does not contain @x@ itself (occurs check).
    --
    --   This is the basic story, but we have added some features:
    --
    --   1. Pruning.
    --   2. Benign cases of non-linearity.
    --   3. @vs@ may contain record patterns.
    --
    --   For a reference to some of these extensions, read
    --   Andreas Abel and Brigitte Pientka's TLCA 2011 paper.

    assign :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
    assign :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
    assign CompareDirection
    dir MetaId
    x Args
    args Term
    v CompareAs
    target = Blocker -> TCM () -> TCM ()
    forall (m :: * -> *) a.
    (PureTCM m, MonadBlock m) =>
    Blocker -> m a -> m a
    addOrUnblocker (MetaId -> Blocker
    unblockOnMeta MetaId
    x) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

      mvar <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    x  -- information associated with meta x
      let t = Judgement MetaId -> Type
    forall a. Judgement a -> Type
    jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mvar

      -- Andreas, 2011-05-20 TODO!
      -- full normalization  (which also happens during occurs check)
      -- is too expensive! (see Issue 415)
      -- need to do something cheaper, especially if
      -- we are dealing with a Miller pattern that can be solved
      -- immediately!
      -- Ulf, 2011-08-25 DONE!
      -- Just instantiating the top-level meta, which is cheaper. The occurs
      -- check will first try without unfolding any definitions (treating
      -- arguments to definitions as flexible), if that fails it tries again
      -- with full unfolding.
      reportSDoc "tc.meta.assign" 25 $ "v = " <+> prettyTCM v
      v <- instantiate v
      reportSDoc "tc.meta.assign" 25 $ "v = " <+> prettyTCM v
      reportSDoc "tc.meta.assign" 45 $
        "MetaVars.assign: assigning meta " <+> prettyTCM (MetaV x []) <+>
        " with args " <+> prettyList_ (map (prettyTCM . unArg) args) <+>
        " to " <+> prettyTCM v
      reportSDoc "tc.meta.assign" 45 $
        "MetaVars.assign: type of meta: " <+> prettyTCM t

      reportSDoc "tc.meta.assign" 75 $
        text "MetaVars.assign: assigning meta  " <> pretty x <> text "  with args  " <> pretty args <> text "  to  " <> pretty v

      let
        boundary Term
    v = do
          cubical <- TCMT IO (Maybe Cubical)
    forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
    cubicalOption
          isip <- isInteractionMetaB x args
          case (,) <$> cubical <*> isip of
            Just (Cubical
    _, (MetaId
    x, InteractionId
    ip, Args
    args)) -> CompareDirection
    -> MetaId -> InteractionId -> Args -> Term -> CompareAs -> TCM ()
    tryAddBoundary CompareDirection
    dir MetaId
    x InteractionId
    ip Args
    args Term
    v CompareAs
    target
            Maybe (Cubical, (MetaId, InteractionId, Args))
    _ -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

      case (v, mvJudgement mvar) of
          (Sort Sort
    s, HasType{}) -> Sort -> TCM ()
    hasBiggerSort Sort
    s
          (Term, Judgement MetaId)
    _                   -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

      -- Jesper, 2019-09-13: When --no-sort-comparison is enabled,
      -- we equate the sort of the solution with the sort of the
      -- metavariable, in order to solve metavariables in sorts.
      -- Jesper, 2020-04-22: We do this before any of the other steps
      -- because comparing the sorts might lead to some metavariables
      -- being solved, which can help with pruning (see #4615).
      -- Jesper, 2020-08-25: --no-sort-comparison is now the default
      -- behaviour.
      --
      -- Under most circumstances, the conversion checker guarantees that
      -- the solution for the meta has the correct type, so there is no
      -- need to check anything. However, there are two circumstances in
      -- which we do need to check the type of the solution:
      --
      -- 1. When comparing two types they are not guaranteed to have the
      --    same sort.
      --
      -- 2. When --cumulativity is enabled the same can happen when
      --    comparing two terms at a sort type.

      cumulativity <- optCumulativity <$> pragmaOptions

      let checkSolutionSort Comparison
    cmp Sort
    s Term
    v = do
            s' <- Term -> TCM Sort
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadConstraint m) =>
    Term -> m Sort
    sortOf Term
    v
            reportSDoc "tc.meta.assign" 40 $
              "Instantiating sort" <+> prettyTCM s <+>
              "to sort" <+> prettyTCM s' <+> "of solution" <+> prettyTCM v
            traceCall (CheckMetaSolution (getRange mvar) x (sort s) v) $
              compareSort cmp s' s

      case (target , mvJudgement mvar) of
        -- Case 1 (comparing term to meta as types)
        (AsTypes{}   , HasType MetaId
    _ Comparison
    cmp0 Type
    t) -> do
            let cmp :: Comparison
    cmp   = if Bool
    cumulativity then Comparison
    cmp0 else Comparison
    CmpEq
                abort :: TCMT IO Empty
    abort = Blocker -> TCMT IO Empty
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (Blocker -> TCMT IO Empty) -> TCM Blocker -> TCMT IO Empty
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Blocker -> TCM Blocker
    forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
    updateBlocker (Type -> Blocker
    forall t. AllMetas t => t -> Blocker
    unblockOnAnyMetaIn Type
    t) -- TODO: make piApplyM' compute unblocker
            t' <- TCMT IO Empty -> Type -> Args -> TCM Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> a -> m Type
    forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> Args -> m Type
    piApplyM' TCMT IO Empty
    abort Type
    t Args
    args
            s <- shouldBeSort t'
            checkSolutionSort cmp s v

        -- Case 2 (comparing term to type-level meta as terms, with --cumulativity)
        (AsTermsOf{} , HasType MetaId
    _ Comparison
    cmp Type
    t)
          | Bool
    cumulativity -> do
              let abort :: TCMT IO Empty
    abort = Blocker -> TCMT IO Empty
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (Blocker -> TCMT IO Empty) -> TCM Blocker -> TCMT IO Empty
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Blocker -> TCM Blocker
    forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
    updateBlocker (Type -> Blocker
    forall t. AllMetas t => t -> Blocker
    unblockOnAnyMetaIn Type
    t)
              t' <- TCMT IO Empty -> Type -> Args -> TCM Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> a -> m Type
    forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> Args -> m Type
    piApplyM' TCMT IO Empty
    abort Type
    t Args
    args
              TelV tel t'' <- telView t'
              addContext tel $ ifNotSort t'' (return ()) $ \Sort
    s -> do
                let v' :: Term
    v' = Nat -> Term -> Term
    forall a. Subst a => Nat -> a -> a
    raise (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel) Term
    v Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` Tele (Dom Type) -> Args
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    tel
                Comparison -> Sort -> Term -> TCM ()
    checkSolutionSort Comparison
    cmp Sort
    s Term
    v'

        (AsTypes{}   , IsSort{}       ) -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        (AsTermsOf{} , Judgement MetaId
    _              ) -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        (AsSizes{}   , Judgement MetaId
    _              ) -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()  -- TODO: should we do something similar for sizes?

      -- We don't instantiate frozen mvars
      when (mvFrozen mvar == Frozen) $ do
        reportSLn "tc.meta.assign" 25 $ "aborting: meta is frozen!"
        -- IApplyConfluence can contribute boundary conditions to frozen metas
        boundary v
        patternViolation neverUnblock

      -- We never get blocked terms here anymore. TODO: we actually do. why?
      whenM (isBlockedTerm x) $ do
        reportSLn "tc.meta.assign" 25 $ "aborting: meta is a blocked term!"
        patternViolation (unblockOnMeta x)

      -- Andreas, 2010-10-15 I want to see whether rhs is blocked
      reportSLn "tc.meta.assign" 50 $ "MetaVars.assign: I want to see whether rhs is blocked"
      reportSDoc "tc.meta.assign" 25 $ do
        v0 <- reduceB v
        case v0 of
          Blocked Blocker
    m0 Term
    _ -> TCMT IO Doc
    "r.h.s. blocked on:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Blocker -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
    prettyTCM Blocker
    m0
          NotBlocked{} -> TCMT IO Doc
    "r.h.s. not blocked"
      reportSDoc "tc.meta.assign" 25 $ "v = " <+> prettyTCM v

      -- Turn the assignment problem @_X args >= SizeLt u@ into
      -- @_X args = SizeLt (_Y args@ and constraint
      -- @_Y args >= u@.
      subtypingForSizeLt dir x mvar t args v $ \ Term
    v -> do

        [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign" Nat
    25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "v = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
        [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign.proj" Nat
    45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          cxt <- TCMT IO (Tele (Dom Type))
    forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
    getContextTelescope
          vcat
            [ "context before projection expansion"
            , nest 2 $ inTopContext $ prettyTCM cxt
            ]

        -- Normalise and eta contract the arguments to the meta. These are
        -- usually small, and simplifying might let us instantiate more metas.
        -- Also, try to expand away projected vars in meta args.

        Args
    -> (Term, CompareAs)
    -> (Args -> (Term, CompareAs) -> TCM ())
    -> TCM ()
    forall a b c.
    (Pretty a, PrettyTCM a, NoProjectedVar a, ReduceAndEtaContract a,
     PrettyTCM b, TermSubst b) =>
    a -> b -> (a -> b -> TCM c) -> TCM c
    expandProjectedVars Args
    args (Term
    v, CompareAs
    target) ((Args -> (Term, CompareAs) -> TCM ()) -> TCM ())
    -> (Args -> (Term, CompareAs) -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Args
    args (Term
    v, CompareAs
    target) -> do

          [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign.proj" Nat
    45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            cxt <- TCMT IO (Tele (Dom Type))
    forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
    getContextTelescope
            vcat
              [ "context after projection expansion"
              , nest 2 $ inTopContext $ prettyTCM cxt
              ]

          -- Andreas, 2019-11-16, issue #4159:
          -- We would like to save the work we put into expanding projected variables.
          -- However, the Conversion checker speculatively tries some assignment
          -- in some places (e.g. shortcut) and relies on an exception to be thrown
          -- to try other alternatives next.
          -- If we catch the exception here, this (brittle) mechanism will be broken.
          -- Maybe one possibility would be to rethrow the exception with the
          -- new constraint.  Then, further up, it could be decided whether
          -- to discard the new constraint and do something different,
          -- or add the new constraint when postponing.

          -- BEGIN attempt #4159
          -- let constraint = case v of
          --       -- Sort s -> dirToCmp SortCmp dir (MetaS x $ map Apply args) s
          --       _      -> dirToCmp (\ cmp -> ValueCmp cmp target) dir (MetaV x $ map Apply args) v
          -- reportSDoc "tc.meta.assign.catch" 40 $ sep
          --   [ "assign: catching constraint:"
          --   , prettyTCM constraint
          --   ]
          -- -- reportSDoc "tc.meta.assign.catch" 60 $ sep
          -- --   [ "assign: catching constraint:"
          -- --   , pretty constraint
          -- --   ]
          -- reportSDoc "tc.meta.assign.catch" 80 $ sep
          --   [ "assign: catching constraint (raw):"
          --   , (text . show) constraint
          --   ]
          -- catchConstraint constraint $ do
          -- END attempt #4159

          -- Andreas, 2011-04-21 do the occurs check first
          -- e.g. _1 x (suc x) = suc (_2 x y)
          -- even though the lhs is not a pattern, we can prune the y from _2

          let
                    vars :: VarMap
    vars              = Args -> VarMap
    forall a c t. (IsVarSet a c, Singleton Nat c, Free t) => t -> c
    freeVars Args
    args
                    relevantVL :: [Nat]
    relevantVL        = (VarOcc -> Bool) -> VarMap -> [Nat]
    filterVarMapToList VarOcc -> Bool
    forall a. LensRelevance a => a -> Bool
    isRelevant VarMap
    vars
                    shapeIrrelevantVL :: [Nat]
    shapeIrrelevantVL = (VarOcc -> Bool) -> VarMap -> [Nat]
    filterVarMapToList VarOcc -> Bool
    forall a. LensRelevance a => a -> Bool
    isShapeIrrelevant VarMap
    vars
                    irrelevantVL :: [Nat]
    irrelevantVL      = (VarOcc -> Bool) -> VarMap -> [Nat]
    filterVarMapToList ((Bool -> Bool -> Bool)
    -> (VarOcc -> Bool) -> (VarOcc -> Bool) -> VarOcc -> Bool
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 Bool -> Bool -> Bool
    (&&) VarOcc -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant VarOcc -> Bool
    forall o a. LensFlexRig o a => o -> Bool
    isUnguarded) VarMap
    vars
                -- Andreas, 2011-10-06 only irrelevant vars that are direct
                -- arguments to the meta, hence, can be abstracted over, may
                -- appear on the rhs.  (test/fail/Issue483b)
                -- Update 2011-03-27: Also irr. vars under record constructors.
                -- Andreas, 2019-06-25:  The reason is that when solving
                -- @X args = v@ we drop all irrelevant arguments that
                -- are not variables (after flattening of record constructors).
                -- (See isVarOrIrrelevant in inverseSubst.)
                -- Thus, the occurs-check needs to ensure only these variables
                -- are mentioned on the rhs.
                -- In the terminology of free variable analysis, the retained
                -- irrelevant variables are exactly the Unguarded ones.
                -- Jesper, 2019-10-15: This is actually wrong since it
                -- will lead to pruning of metas that should not be
                -- pruned, see #4136.

          [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              let pr :: Term -> m Doc
    pr (Var Nat
    n []) = [Char] -> m Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (Nat -> [Char]
    forall a. Show a => a -> [Char]
    show Nat
    n)
                  pr (Def QName
    c []) = QName -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    c
                  pr Term
    _          = m Doc
    ".."
              in [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
                   [ TCMT IO Doc
    "mvar args:" 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, Foldable t) =>
    t (m Doc) -> m Doc
    sep ((Arg Term -> TCMT IO Doc) -> Args -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Term -> TCMT IO Doc
    forall {m :: * -> *}.
    (MonadFresh NameId m, MonadInteractionPoints m,
     MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
     Semigroup (m Doc)) =>
    Term -> m Doc
    pr (Term -> TCMT IO Doc)
    -> (Arg Term -> Term) -> Arg Term -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    forall e. Arg e -> e
    unArg) Args
    args)
                   , TCMT IO Doc
    "fvars lhs (relevant)        :" 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, Foldable t) =>
    t (m Doc) -> m Doc
    sep ((Nat -> TCMT IO Doc) -> [Nat] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> (Nat -> [Char]) -> Nat -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> [Char]
    forall a. Show a => a -> [Char]
    show) [Nat]
    relevantVL)
                   , TCMT IO Doc
    "fvars lhs (shape-irrelevant):" 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, Foldable t) =>
    t (m Doc) -> m Doc
    sep ((Nat -> TCMT IO Doc) -> [Nat] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> (Nat -> [Char]) -> Nat -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> [Char]
    forall a. Show a => a -> [Char]
    show) [Nat]
    shapeIrrelevantVL)
                   , TCMT IO Doc
    "fvars lhs (irrelevant)      :" 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, Foldable t) =>
    t (m Doc) -> m Doc
    sep ((Nat -> TCMT IO Doc) -> [Nat] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> (Nat -> [Char]) -> Nat -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> [Char]
    forall a. Show a => a -> [Char]
    show) [Nat]
    irrelevantVL)
                   ]

          -- Check that the x doesn't occur in the right hand side.
          -- Prune mvars on rhs such that they can only depend on lhs vars.
          -- Herein, distinguish relevant and irrelevant vars,
          -- since when abstracting irrelevant lhs vars, they may only occur
          -- irrelevantly on rhs.
          -- v <- liftTCM $ occursCheck x (relevantVL, nonstrictVL, irrelevantVL) v
          v <- TCM Term -> TCM Term
    forall a. TCM a -> TCM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Term -> TCM Term) -> TCM Term -> TCM Term
    forall a b. (a -> b) -> a -> b
    $ MetaId -> VarMap -> Term -> TCM Term
    occursCheck MetaId
    x VarMap
    vars Term
    v

          reportSLn "tc.meta.assign" 15 "passed occursCheck"
          reportSDoc "tc.meta.assign" 25 $ "v = " <+> prettyTCM v
          verboseS "tc.meta.assign" 30 $ do
            let n = Term -> Nat
    forall a. TermSize a => a -> Nat
    termSize Term
    v
            when (n > 200) $ reportSDoc "tc.meta.assign" 30 $
              sep [ "size" <+> text (show n)
    --              , nest 2 $ "type" <+> prettyTCM t
                  , nest 2 $ "term" <+> prettyTCM v
                  ]

          -- Check linearity of @ids@
          -- Andreas, 2010-09-24: Herein, ignore the variables which are not
          -- free in v
          -- Ulf, 2011-09-22: we need to respect irrelevant vars as well, otherwise
          -- we'll build solutions where the irrelevant terms are not valid
          let fvs = Term -> VarSet
    forall t. Free t => t -> VarSet
    allFreeVars Term
    v
          reportSDoc "tc.meta.assign" 20 $
            "fvars rhs:" <+> sep (map (text . show) $ VarSet.toList fvs)

          -- Check that the arguments are variables
          mids <- do
            res <- runExceptT $ inverseSubst' (const False) args
            case res of
              -- all args are variables
              Right [(Nat, Term)]
    ids -> do
                [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign" Nat
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                  TCMT IO Doc
    "inverseSubst returns:" 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, Foldable t) =>
    t (m Doc) -> m Doc
    sep (((Nat, Term) -> TCMT IO Doc) -> [(Nat, Term)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Nat, Term) -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [(Nat, Term)]
    ids)
                [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign" Nat
    50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                  TCMT IO Doc
    "inverseSubst returns:" 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, Foldable t) =>
    t (m Doc) -> m Doc
    sep (((Nat, Term) -> TCMT IO Doc) -> [(Nat, Term)] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Nat, Term) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => (Nat, Term) -> m Doc
    prettyTCM [(Nat, Term)]
    ids)
                let boundVars :: VarSet
    boundVars = [Nat] -> VarSet
    VarSet.fromList ([Nat] -> VarSet) -> [Nat] -> VarSet
    forall a b. (a -> b) -> a -> b
    $ ((Nat, Term) -> Nat) -> [(Nat, Term)] -> [Nat]
    forall a b. (a -> b) -> [a] -> [b]
    map (Nat, Term) -> Nat
    forall a b. (a, b) -> a
    fst [(Nat, Term)]
    ids
                if VarSet
    fvs VarSet -> VarSet -> Bool
    `VarSet.isSubsetOf` VarSet
    boundVars
                  then Maybe [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)]))
    -> Maybe [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
    forall a b. (a -> b) -> a -> b
    $ [(Nat, Term)] -> Maybe [(Nat, Term)]
    forall a. a -> Maybe a
    Just [(Nat, Term)]
    ids
                  else Maybe [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe [(Nat, Term)]
    forall a. Maybe a
    Nothing
              -- we have proper values as arguments which could be cased on
              -- here, we cannot prune, since offending vars could be eliminated
              Left (CantInvert Term
    tm) -> Maybe [(Nat, Term)]
    forall a. Maybe a
    Nothing Maybe [(Nat, Term)] -> TCM () -> TCMT IO (Maybe [(Nat, Term)])
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Term -> TCM ()
    boundary Term
    v
              -- we have non-variables, but these are not eliminateable
              Left InvertExcept
    NeutralArg  -> [(Nat, Term)] -> Maybe [(Nat, Term)]
    forall a. a -> Maybe a
    Just ([(Nat, Term)] -> Maybe [(Nat, Term)])
    -> TCMT IO [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> Args -> VarSet -> TCMT IO [(Nat, Term)]
    forall a. MetaId -> Args -> VarSet -> TCM a
    attemptPruning MetaId
    x Args
    args VarSet
    fvs
              -- we have a projected variable which could not be eta-expanded away:
              -- same as neutral
              Left ProjVar{}   -> [(Nat, Term)] -> Maybe [(Nat, Term)]
    forall a. a -> Maybe a
    Just ([(Nat, Term)] -> Maybe [(Nat, Term)])
    -> TCMT IO [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> Args -> VarSet -> TCMT IO [(Nat, Term)]
    forall a. MetaId -> Args -> VarSet -> TCM a
    attemptPruning MetaId
    x Args
    args VarSet
    fvs

          case mids of  -- vv Ulf 2014-07-13: actually not needed after all: attemptInertRHSImprovement x args v
            Maybe [(Nat, Term)]
    Nothing  -> Blocker -> TCM ()
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (Blocker -> TCM ()) -> TCM Blocker -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Blocker -> TCM Blocker
    forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
    updateBlocker (Term -> Blocker
    forall t. AllMetas t => t -> Blocker
    unblockOnAnyMetaIn Term
    v)  -- TODO: more precise
            Just [(Nat, Term)]
    ids -> do
              -- Check linearity
              ids <- do
                res <- ExceptT () (TCMT IO) [(Nat, Term)] -> TCM (Either () [(Nat, Term)])
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT () (TCMT IO) [(Nat, Term)]
     -> TCM (Either () [(Nat, Term)]))
    -> ExceptT () (TCMT IO) [(Nat, Term)]
    -> TCM (Either () [(Nat, Term)])
    forall a b. (a -> b) -> a -> b
    $ [(Nat, Term)] -> ExceptT () (TCMT IO) [(Nat, Term)]
    checkLinearity {- (`VarSet.member` fvs) -} [(Nat, Term)]
    ids
                case res of
                  -- case: linear
                  Right [(Nat, Term)]
    ids -> [(Nat, Term)] -> TCMT IO [(Nat, Term)]
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Nat, Term)]
    ids
                  -- case: non-linear variables that could possibly be pruned
                  -- If pruning fails we need to unblock on any meta in the rhs, since they might get
                  -- rid of the dependency on the non-linear variable. TODO: be more precise (all metas
                  -- using non-linear variables need to be solved).
                  Left ()   -> do
                    block <- Blocker -> TCM Blocker
    forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
    updateBlocker (Blocker -> TCM Blocker) -> Blocker -> TCM Blocker
    forall a b. (a -> b) -> a -> b
    $ Term -> Blocker
    forall t. AllMetas t => t -> Blocker
    unblockOnAnyMetaIn Term
    v
                    addOrUnblocker block $ attemptPruning x args fvs

              -- Check ids is time respecting.
              () <- do
                let idvars = ((Nat, Term) -> (Nat, VarSet)) -> [(Nat, Term)] -> [(Nat, VarSet)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> VarSet) -> (Nat, Term) -> (Nat, VarSet)
    forall b d a. (b -> d) -> (a, b) -> (a, d)
    mapSnd Term -> VarSet
    forall t. Free t => t -> VarSet
    allFreeVars) [(Nat, Term)]
    ids
                -- earlierThan α v := v "arrives" before α
                let earlierThan a
    l a
    j = a
    j a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    > a
    l
                TelV tel' _ <- telViewUpToPath (length args) t
                forM_ ids $ \(Nat
    i,Term
    u) -> do
                  d <- Nat -> TCMT IO (Dom Type)
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Nat -> m (Dom Type)
    domOfBV Nat
    i
                  case getLock (getArgInfo d) of
                    Lock
    IsNotLock -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
                    IsLock{} -> do
                    let us :: VarSet
    us = [VarSet] -> VarSet
    forall (f :: * -> *). Foldable f => f VarSet -> VarSet
    IntSet.unions ([VarSet] -> VarSet) -> [VarSet] -> VarSet
    forall a b. (a -> b) -> a -> b
    $ ((Nat, VarSet) -> VarSet) -> [(Nat, VarSet)] -> [VarSet]
    forall a b. (a -> b) -> [a] -> [b]
    map (Nat, VarSet) -> VarSet
    forall a b. (a, b) -> b
    snd ([(Nat, VarSet)] -> [VarSet]) -> [(Nat, VarSet)] -> [VarSet]
    forall a b. (a -> b) -> a -> b
    $ ((Nat, VarSet) -> Bool) -> [(Nat, VarSet)] -> [(Nat, VarSet)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    earlierThan Nat
    i (Nat -> Bool) -> ((Nat, VarSet) -> Nat) -> (Nat, VarSet) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Nat, VarSet) -> Nat
    forall a b. (a, b) -> a
    fst) [(Nat, VarSet)]
    idvars
                    -- us Earlier than u
                    TCM Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (Tele (Dom Type) -> TCM Bool -> TCM Bool
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Tele (Dom Type) -> m a -> m a
    addContext Tele (Dom Type)
    tel' (TCM Bool -> TCM Bool) -> TCM Bool -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ Term -> VarSet -> TCM Bool
    checkEarlierThan Term
    u VarSet
    us) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                      Blocker -> TCM ()
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (MetaId -> Blocker
    unblockOnMeta MetaId
    x)  -- If the earlier check hard-fails we need to
                                                          -- solve this meta in some other way.

              let n = Args -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Args
    args
              TelV tel' _ <- telViewUpToPath n t

              -- Check subtyping constraints on the context variables.

              -- Intuition: suppose @_X : (x : A) → B@, then to turn
              --   @
              --     Γ(x : A') ⊢ _X x =?= v : B'@
              --   @
              -- into
              --   @
              --     Γ ⊢ _X =?= λ x → v
              --   @
              -- we need to check that @A <: A'@ (due to contravariance).
              let sigma = [Term] -> Substitution
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution) -> [Term] -> Substitution
    forall a b. (a -> b) -> a -> b
    $ [Term] -> [Term]
    forall a. [a] -> [a]
    reverse ([Term] -> [Term]) -> [Term] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Term) -> Args -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg Args
    args
              hasSubtyping <- optCumulativity <$> pragmaOptions
              when hasSubtyping $ forM_ ids $ \(Nat
    i , Term
    u) -> do
                -- @u@ is a (projected) variable, so we can infer its type
                a  <- Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Type)
    sigma (Type -> Type) -> TCM Type -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Tele (Dom Type) -> TCM Type -> TCM Type
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Tele (Dom Type) -> m a -> m a
    addContext Tele (Dom Type)
    tel' (Term -> TCM Type
    forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
    infer Term
    u)
                a' <- typeOfBV i
                checkSubtypeIsEqual a' a
                  `catchError` \case
                    TypeError{} -> Blocker -> TCM ()
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (MetaId -> Blocker
    unblockOnMeta MetaId
    x) -- If the subtype check hard-fails we need to
                    TCErr
    err         -> TCErr -> TCM ()
    forall a. TCErr -> TCMT IO a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err                     -- solve this meta in some other way.

              -- Solve.
              m <- getContextSize
              assignMeta' m x t n ids v
      where
        -- Try to remove meta arguments from lhs that mention variables not occurring on rhs.
        attemptPruning
          :: MetaId  -- Meta-variable (lhs)
          -> Args    -- Meta arguments (lhs)
          -> FVs     -- Variables occuring on the rhs
          -> TCM a
        attemptPruning :: forall a. MetaId -> Args -> VarSet -> TCM a
    attemptPruning MetaId
    x Args
    args VarSet
    fvs = do
          -- non-linear lhs: we cannot solve, but prune
          killResult <- MetaId -> Args -> (Nat -> Bool) -> TCMT IO PruneResult
    forall (m :: * -> *).
    (PureTCM m, MonadMetaSolver m) =>
    MetaId -> Args -> (Nat -> Bool) -> m PruneResult
    prune MetaId
    x Args
    args ((Nat -> Bool) -> TCMT IO PruneResult)
    -> (Nat -> Bool) -> TCMT IO PruneResult
    forall a b. (a -> b) -> a -> b
    $ (Nat -> VarSet -> Bool
    `VarSet.member` VarSet
    fvs)
          let success = PruneResult
    killResult PruneResult -> [PruneResult] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [PruneResult
    PrunedSomething,PruneResult
    PrunedEverything]
          reportSDoc "tc.meta.assign" 10 $
            "pruning" <+> prettyTCM x <+> do text $ if success then "succeeded" else "failed"
          blocker <- if
            | success   -> return alwaysUnblock  -- If pruning succeeded we want to retry right away
            | otherwise -> unblockOnAnyMetaIn . MetaV x . map Apply <$> instantiateFull args
                 -- TODO: could be more precise: only unblock on metas
                 --       applied to offending variables
          patternViolation blocker

    -- | Is the given metavariable application secretly an interaction point
    -- application? Ugly.
    isInteractionMetaB
      :: forall m. (ReadTCState m, MonadReduce m, MonadPretty m)
      => MetaId
      -> Args
      -> m (Maybe (MetaId, InteractionId, Args))
    isInteractionMetaB :: forall (m :: * -> *).
    (ReadTCState m, MonadReduce m, MonadPretty m) =>
    MetaId -> Args -> m (Maybe (MetaId, InteractionId, Args))
    isInteractionMetaB MetaId
    mid Args
    args =
      MaybeT m (MetaId, InteractionId, Args)
    -> m (Maybe (MetaId, InteractionId, Args))
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT m (MetaId, InteractionId, Args)
     -> m (Maybe (MetaId, InteractionId, Args)))
    -> MaybeT m (MetaId, InteractionId, Args)
    -> m (Maybe (MetaId, InteractionId, Args))
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Args -> MaybeT m (MetaId, InteractionId, Args)
    forall {m :: * -> *} {c}.
    ReadTCState m =>
    MetaId -> c -> MaybeT m (MetaId, InteractionId, c)
    here MetaId
    mid Args
    args MaybeT m (MetaId, InteractionId, Args)
    -> MaybeT m (MetaId, InteractionId, Args)
    -> MaybeT m (MetaId, InteractionId, Args)
    forall a. MaybeT m a -> MaybeT m a -> MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus` do
        -- If the meta isn't literally an interaction point it might still
        -- be instantiable to an interaction point, as long as we ignore
        -- blocking
        m Term -> MaybeT m Term
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (Term -> m Term
    instantiateBlockingFull (MetaId -> Elims -> Term
    MetaV MetaId
    mid (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim) -> Args -> Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Args
    args))) MaybeT m Term
    -> (Term -> MaybeT m (MetaId, InteractionId, Args))
    -> MaybeT m (MetaId, InteractionId, Args)
    forall a b. MaybeT m a -> (a -> MaybeT m b) -> MaybeT m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Term -> MaybeT m (MetaId, InteractionId, Args)
    there
      where
        here :: MetaId -> c -> MaybeT m (MetaId, InteractionId, c)
    here MetaId
    mid c
    args = do
          iid <- m (Maybe InteractionId) -> MaybeT m InteractionId
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (MetaId -> m (Maybe InteractionId)
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe InteractionId)
    isInteractionMeta MetaId
    mid)
          pure (mid, iid, args)

        instantiateBlockingFull :: Term -> m Term
    instantiateBlockingFull = Lens' TCState Bool -> (Bool -> Bool) -> m Term -> m Term
    forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
    forall (m :: * -> *) a b.
    ReadTCState m =>
    Lens' TCState a -> (a -> a) -> m b -> m b
    locallyTCState (Bool -> f Bool) -> TCState -> f TCState
    Lens' TCState Bool
    stInstantiateBlocking (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (m Term -> m Term) -> (Term -> m Term) -> Term -> m Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> m Term
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull

        there :: Term -> MaybeT m (MetaId, InteractionId, Args)
        there :: Term -> MaybeT m (MetaId, InteractionId, Args)
    there (MetaV MetaId
    m Elims
    args) = do
          iid  <- m (Maybe InteractionId) -> MaybeT m InteractionId
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (MetaId -> m (Maybe InteractionId)
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Maybe InteractionId)
    isInteractionMeta MetaId
    m)
          args <- MaybeT (pure (allApplyElims args))
          pure (m, iid, args)
        -- It might be the case that the inner meta (the interaction point)
        -- exists in a larger context, so instantiating the outer meta (the
        -- original argument) will produce lambdas.
        --
        -- Since the boundary code runs in the inner, larger context, we can
        -- peel off the lambdas without running afoul of the scope.
        there (Lam ArgInfo
    _ Abs Term
    as) = Term -> MaybeT m (MetaId, InteractionId, Args)
    there (Abs Term -> SubstArg Term -> Term
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp Abs Term
    as (Nat -> Term
    var Nat
    0))
        there Term
    _ = MaybeT m (MetaId, InteractionId, Args)
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

    {- UNUSED
    -- | When faced with @_X us == D vs@ for an inert D we can solve this by
    --   @_X xs := D _Ys@ with new constraints @_Yi us == vi@. This is important
    --   for instance arguments, where knowing the head D might enable progress.
    attemptInertRHSImprovement :: MetaId -> Args -> Term -> TCM ()
    attemptInertRHSImprovement m args v = do
      reportSDoc "tc.meta.inert" 30 $ vcat
        [ "attempting inert rhs improvement"
        , nest 2 $ sep [ prettyTCM (MetaV m $ map Apply args) <+> "=="
                       , prettyTCM v ] ]
      -- Check that the right-hand side has the form D vs, for some inert constant D.
      -- Returns the type of D and a function to build an application of D.
      (a, mkRHS) <- ensureInert v
      -- Check that all arguments to the meta are neutral and does not have head D.
      -- If there are non-neutral arguments there could be solutions to the meta
      -- that computes over these arguments. If D is an argument to the meta we get
      -- multiple solutions (for instance: _M Nat == Nat can be solved by both
      -- _M := \ x -> x and _M := \ x -> Nat).
      mapM_ (ensureNeutral (mkRHS []) . unArg) args
      tel <- theTel <$> (telView =<< getMetaType m)
      -- When attempting shortcut meta solutions, metas aren't necessarily fully
      -- eta expanded. If this is the case we skip inert improvement.
      when (length args < size tel) $ do
        reportSDoc "tc.meta.inert" 30 $ "not fully applied"
        patternViolation
      -- Solve the meta with _M := \ xs -> D (_Y1 xs) .. (_Yn xs), for fresh metas
      -- _Yi.
      metaArgs <- inTopContext $ addContext tel $ newArgsMeta a
      let varArgs = map Apply $ reverse $ zipWith (\i a -> var i <$ a) [0..] (reverse args)
          sol     = mkRHS metaArgs
          argTel  = map ("x" <$) args
      reportSDoc "tc.meta.inert" 30 $ nest 2 $ vcat
        [ "a       =" <+> prettyTCM a
        , "tel     =" <+> prettyTCM tel
        , "metas   =" <+> prettyList (map prettyTCM metaArgs)
        , "sol     =" <+> prettyTCM sol
        ]
      assignTerm m argTel sol
      patternViolation  -- throwing a pattern violation here lets the constraint
                        -- machinery worry about restarting the comparison.
      where
        ensureInert :: Term -> TCM (Type, Args -> Term)
        ensureInert v = do
          let notInert = do
                reportSDoc "tc.meta.inert" 30 $ nest 2 $ "not inert:" <+> prettyTCM v
                patternViolation
              toArgs elims =
                case allApplyElims elims of
                  Nothing -> do
                    reportSDoc "tc.meta.inert" 30 $ nest 2 $ "can't do projections from inert"
                    patternViolation
                  Just args -> return args
          case v of
            Var x elims -> (, Var x . map Apply) <$> typeOfBV x
            Con c ci args  -> notInert -- (, Con c ci) <$> defType <$> getConstInfo (conName c)
            Def f elims -> do
              def <- getConstInfo f
              let good = return (defType def, Def f . map Apply)
              case theDef def of
                Axiom{}       -> good
                Datatype{}    -> good
                Record{}      -> good
                Function{}    -> notInert
                Primitive{}   -> notInert
                Constructor{} -> __IMPOSSIBLE__

            Pi{}       -> notInert -- this is actually inert but improving doesn't buy us anything for Pi
            Lam{}      -> notInert
            Sort{}     -> notInert
            Lit{}      -> notInert
            Level{}    -> notInert
            MetaV{}    -> notInert
            DontCare{} -> notInert

        ensureNeutral :: Term -> Term -> TCM ()
        ensureNeutral rhs v = do
          b <- reduceB v
          let notNeutral v = do
                reportSDoc "tc.meta.inert" 30 $ nest 2 $ "not neutral:" <+> prettyTCM v
                patternViolation
              checkRHS arg
                | arg == rhs = do
                  reportSDoc "tc.meta.inert" 30 $ nest 2 $ "argument shares head with RHS:" <+> prettyTCM arg
                  patternViolation
                | otherwise  = return ()
          case b of
            Blocked{}      -> notNeutral v
            NotBlocked r v ->                      -- Andrea(s) 2014-12-06 can r be useful?
              case v of
                Var x _    -> checkRHS (Var x [])
                Def f _    -> checkRHS (Def f [])
                Pi{}       -> return ()
                Sort{}     -> return ()
                Level{}    -> return ()
                Lit{}      -> notNeutral v
                DontCare{} -> notNeutral v
                Con{}      -> notNeutral v
                Lam{}      -> notNeutral v
                MetaV{}    -> __IMPOSSIBLE__
    -- END UNUSED -}

    -- | @assignMeta m x t ids u@ solves @x ids = u@ for meta @x@ of type @t@,
    --   where term @u@ lives in a context of length @m@.
    --   Precondition: @ids@ is linear.
    assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
    assignMeta :: Nat -> MetaId -> Type -> [Nat] -> Term -> TCM ()
    assignMeta Nat
    m MetaId
    x Type
    t [Nat]
    ids Term
    v = do
      let n :: Nat
    n    = [Nat] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Nat]
    ids
          cand :: [(Nat, Term)]
    cand = [(Nat, Term)] -> [(Nat, Term)]
    forall a. Ord a => [a] -> [a]
    List.sort ([(Nat, Term)] -> [(Nat, Term)]) -> [(Nat, Term)] -> [(Nat, Term)]
    forall a b. (a -> b) -> a -> b
    $ [Nat] -> [Term] -> [(Nat, Term)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Nat]
    ids ([Term] -> [(Nat, Term)]) -> [Term] -> [(Nat, 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
    n
      Nat -> MetaId -> Type -> Nat -> [(Nat, Term)] -> Term -> TCM ()
    assignMeta' Nat
    m MetaId
    x Type
    t Nat
    n [(Nat, Term)]
    cand Term
    v

    -- | @assignMeta' m x t ids u@ solves @x = [ids]u@ for meta @x@ of type @t@,
    --   where term @u@ lives in a context of length @m@,
    --   and @ids@ is a partial substitution.
    assignMeta' :: Int -> MetaId -> Type -> Int -> SubstCand -> Term -> TCM ()
    assignMeta' :: Nat -> MetaId -> Type -> Nat -> [(Nat, Term)] -> Term -> TCM ()
    assignMeta' Nat
    m MetaId
    x Type
    t Nat
    n [(Nat, Term)]
    ids Term
    v = do
      -- we are linear, so we can solve!
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign" Nat
    25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO Doc
    "preparing to instantiate: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v

      -- Rename the variables in v to make it suitable for abstraction over ids.
      -- Basically, if
      --   Γ   = a b c d e
      --   ids = d b e
      -- then
      --   v' = (λ a b c d e. v) _ 1 _ 2 0
      --
      -- Andreas, 2013-10-25 Solve using substitutions:
      -- Convert assocList @ids@ (which is sorted) into substitution,
      -- filling in __IMPOSSIBLE__ for the missing terms, e.g.
      -- [(0,0),(1,2),(3,1)] --> [0, 2, __IMP__, 1, __IMP__]
      -- ALT 1: O(m * size ids), serves as specification
      -- let ivs = [fromMaybe __IMPOSSIBLE__ $ lookup i ids | i <- [0..m-1]]
      -- ALT 2: O(m)
      let assocToList :: Nat -> [(Nat, Term)] -> [Maybe Term]
    assocToList Nat
    i = \case
            [(Nat, Term)]
    _           | Nat
    i Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Nat
    m -> []
            ((Nat
    j,Term
    u) : [(Nat, Term)]
    l) | Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    j -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    u  Maybe Term -> [Maybe Term] -> [Maybe Term]
    forall a. a -> [a] -> [a]
    : Nat -> [(Nat, Term)] -> [Maybe Term]
    assocToList (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) [(Nat, Term)]
    l
            [(Nat, Term)]
    l                    -> Maybe Term
    forall a. Maybe a
    Nothing Maybe Term -> [Maybe Term] -> [Maybe Term]
    forall a. a -> [a] -> [a]
    : Nat -> [(Nat, Term)] -> [Maybe Term]
    assocToList (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) [(Nat, Term)]
    l
          ivs :: [Maybe Term]
    ivs = Nat -> [(Nat, Term)] -> [Maybe Term]
    assocToList Nat
    0 [(Nat, Term)]
    ids
          rho :: Substitution
    rho = Impossible -> [Maybe Term] -> Substitution -> Substitution
    forall a.
    DeBruijn a =>
    Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
    prependS Impossible
    HasCallStack => Impossible
    impossible [Maybe Term]
    ivs (Substitution -> Substitution) -> Substitution -> Substitution
    forall a b. (a -> b) -> a -> b
    $ Nat -> Substitution
    forall a. Nat -> Substitution' a
    raiseS Nat
    n
          v' :: Term
    v'  = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    rho Term
    v

      -- Metas are top-level so we do the assignment at top-level.
      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
    $ do
        -- Andreas, 2011-04-18 to work with irrelevant parameters
        -- we need to construct tel' from the type of the meta variable
        -- (no longer from ids which may not be the complete variable list
        -- any more)
        [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign" Nat
    15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "type of meta =" 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
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t

        (telv@(TelV tel' a), bs) <- Nat -> Type -> TCMT IO (TelV Type, Boundary)
    forall (m :: * -> *).
    PureTCM m =>
    Nat -> Type -> m (TelV Type, Boundary)
    telViewUpToPathBoundary Nat
    n Type
    t
        reportSDoc "tc.meta.assign" 30 $ "tel'  =" <+> prettyTCM tel'
        reportSDoc "tc.meta.assign" 30 $ "#args =" <+> text (show n)
        -- Andreas, 2013-09-17 (AIM XVIII): if t does not provide enough
        -- types for the arguments, it might be blocked by a meta;
        -- then we give up. (Issue 903)
        when (size tel' < n) $ do
          a <- abortIfBlocked a
          reportSDoc "impossible" 10 $ "not enough pis, but not blocked?" <?> pretty a
          __IMPOSSIBLE__   -- If we get here it was _not_ blocked by a meta!

        -- Perform the assignment (and wake constraints).

        let vsol = Tele (Dom Type) -> Term -> Term
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel' Term
    v'

        -- Andreas, 2013-10-25 double check solution before assigning
        whenM (optDoubleCheck  <$> pragmaOptions) $ do
          m <- lookupLocalMeta x
          reportSDoc "tc.meta.check" 30 $ "double checking solution"
          catchConstraint (CheckMetaInst x) $
            addContext tel' $ checkSolutionForMeta x m v' a

        reportSDoc "tc.meta.assign" 10 $
          "solving" <+> prettyTCM x <+> ":=" <+> prettyTCM vsol

        v' <- blockOnBoundary telv bs v'

        assignTerm x (telToArgs tel') v'
      where
        blockOnBoundary :: TelView -> Boundary -> Term -> TCM Term
        blockOnBoundary :: TelV Type -> Boundary -> Term -> TCM Term
    blockOnBoundary TelV Type
    telv         (Boundary []) Term
    v = Term -> TCM Term
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
        blockOnBoundary (TelV Tele (Dom Type)
    tel Type
    t) (Boundary [(Nat, (Term, Term))]
    bs) Term
    v = Tele (Dom Type) -> TCM Term -> TCM Term
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Tele (Dom Type) -> m a -> m a
    addContext Tele (Dom Type)
    tel (TCM Term -> TCM Term) -> TCM Term -> TCM Term
    forall a b. (a -> b) -> a -> b
    $
          Type -> TCM Term -> TCM Term
    forall (m :: * -> *).
    (MonadMetaSolver m, MonadConstraint m, MonadFresh Nat m,
     MonadFresh ProblemId m) =>
    Type -> m Term -> m Term
    blockTerm Type
    t (TCM Term -> TCM Term) -> TCM Term -> TCM Term
    forall a b. (a -> b) -> a -> b
    $ do
            neg <- TCM Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primINeg
            forM_ bs $ \ (Nat
    i,(Term
    x,Term
    y)) -> do
              let r :: Term
    r = Nat -> Term
    var Nat
    i
              Term -> Type -> Term -> Term -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    Term -> Type -> Term -> Term -> m ()
    equalTermOnFace (Term
    neg Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    `apply1` Term
    r) Type
    t Term
    x Term
    v
              Term -> Type -> Term -> Term -> TCM ()
    forall (m :: * -> *).
    MonadConversion m =>
    Term -> Type -> Term -> Term -> m ()
    equalTermOnFace Term
    r  Type
    t Term
    y Term
    v
            return v

    -- | Check that the instantiation of the given metavariable fits the
    --   type of the metavariable. If the metavariable is not yet
    --   instantiated, add a constraint to check the instantiation later.
    checkMetaInst :: MetaId -> TCM ()
    checkMetaInst :: MetaId -> TCM ()
    checkMetaInst MetaId
    x = do
      m <- MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (HasCallStack, MonadDebug m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupLocalMeta MetaId
    x
      let postpone = Blocker -> Constraint -> TCM ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint (MetaId -> Blocker
    unblockOnMeta MetaId
    x) (Constraint -> TCM ()) -> Constraint -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Constraint
    CheckMetaInst MetaId
    x
      case mvInstantiation m of
        BlockedConst{} -> TCM ()
    postpone
        PostponedTypeCheckingProblem{} -> TCM ()
    postpone
        OpenMeta{} -> TCM ()
    postpone
        InstV Instantiation
    inst -> do
          let n :: Nat
    n = [Arg [Char]] -> Nat
    forall a. Sized a => a -> Nat
    size (Instantiation -> [Arg [Char]]
    instTel Instantiation
    inst)
              t :: Type
    t = Judgement MetaId -> Type
    forall a. Judgement a -> Type
    jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    m
          (telv@(TelV tel a),bs) <- Nat -> Type -> TCMT IO (TelV Type, Boundary)
    forall (m :: * -> *).
    PureTCM m =>
    Nat -> Type -> m (TelV Type, Boundary)
    telViewUpToPathBoundary Nat
    n Type
    t
          catchConstraint (CheckMetaInst x) $ addContext tel $
            checkSolutionForMeta x m (instBody inst) a

    -- | Check that the instantiation of the metavariable with the given
    --   term is well-typed.
    checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM ()
    checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM ()
    checkSolutionForMeta MetaId
    x MetaVariable
    m Term
    v Type
    a = do
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.check" Nat
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "checking solution for meta" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    x
      case MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    m of
        HasType{ jComparison :: forall a. Judgement a -> Comparison
    jComparison = Comparison
    cmp } -> do
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.check" Nat
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ 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
    $
            MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    x 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
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a 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
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.check" Nat
    50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ 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
    $ do
            ctx <- TCMT IO Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
            inTopContext $ "in context: " <+> prettyTCM (PrettyContext ctx)
          Call -> TCM () -> TCM ()
    forall a. Call -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> MetaId -> Type -> Term -> Call
    CheckMetaSolution (MetaVariable -> Range
    forall a. HasRange a => a -> Range
    getRange MetaVariable
    m) MetaId
    x Type
    a Term
    v) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            Term -> Comparison -> TypeOf Term -> TCM ()
    forall a (m :: * -> *).
    (CheckInternal a, MonadCheckInternal m) =>
    a -> Comparison -> TypeOf a -> m ()
    forall (m :: * -> *).
    MonadCheckInternal m =>
    Term -> Comparison -> TypeOf Term -> m ()
    checkInternal Term
    v Comparison
    cmp TypeOf Term
    Type
    a
        IsSort{}  -> TCM () -> TCM ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.check" Nat
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ 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
    $
            MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    x 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
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " is a sort"
          s <- Type -> TCM Sort
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m, MonadError TCErr m) =>
    Type -> m Sort
    shouldBeSort (Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    HasCallStack => Sort
    __DUMMY_SORT__ Term
    v)
          traceCall (CheckMetaSolution (getRange m) x (sort (univSort s)) (Sort s)) $
            inferInternal s

    -- | Given two types @a@ and @b@ with @a <: b@, check that @a == b@.
    checkSubtypeIsEqual :: Type -> Type -> TCM ()
    checkSubtypeIsEqual :: Type -> Type -> TCM ()
    checkSubtypeIsEqual Type
    a Type
    b = do
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.subtype" Nat
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "checking that subtype" 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
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    a TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
        TCMT IO Doc
    "of" 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
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    b TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "is actually equal."
      Type
    -> Type
    -> (Type -> Type -> TCM ())
    -> (Type -> Type -> TCM ())
    -> TCM ()
    forall a (m :: * -> *) b.
    (Instantiate a, SynEq a, MonadReduce m) =>
    a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
    SynEq.checkSyntacticEquality Type
    a Type
    b (\Type
    _ Type
    _ -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) ((Type -> Type -> TCM ()) -> TCM ())
    -> (Type -> Type -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \Type
    a Type
    b -> do
        cumulativity <- PragmaOptions -> Bool
    optCumulativity (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
        abortIfBlocked (unEl b) >>= \case
          Sort Sort
    sb -> Term -> TCM Term
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    a) TCM Term -> (Term -> TCM ()) -> TCM ()
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Sort Sort
    sa | Bool
    cumulativity -> Sort -> Sort -> TCM ()
    forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
    equalSort Sort
    sa Sort
    sb
                                 | Bool
    otherwise    -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            Dummy{} -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return () -- TODO: this shouldn't happen but
                                 -- currently does because of generalized
                                 -- metas being created in a dummy context
            Term
    a -> Blocker -> TCM ()
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (Blocker -> TCM ()) -> TCM Blocker -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Blocker -> TCM Blocker
    forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
    updateBlocker (Term -> Blocker
    forall t. AllMetas t => t -> Blocker
    unblockOnAnyMetaIn Term
    a) -- TODO: can this happen?
          Pi Dom Type
    b1 Abs Type
    b2 -> Term -> TCM Term
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    a) TCM Term -> (Term -> TCM ()) -> TCM ()
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Pi Dom Type
    a1 Abs Type
    a2
              | Dom Type -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Dom Type
    a1 Relevance -> Relevance -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Dom Type -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Dom Type
    b1 -> Blocker -> TCM ()
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    neverUnblock -- Can we recover from this?
              | Dom Type -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity  Dom Type
    a1 Quantity -> Quantity -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Dom Type -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity  Dom Type
    b1 -> Blocker -> TCM ()
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    neverUnblock
              | Dom Type -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion  Dom Type
    a1 Cohesion -> Cohesion -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Dom Type -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion  Dom Type
    b1 -> Blocker -> TCM ()
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    neverUnblock
              | Dom Type -> PolarityModality
    forall a. LensModalPolarity a => a -> PolarityModality
    getModalPolarity Dom Type
    a1 PolarityModality -> PolarityModality -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Dom Type -> PolarityModality
    forall a. LensModalPolarity a => a -> PolarityModality
    getModalPolarity Dom Type
    b1 -> Blocker -> TCM ()
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation Blocker
    neverUnblock
              | Bool
    otherwise -> do
                  Type -> Type -> TCM ()
    checkSubtypeIsEqual (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    b1) (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a1)
                  Dom Type -> Abs Type -> (Type -> TCM ()) -> TCM ()
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstractionAbs Dom Type
    a1 Abs Type
    a2 ((Type -> TCM ()) -> TCM ()) -> (Type -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \Type
    a2' -> Type -> Type -> TCM ()
    checkSubtypeIsEqual Type
    a2' (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b2)
            Dummy{} -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return () -- TODO: this shouldn't happen but
                                 -- currently does because of generalized
                                 -- metas being created in a dummy context
            Term
    a -> Blocker -> TCM ()
    forall a. Blocker -> TCMT IO a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (Blocker -> TCM ()) -> TCM Blocker -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Blocker -> TCM Blocker
    forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
    updateBlocker (Term -> Blocker
    forall t. AllMetas t => t -> Blocker
    unblockOnAnyMetaIn Term
    a)
          -- TODO: check subtyping for Size< types
          Term
    _ -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | Turn the assignment problem @_X args <= SizeLt u@ into
    -- @_X args = SizeLt (_Y args)@ and constraint
    -- @_Y args <= u@.
    subtypingForSizeLt
      :: CompareDirection -- ^ @dir@
      -> MetaId           -- ^ The local meta-variable @x@.
      -> MetaVariable     -- ^ Its associated information @mvar <- lookupLocalMeta x@.
      -> Type             -- ^ Its type @t = jMetaType $ mvJudgement mvar@
      -> Args             -- ^ Its arguments.
      -> Term             -- ^ Its to-be-assigned value @v@, such that @x args `dir` v@.
      -> (Term -> TCM ()) -- ^ Continuation taking its possibly assigned value.
      -> TCM ()
    subtypingForSizeLt :: CompareDirection
    -> MetaId
    -> MetaVariable
    -> Type
    -> Args
    -> Term
    -> (Term -> TCM ())
    -> TCM ()
    subtypingForSizeLt CompareDirection
    DirEq MetaId
    x MetaVariable
    mvar Type
    t Args
    args Term
    v Term -> TCM ()
    cont = Term -> TCM ()
    cont Term
    v
    subtypingForSizeLt CompareDirection
    dir   MetaId
    x MetaVariable
    mvar Type
    t Args
    args Term
    v Term -> TCM ()
    cont = do
      let fallback :: TCM ()
    fallback = Term -> TCM ()
    cont Term
    v
      -- Check whether we have built-ins SIZE and SIZELT
      (mSize, mSizeLt) <- TCMT IO (Maybe QName, Maybe QName)
    forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
    getBuiltinSize
      caseMaybe mSize   fallback $ \ QName
    qSize   -> do
        Maybe QName -> TCM () -> (QName -> TCM ()) -> TCM ()
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe QName
    mSizeLt TCM ()
    fallback ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    qSizeLt -> do
          -- Check whether v is a SIZELT
          v <- Term -> TCM Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v
          case v of
            Def QName
    q [Apply (Arg ArgInfo
    ai Term
    u)] | QName
    q QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    qSizeLt -> do
              -- Clone the meta into a new size meta @y@.
              -- To this end, we swap the target of t for Size.
              TelV tel _ <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t
              let size = QName -> Type
    sizeType_ QName
    qSize
                  t'   = Tele (Dom Type) -> Type -> Type
    telePi Tele (Dom Type)
    tel Type
    size
              y <- newMeta Instantiable (mvInfo mvar) (mvPriority mvar) (mvPermutation mvar)
                           (HasType __IMPOSSIBLE__ CmpLeq t')
              -- Note: no eta-expansion of new meta possible/necessary.
              -- Add the size constraint @y args `dir` u@.
              let yArgs = MetaId -> Elims -> Term
    MetaV MetaId
    y (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Args
    args
              addConstraint (unblockOnMeta y) $ dirToCmp (`ValueCmp` AsSizes) dir yArgs u
              -- We continue with the new assignment problem, and install
              -- an exception handler, since we created a meta and a constraint,
              -- so we cannot fall back to the original handler.
              let xArgs = MetaId -> Elims -> Term
    MetaV MetaId
    x (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Args
    args
                  v'    = QName -> Elims -> Term
    Def QName
    qSizeLt [Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim) -> Arg Term -> Elim
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai Term
    yArgs]
                  c     = (Comparison -> Term -> Term -> Constraint)
    -> CompareDirection -> Term -> Term -> Constraint
    forall a c.
    (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
    dirToCmp (Comparison -> CompareAs -> Term -> Term -> Constraint
    `ValueCmp` (Type -> CompareAs
    AsTermsOf Type
    sizeUniv)) CompareDirection
    dir Term
    xArgs Term
    v'
              catchConstraint c $ cont v'
            Term
    _ -> TCM ()
    fallback

    -- | Eta-expand bound variables like @z@ in @X (fst z)@.
    expandProjectedVars
      :: ( Pretty a, PrettyTCM a, NoProjectedVar a
         -- , Normalise a, TermLike a, Subst Term a
         , ReduceAndEtaContract a
         , PrettyTCM b, TermSubst b
         )
      => a  -- ^ Meta variable arguments.
      -> b  -- ^ Right hand side.
      -> (a -> b -> TCM c)
      -> TCM c
    expandProjectedVars :: forall a b c.
    (Pretty a, PrettyTCM a, NoProjectedVar a, ReduceAndEtaContract a,
     PrettyTCM b, TermSubst b) =>
    a -> b -> (a -> b -> TCM c) -> TCM c
    expandProjectedVars a
    args b
    v a -> b -> TCM c
    ret = (a, b) -> TCM c
    loop (a
    args, b
    v) where
      loop :: (a, b) -> TCM c
    loop (a
    args, b
    v) = do
        [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign.proj" Nat
    45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "meta args: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    args
        args <- TCM a -> TCM a
    forall a. TCM a -> TCM a
    callByName (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ a -> TCM a
    forall a. ReduceAndEtaContract a => a -> TCM a
    reduceAndEtaContract a
    args
        reportSDoc "tc.meta.assign.proj" 45 $ "norm args: " <+> prettyTCM args
        reportSDoc "tc.meta.assign.proj" 85 $ "norm args: " <+> pretty args
        let done = a -> b -> TCM c
    ret a
    args b
    v
        case noProjectedVar args of
          Right ()              -> do
            [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign.proj" Nat
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
              TCMT IO Doc
    "no projected var found in args: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    args
            TCM c
    done
          Left (ProjectedVar Nat
    i [(ProjOrigin, QName)]
    _) -> Nat -> (a, b) -> TCM c -> ((a, b) -> TCM c) -> TCM c
    forall a c.
    (PrettyTCM a, TermSubst a) =>
    Nat -> a -> TCM c -> (a -> TCM c) -> TCM c
    etaExpandProjectedVar Nat
    i (a
    args, b
    v) TCM c
    done (a, b) -> TCM c
    loop

    -- | Eta-expand a de Bruijn index of record type in context and passed term(s).
    etaExpandProjectedVar :: (PrettyTCM a, TermSubst a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c
    etaExpandProjectedVar :: forall a c.
    (PrettyTCM a, TermSubst a) =>
    Nat -> a -> TCM c -> (a -> TCM c) -> TCM c
    etaExpandProjectedVar Nat
    i a
    v TCM c
    fail a -> TCM c
    succeed = do
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign.proj" Nat
    40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "trying to expand projected variable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Nat -> Term
    var Nat
    i)
      TCMT IO (Maybe (Tele (Dom Type), Substitution, Substitution))
    -> TCM c
    -> ((Tele (Dom Type), Substitution, Substitution) -> TCM c)
    -> TCM c
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Nat
    -> TCMT IO (Maybe (Tele (Dom Type), Substitution, Substitution))
    etaExpandBoundVar Nat
    i) TCM c
    fail (((Tele (Dom Type), Substitution, Substitution) -> TCM c) -> TCM c)
    -> ((Tele (Dom Type), Substitution, Substitution) -> TCM c)
    -> TCM c
    forall a b. (a -> b) -> a -> b
    $ \ (Tele (Dom Type)
    delta, Substitution
    sigma, Substitution
    tau) -> do
        [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign.proj" Nat
    25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO Doc
    "eta-expanding var " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Nat -> Term
    var Nat
    i) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
          TCMT IO Doc
    " in terms " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    v
        TCM c -> TCM c
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    unsafeInTopContext (TCM c -> TCM c) -> TCM c -> TCM c
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> TCM c -> TCM c
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Tele (Dom Type) -> m a -> m a
    addContext Tele (Dom Type)
    delta (TCM c -> TCM c) -> TCM c -> TCM c
    forall a b. (a -> b) -> a -> b
    $
          a -> TCM c
    succeed (a -> TCM c) -> a -> TCM c
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg a)
    tau a
    v

    -- | Check whether one of the meta args is a projected var.
    class NoProjectedVar a where
      noProjectedVar :: a -> Either ProjectedVar ()

      default noProjectedVar
        :: (NoProjectedVar b, Foldable t, t b ~ a)
        => a -> Either ProjectedVar ()
      noProjectedVar = (b -> Either ProjectedVar ()) -> t b -> Either ProjectedVar ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    Fold.mapM_ b -> Either ProjectedVar ()
    forall a. NoProjectedVar a => a -> Either ProjectedVar ()
    noProjectedVar

    instance NoProjectedVar a => NoProjectedVar (Arg a)
    instance NoProjectedVar a => NoProjectedVar [a]

    instance NoProjectedVar Term where
      noProjectedVar :: Term -> Either ProjectedVar ()
    noProjectedVar = \case
          Var Nat
    i Elims
    es
            | qs :: [(ProjOrigin, QName)]
    qs@((ProjOrigin, QName)
    _:[(ProjOrigin, QName)]
    _) <- (Maybe (ProjOrigin, QName) -> Maybe (ProjOrigin, QName))
    -> [Maybe (ProjOrigin, QName)] -> [(ProjOrigin, QName)]
    forall a b. (a -> Maybe b) -> [a] -> Prefix b
    takeWhileJust Maybe (ProjOrigin, QName) -> Maybe (ProjOrigin, QName)
    forall a. a -> a
    id ([Maybe (ProjOrigin, QName)] -> [(ProjOrigin, QName)])
    -> [Maybe (ProjOrigin, QName)] -> [(ProjOrigin, QName)]
    forall a b. (a -> b) -> a -> b
    $ (Elim -> Maybe (ProjOrigin, QName))
    -> Elims -> [Maybe (ProjOrigin, QName)]
    forall a b. (a -> b) -> [a] -> [b]
    map Elim -> Maybe (ProjOrigin, QName)
    forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
    isProjElim Elims
    es
            -> ProjectedVar -> Either ProjectedVar ()
    forall a b. a -> Either a b
    Left (ProjectedVar -> Either ProjectedVar ())
    -> ProjectedVar -> Either ProjectedVar ()
    forall a b. (a -> b) -> a -> b
    $ Nat -> [(ProjOrigin, QName)] -> ProjectedVar
    ProjectedVar Nat
    i [(ProjOrigin, QName)]
    qs
          -- Andreas, 2015-09-12 Issue #1316:
          -- Also look in inductive record constructors
          Con (ConHead QName
    _ IsRecord{} Induction
    Inductive [Arg QName]
    _) ConInfo
    _ Elims
    es
            | Just Args
    vs <- Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
            -> Args -> Either ProjectedVar ()
    forall a. NoProjectedVar a => a -> Either ProjectedVar ()
    noProjectedVar Args
    vs
          Term
    _ -> () -> Either ProjectedVar ()
    forall a. a -> Either ProjectedVar a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    -- | Normalize just far enough to be able to eta-contract maximally.
    class (TermLike a, TermSubst a, Reduce a) => ReduceAndEtaContract a where
      reduceAndEtaContract :: a -> TCM a

      default reduceAndEtaContract
        :: (Traversable f, TermLike b, Subst b, Reduce b, ReduceAndEtaContract b, f b ~ a)
        => a -> TCM a
      reduceAndEtaContract = (b -> TCMT IO b) -> f b -> TCMT IO (f b)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> f a -> m (f b)
    Trav.mapM b -> TCMT IO b
    forall a. ReduceAndEtaContract a => a -> TCM a
    reduceAndEtaContract

    instance ReduceAndEtaContract a => ReduceAndEtaContract [a]
    instance ReduceAndEtaContract a => ReduceAndEtaContract (Arg a)

    instance ReduceAndEtaContract Term where
      reduceAndEtaContract :: Term -> TCM Term
    reduceAndEtaContract Term
    u = do
        [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta" Nat
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "trying to eta-contract u =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u
        u <- Term -> TCM Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    u
        reportSDoc "tc.meta" 30 $ "               reduced u =" <+> prettyTCM u
        case u of
          -- In case of lambda or record constructor, it makes sense to
          -- reduce further.
          Lam ArgInfo
    ai Abs Term
    bAbs -> Abs Term -> (Term -> TCM Term) -> TCM Term
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Abs a -> (a -> m b) -> m b
    underAbstraction_ Abs Term
    bAbs ((Term -> TCM Term) -> TCM Term) -> (Term -> TCM Term) -> TCM Term
    forall a b. (a -> b) -> a -> b
    $ \Term
    b ->
            ArgInfo -> [Char] -> Term -> TCM Term
    forall (m :: * -> *).
    (MonadTCEnv m, HasConstInfo m, HasOptions m) =>
    ArgInfo -> [Char] -> Term -> m Term
    etaLam ArgInfo
    ai (Abs Term -> [Char]
    forall a. Abs a -> [Char]
    absName Abs Term
    bAbs) (Term -> TCM Term) -> TCM Term -> TCM Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> TCM Term
    forall a. ReduceAndEtaContract a => a -> TCM a
    reduceAndEtaContract Term
    b
          Con ConHead
    c ConInfo
    ci Elims
    es -> ConHead
    -> ConInfo
    -> Elims
    -> (QName -> ConHead -> ConInfo -> Args -> TCM Term)
    -> TCM Term
    forall (m :: * -> *).
    (MonadTCEnv m, HasConstInfo m, HasOptions m) =>
    ConHead
    -> ConInfo
    -> Elims
    -> (QName -> ConHead -> ConInfo -> Args -> m Term)
    -> m Term
    etaCon ConHead
    c ConInfo
    ci Elims
    es ((QName -> ConHead -> ConInfo -> Args -> TCM Term) -> TCM Term)
    -> (QName -> ConHead -> ConInfo -> Args -> TCM Term) -> TCM Term
    forall a b. (a -> b) -> a -> b
    $ \ QName
    r ConHead
    c ConInfo
    ci Args
    args -> do
            args <- Args -> TCM Args
    forall a. ReduceAndEtaContract a => a -> TCM a
    reduceAndEtaContract Args
    args
            etaContractRecord r c ci args
          Term
    v -> Term -> TCM Term
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v

    {- UNUSED, BUT KEEP!
    -- Wrong attempt at expanding bound variables.
    -- The following code curries meta instead.

    -- | @etaExpandProjectedVar mvar x t n qs@
    --
    --   @mvar@ is the meta var info.
    --   @x@ is the meta variable we are trying to solve for.
    --   @t@ is its type.
    --   @n@ is the number of the meta arg we want to curry (starting at 0).
    --   @qs@ is the projection path along which we curry.
    --
    etaExpandProjectedVar :: MetaVariable -> MetaId -> Type -> Int -> [QName] -> TCM a
    etaExpandProjectedVar mvar x t n qs = inTopContext $ do
      (_, uncurry, t') <- curryAt t n
      let TelV tel a = telView' t'
          perm       = idP (size tel)
      y <- newMeta (mvInfo mvar) (mvPriority mvar) perm (HasType __IMPOSSIBLE__ t')
      assignTerm' x (uncurry $ MetaV y [])
      patternViolation
    -}

    {-
      -- first, strip the leading n domains (which remain unchanged)
      TelV gamma core <- telViewUpTo n t
      case unEl core of
        -- There should be at least one domain left
        Pi (Dom ai a) b -> do
          -- Eta-expand @dom@ along @qs@ into a telescope @tel@, computing a substitution.
          -- For now, we only eta-expand once.
          -- This might trigger another call to @etaExpandProjectedVar@ later.
          -- A more efficient version does all the eta-expansions at once here.
          (r, pars, def) <- fromMaybe __IMPOSSIBLE__ <$> isRecordType a
          unless (recEtaEquality def) __IMPOSSIBLE__
          let tel = recTel def `apply` pars
              m   = size tel
              v   = Con (recConHead def) $ map var $ downFrom m
              b'  = raise m b `absApp` v
              fs  = recFields def
              vs  = zipWith (\ f i -> Var i [Proj f]) fs $ downFrom m
              -- v = c (n-1) ... 1 0
          (tel, u) <- etaExpandAtRecordType a $ var 0
          -- TODO: compose argInfo ai with tel.
          -- Substitute into @b@.
          -- Abstract over @tel@.
          -- Abstract over @gamma@.
          -- Create new meta.
          -- Solve old meta, using substitution.
          patternViolation
        _ -> __IMPOSSIBLE__
    -}

    type FVs = VarSet
    type SubstCand = [(Int,Term)] -- ^ a possibly non-deterministic substitution

    -- | Turn non-det substitution into proper substitution, if possible.
    --   Otherwise, raise the error.
    checkLinearity :: SubstCand -> ExceptT () TCM SubstCand
    checkLinearity :: [(Nat, Term)] -> ExceptT () (TCMT IO) [(Nat, Term)]
    checkLinearity [(Nat, Term)]
    ids = do
      -- see issue #920
      [(Nat, Term)] -> [(Nat, Term)]
    [(Nat, Term)] -> [Item [(Nat, Term)]]
    forall l. IsList l => l -> [Item l]
    List1.toList ([(Nat, Term)] -> [(Nat, Term)])
    -> ExceptT () (TCMT IO) [(Nat, Term)]
    -> ExceptT () (TCMT IO) [(Nat, Term)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (List1 (Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term))
    -> [List1 (Nat, Term)] -> ExceptT () (TCMT IO) [(Nat, Term)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM List1 (Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term)
    makeLinear (((Nat, Term) -> Nat) -> [(Nat, Term)] -> [List1 (Nat, Term)]
    forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
    List1.groupOn (Nat, Term) -> Nat
    forall a b. (a, b) -> a
    fst [(Nat, Term)]
    ids)
      where
        -- Non-determinism can be healed if type is singleton. [Issue 593]
        -- (Same as for irrelevance.)
        makeLinear :: List1 (Int, Term) -> ExceptT () TCM (Int, Term)
        makeLinear :: List1 (Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term)
    makeLinear ((Nat, Term)
    p       :| []) = (Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term)
    forall a. a -> ExceptT () (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Nat, Term)
    p
        makeLinear (p :: (Nat, Term)
    p@(Nat
    i,Term
    t) :| [(Nat, Term)]
    _ ) =
          ExceptT () (TCMT IO) Bool
    -> ExceptT () (TCMT IO) (Nat, Term)
    -> ExceptT () (TCMT IO) (Nat, Term)
    -> ExceptT () (TCMT IO) (Nat, Term)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ((Bool -> Either Blocker Bool
    forall a b. b -> Either a b
    Right Bool
    True Either Blocker Bool -> Either Blocker Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Either Blocker Bool -> Bool)
    -> ExceptT () (TCMT IO) (Either Blocker Bool)
    -> ExceptT () (TCMT IO) Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do TCM (Either Blocker Bool)
    -> ExceptT () (TCMT IO) (Either Blocker Bool)
    forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM (Either Blocker Bool)
     -> ExceptT () (TCMT IO) (Either Blocker Bool))
    -> (Type -> TCM (Either Blocker Bool))
    -> Type
    -> ExceptT () (TCMT IO) (Either Blocker Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BlockT (TCMT IO) Bool -> TCM (Either Blocker Bool)
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked (BlockT (TCMT IO) Bool -> TCM (Either Blocker Bool))
    -> (Type -> BlockT (TCMT IO) Bool)
    -> Type
    -> TCM (Either Blocker Bool)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> BlockT (TCMT IO) Bool
    forall (m :: * -> *). (PureTCM m, MonadBlock m) => Type -> m Bool
    isSingletonTypeModuloRelevance (Type -> ExceptT () (TCMT IO) (Either Blocker Bool))
    -> ExceptT () (TCMT IO) Type
    -> ExceptT () (TCMT IO) (Either Blocker Bool)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Nat -> ExceptT () (TCMT IO) Type
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Nat -> m Type
    typeOfBV Nat
    i)
            ((Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term)
    forall a. a -> ExceptT () (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Nat, Term)
    p)
            (() -> ExceptT () (TCMT IO) (Nat, Term)
    forall a. () -> ExceptT () (TCMT IO) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError ())

    -- Intermediate result in the following function
    type Res = [(Arg Nat, Term)]

    -- | Exceptions raised when substitution cannot be inverted.
    data InvertExcept
      = CantInvert Term           -- ^ Cannot recover.
      | NeutralArg                -- ^ A potentially neutral arg: can't invert, but can try pruning.
      | ProjVar ProjectedVar      -- ^ Try to eta-expand var to remove projs.

    -- | Check that arguments @args@ to a metavar are in pattern fragment.
    --   Assumes all arguments already in whnf and eta-reduced.
    --   Parameters are represented as @Var@s so @checkArgs@ really
    --   checks that all args are @Var@s and returns the "substitution"
    --   to be applied to the rhs of the equation to solve.
    --   (If @args@ is considered a substitution, its inverse is returned.)
    --
    --   The returned list might not be ordered.
    --   Linearity, i.e., whether the substitution is deterministic,
    --   has to be checked separately.
    --
    inverseSubst' :: (Term -> Bool) -> Args -> ExceptT InvertExcept TCM SubstCand
    inverseSubst' :: (Term -> Bool)
    -> Args -> ExceptT InvertExcept (TCMT IO) [(Nat, Term)]
    inverseSubst' Term -> Bool
    skip Args
    args = ((Arg Nat, Term) -> (Nat, Term))
    -> [(Arg Nat, Term)] -> [(Nat, Term)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Arg Nat -> Nat) -> (Arg Nat, Term) -> (Nat, Term)
    forall a c b. (a -> c) -> (a, b) -> (c, b)
    mapFst Arg Nat -> Nat
    forall e. Arg e -> e
    unArg) ([(Arg Nat, Term)] -> [(Nat, Term)])
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    -> ExceptT InvertExcept (TCMT IO) [(Nat, Term)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Arg Term, Term)]
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    loop (Args -> [Term] -> [(Arg Term, Term)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip Args
    args [Term]
    terms)
      where
      loop :: [(Arg Term, Term)]
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    loop  = ([(Arg Nat, Term)]
     -> (Arg Term, Term)
     -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
    -> [(Arg Nat, Term)]
    -> [(Arg Term, Term)]
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM [(Arg Nat, Term)]
    -> (Arg Term, Term)
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    isVarOrIrrelevant []
      terms :: [Term]
    terms = (Nat -> Term) -> [Nat] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Nat -> Term
    var (Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom (Args -> Nat
    forall a. Sized a => a -> Nat
    size Args
    args))
      failure :: Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    failure Term
    c = do
        TCM () -> ExceptT InvertExcept (TCMT IO) ()
    forall (m :: * -> *) a. Monad m => m a -> ExceptT InvertExcept m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> ExceptT InvertExcept (TCMT IO) ())
    -> TCM () -> ExceptT InvertExcept (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.meta.assign" Nat
    15 (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
    "not all arguments are variables: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Args -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Args -> m Doc
    prettyTCM Args
    args
          , TCMT IO Doc
    "  aborting assignment" ]
        InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall a. InvertExcept -> ExceptT InvertExcept (TCMT IO) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (Term -> InvertExcept
    CantInvert Term
    c)
      neutralArg :: ExceptT InvertExcept (TCMT IO) a
    neutralArg = InvertExcept -> ExceptT InvertExcept (TCMT IO) a
    forall a. InvertExcept -> ExceptT InvertExcept (TCMT IO) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError InvertExcept
    NeutralArg

      isVarOrIrrelevant :: Res -> (Arg Term, Term) -> ExceptT InvertExcept TCM Res
      isVarOrIrrelevant :: [(Arg Nat, Term)]
    -> (Arg Term, Term)
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    isVarOrIrrelevant [(Arg Nat, Term)]
    vars (Arg ArgInfo
    info Term
    v, Term
    t) = do
        let irr :: Bool
    irr | ArgInfo -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant ArgInfo
    info = Bool
    True
                | DontCare{} <- Term
    v   = Bool
    True
                | Bool
    otherwise         = Bool
    False
        ineg <- PrimitiveId -> ExceptT InvertExcept (TCMT IO) (Maybe QName)
    forall (m :: * -> *).
    HasBuiltins m =>
    PrimitiveId -> m (Maybe QName)
    getPrimitiveName' PrimitiveId
    builtinINeg
        case stripDontCare v of
          -- i := x
          Var Nat
    i [] -> [(Arg Nat, Term)]
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall a. a -> ExceptT InvertExcept (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Arg Nat, Term)]
     -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
    -> [(Arg Nat, Term)]
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall a b. (a -> b) -> a -> b
    $ (ArgInfo -> Nat -> Arg Nat
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info Nat
    i, Term
    t) (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
    `cons` [(Arg Nat, Term)]
    vars

          -- π i := x  try to eta-expand projection π away!
          Var Nat
    i Elims
    es | Just [(ProjOrigin, QName)]
    qs <- (Elim -> Maybe (ProjOrigin, QName))
    -> Elims -> Maybe [(ProjOrigin, QName)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Elim -> Maybe (ProjOrigin, QName)
    forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
    isProjElim Elims
    es ->
            InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall a. InvertExcept -> ExceptT InvertExcept (TCMT IO) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
    -> InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall a b. (a -> b) -> a -> b
    $ ProjectedVar -> InvertExcept
    ProjVar (ProjectedVar -> InvertExcept) -> ProjectedVar -> InvertExcept
    forall a b. (a -> b) -> a -> b
    $ Nat -> [(ProjOrigin, QName)] -> ProjectedVar
    ProjectedVar Nat
    i [(ProjOrigin, QName)]
    qs

          -- (i, j) := x  becomes  [i := fst x, j := snd x]
          -- Andreas, 2013-09-17 but only if constructor is fully applied
          tm :: Term
    tm@(Con ConHead
    c ConInfo
    ci Elims
    es) -> do
            let fallback :: ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    fallback
                 | ArgInfo -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant ArgInfo
    info = [(Arg Nat, Term)]
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall a. a -> ExceptT InvertExcept (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Arg Nat, Term)]
    vars
                 | Term -> Bool
    skip Term
    tm           = [(Arg Nat, Term)]
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall a. a -> ExceptT InvertExcept (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Arg Nat, Term)]
    vars
                 | Bool
    otherwise         = Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    failure Term
    tm
            irrProj <- PragmaOptions -> Bool
    optIrrelevantProjections (PragmaOptions -> Bool)
    -> ExceptT InvertExcept (TCMT IO) PragmaOptions
    -> ExceptT InvertExcept (TCMT IO) Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ExceptT InvertExcept (TCMT IO) PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
            lift (isEtaRecordConstructor $ conName c) >>= \case
              -- Andreas, 2019-11-10, issue #4185: only for eta-records
              Just (QName
    _, RecordData{ _recFields :: RecordData -> [Dom QName]
    _recFields = [Dom QName]
    fs })
                | [Dom QName] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Dom QName]
    fs Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Elims -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Elims
    es
                , ArgInfo -> Bool
    forall a. LensQuantity a => a -> Bool
    hasQuantity0 ArgInfo
    info Bool -> Bool -> Bool
    || (Dom QName -> Bool) -> [Dom QName] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Dom QName -> Bool
    forall a. LensQuantity a => a -> Bool
    usableQuantity [Dom QName]
    fs     -- Andreas, 2019-11-12/17, issue #4168b
                , Bool
    irrProj Bool -> Bool -> Bool
    || (Dom QName -> Bool) -> [Dom QName] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Dom QName -> Bool
    forall a. LensRelevance a => a -> Bool
    isRelevant [Dom QName]
    fs -> do
                  let aux :: Arg Term -> Dom QName -> (Arg Term, Term)
    aux (Arg ArgInfo
    _ Term
    v) Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    info', unDom :: forall t e. Dom' t e -> e
    unDom = QName
    f} =
                        (ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai Term
    v,) (Term -> (Arg Term, Term)) -> Term -> (Arg Term, Term)
    forall a b. (a -> b) -> a -> b
    $ Term
    t Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [ProjOrigin -> QName -> Elim
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    f]
                        where
                        ai :: ArgInfo
    ai = ArgInfo
                          { argInfoHiding :: Hiding
    argInfoHiding   = Hiding -> Hiding -> Hiding
    forall a. Ord a => a -> a -> a
    min (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    info) (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    info')
                          , argInfoModality :: Modality
    argInfoModality = Modality
                            { modRelevance :: Relevance
    modRelevance  = Relevance -> Relevance -> Relevance
    forall a. Ord a => a -> a -> a
    max (ArgInfo -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance ArgInfo
    info) (ArgInfo -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance ArgInfo
    info')
                            , modQuantity :: Quantity
    modQuantity   = Quantity -> Quantity -> Quantity
    forall a. Ord a => a -> a -> a
    max (ArgInfo -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity  ArgInfo
    info) (ArgInfo -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity  ArgInfo
    info')
                            , modCohesion :: Cohesion
    modCohesion   = Cohesion -> Cohesion -> Cohesion
    forall a. Ord a => a -> a -> a
    max (ArgInfo -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion  ArgInfo
    info) (ArgInfo -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion  ArgInfo
    info')
                            , modPolarity :: PolarityModality
    modPolarity   = PolarityModality -> PolarityModality -> PolarityModality
    addPolarity (ArgInfo -> PolarityModality
    forall a. LensModalPolarity a => a -> PolarityModality
    getModalPolarity ArgInfo
    info) (ArgInfo -> PolarityModality
    forall a. LensModalPolarity a => a -> PolarityModality
    getModalPolarity ArgInfo
    info') -- XXX
                            }
                          , argInfoOrigin :: Origin
    argInfoOrigin   = Origin -> Origin -> Origin
    forall a. Ord a => a -> a -> a
    min (ArgInfo -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin ArgInfo
    info) (ArgInfo -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin ArgInfo
    info')
                          , argInfoFreeVariables :: FreeVariables
    argInfoFreeVariables = FreeVariables
    unknownFreeVariables
                          , argInfoAnnotation :: Annotation
    argInfoAnnotation    = ArgInfo -> Annotation
    argInfoAnnotation ArgInfo
    info'
                          }
                      vs :: Args
    vs = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
                  res <- [(Arg Term, Term)]
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    loop ([(Arg Term, Term)]
     -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
    -> [(Arg Term, Term)]
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Dom QName -> (Arg Term, Term))
    -> Args -> [Dom QName] -> [(Arg Term, Term)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Arg Term -> Dom QName -> (Arg Term, Term)
    aux Args
    vs [Dom QName]
    fs
                  return $ res `append` vars
                | Bool
    otherwise -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    fallback
              Maybe (QName, RecordData)
    _ -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    fallback

          -- An irrelevant argument which is not an irrefutable pattern is dropped
          Term
    _ | Bool
    irr -> [(Arg Nat, Term)]
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall a. a -> ExceptT InvertExcept (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Arg Nat, Term)]
    vars

          -- Distinguish args that can be eliminated (Con,Lit,Lam,unsure) ==> failure
          -- from those that can only put somewhere as a whole ==> neutralArg
          Var{}      -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall {a}. ExceptT InvertExcept (TCMT IO) a
    neutralArg

          -- primINeg i := x becomes i := primINeg x
          -- (primINeg is a definitional involution)
          Def QName
    qn Elims
    es | Just [Arg ArgInfo
    _ (Var Nat
    i [])] <- Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es, QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    qn Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    ineg ->
            [(Arg Nat, Term)]
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall a. a -> ExceptT InvertExcept (TCMT IO) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([(Arg Nat, Term)]
     -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
    -> [(Arg Nat, Term)]
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall a b. (a -> b) -> a -> b
    $ (ArgInfo -> Nat -> Arg Nat
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info Nat
    i, QName -> Elims -> Term
    Def QName
    qn [Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    t)]) (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
    `cons` [(Arg Nat, Term)]
    vars

          Def{}      -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall {a}. ExceptT InvertExcept (TCMT IO) a
    neutralArg  -- Note that this Def{} is in normal form and might be prunable.
          t :: Term
    t@Lam{}    -> Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    failure Term
    t
          t :: Term
    t@Lit{}    -> Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    failure Term
    t
          t :: Term
    t@MetaV{}  -> Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    failure Term
    t
          Pi{}       -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall {a}. ExceptT InvertExcept (TCMT IO) a
    neutralArg
          Sort{}     -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall {a}. ExceptT InvertExcept (TCMT IO) a
    neutralArg
          Level{}    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall {a}. ExceptT InvertExcept (TCMT IO) a
    neutralArg
          DontCare{} -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- Ruled out by stripDontCare
          Dummy [Char]
    s Elims
    _  -> [Char] -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__ [Char]
    s

      -- managing an assoc list where duplicate indizes cannot be irrelevant vars
      append :: Res -> Res -> Res
      append :: [(Arg Nat, Term)] -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
    append [(Arg Nat, Term)]
    res [(Arg Nat, Term)]
    vars = ((Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)])
    -> [(Arg Nat, Term)] -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
    cons [(Arg Nat, Term)]
    vars [(Arg Nat, Term)]
    res

      -- adding an irrelevant entry only if not present
      cons :: (Arg Nat, Term) -> Res -> Res
      cons :: (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
    cons a :: (Arg Nat, Term)
    a@(Arg ArgInfo
    ai Nat
    i, Term
    t) [(Arg Nat, Term)]
    vars
        | ArgInfo -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant ArgInfo
    ai = Bool
    -> ([(Arg Nat, Term)] -> [(Arg Nat, Term)])
    -> [(Arg Nat, Term)]
    -> [(Arg Nat, Term)]
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyUnless (((Arg Nat, Term) -> Bool) -> [(Arg Nat, Term)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any ((Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Nat -> Bool)
    -> ((Arg Nat, Term) -> Nat) -> (Arg Nat, Term) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Nat -> Nat
    forall e. Arg e -> e
    unArg (Arg Nat -> Nat)
    -> ((Arg Nat, Term) -> Arg Nat) -> (Arg Nat, Term) -> Nat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Nat, Term) -> Arg Nat
    forall a b. (a, b) -> a
    fst) [(Arg Nat, Term)]
    vars) ((Arg Nat, Term)
    a (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
    forall a. a -> [a] -> [a]
    :) [(Arg Nat, Term)]
    vars
        | Bool
    otherwise       = (Arg Nat, Term)
    a (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
    forall a. a -> [a] -> [a]
    :  -- adding a relevant entry
            -- filter out duplicate irrelevants
            ((Arg Nat, Term) -> Bool) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool)
    -> ((Arg Nat, Term) -> Bool) -> (Arg Nat, Term) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (\ a :: (Arg Nat, Term)
    a@(Arg ArgInfo
    info Nat
    j, Term
    t) -> ArgInfo -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant ArgInfo
    info Bool -> Bool -> Bool
    && Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    j)) [(Arg Nat, Term)]
    vars

    -- | If the given metavariable application represents a face, return:
    --
    --    * The metavariable information;
    --    * The actual face, as an assignment of booleans to variables;
    --
    --    * The substitution candidate resulting from @inverseSubst'@. This
    --    is guaranteed to be linear and deterministic.
    --
    --    * The actual substitution, mapping from the constraint context to
    --    the metavariable's context.
    --
    --  Put concisely, a face constraint is an equation in the pattern
    --  fragment modulo the presence of endpoints (@i0@ and @i1@) in the
    --  telescope. In more detail, a face constraint has the form
    --
    --    @?0 Δ (i = i0) (j = i0) Γ (k = i1) Θ (l = i0) = t@
    --
    --  where all the greek letters consist entirely of distinct bound
    --  variables (and, of course, arbitrarily many endpoints are allowed
    --  between each substitution fragment).
    isFaceConstraint
      :: MetaId
      -> Args
      -> TCM (Maybe (MetaVariable, IntMap.IntMap Bool, SubstCand, Substitution))
    isFaceConstraint :: MetaId
    -> Args
    -> TCM
         (Maybe (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution))
    isFaceConstraint MetaId
    mid Args
    args = MaybeT
      (TCMT IO) (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution)
    -> TCM
         (Maybe (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution))
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT
       (TCMT IO) (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution)
     -> TCM
          (Maybe (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution)))
    -> MaybeT
         (TCMT IO) (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution)
    -> TCM
         (Maybe (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution))
    forall a b. (a -> b) -> a -> b
    $ do
      iv   <- MaybeT (TCMT IO) (Term -> IntervalView)
    forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
    intervalView'
      mvar <- lookupLocalMeta mid  -- information associated with meta x
      -- Make sure that this is actually an interaction point:
      (_, _, _) <- MaybeT $ isInteractionMetaB mid args

      let
        t = Judgement MetaId -> Type
    forall a. Judgement a -> Type
    jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mvar
        n = Args -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Args
    args

        isEndpoint Term
    tm = Maybe (Nat, Bool) -> Bool
    forall a. Maybe a -> Bool
    isJust (Arg Term -> Nat -> Maybe (Nat, Bool)
    fin (Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    tm) Nat
    0)

        fin (Arg ArgInfo
    _ Term
    tm) Nat
    i = case Term -> IntervalView
    iv Term
    tm of
          IntervalView
    IOne  -> (Nat, Bool) -> Maybe (Nat, Bool)
    forall a. a -> Maybe a
    Just (Nat
    i, Bool
    True)
          IntervalView
    IZero -> (Nat, Bool) -> Maybe (Nat, Bool)
    forall a. a -> Maybe a
    Just (Nat
    i, Bool
    False)
          IntervalView
    _     -> Maybe (Nat, Bool)
    forall a. Maybe a
    Nothing

      -- The logic here is essentially the same as for actually solving the
      -- meta.. We just return the pieces instead of doing the assignment.
      -- We must check the "face condition" (the relaxed pattern condition)
      -- and check linearity of the substitution candidate, otherwise the
      -- equation can't be inverted into a face constraint.
      sub <- MaybeT $ either (const Nothing) Just <$> runExceptT (inverseSubst' isEndpoint args)
      ids <- MaybeT $ either (const Nothing) Just <$> runExceptT (checkLinearity sub)

      m           <- getContextSize
      TelV tel' _ <- telViewUpToPath n t
      tel''       <- enterClosure mvar $ \Range
    _ -> MaybeT (TCMT IO) (Tele (Dom Type))
    forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
    getContextTelescope

      let
        assocToList Nat
    i = \case
          [(Nat, Term)]
    _           | Nat
    i Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Nat
    m -> []
          ((Nat
    j,Term
    u) : [(Nat, Term)]
    l) | Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    j -> Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    u  Maybe Term -> [Maybe Term] -> [Maybe Term]
    forall a. a -> [a] -> [a]
    : Nat -> [(Nat, Term)] -> [Maybe Term]
    assocToList (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) [(Nat, Term)]
    l
          [(Nat, Term)]
    l                    -> Maybe Term
    forall a. Maybe a
    Nothing Maybe Term -> [Maybe Term] -> [Maybe Term]
    forall a. a -> [a] -> [a]
    : Nat -> [(Nat, Term)] -> [Maybe Term]
    assocToList (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) [(Nat, Term)]
    l
        ivs = Nat -> [(Nat, Term)] -> [Maybe Term]
    assocToList Nat
    0 [(Nat, Term)]
    ids
        rho = Impossible -> [Maybe Term] -> Substitution -> Substitution
    forall a.
    DeBruijn a =>
    Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
    prependS Impossible
    HasCallStack => Impossible
    impossible [Maybe Term]
    ivs (Substitution -> Substitution) -> Substitution -> Substitution
    forall a b. (a -> b) -> a -> b
    $ Nat -> Substitution
    forall a. Nat -> Substitution' a
    raiseS Nat
    n

        over  = Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel' Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel''
        endps = [(Nat, Bool)] -> IntMap Bool
    forall a. [(Nat, a)] -> IntMap a
    IntMap.fromList ([(Nat, Bool)] -> IntMap Bool) -> [(Nat, Bool)] -> IntMap Bool
    forall a b. (a -> b) -> a -> b
    $ [Maybe (Nat, Bool)] -> [(Nat, Bool)]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe (Nat, Bool)] -> [(Nat, Bool)])
    -> [Maybe (Nat, Bool)] -> [(Nat, Bool)]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Nat -> Maybe (Nat, Bool))
    -> Args -> [Nat] -> [Maybe (Nat, Bool)]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\Arg Term
    a Nat
    i -> Arg Term -> Nat -> Maybe (Nat, Bool)
    fin Arg Term
    a (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    over)) Args
    args (Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom Nat
    n)

      reportSDoc "tc.ip.boundary" 45 $ vcat
        [ "ivs   =" <+> prettyTCM ivs
        , "tel'  =" <+> prettyTCM tel'
        , "tel'' =" <+> prettyTCM tel''
        , "ids   =" <+> prettyTCM ids
        , "sub   =" <+> prettyTCM sub
        , "endps =" <+> pretty endps
        ]

      guard (not (IntMap.null endps))
      -- Can happen when the metavariable's context does not yet know about
      -- an interval variable it will be applied to later, eg in the partial
      -- argument to hcomp:
      guard (all (>= 0) (IntMap.keys endps))
      -- In that case we fail here — when the user writes some more
      -- patterns, they'll become positive
      pure (mvar, endps, ids, rho)

    -- | Record a "face" equation onto an interaction point into the actual
    -- interaction point boundary. Takes all the same arguments as
    -- @assignMeta'@.
    tryAddBoundary :: CompareDirection -> MetaId -> InteractionId -> Args -> Term -> CompareAs -> TCM ()
    tryAddBoundary :: CompareDirection
    -> MetaId -> InteractionId -> Args -> Term -> CompareAs -> TCM ()
    tryAddBoundary CompareDirection
    dir MetaId
    x InteractionId
    iid Args
    args Term
    v CompareAs
    target = do
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.ip.boundary" 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
    "boundary: looking at equational constraint"
        , Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (MetaId -> Elims -> Term
    MetaV MetaId
    x (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim) -> Args -> Elims
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Args
    args)) 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
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
        ]
      iv   <- TCMT IO (Term -> IntervalView)
    forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
    intervalView'
      mvar <- lookupLocalMeta x  -- information associated with meta x

      let
        t = Judgement MetaId -> Type
    forall a. Judgement a -> Type
    jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mvar
        n = Args -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Args
    args
        rhsv = Term -> VarSet
    forall t. Free t => t -> VarSet
    allFreeVars Term
    v

        allVars :: SubstCand -> Bool
        allVars [(Nat, Term)]
    sub = VarSet
    rhsv VarSet -> VarSet -> Bool
    `VarSet.isSubsetOf` [Nat] -> VarSet
    VarSet.fromList (((Nat, Term) -> Nat) -> [(Nat, Term)] -> [Nat]
    forall a b. (a -> b) -> [a] -> [b]
    map (Nat, Term) -> Nat
    forall a b. (a, b) -> a
    fst [(Nat, Term)]
    sub)

      TelV tel' _ <- telViewUpToPath n t

      void . runMaybeT $ do
        -- Make sure we're looking at a face constraint:
        (_, endps, ids, rho) <- MaybeT $ isFaceConstraint x args
        -- And that the non-endpoint parts of the 'Args' cover the free
        -- variables of the RHS:
        guard (allVars ids)

        -- ρ is a substitution from the "constraint context" (the context
        -- we're in) to the metavariable's context. moreover, v[ρ] is
        -- well-scoped in the meta's context.
        let v' = Tele (Dom Type) -> Term -> Term
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel' (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Term)
    rho Term
    v
        -- We store the boundary faces directly as lambdas for simplicity.

        enterClosure mvar $ \Range
    _ -> do
          [Char] -> Nat -> TCMT IO Doc -> MaybeT (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.ip.boundary" Nat
    30 (TCMT IO Doc -> MaybeT (TCMT IO) ())
    -> TCMT IO Doc -> MaybeT (TCMT IO) ()
    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
    "recovered interaction point boundary"
            , TCMT IO Doc
    "  endps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> IntMap Bool -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty IntMap Bool
    endps
            , TCMT IO Doc
    "  rho   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Substitution -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Substitution
    rho
            , TCMT IO Doc
    "  t     =" 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 (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t)
            , TCMT IO Doc
    "  v'    =" 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 (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v')
            ]

          let
            -- Always store the constraint with the smaller termSize:
            upd :: IPBoundary' Term -> IPBoundary' Term
    upd (IPBoundary Map (IntMap Bool) Term
    m) = case IntMap Bool -> Map (IntMap Bool) Term -> Maybe Term
    forall k a. Ord k => k -> Map k a -> Maybe a
    MapS.lookup IntMap Bool
    endps Map (IntMap Bool) Term
    m of
              Just Term
    t -> if Term -> Nat
    forall a. TermSize a => a -> Nat
    termSize Term
    t Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Term -> Nat
    forall a. TermSize a => a -> Nat
    termSize Term
    v'
                then Map (IntMap Bool) Term -> IPBoundary' Term
    forall t. Map (IntMap Bool) t -> IPBoundary' t
    IPBoundary Map (IntMap Bool) Term
    m
                else Map (IntMap Bool) Term -> IPBoundary' Term
    forall t. Map (IntMap Bool) t -> IPBoundary' t
    IPBoundary (Map (IntMap Bool) Term -> IPBoundary' Term)
    -> Map (IntMap Bool) Term -> IPBoundary' Term
    forall a b. (a -> b) -> a -> b
    $ IntMap Bool
    -> Term -> Map (IntMap Bool) Term -> Map (IntMap Bool) Term
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    MapS.insert IntMap Bool
    endps Term
    v' Map (IntMap Bool) Term
    m
              Maybe Term
    Nothing -> Map (IntMap Bool) Term -> IPBoundary' Term
    forall t. Map (IntMap Bool) t -> IPBoundary' t
    IPBoundary (Map (IntMap Bool) Term -> IPBoundary' Term)
    -> Map (IntMap Bool) Term -> IPBoundary' Term
    forall a b. (a -> b) -> a -> b
    $ IntMap Bool
    -> Term -> Map (IntMap Bool) Term -> Map (IntMap Bool) Term
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    MapS.insert IntMap Bool
    endps Term
    v' Map (IntMap Bool) Term
    m
            f :: InteractionPoint -> InteractionPoint
    f InteractionPoint
    ip = InteractionPoint
    ip{ ipBoundary = upd (ipBoundary ip) }

          TCM () -> MaybeT (TCMT IO) ()
    forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCM () -> MaybeT (TCMT IO) ()) -> TCM () -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ (InteractionPoints -> InteractionPoints) -> TCM ()
    forall (m :: * -> *).
    MonadInteractionPoints m =>
    (InteractionPoints -> InteractionPoints) -> m ()
    modifyInteractionPoints ((InteractionPoint -> InteractionPoint)
    -> InteractionId -> InteractionPoints -> InteractionPoints
    forall k v.
    (Ord k, Ord (Tag v), HasTag v) =>
    (v -> v) -> k -> BiMap k v -> BiMap k v
    BiMap.adjust InteractionPoint -> InteractionPoint
    f InteractionId
    iid)

    -- | Turn open metas into postulates.
    --
    --   Preconditions:
    --
    --   1. We are 'inTopContext'.
    --
    --   2. 'envCurrentModule' is set to the top-level module.
    --
    openMetasToPostulates :: TCM ()
    openMetasToPostulates :: TCM ()
    openMetasToPostulates = do
      m <- (TCEnv -> ModuleName) -> TCMT IO ModuleName
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> ModuleName
    envCurrentModule

      -- Go through all open metas.
      ms <- MapS.assocs <$> useTC stOpenMetaStore
      forM_ ms $ \ (MetaId
    x, MetaVariable
    mv) -> do
        let t :: Type
    t = Type -> Type
    dummyTypeToOmega (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Judgement MetaId -> Type
    forall a. Judgement a -> Type
    jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> Judgement MetaId
    mvJudgement MetaVariable
    mv

        -- Create a name for the new postulate.
        let r :: Range
    r = Closure Range -> Range
    forall a. Closure a -> a
    clValue (Closure Range -> Range) -> Closure Range -> Range
    forall a b. (a -> b) -> a -> b
    $ MetaInfo -> Closure Range
    miClosRange (MetaInfo -> Closure Range) -> MetaInfo -> Closure Range
    forall a b. (a -> b) -> a -> b
    $ MetaVariable -> MetaInfo
    mvInfo MetaVariable
    mv
        s' <- Doc -> [Char]
    forall a. Doc a -> [Char]
    render (Doc -> [Char]) -> TCMT IO Doc -> TCMT IO [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
    prettyTCM MetaId
    x -- Using _ is a bad idea, as it prints as prefix op
        let s = [Char]
    "unsolved#meta." [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ (Char -> Bool) -> [Char] -> [Char]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    '_') [Char]
    s'
        n <- freshName r s
        let q = ModuleName -> Name -> QName
    A.QName ModuleName
    m Name
    n

        -- Debug.
        reportSDoc "meta.postulate" 20 $ vcat
          [ text ("Turning " ++ if isSortMeta_ mv then "sort" else "value" ++ " meta ")
              <+> prettyTCM x <+> " into postulate."
          , nest 2 $ vcat
            [ "Name: " <+> prettyTCM q
            , "Type: " <+> prettyTCM t
            ]
          ]

        -- Add the new postulate to the signature.
        addConstant' q defaultArgInfo t defaultAxiom

        -- Solve the meta.
        let inst = Instantiation -> MetaInstantiation
    InstV (Instantiation -> MetaInstantiation)
    -> Instantiation -> MetaInstantiation
    forall a b. (a -> b) -> a -> b
    $ Instantiation
                     { instTel :: [Arg [Char]]
    instTel = [], instBody :: Term
    instBody = QName -> Elims -> Term
    Def QName
    q [] }
        updateMetaVar x $ \ MetaVariable
    mv0 -> MetaVariable
    mv0 { mvInstantiation = inst }
        return ()
      where
        -- Unsolved sort metas can have a type ending in a Dummy if they are allowed to be instantiated
        -- to Setω. This will crash the serializer (issue #3730). To avoid this we replace dummy type
        -- codomains by Setω.
        dummyTypeToOmega :: Type -> Type
    dummyTypeToOmega Type
    t =
          case Type -> TelV Type
    telView' Type
    t of
            TelV Tele (Dom Type)
    tel (El Sort
    _ Dummy{}) -> Tele (Dom Type) -> Type -> Type
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    tel (Sort -> Type
    sort (Sort -> Type) -> Sort -> Type
    forall a b. (a -> b) -> a -> b
    $ Univ -> Integer -> Sort
    forall t. Univ -> Integer -> Sort' t
    Inf Univ
    UType Integer
    0)
            TelV Type
    _ -> Type
    t

    -- | Sort metas in dependency order.
    dependencySortMetas :: [MetaId] -> TCM (Maybe [MetaId])
    dependencySortMetas :: [MetaId] -> TCM (Maybe [MetaId])
    dependencySortMetas [MetaId]
    metas = do
      metaGraph <- [[(MetaId, MetaId)]] -> [(MetaId, MetaId)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[(MetaId, MetaId)]] -> [(MetaId, MetaId)])
    -> TCMT IO [[(MetaId, MetaId)]] -> TCMT IO [(MetaId, MetaId)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        [MetaId]
    -> (MetaId -> TCMT IO [(MetaId, MetaId)])
    -> TCMT IO [[(MetaId, MetaId)]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [MetaId]
    metas ((MetaId -> TCMT IO [(MetaId, MetaId)])
     -> TCMT IO [[(MetaId, MetaId)]])
    -> (MetaId -> TCMT IO [(MetaId, MetaId)])
    -> TCMT IO [[(MetaId, MetaId)]]
    forall a b. (a -> b) -> a -> b
    $ \ MetaId
    m -> do
          deps <- (MetaId -> Set MetaId) -> Maybe Type -> Set MetaId
    forall m. Monoid m => (MetaId -> m) -> Maybe Type -> m
    forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
    allMetas (\MetaId
    m' -> if MetaId
    m' MetaId -> Set MetaId -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set MetaId
    metas'
                                   then MetaId -> Set MetaId
    forall el coll. Singleton el coll => el -> coll
    singleton MetaId
    m'
                                   else Set MetaId
    forall a. Monoid a => a
    mempty) (Maybe Type -> Set MetaId)
    -> TCMT IO (Maybe Type) -> TCMT IO (Set MetaId)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                    MetaId -> TCMT IO (Maybe Type)
    forall {m :: * -> *}. MonadReduce m => MetaId -> m (Maybe Type)
    getType MetaId
    m
          return [ (m, m') | m' <- Set.toList deps ]

      return $ Graph.topSort metas' metaGraph

      where
        metas' :: Set MetaId
    metas' = [MetaId] -> Set MetaId
    forall a. Ord a => [a] -> Set a
    Set.fromList [MetaId]
    metas

        -- Sort metas don't have types, but we still want to sort them.
        getType :: MetaId -> m (Maybe Type)
    getType MetaId
    m = do
          j <- MetaId -> m (Judgement MetaId)
    forall (m :: * -> *).
    ReadTCState m =>
    MetaId -> m (Judgement MetaId)
    lookupMetaJudgement MetaId
    m
          case j of
            IsSort{}                 -> Maybe Type -> m (Maybe Type)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Type
    forall a. Maybe a
    Nothing
            HasType{ jMetaType :: forall a. Judgement a -> Type
    jMetaType = Type
    t } -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> m Type -> m (Maybe Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m Type
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Type
    t