    {- |

    "Injectivity", or more precisely, "constructor headedness", is a
    property of functions defined by pattern matching that helps us solve
    constraints involving blocked applications of such functions.
    "Blocked" shall mean here that pattern matching is blocked on a meta
    variable, and constructor headedness lets us learn more about that
    meta variable.

    Consider the simple example:
    @
      isZero : Nat -> Bool
      isZero zero    = true
      isZero (suc n) = false
    @
    This function is constructor-headed, meaning that all rhss are headed
    by a distinct constructor.  Thus, on a constraint like
    @
      isZero ?X = false : Bool
    @
    involving an application of @isZero@ that is blocked on meta variable @?X@,
    we can exploit injectivity and learn that @?X = suc ?Y@ for a new
    meta-variable @?Y@.

    Which functions qualify for injectivity?

    1. The function needs to have at least one non-absurd clause that has
    a proper match, meaning that the function can actually be blocked on a
    meta.  Proper matches are these patterns:

      - data constructor (@ConP@, but not record constructor)
      - literal (@LitP@)
      - HIT-patterns (@DefP@)

    Projection patterns (@ProjP@) are excluded because metas cannot occupy their place!

    2. All the clauses that satisfy (1.) need to be headed by a distinct constructor.

    -}

    module Agda.TypeChecking.Injectivity where

    import Control.Applicative
    import Control.Monad.Except       ( MonadError )
    import Control.Monad.State        ( evalStateT, MonadState, gets, put )
    import Control.Monad.Reader       ( runReaderT, MonadReader, ask )
    import Control.Monad.Trans.Maybe  ( MaybeT(MaybeT), runMaybeT )

    import qualified Data.Map as Map
    import qualified Data.Set as Set
    import Data.Maybe
    import Data.Traversable hiding (for)
    import Data.Semigroup ((<>))
    import Data.Foldable (fold)

    import qualified Agda.Syntax.Abstract.Name as A
    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern

    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Irrelevance (isIrrelevantOrPropM)
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Patterns.Match (properlyMatching')
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope.Path
    import Agda.TypeChecking.Reduce
    import {-# SOURCE #-} Agda.TypeChecking.MetaVars
    import {-# SOURCE #-} Agda.TypeChecking.Conversion
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Polarity
    import Agda.TypeChecking.Warnings

    import Agda.Interaction.Options

    import Agda.Utils.Either
    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Permutation
    import Agda.Syntax.Common.Pretty ( prettyShow )
    import qualified Agda.Utils.ProfileOptions as Profile

    import Agda.Utils.Impossible

    headSymbol :: Term -> TCM (Maybe TermHead)
    headSymbol :: Term -> TCM (Maybe TermHead)
    headSymbol Term
    v = do -- ignoreAbstractMode $ do
      -- Andreas, 2013-02-18 ignoreAbstractMode leads to information leakage

      v <- Term -> TCMT IO Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Blocked' Term Term -> Term
    forall t a. Blocked' t a -> a
    ignoreBlocking (Blocked' Term Term -> Term)
    -> TCMT IO (Blocked' Term Term) -> TCMT IO Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> TCMT IO (Blocked' Term Term)
    forall (m :: * -> *). PureTCM m => Term -> m (Blocked' Term Term)
    reduceHead Term
    v
      case v of
        Def QName
    f Elims
    _ -> do
          let yes :: TCM (Maybe TermHead)
    yes = Maybe TermHead -> TCM (Maybe TermHead)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe TermHead -> TCM (Maybe TermHead))
    -> Maybe TermHead -> TCM (Maybe TermHead)
    forall a b. (a -> b) -> a -> b
    $ TermHead -> Maybe TermHead
    forall a. a -> Maybe a
    Just (TermHead -> Maybe TermHead) -> TermHead -> Maybe TermHead
    forall a b. (a -> b) -> a -> b
    $ QName -> TermHead
    ConsHead QName
    f
              no :: TCMT IO (Maybe a)
    no  = Maybe a -> TCMT IO (Maybe a)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe a -> TCMT IO (Maybe a)) -> Maybe a -> TCMT IO (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ Maybe a
    forall a. Maybe a
    Nothing
          def <- Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do TCMT IO Definition -> TCMT IO Definition
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (TCMT IO Definition -> TCMT IO Definition)
    -> TCMT IO Definition -> TCMT IO Definition
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
            -- Andreas, 2013-02-18
            -- if we do not ignoreAbstractMode here, abstract Functions get turned
            -- into Axioms, but we want to distinguish these.
          case def of
            Datatype{}  -> TCM (Maybe TermHead)
    yes
            Record{}    -> TCM (Maybe TermHead)
    yes
            DataOrRecSig{} -> TCM (Maybe TermHead)
    yes
            Axiom{}     -> do
              [Char] -> Nat -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.inj.axiom" Nat
    50 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "headSymbol: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    f [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " is an Axiom."
              -- Don't treat axioms in the current mutual block
              -- as constructors (they might have definitions we
              -- don't know about yet).
              TCMT IO (Maybe MutualId)
    -> TCM (Maybe TermHead)
    -> (MutualId -> TCM (Maybe TermHead))
    -> TCM (Maybe TermHead)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM ((TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
    forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
    asksTC TCEnv -> Maybe MutualId
    envMutualBlock) TCM (Maybe TermHead)
    yes ((MutualId -> TCM (Maybe TermHead)) -> TCM (Maybe TermHead))
    -> (MutualId -> TCM (Maybe TermHead)) -> TCM (Maybe TermHead)
    forall a b. (a -> b) -> a -> b
    $ \ MutualId
    mb -> do
                fs <- MutualBlock -> Set QName
    mutualNames (MutualBlock -> Set QName)
    -> TCMT IO MutualBlock -> TCMT IO (Set QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MutualId -> TCMT IO MutualBlock
    forall (tcm :: * -> *).
    ReadTCState tcm =>
    MutualId -> tcm MutualBlock
    lookupMutualBlock MutualId
    mb
                if Set.member f fs then no else yes
            Function{}    -> TCM (Maybe TermHead)
    forall {a}. TCMT IO (Maybe a)
    no
            Primitive{}   -> TCM (Maybe TermHead)
    forall {a}. TCMT IO (Maybe a)
    no
            PrimitiveSort{} -> TCM (Maybe TermHead)
    forall {a}. TCMT IO (Maybe a)
    no
            GeneralizableVar{} -> TCM (Maybe TermHead)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            Constructor{} -> TCM (Maybe TermHead)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            AbstractDefn{}-> TCM (Maybe TermHead)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        -- Andreas, 2019-07-10, issue #3900: canonicalName needs ignoreAbstractMode
        Con ConHead
    c ConInfo
    _ Elims
    _ -> TCM (Maybe TermHead) -> TCM (Maybe TermHead)
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (TCM (Maybe TermHead) -> TCM (Maybe TermHead))
    -> TCM (Maybe TermHead) -> TCM (Maybe TermHead)
    forall a b. (a -> b) -> a -> b
    $ do
                     q <- QName -> TCMT IO QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName (ConHead -> QName
    conName ConHead
    c)
                     ifM (isPathCons q) (return Nothing) $
                         {- else -}     return $ Just $ ConsHead q
        Sort Sort
    _  -> Maybe TermHead -> TCM (Maybe TermHead)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TermHead -> Maybe TermHead
    forall a. a -> Maybe a
    Just TermHead
    SortHead)
        Pi Dom Type
    _ Abs Type
    _  -> Maybe TermHead -> TCM (Maybe TermHead)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TermHead -> Maybe TermHead
    forall a. a -> Maybe a
    Just TermHead
    PiHead)
        Var Nat
    i [] -> Maybe TermHead -> TCM (Maybe TermHead)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TermHead -> Maybe TermHead
    forall a. a -> Maybe a
    Just (TermHead -> Maybe TermHead) -> TermHead -> Maybe TermHead
    forall a b. (a -> b) -> a -> b
    $ Nat -> TermHead
    VarHead Nat
    i) -- Only naked variables. Otherwise substituting a neutral term is not guaranteed to stay neutral.
        Lit Literal
    _   -> Maybe TermHead -> TCM (Maybe TermHead)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing -- TODO: LitHead (for literals with no constructorForm)
        Lam{}   -> Maybe TermHead -> TCM (Maybe TermHead)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
        Var{}   -> Maybe TermHead -> TCM (Maybe TermHead)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
        Level{} -> Maybe TermHead -> TCM (Maybe TermHead)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
        MetaV{} -> Maybe TermHead -> TCM (Maybe TermHead)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
        DontCare{} -> Maybe TermHead -> TCM (Maybe TermHead)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
        Dummy [Char]
    s Elims
    _ -> [Char] -> TCM (Maybe TermHead)
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__ [Char]
    s

    -- | Is this a matchable definition, or constructor, which reduces based
    -- on interval substitutions?
    isUnstableDef :: PureTCM m => QName -> m Bool
    isUnstableDef :: forall (m :: * -> *). PureTCM m => QName -> m Bool
    isUnstableDef QName
    qn = do
      defn <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    qn
      prims <- traverse getPrimitiveName'
        [ builtinHComp
        , builtinComp
        , builtinTrans
        , builtinGlue
        , builtin_glue
        , builtin_glueU ]
      case theDef defn of
        Defn
    _ | (QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    qn) Maybe QName -> [Maybe QName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Maybe QName]
    prims -> Bool -> m Bool
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    True
        Function{funIsKanOp :: Defn -> Maybe QName
    funIsKanOp = Just QName
    _} -> Bool -> m Bool
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    True
        Defn
    _ -> Bool -> m Bool
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False

    -- | Do a full whnf and treat neutral terms as rigid. Used on the arguments to
    --   an injective functions and to the right-hand side. Only returns
    --   heads which are stable under interval substitution, i.e. NOT path
    --   constructors or generated hcomp/transp!
    headSymbol'
      :: (PureTCM m, MonadError TCErr m)
      => Term -> m (Maybe TermHead)
    headSymbol' :: forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m) =>
    Term -> m (Maybe TermHead)
    headSymbol' Term
    v = do
      v <- (Term -> m Term) -> Blocked' Term Term -> m (Blocked' Term Term)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Blocked' Term a -> f (Blocked' Term b)
    traverse Term -> m Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm (Blocked' Term Term -> m (Blocked' Term Term))
    -> m (Blocked' Term Term) -> m (Blocked' Term Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> m (Blocked' Term Term)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Term
    v
      case v of
        Blocked{} -> Maybe TermHead -> m (Maybe TermHead)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
        NotBlocked NotBlocked' Term
    _ Term
    v -> case Term
    v of
          Def QName
    g Elims
    _    ->
            m Bool
    -> m (Maybe TermHead) -> m (Maybe TermHead) -> m (Maybe TermHead)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> m Bool
    forall (m :: * -> *). PureTCM m => QName -> m Bool
    isUnstableDef QName
    g)
              (Maybe TermHead -> m (Maybe TermHead)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe TermHead
    forall a. Maybe a
    Nothing)
              (Maybe TermHead -> m (Maybe TermHead)
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Maybe TermHead -> m (Maybe TermHead))
    -> (TermHead -> Maybe TermHead) -> TermHead -> m (Maybe TermHead)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TermHead -> Maybe TermHead
    forall a. a -> Maybe a
    Just (TermHead -> m (Maybe TermHead)) -> TermHead -> m (Maybe TermHead)
    forall a b. (a -> b) -> a -> b
    $ QName -> TermHead
    ConsHead QName
    g)
          Con ConHead
    c ConInfo
    _ Elims
    _  -> do
            q <- QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName (ConHead -> QName
    conName ConHead
    c)
            ifM (isPathCons q)
              (pure Nothing)
              (return $ Just $ ConsHead q)
          Var Nat
    i Elims
    _    -> Maybe TermHead -> m (Maybe TermHead)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe TermHead -> m (Maybe TermHead))
    -> Maybe TermHead -> m (Maybe TermHead)
    forall a b. (a -> b) -> a -> b
    $ TermHead -> Maybe TermHead
    forall a. a -> Maybe a
    Just (Nat -> TermHead
    VarHead Nat
    i)
          Sort Sort
    _     -> Maybe TermHead -> m (Maybe TermHead)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe TermHead -> m (Maybe TermHead))
    -> Maybe TermHead -> m (Maybe TermHead)
    forall a b. (a -> b) -> a -> b
    $ TermHead -> Maybe TermHead
    forall a. a -> Maybe a
    Just TermHead
    SortHead
          Pi Dom Type
    _ Abs Type
    _     -> Maybe TermHead -> m (Maybe TermHead)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe TermHead -> m (Maybe TermHead))
    -> Maybe TermHead -> m (Maybe TermHead)
    forall a b. (a -> b) -> a -> b
    $ TermHead -> Maybe TermHead
    forall a. a -> Maybe a
    Just TermHead
    PiHead
          Lit Literal
    _      -> Maybe TermHead -> m (Maybe TermHead)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
          Lam{}      -> Maybe TermHead -> m (Maybe TermHead)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
          Level{}    -> Maybe TermHead -> m (Maybe TermHead)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
          DontCare{} -> Maybe TermHead -> m (Maybe TermHead)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
          MetaV{}    -> m (Maybe TermHead)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          Dummy [Char]
    s Elims
    _  -> [Char] -> m (Maybe TermHead)
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__ [Char]
    s

    -- | Does deBruijn variable i correspond to a top-level argument, and if so
    --   which one (index from the left).
    topLevelArg :: Clause -> Int -> Maybe TermHead
    topLevelArg :: Clause -> Nat -> Maybe TermHead
    topLevelArg Clause{ namedClausePats :: Clause -> NAPs
    namedClausePats = NAPs
    ps } Nat
    i =
      case [ Nat
    n | (Nat
    n, VarP PatternInfo
    _ (DBPatVar [Char]
    _ Nat
    j)) <- [Nat] -> [DeBruijnPattern] -> [(Nat, DeBruijnPattern)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Nat
    0..] ([DeBruijnPattern] -> [(Nat, DeBruijnPattern)])
    -> [DeBruijnPattern] -> [(Nat, DeBruijnPattern)]
    forall a b. (a -> b) -> a -> b
    $ (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> NAPs -> [DeBruijnPattern]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg NAPs
    ps, Nat
    i Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    j ] of
        []    -> Maybe TermHead
    forall a. Maybe a
    Nothing
        [Nat
    n]   -> TermHead -> Maybe TermHead
    forall a. a -> Maybe a
    Just (Nat -> TermHead
    VarHead Nat
    n)
        Nat
    _:Nat
    _:[Nat]
    _ -> Maybe TermHead
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Join a list of inversion maps.
    joinHeadMaps :: [InversionMap c] -> InversionMap c
    joinHeadMaps :: forall c. [InversionMap c] -> InversionMap c
    joinHeadMaps = ([c] -> [c] -> [c]) -> [Map TermHead [c]] -> Map TermHead [c]
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    (a -> a -> a) -> f (Map k a) -> Map k a
    Map.unionsWith [c] -> [c] -> [c]
    forall a. Semigroup a => a -> a -> a
    (<>)

    -- | Update the heads of an inversion map.
    updateHeads :: Monad m => (TermHead -> [c] -> m TermHead) -> InversionMap c -> m (InversionMap c)
    updateHeads :: forall (m :: * -> *) c.
    Monad m =>
    (TermHead -> [c] -> m TermHead)
    -> InversionMap c -> m (InversionMap c)
    updateHeads TermHead -> [c] -> m TermHead
    f InversionMap c
    m = [InversionMap c] -> InversionMap c
    forall c. [InversionMap c] -> InversionMap c
    joinHeadMaps ([InversionMap c] -> InversionMap c)
    -> m [InversionMap c] -> m (InversionMap c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((TermHead, [c]) -> m (InversionMap c))
    -> [(TermHead, [c])] -> m [InversionMap c]
    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 (TermHead, [c]) -> m (InversionMap c)
    f' (InversionMap c -> [(TermHead, [c])]
    forall k a. Map k a -> [(k, a)]
    Map.toList InversionMap c
    m)
      where f' :: (TermHead, [c]) -> m (InversionMap c)
    f' (TermHead
    h, [c]
    c) = (TermHead -> [c] -> InversionMap c
    forall k a. k -> a -> Map k a
    `Map.singleton` [c]
    c) (TermHead -> InversionMap c) -> m TermHead -> m (InversionMap c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TermHead -> [c] -> m TermHead
    f TermHead
    h [c]
    c

    checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
    checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
    checkInjectivity QName
    f [Clause]
    cs0 = do
        TCMT IO Bool
    -> TCM FunctionInverse
    -> TCM FunctionInverse
    -> TCM FunctionInverse
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ((Clause -> TCMT IO Bool) -> [Clause] -> TCMT IO Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Foldable f, Monad m) =>
    (a -> m Bool) -> f a -> m Bool
    anyM Clause -> TCMT IO Bool
    properlyMatchingClause [Clause]
    cs) {-then-} (QName -> [Clause] -> TCM FunctionInverse
    checkInjectivity' QName
    f [Clause]
    cs) {-else-} do
          [Char] -> Nat -> [Char] -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.inj.check.pointless" Nat
    35 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            [Char]
    "Injectivity of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (QName -> QName
    A.qnameToConcrete QName
    f) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " would be pointless."
          FunctionInverse -> TCM FunctionInverse
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return FunctionInverse
    forall c. FunctionInverse' c
    NotInjective
      where
        -- We can filter out absurd clauses.
        cs :: [Clause]
    cs = (Clause -> Bool) -> [Clause] -> [Clause]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Maybe Term -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Term -> Bool) -> (Clause -> Maybe Term) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Maybe Term
    clauseBody) [Clause]
    cs0
        -- We cannot filter out clauses that have no proper match, because
        -- these could be catch-all clauses.
        -- However, we need at least one proper match to get injectivity started.
        properlyMatchingClause :: Clause -> TCMT IO Bool
    properlyMatchingClause =
          (NamedArg DeBruijnPattern -> TCMT IO Bool) -> NAPs -> TCMT IO Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Foldable f, Monad m) =>
    (a -> m Bool) -> f a -> m Bool
    anyM (Bool -> Bool -> DeBruijnPattern -> TCMT IO Bool
    forall (m :: * -> *) a.
    HasConstInfo m =>
    Bool -> Bool -> Pattern' a -> m Bool
    properlyMatching' Bool
    False Bool
    False (DeBruijnPattern -> TCMT IO Bool)
    -> (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> TCMT IO Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) (NAPs -> TCMT IO Bool)
    -> (Clause -> NAPs) -> Clause -> TCMT IO Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> NAPs
    namedClausePats

    -- | Precondition: all the given clauses are non-absurd and contain a proper match.
    checkInjectivity' :: QName -> [Clause] -> TCM FunctionInverse
    checkInjectivity' :: QName -> [Clause] -> TCM FunctionInverse
    checkInjectivity' QName
    f [Clause]
    cs = FunctionInverse -> Maybe FunctionInverse -> FunctionInverse
    forall a. a -> Maybe a -> a
    fromMaybe FunctionInverse
    forall c. FunctionInverse' c
    NotInjective (Maybe FunctionInverse -> FunctionInverse)
    -> (MaybeT (TCMT IO) FunctionInverse
        -> TCMT IO (Maybe FunctionInverse))
    -> MaybeT (TCMT IO) FunctionInverse
    -> TCM FunctionInverse
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> MaybeT (TCMT IO) FunctionInverse -> TCMT IO (Maybe FunctionInverse)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT (TCMT IO) FunctionInverse -> TCM FunctionInverse)
    -> MaybeT (TCMT IO) FunctionInverse -> TCM FunctionInverse
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Nat -> [Char] -> MaybeT (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "tc.inj.check" Nat
    40 ([Char] -> MaybeT (TCMT IO) ()) -> [Char] -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Checking injectivity of " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    f

      let varToArg :: Clause -> TermHead -> MaybeT TCM TermHead
          varToArg :: Clause -> TermHead -> MaybeT (TCMT IO) TermHead
    varToArg Clause
    c (VarHead Nat
    i) = TCM (Maybe TermHead) -> MaybeT (TCMT IO) TermHead
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (TCM (Maybe TermHead) -> MaybeT (TCMT IO) TermHead)
    -> TCM (Maybe TermHead) -> MaybeT (TCMT IO) TermHead
    forall a b. (a -> b) -> a -> b
    $ Maybe TermHead -> TCM (Maybe TermHead)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe TermHead -> TCM (Maybe TermHead))
    -> Maybe TermHead -> TCM (Maybe TermHead)
    forall a b. (a -> b) -> a -> b
    $ Clause -> Nat -> Maybe TermHead
    topLevelArg Clause
    c Nat
    i
          varToArg Clause
    _ TermHead
    h           = TermHead -> MaybeT (TCMT IO) TermHead
    forall a. a -> MaybeT (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TermHead
    h

      -- We don't need to consider absurd clauses
      let computeHead :: Clause -> MaybeT (TCMT IO) [Map TermHead [Clause]]
    computeHead Clause
    c | NAPs -> Bool
    hasDefP (Clause -> NAPs
    namedClausePats Clause
    c) = [Map TermHead [Clause]] -> MaybeT (TCMT IO) [Map TermHead [Clause]]
    forall a. a -> MaybeT (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          -- hasDefP clauses are skipped, these matter only for --cubical, in which case the function will behave as NotInjective.
          computeHead c :: Clause
    c@Clause{ clauseBody :: Clause -> Maybe Term
    clauseBody = Just Term
    body , clauseType :: Clause -> Maybe (Arg Type)
    clauseType = Just Arg Type
    tbody } = Telescope
    -> MaybeT (TCMT IO) [Map TermHead [Clause]]
    -> MaybeT (TCMT IO) [Map TermHead [Clause]]
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext (Clause -> Telescope
    clauseTel Clause
    c) (MaybeT (TCMT IO) [Map TermHead [Clause]]
     -> MaybeT (TCMT IO) [Map TermHead [Clause]])
    -> MaybeT (TCMT IO) [Map TermHead [Clause]]
    -> MaybeT (TCMT IO) [Map TermHead [Clause]]
    forall a b. (a -> b) -> a -> b
    $ do
            maybeIrr <- (Blocker -> Bool) -> Either Blocker Bool -> Bool
    forall a b. (a -> b) -> Either a b -> b
    fromRight (Bool -> Blocker -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (Either Blocker Bool -> Bool)
    -> (BlockT (MaybeT (TCMT IO)) Bool
        -> MaybeT (TCMT IO) (Either Blocker Bool))
    -> BlockT (MaybeT (TCMT IO)) Bool
    -> MaybeT (TCMT IO) Bool
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> BlockT (MaybeT (TCMT IO)) Bool
    -> MaybeT (TCMT IO) (Either Blocker Bool)
    forall (m :: * -> *) a.
    Monad m =>
    BlockT m a -> m (Either Blocker a)
    runBlocked (BlockT (MaybeT (TCMT IO)) Bool -> MaybeT (TCMT IO) Bool)
    -> BlockT (MaybeT (TCMT IO)) Bool -> MaybeT (TCMT IO) Bool
    forall a b. (a -> b) -> a -> b
    $ Arg Type -> BlockT (MaybeT (TCMT IO)) Bool
    forall a (m :: * -> *).
    (LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
     MonadBlock m) =>
    a -> m Bool
    isIrrelevantOrPropM Arg Type
    tbody
            -- We treat ordinary clauses with IApply copatterns as *immediately*
            -- failing the injectivity check. Consider e.g.
            --   foo x = T
            --   foo (y i) = Glue U λ { (i = i0) → T , _ ; (i = i1) → T , _ }
            -- seeing foo α = Glue ... and inverting it to α = y β loses solutions. E.g. if we
            -- later had some other α = x, now we're screwed, x ≠ y β. But if we had postponed
            -- originally we'd just compare T = Glue ... which has a chance of going through.
            let ivars = NAPs -> [Nat]
    forall p. IApplyVars p => p -> [Nat]
    iApplyVars (Clause -> NAPs
    namedClausePats Clause
    c)
            guard (null ivars)
            h <- if maybeIrr then return UnknownHead else
              varToArg c =<< do
                lift $ fromMaybe UnknownHead <$> do
                  headSymbol body
            return [Map.singleton h [c]]
          computeHead Clause
    _ = [Map TermHead [Clause]] -> MaybeT (TCMT IO) [Map TermHead [Clause]]
    forall a. a -> MaybeT (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

      hdMap <- [Map TermHead [Clause]] -> Map TermHead [Clause]
    forall c. [InversionMap c] -> InversionMap c
    joinHeadMaps ([Map TermHead [Clause]] -> Map TermHead [Clause])
    -> ([[Map TermHead [Clause]]] -> [Map TermHead [Clause]])
    -> [[Map TermHead [Clause]]]
    -> Map TermHead [Clause]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [[Map TermHead [Clause]]] -> [Map TermHead [Clause]]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[Map TermHead [Clause]]] -> Map TermHead [Clause])
    -> MaybeT (TCMT IO) [[Map TermHead [Clause]]]
    -> MaybeT (TCMT IO) (Map TermHead [Clause])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Clause -> MaybeT (TCMT IO) [Map TermHead [Clause]])
    -> [Clause] -> MaybeT (TCMT IO) [[Map TermHead [Clause]]]
    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 Clause -> MaybeT (TCMT IO) [Map TermHead [Clause]]
    computeHead [Clause]
    cs

      case Map.lookup UnknownHead hdMap of
        Just (Clause
    _:Clause
    _:[Clause]
    _) -> MaybeT (TCMT IO) ()
    forall a. MaybeT (TCMT IO) a
    forall (f :: * -> *) a. Alternative f => f a
    empty -- More than one unknown head: we can't really do anything in that case.
        Maybe [Clause]
    _            -> () -> MaybeT (TCMT IO) ()
    forall a. a -> MaybeT (TCMT IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

      reportSLn  "tc.inj.check" 20 $ prettyShow f ++ " is potentially injective."
      reportSDoc "tc.inj.check" 30 $ nest 2 $ vcat $
        for (Map.toList hdMap) $ \ (TermHead
    h, [Clause]
    uc) ->
          [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (TermHead -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow TermHead
    h) 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
    <+>
          case [Clause]
    uc of
            [Clause
    c] -> [DeBruijnPattern] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [DeBruijnPattern] -> m Doc
    prettyTCM ([DeBruijnPattern] -> TCMT IO Doc)
    -> [DeBruijnPattern] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> NAPs -> [DeBruijnPattern]
    forall a b. (a -> b) -> [a] -> [b]
    map NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg (NAPs -> [DeBruijnPattern]) -> NAPs -> [DeBruijnPattern]
    forall a b. (a -> b) -> a -> b
    $ Clause -> NAPs
    namedClausePats Clause
    c
            [Clause]
    _   -> TCMT IO Doc
    "(multiple clauses)"
      return $ Inverse hdMap

    -- | If a clause is over-applied we can't trust the head (Issue 2944). For
    --   instance, the clause might be `f ps = u , v` and the actual call `f vs
    --   .fst`. In this case the head will be the head of `u` rather than `_,_`.
    checkOverapplication
      :: forall m. (HasConstInfo m)
      => Elims -> InversionMap Clause -> m (InversionMap Clause)
    checkOverapplication :: forall (m :: * -> *).
    HasConstInfo m =>
    Elims -> Map TermHead [Clause] -> m (Map TermHead [Clause])
    checkOverapplication Elims
    es = (TermHead -> [Clause] -> m TermHead)
    -> Map TermHead [Clause] -> m (Map TermHead [Clause])
    forall (m :: * -> *) c.
    Monad m =>
    (TermHead -> [c] -> m TermHead)
    -> InversionMap c -> m (InversionMap c)
    updateHeads TermHead -> [Clause] -> m TermHead
    overapplied
      where
        overapplied :: TermHead -> [Clause] -> m TermHead
        overapplied :: TermHead -> [Clause] -> m TermHead
    overapplied TermHead
    h [Clause]
    cs | (Clause -> Bool) -> [Clause] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Bool -> Bool
    not (Bool -> Bool) -> (Clause -> Bool) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Bool
    isOverapplied) [Clause]
    cs = TermHead -> m TermHead
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TermHead
    h
        overapplied TermHead
    h [Clause]
    cs = m Bool -> m TermHead -> m TermHead -> m TermHead
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (TermHead -> m Bool
    forall {m :: * -> *}. HasConstInfo m => TermHead -> m Bool
    isSuperRigid TermHead
    h) (TermHead -> m TermHead
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TermHead
    h) (TermHead -> m TermHead
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TermHead
    UnknownHead)

        -- A super-rigid head is one that can't be eliminated. Crucially, this is
        -- applied after instantiateVars, so VarHeads are really bound variables.
        isSuperRigid :: TermHead -> m Bool
    isSuperRigid TermHead
    SortHead     = Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        isSuperRigid TermHead
    PiHead       = Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        isSuperRigid VarHead{}    = Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        isSuperRigid TermHead
    UnknownHead  = Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True -- or False, doesn't matter
        isSuperRigid (ConsHead QName
    q) = do
          def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
          return $ case theDef def of
            Axiom{}        -> Bool
    True
            DataOrRecSig{} -> Bool
    True
            AbstractDefn{} -> Bool
    True
            Function{}     -> Bool
    False
            Datatype{}     -> Bool
    True
            Record{}       -> Bool
    True
            Constructor{conSrcCon :: Defn -> ConHead
    conSrcCon = ConHead{ conDataRecord :: ConHead -> DataOrRecord
    conDataRecord = DataOrRecord
    d, conFields :: ConHead -> [Arg QName]
    conFields = [Arg QName]
    fs }}
                           -> DataOrRecord
    d DataOrRecord -> DataOrRecord -> Bool
    forall a. Eq a => a -> a -> Bool
    == DataOrRecord
    forall p. DataOrRecord' p
    IsData Bool -> Bool -> Bool
    || [Arg QName] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Arg QName]
    fs   -- Record constructors can be eliminated by projections
            Primitive{}    -> Bool
    False
            PrimitiveSort{} -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            GeneralizableVar{} -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        isOverapplied :: Clause -> Bool
    isOverapplied Clause{ namedClausePats :: Clause -> NAPs
    namedClausePats = NAPs
    ps } = Elims -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Elims
    es Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > NAPs -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length NAPs
    ps

    -- | Turn variable heads, referring to top-level argument positions, into
    --   proper heads. These might still be `VarHead`, but in that case they refer to
    --   deBruijn variables. Checks that the instantiated heads are still rigid and
    --   distinct.
    instantiateVarHeads
      :: forall m c. (PureTCM m, MonadError TCErr m)
      => QName -> Elims -> InversionMap c -> m (Maybe (InversionMap c))
    instantiateVarHeads :: forall (m :: * -> *) c.
    (PureTCM m, MonadError TCErr m) =>
    QName -> Elims -> InversionMap c -> m (Maybe (InversionMap c))
    instantiateVarHeads QName
    f Elims
    es InversionMap c
    m = MaybeT m (InversionMap c) -> m (Maybe (InversionMap c))
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT m (InversionMap c) -> m (Maybe (InversionMap c)))
    -> MaybeT m (InversionMap c) -> m (Maybe (InversionMap c))
    forall a b. (a -> b) -> a -> b
    $ (TermHead -> [c] -> MaybeT m TermHead)
    -> InversionMap c -> MaybeT m (InversionMap c)
    forall (m :: * -> *) c.
    Monad m =>
    (TermHead -> [c] -> m TermHead)
    -> InversionMap c -> m (InversionMap c)
    updateHeads (MaybeT m TermHead -> [c] -> MaybeT m TermHead
    forall a b. a -> b -> a
    const (MaybeT m TermHead -> [c] -> MaybeT m TermHead)
    -> (TermHead -> MaybeT m TermHead)
    -> TermHead
    -> [c]
    -> MaybeT m TermHead
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TermHead -> MaybeT m TermHead
    instHead) InversionMap c
    m
      where
        instHead :: TermHead -> MaybeT m TermHead
        instHead :: TermHead -> MaybeT m TermHead
    instHead h :: TermHead
    h@(VarHead Nat
    i)
          | Just (Apply Arg Term
    arg) <- Elims
    es Elims -> Nat -> Maybe Elim
    forall a. [a] -> Nat -> Maybe a
    !!! Nat
    i = m (Maybe TermHead) -> MaybeT m TermHead
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (m (Maybe TermHead) -> MaybeT m TermHead)
    -> m (Maybe TermHead) -> MaybeT m TermHead
    forall a b. (a -> b) -> a -> b
    $ Term -> m (Maybe TermHead)
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m) =>
    Term -> m (Maybe TermHead)
    headSymbol' (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg)
          | Bool
    otherwise = MaybeT m TermHead
    forall a. MaybeT m a
    forall (f :: * -> *) a. Alternative f => f a
    empty   -- impossible?
        instHead TermHead
    h = TermHead -> MaybeT m TermHead
    forall a. a -> MaybeT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return TermHead
    h

    -- | Argument should be in weak head normal form.
    functionInverse
      :: (PureTCM m, MonadError TCErr m)
      => Term -> m InvView
    functionInverse :: forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m) =>
    Term -> m InvView
    functionInverse = \case
      Def QName
    f Elims
    es -> do
        inv <- Definition -> FunctionInverse
    defInverse (Definition -> FunctionInverse)
    -> m Definition -> m FunctionInverse
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
        cubical <- cubicalOption
        case inv of
          FunctionInverse
    NotInjective -> InvView -> m InvView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return InvView
    NoInv
          Inverse Map TermHead [Clause]
    m -> InvView
    -> (Map TermHead [Clause] -> InvView)
    -> Maybe (Map TermHead [Clause])
    -> InvView
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe InvView
    NoInv (QName -> Elims -> Map TermHead [Clause] -> InvView
    Inv QName
    f Elims
    es) (Maybe (Map TermHead [Clause]) -> InvView)
    -> m (Maybe (Map TermHead [Clause])) -> m InvView
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Map TermHead [Clause] -> m (Map TermHead [Clause]))
    -> Maybe (Map TermHead [Clause])
    -> m (Maybe (Map TermHead [Clause]))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Maybe a -> f (Maybe b)
    traverse (Elims -> Map TermHead [Clause] -> m (Map TermHead [Clause])
    forall (m :: * -> *).
    HasConstInfo m =>
    Elims -> Map TermHead [Clause] -> m (Map TermHead [Clause])
    checkOverapplication Elims
    es) (Maybe (Map TermHead [Clause])
     -> m (Maybe (Map TermHead [Clause])))
    -> m (Maybe (Map TermHead [Clause]))
    -> m (Maybe (Map TermHead [Clause]))
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName
    -> Elims
    -> Map TermHead [Clause]
    -> m (Maybe (Map TermHead [Clause]))
    forall (m :: * -> *) c.
    (PureTCM m, MonadError TCErr m) =>
    QName -> Elims -> InversionMap c -> m (Maybe (InversionMap c))
    instantiateVarHeads QName
    f Elims
    es Map TermHead [Clause]
    m)
            -- NB: Invertible functions are never classified as
            --     projection-like, so this is fine, we are not
            --     missing parameters.  (Andreas, 2013-11-01)
      Term
    _ -> InvView -> m InvView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return InvView
    NoInv

    data InvView = Inv QName [Elim] (InversionMap Clause)
                 | NoInv

    -- | Precondition: The first term must be blocked on the given meta and the second must be neutral.
    useInjectivity :: MonadConversion m => CompareDirection -> Blocker -> CompareAs -> Term -> Term -> m ()
    useInjectivity :: forall (m :: * -> *).
    MonadConversion m =>
    CompareDirection -> Blocker -> CompareAs -> Term -> Term -> m ()
    useInjectivity CompareDirection
    dir Blocker
    blocker CompareAs
    ty Term
    blk Term
    neu = Lens' TCEnv Nat -> (Nat -> Nat) -> m () -> m ()
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (Nat -> f Nat) -> TCEnv -> f TCEnv
    Lens' TCEnv Nat
    eInjectivityDepth Nat -> Nat
    forall a. Enum a => a -> a
    succ (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
      inv <- Term -> m InvView
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m) =>
    Term -> m InvView
    functionInverse Term
    blk
      -- Injectivity might cause non-termination for unsatisfiable constraints
      -- (#431, #3067). Look at the number of active problems and the injectivity
      -- depth to detect this.
      nProblems <- Set.size <$> viewTC eActiveProblems
      injDepth  <- viewTC eInjectivityDepth
      let depth = Nat -> Nat -> Nat
    forall a. Ord a => a -> a -> a
    max Nat
    nProblems Nat
    injDepth
      maxDepth  <- maxInversionDepth
      case inv of
        InvView
    NoInv            -> m ()
    fallback  -- not invertible
        Inv QName
    f Elims
    blkArgs Map TermHead [Clause]
    hdMap
          | Nat
    depth Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    maxDepth -> Warning -> m ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (QName -> Warning
    InversionDepthReached QName
    f) m () -> m () -> m ()
    forall a b. m a -> m b -> m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> m ()
    fallback
          | Bool
    otherwise -> do
          [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.inj.use" Nat
    30 (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] -> 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]
    pwords [Char]
    "useInjectivity on" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++
            [ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    blk, Comparison -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
    prettyTCM Comparison
    cmp, Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    neu, CompareAs -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => CompareAs -> m Doc
    prettyTCM CompareAs
    ty]
          ProfileOption -> m () -> m ()
    forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
    whenProfile ProfileOption
    Profile.Conversion (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> m ()
    forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
    tick [Char]
    "compare by reduction: injectivity"
          let canReduceToSelf :: Bool
    canReduceToSelf = TermHead -> Map TermHead [Clause] -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    Map.member (QName -> TermHead
    ConsHead QName
    f) Map TermHead [Clause]
    hdMap Bool -> Bool -> Bool
    || TermHead -> Map TermHead [Clause] -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    Map.member TermHead
    UnknownHead Map TermHead [Clause]
    hdMap
          case Term
    neu of
            -- f us == f vs  <=>  us == vs
            -- Crucially, this relies on `f vs` being neutral and only works
            -- if `f` is not a possible head for `f us`.
            Def QName
    f' Elims
    neuArgs | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f', Bool -> Bool
    not Bool
    canReduceToSelf -> do
              fTy <- Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
              reportSDoc "tc.inj.use" 20 $ vcat
                [ fsep (pwords "comparing application of injective function" ++ [prettyTCM f] ++
                      pwords "at")
                , nest 2 $ fsep $ punctuate comma $ map prettyTCM blkArgs
                , nest 2 $ fsep $ punctuate comma $ map prettyTCM neuArgs
                , nest 2 $ "and type" <+> prettyTCM fTy
                ]
              fs  <- getForcedArgs f
              pol <- getPolarity' cmp f
              reportSDoc "tc.inj.invert.success" 20 $ hsep ["Successful spine comparison of", prettyTCM f]
              whenProfile Profile.Conversion $ tick "compare by reduction: injectivity successful"
              app (compareElims pol fs fTy (Def f [])) blkArgs neuArgs

            -- f us == c vs
            --    Find the clause unique clause `f ps` with head `c` and unify
            --    us == ps  with fresh metas for the pattern variables of ps.
            --    If there's no such clause we can safely throw an error.
            Term
    _ -> Term -> m (Maybe TermHead)
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m) =>
    Term -> m (Maybe TermHead)
    headSymbol' Term
    neu m (Maybe TermHead) -> (Maybe TermHead -> m ()) -> m ()
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ case
              Maybe TermHead
    Nothing -> do
                [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.inj.use" Nat
    20 (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] -> 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]
    pwords [Char]
    "no head symbol found for" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    neu] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [TCMT IO Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    ", so not inverting"
                m ()
    fallback
              Just (ConsHead QName
    f') | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f', Bool
    canReduceToSelf -> do
                [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.inj.use" Nat
    20 (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] -> 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]
    pwords [Char]
    "head symbol" [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++ [QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    f'] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [TCMT IO Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "can reduce to self, so not inverting"
                m ()
    fallback
                                        -- We can't invert in this case, since we can't
                                        -- tell the difference between a solution that makes
                                        -- the blocked term neutral and one that makes progress.
              Just TermHead
    hd -> Comparison
    -> Term
    -> InvView
    -> TermHead
    -> m ()
    -> m ()
    -> (Term -> m ())
    -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison
    -> Term
    -> InvView
    -> TermHead
    -> m ()
    -> m ()
    -> (Term -> m ())
    -> m ()
    invertFunction Comparison
    cmp Term
    blk InvView
    inv TermHead
    hd m ()
    fallback m ()
    err Term -> m ()
    success
                where err :: m ()
    err = TypeError -> m ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m ()) -> TypeError -> m ()
    forall a b. (a -> b) -> a -> b
    $ (Term -> Term -> TypeError) -> Term -> Term -> TypeError
    forall {a} {b}. (a -> a -> b) -> a -> a -> b
    app (\ Term
    u Term
    v -> Comparison -> Term -> Term -> CompareAs -> TypeError
    UnequalTerms Comparison
    cmp Term
    u Term
    v CompareAs
    ty) Term
    blk Term
    neu
      where
        fallback :: m ()
    fallback     = Blocker -> Constraint -> m ()
    forall (m :: * -> *).
    MonadConstraint m =>
    Blocker -> Constraint -> m ()
    addConstraint Blocker
    blocker (Constraint -> m ()) -> Constraint -> m ()
    forall a b. (a -> b) -> a -> b
    $ (Term -> Term -> Constraint) -> Term -> Term -> Constraint
    forall {a} {b}. (a -> a -> b) -> a -> a -> b
    app (Comparison -> CompareAs -> Term -> Term -> Constraint
    ValueCmp Comparison
    cmp CompareAs
    ty) Term
    blk Term
    neu
        success :: Term -> m ()
    success Term
    blk' = (Term -> Term -> m ()) -> Term -> Term -> m ()
    forall {a} {b}. (a -> a -> b) -> a -> a -> b
    app (Comparison -> CompareAs -> Term -> Term -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison -> CompareAs -> Term -> Term -> m ()
    compareAs Comparison
    cmp CompareAs
    ty) Term
    blk' Term
    neu

        cmpApp :: (Comparison, (a -> a -> b) -> a -> a -> b)
        cmpApp :: forall a b. (Comparison, (a -> a -> b) -> a -> a -> b)
    cmpApp = case CompareDirection
    dir of
          CompareDirection
    DirEq -> (Comparison
    CmpEq, (a -> a -> b) -> a -> a -> b
    forall a. a -> a
    id)
          CompareDirection
    DirLeq -> (Comparison
    CmpLeq, (a -> a -> b) -> a -> a -> b
    forall a. a -> a
    id)
          CompareDirection
    DirGeq -> (Comparison
    CmpLeq, (a -> a -> b) -> a -> a -> b
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip)
        (Comparison
    cmp, (a -> a -> b) -> a -> a -> b
    app) = (Comparison, (a -> a -> b) -> a -> a -> b)
    forall a b. (Comparison, (a -> a -> b) -> a -> a -> b)
    cmpApp

    -- | The second argument should be a blocked application and the third argument
    --   the inverse of the applied function.
    invertFunction
      :: MonadConversion m
      => Comparison -> Term -> InvView -> TermHead -> m () -> m () -> (Term -> m ()) -> m ()
    invertFunction :: forall (m :: * -> *).
    MonadConversion m =>
    Comparison
    -> Term
    -> InvView
    -> TermHead
    -> m ()
    -> m ()
    -> (Term -> m ())
    -> m ()
    invertFunction Comparison
    _ Term
    _ InvView
    NoInv TermHead
    _ m ()
    fallback m ()
    _ Term -> m ()
    _ = m ()
    fallback
    invertFunction Comparison
    cmp Term
    blk (Inv QName
    f Elims
    blkArgs Map TermHead [Clause]
    hdMap) TermHead
    hd m ()
    fallback m ()
    err Term -> m ()
    success = do
        fTy <- Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
        reportSDoc "tc.inj.use" 20 $ vcat
          [ "inverting injective function" <?> hsep [prettyTCM f, ":", prettyTCM fTy]
          , "for" <?> pretty hd
          , nest 2 $ "args =" <+> prettyList (map prettyTCM blkArgs)
          ]                         -- Clauses with unknown heads are also possible candidates
        case fromMaybe [] $ Map.lookup hd hdMap <> Map.lookup UnknownHead hdMap of
          [] -> m ()
    err
          Clause
    _:Clause
    _:[Clause]
    _ -> m ()
    fallback
          [cl :: Clause
    cl@Clause{ clauseTel :: Clause -> Telescope
    clauseTel  = Telescope
    tel }] -> m () -> m KeepMetas -> m ()
    forall (m :: * -> *).
    MonadMetaSolver m =>
    m () -> m KeepMetas -> m ()
    speculateMetas m ()
    fallback (m KeepMetas -> m ()) -> m KeepMetas -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
              let ps :: [Arg DeBruijnPattern]
    ps   = Clause -> [Arg DeBruijnPattern]
    clausePats Clause
    cl
                  perm :: Permutation
    perm = Permutation -> Maybe Permutation -> Permutation
    forall a. a -> Maybe a -> a
    fromMaybe Permutation
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Permutation -> Permutation)
    -> Maybe Permutation -> Permutation
    forall a b. (a -> b) -> a -> b
    $ Clause -> Maybe Permutation
    clausePerm Clause
    cl
              -- These are what dot patterns should be instantiated at
              ms <- (Arg Term -> Term) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg ([Arg Term] -> [Term]) -> m [Arg Term] -> m [Term]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope -> m [Arg Term]
    forall (m :: * -> *).
    MonadMetaSolver m =>
    Telescope -> m [Arg Term]
    newTelMeta Telescope
    tel
              reportSDoc "tc.inj.invert" 20 $ vcat
                [ "meta patterns" <+> prettyList (map prettyTCM ms)
                , "  perm =" <+> text (show perm)
                , "  tel  =" <+> prettyTCM tel
                , "  ps   =" <+> prettyList (map (text . prettyShow) ps)
                ]
              -- and this is the order the variables occur in the patterns
              let msAux = Permutation -> [Term] -> [Term]
    forall a. Permutation -> [a] -> [a]
    permute (Nat -> Permutation -> Permutation
    invertP Nat
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Permutation -> Permutation) -> Permutation -> Permutation
    forall a b. (a -> b) -> a -> b
    $ Permutation -> Permutation
    compactP Permutation
    perm) [Term]
    ms
              let sub   = [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> [Term]
    forall a. [a] -> [a]
    reverse [Term]
    ms)
              margs <- runReaderT (evalStateT (mapM metaElim ps) msAux) sub
              reportSDoc "tc.inj.invert" 20 $ vcat
                [ "inversion"
                , nest 2 $ vcat
                  [ "lhs  =" <+> prettyTCM margs
                  , "rhs  =" <+> prettyTCM blkArgs
                  , "type =" <+> prettyTCM fTy
                  ]
                ]
              -- Since we do not care for the value of non-variant metas here,
              -- we can treat 'Nonvariant' as 'Invariant'.
              -- That ensures these metas do not remain unsolved.
              pol <- purgeNonvariant <$> getPolarity' cmp f
              fs  <- getForcedArgs f
              -- The clause might not give as many patterns as there
              -- are arguments (point-free style definitions).
              let blkArgs' = Nat -> Elims -> Elims
    forall a. Nat -> [a] -> [a]
    take (Elims -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Elims
    margs) Elims
    blkArgs
              compareElims pol fs fTy (Def f []) margs blkArgs'

              -- Check that we made progress.
              r <- liftReduce $ unfoldDefinitionStep (Def f []) f blkArgs
              case r of
                YesReduction Simplification
    _ Term
    blk' -> do
                  [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.inj.invert.success" Nat
    20 (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
    hsep [TCMT IO Doc
    "Successful inversion of", QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    f, TCMT IO Doc
    "at", TermHead -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty TermHead
    hd]
                  KeepMetas
    KeepMetas KeepMetas -> m () -> m KeepMetas
    forall a b. a -> m b -> m a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Term -> m ()
    success Term
    blk'
                NoReduction{}       -> do
                  [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.inj.invert" Nat
    30 (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
    vcat
                    [ TCMT IO Doc
    "aborting inversion;" 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
    blk
                    , TCMT IO Doc
    "does not reduce"
                    ]
                  KeepMetas -> m KeepMetas
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return KeepMetas
    RollBackMetas
      where
        nextMeta :: (MonadState [Term] m) => m Term
        nextMeta :: forall (m :: * -> *). MonadState [Term] m => m Term
    nextMeta = do
          (m, ms) <- ([Term] -> (Term, [Term])) -> m (Term, [Term])
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ((Term, [Term]) -> Maybe (Term, [Term]) -> (Term, [Term])
    forall a. a -> Maybe a -> a
    fromMaybe (Term, [Term])
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (Term, [Term]) -> (Term, [Term]))
    -> ([Term] -> Maybe (Term, [Term])) -> [Term] -> (Term, [Term])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Term] -> Maybe (Term, [Term])
    forall a. [a] -> Maybe (a, [a])
    uncons)
          put ms
          return m

        dotP :: MonadReader Substitution m => Term -> m Term
        dotP :: forall (m :: * -> *).
    MonadReader (Substitution' Term) m =>
    Term -> m Term
    dotP Term
    v = do
          sub <- m (Substitution' Term)
    forall r (m :: * -> *). MonadReader r m => m r
    ask
          return $ applySubst sub v

        metaElim
          :: (MonadState [Term] m, MonadReader Substitution m, HasConstInfo m)
          => Arg DeBruijnPattern -> m Elim
        metaElim :: forall (m :: * -> *).
    (MonadState [Term] m, MonadReader (Substitution' Term) m,
     HasConstInfo m) =>
    Arg DeBruijnPattern -> m Elim
    metaElim (Arg ArgInfo
    _ (ProjP ProjOrigin
    o QName
    p))  = ProjOrigin -> QName -> Elim
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o (QName -> Elim) -> m QName -> m Elim
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getOriginalProjection QName
    p
        metaElim (Arg ArgInfo
    info DeBruijnPattern
    p)         = Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim) -> (Term -> Arg Term) -> Term -> Elim
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    info (Term -> Elim) -> m Term -> m Elim
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> DeBruijnPattern -> m Term
    forall (m :: * -> *).
    (MonadState [Term] m, MonadReader (Substitution' Term) m) =>
    DeBruijnPattern -> m Term
    metaPat DeBruijnPattern
    p

        metaArgs
          :: (MonadState [Term] m, MonadReader Substitution m)
          => [NamedArg DeBruijnPattern] -> m Args
        metaArgs :: forall (m :: * -> *).
    (MonadState [Term] m, MonadReader (Substitution' Term) m) =>
    NAPs -> m [Arg Term]
    metaArgs NAPs
    args = (NamedArg DeBruijnPattern -> m (Arg Term)) -> NAPs -> m [Arg 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 ((Named NamedName DeBruijnPattern -> m Term)
    -> NamedArg DeBruijnPattern -> m (Arg Term)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse ((Named NamedName DeBruijnPattern -> m Term)
     -> NamedArg DeBruijnPattern -> m (Arg Term))
    -> (Named NamedName DeBruijnPattern -> m Term)
    -> NamedArg DeBruijnPattern
    -> m (Arg Term)
    forall a b. (a -> b) -> a -> b
    $ DeBruijnPattern -> m Term
    forall (m :: * -> *).
    (MonadState [Term] m, MonadReader (Substitution' Term) m) =>
    DeBruijnPattern -> m Term
    metaPat (DeBruijnPattern -> m Term)
    -> (Named NamedName DeBruijnPattern -> DeBruijnPattern)
    -> Named NamedName DeBruijnPattern
    -> m Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Named NamedName DeBruijnPattern -> DeBruijnPattern
    forall name a. Named name a -> a
    namedThing) NAPs
    args

        metaPat
          :: (MonadState [Term] m, MonadReader Substitution m)
          => DeBruijnPattern -> m Term
        metaPat :: forall (m :: * -> *).
    (MonadState [Term] m, MonadReader (Substitution' Term) m) =>
    DeBruijnPattern -> m Term
    metaPat (DotP PatternInfo
    _ Term
    v)       = Term -> m Term
    forall (m :: * -> *).
    MonadReader (Substitution' Term) m =>
    Term -> m Term
    dotP Term
    v
        metaPat (VarP PatternInfo
    _ DBPatVar
    _)       = m Term
    forall (m :: * -> *). MonadState [Term] m => m Term
    nextMeta
        metaPat (IApplyP{})      = m Term
    forall (m :: * -> *). MonadState [Term] m => m Term
    nextMeta
        metaPat (ConP ConHead
    c ConPatternInfo
    mt NAPs
    args) = ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c (ConPatternInfo -> ConInfo
    fromConPatternInfo ConPatternInfo
    mt) (Elims -> Term) -> ([Arg Term] -> Elims) -> [Arg Term] -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply ([Arg Term] -> Term) -> m [Arg Term] -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NAPs -> m [Arg Term]
    forall (m :: * -> *).
    (MonadState [Term] m, MonadReader (Substitution' Term) m) =>
    NAPs -> m [Arg Term]
    metaArgs NAPs
    args
        metaPat (DefP PatternInfo
    o QName
    q NAPs
    args)  = QName -> Elims -> Term
    Def QName
    q (Elims -> Term) -> ([Arg Term] -> Elims) -> [Arg Term] -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply ([Arg Term] -> Term) -> m [Arg Term] -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NAPs -> m [Arg Term]
    forall (m :: * -> *).
    (MonadState [Term] m, MonadReader (Substitution' Term) m) =>
    NAPs -> m [Arg Term]
    metaArgs NAPs
    args
        metaPat (LitP PatternInfo
    _ Literal
    l)       = Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> m Term) -> Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ Literal -> Term
    Lit Literal
    l
        metaPat ProjP{}          = m Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    forcePiUsingInjectivity :: Type -> TCM Type
    forcePiUsingInjectivity :: Type -> TCM Type
    forcePiUsingInjectivity Type
    t = Type -> TCMT IO (Blocked Type)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Type
    t TCMT IO (Blocked Type) -> (Blocked Type -> TCM Type) -> TCM Type
    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
        Blocked Blocker
    _ Type
    blkTy -> do
          let blk :: Term
    blk = Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    blkTy
          inv <- Term -> TCMT IO InvView
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m) =>
    Term -> m InvView
    functionInverse Term
    blk
          blkTy <$ invertFunction CmpEq blk inv PiHead fallback err success
        NotBlocked NotBlocked' Term
    _ Type
    t -> Type -> TCM Type
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    t
      where
        fallback :: TCMT IO ()
    fallback  = () -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        err :: TCMT IO ()
    err       = TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (Type -> TypeError
    ShouldBePi Type
    t)
        success :: p -> m ()
    success p
    _ = () -> m ()
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()