    {- |

    "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
    import Control.Monad.Fail
    import Control.Monad.State
    import Control.Monad.Reader
    import Control.Monad.Trans.Maybe

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

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

    import Agda.TypeChecking.Irrelevance (isIrrelevantOrPropM)
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Substitute
    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.Utils.Either
    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Permutation
    import Agda.Utils.Pretty ( prettyShow )

    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

      Term
    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 Term
    v of
        Def QName
    f Elims
    _ -> do
          let yes :: TCM (Maybe TermHead)
    yes = Maybe TermHead -> TCM (Maybe TermHead)
    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 (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
          Defn
    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 Defn
    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
                Set QName
    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
    lookupMutualBlock MutualId
    mb
                if QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member QName
    f Set QName
    fs then TCM (Maybe TermHead)
    forall {a}. TCMT IO (Maybe a)
    no else TCM (Maybe TermHead)
    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
    $ TermHead -> Maybe TermHead
    forall a. a -> Maybe a
    Just (TermHead -> Maybe TermHead)
    -> (QName -> TermHead) -> QName -> Maybe TermHead
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> TermHead
    ConsHead (QName -> Maybe TermHead) -> TCMT IO QName -> TCM (Maybe TermHead)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName (ConHead -> QName
    conName ConHead
    c)
        Sort Sort
    _  -> Maybe TermHead -> TCM (Maybe TermHead)
    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 (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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
        Var{}   -> Maybe TermHead -> TCM (Maybe TermHead)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
        Level{} -> Maybe TermHead -> TCM (Maybe TermHead)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
        MetaV{} -> Maybe TermHead -> TCM (Maybe TermHead)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
        DontCare{} -> Maybe TermHead -> TCM (Maybe TermHead)
    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

    -- | Do a full whnf and treat neutral terms as rigid. Used on the arguments to
    --   an injective functions and to the right-hand side.
    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
      Blocked' Term Term
    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)
    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 Blocked' Term Term
    v of
        Blocked{} -> Maybe TermHead -> m (Maybe TermHead)
    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
    _    -> Maybe TermHead -> m (Maybe TermHead)
    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 -> Maybe TermHead) -> TermHead -> Maybe TermHead
    forall a b. (a -> b) -> a -> b
    $ QName -> TermHead
    ConsHead QName
    g
          Con ConHead
    c ConInfo
    _ Elims
    _  -> Maybe TermHead -> m (Maybe TermHead)
    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 -> Maybe TermHead) -> TermHead -> Maybe TermHead
    forall a b. (a -> b) -> a -> b
    $ QName -> TermHead
    ConsHead (QName -> TermHead) -> QName -> TermHead
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    c
          Var Nat
    i Elims
    _    -> Maybe TermHead -> m (Maybe TermHead)
    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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
          Lam{}      -> Maybe TermHead -> m (Maybe TermHead)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
          Level{}    -> Maybe TermHead -> m (Maybe TermHead)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe TermHead
    forall a. Maybe a
    Nothing
          DontCare{} -> Maybe TermHead -> m (Maybe TermHead)
    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)
    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
      | Bool -> Bool
    not ((Clause -> Bool) -> [Clause] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Clause -> Bool
    properlyMatchingClause [Clause]
    cs) = 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 (m :: * -> *) a. Monad m => a -> m a
    return FunctionInverse
    forall c. FunctionInverse' c
    NotInjective
      | Bool
    otherwise = QName -> [Clause] -> TCM FunctionInverse
    checkInjectivity' QName
    f [Clause]
    cs
      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 -> Bool
    properlyMatchingClause =
          (NamedArg DeBruijnPattern -> Bool) -> NAPs -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Bool -> Bool -> DeBruijnPattern -> Bool
    forall a. Bool -> Bool -> Pattern' a -> Bool
    properlyMatching' Bool
    False Bool
    False (DeBruijnPattern -> Bool)
    -> (NamedArg DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DeBruijnPattern -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg) (NAPs -> Bool) -> (Clause -> NAPs) -> Clause -> 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
        -> TCM (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 -> TCM (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 (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 (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 c :: Clause
    c@Clause{ clauseBody :: Clause -> Maybe Term
    clauseBody = Just Term
    body , clauseType :: Clause -> Maybe (Arg Type)
    clauseType = Just Arg Type
    tbody } = do
            Bool
    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
            TermHead
    h <- if Bool
    maybeIrr then TermHead -> MaybeT (TCMT IO) TermHead
    forall (m :: * -> *) a. Monad m => a -> m a
    return TermHead
    UnknownHead else
              Clause -> TermHead -> MaybeT (TCMT IO) TermHead
    varToArg Clause
    c (TermHead -> MaybeT (TCMT IO) TermHead)
    -> MaybeT (TCMT IO) TermHead -> MaybeT (TCMT IO) TermHead
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
                TCMT IO TermHead -> MaybeT (TCMT IO) TermHead
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO TermHead -> MaybeT (TCMT IO) TermHead)
    -> TCMT IO TermHead -> MaybeT (TCMT IO) TermHead
    forall a b. (a -> b) -> a -> b
    $ TermHead -> Maybe TermHead -> TermHead
    forall a. a -> Maybe a -> a
    fromMaybe TermHead
    UnknownHead (Maybe TermHead -> TermHead)
    -> TCM (Maybe TermHead) -> TCMT IO TermHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
                  Telescope -> TCM (Maybe TermHead) -> TCM (Maybe TermHead)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Clause -> Telescope
    clauseTel Clause
    c) (TCM (Maybe TermHead) -> TCM (Maybe TermHead))
    -> TCM (Maybe TermHead) -> TCM (Maybe TermHead)
    forall a b. (a -> b) -> a -> b
    $
                    Term -> TCM (Maybe TermHead)
    headSymbol Term
    body
            [Map TermHead [Clause]] -> MaybeT (TCMT IO) [Map TermHead [Clause]]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [TermHead -> [Clause] -> Map TermHead [Clause]
    forall k a. k -> a -> Map k a
    Map.singleton TermHead
    h [Clause
    c]]
          computeHead Clause
    _ = [Map TermHead [Clause]] -> MaybeT (TCMT IO) [Map TermHead [Clause]]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

      Map TermHead [Clause]
    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)
    mapM Clause -> MaybeT (TCMT IO) [Map TermHead [Clause]]
    computeHead [Clause]
    cs

      case TermHead -> Map TermHead [Clause] -> Maybe [Clause]
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TermHead
    UnknownHead Map TermHead [Clause]
    hdMap of
        Just (Clause
    _:Clause
    _:[Clause]
    _) -> MaybeT (TCMT IO) ()
    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 (m :: * -> *) a. Monad m => a -> m a
    return ()

      [Char] -> Nat -> [Char] -> MaybeT (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn  [Char]
    "tc.inj.check" Nat
    20 ([Char] -> MaybeT (TCMT IO) ()) -> [Char] -> MaybeT (TCMT IO) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    f [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " is potentially injective."
      [Char] -> Nat -> TCMT IO Doc -> MaybeT (TCMT IO) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.inj.check" Nat
    30 (TCMT IO Doc -> MaybeT (TCMT IO) ())
    -> TCMT IO Doc -> MaybeT (TCMT IO) ()
    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
    $ [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
    $
        [(TermHead, [Clause])]
    -> ((TermHead, [Clause]) -> TCMT IO Doc) -> [TCMT IO Doc]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for (Map TermHead [Clause] -> [(TermHead, [Clause])]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map TermHead [Clause]
    hdMap) (((TermHead, [Clause]) -> TCMT IO Doc) -> [TCMT IO Doc])
    -> ((TermHead, [Clause]) -> TCMT IO Doc) -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ \ (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
    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)"

      FunctionInverse -> MaybeT (TCMT IO) FunctionInverse
    forall (m :: * -> *) a. Monad m => a -> m a
    return (FunctionInverse -> MaybeT (TCMT IO) FunctionInverse)
    -> FunctionInverse -> MaybeT (TCMT IO) FunctionInverse
    forall a b. (a -> b) -> a -> b
    $ Map TermHead [Clause] -> FunctionInverse
    forall c. InversionMap c -> FunctionInverse' c
    Inverse Map TermHead [Clause]
    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 (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 (m :: * -> *) a. Monad m => a -> m a
    return TermHead
    h) (TermHead -> m TermHead
    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 (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        isSuperRigid TermHead
    PiHead       = Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        isSuperRigid VarHead{}    = Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        isSuperRigid TermHead
    UnknownHead  = Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True -- or False, doesn't matter
        isSuperRigid (ConsHead QName
    q) = do
          Definition
    def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
          Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ case Definition -> Defn
    theDef Definition
    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
    IsData Bool -> Bool -> Bool
    || [Arg QName] -> 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 (t :: * -> *) a. Foldable t => t a -> Nat
    length Elims
    es Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > NAPs -> 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 (f :: * -> *) a. Alternative f => f a
    empty   -- impossible?
        instHead TermHead
    h = TermHead -> MaybeT m TermHead
    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
        FunctionInverse
    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
        case FunctionInverse
    inv of
          FunctionInverse
    NotInjective -> InvView -> m InvView
    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)
    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 (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' Nat TCEnv -> (Nat -> Nat) -> m () -> m ()
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' Nat TCEnv
    eInjectivityDepth Nat -> Nat
    forall a. Enum a => a -> a
    succ (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
      InvView
    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.
      Nat
    nProblems <- Set ProblemId -> Nat
    forall a. Set a -> Nat
    Set.size (Set ProblemId -> Nat) -> m (Set ProblemId) -> m Nat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' (Set ProblemId) TCEnv -> m (Set ProblemId)
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' (Set ProblemId) TCEnv
    eActiveProblems
      Nat
    injDepth  <- Lens' Nat TCEnv -> m Nat
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' Nat TCEnv
    eInjectivityDepth
      let depth :: Nat
    depth = Nat -> Nat -> Nat
    forall a. Ord a => a -> a -> a
    max Nat
    nProblems Nat
    injDepth
      Nat
    maxDepth  <- m Nat
    forall (m :: * -> *). HasOptions m => m Nat
    maxInversionDepth
      case InvView
    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 (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
    prettyTCM Term
    blk, Comparison -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Comparison
    cmp, Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    neu, CompareAs -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM CompareAs
    ty]
          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
              Type
    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
              [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
    vcat
                [ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([Char] -> [TCMT IO Doc]
    forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
    pwords [Char]
    "comparing application of injective function" [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
    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]
    "at")
                , 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] -> 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
    $ TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (Elim -> TCMT IO Doc) -> Elims -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Elim -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Elims
    blkArgs
                , 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] -> 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
    $ TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (Elim -> TCMT IO Doc) -> Elims -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Elim -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Elims
    neuArgs
                , 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
    "and type" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    fTy
                ]
              [IsForced]
    fs  <- QName -> m [IsForced]
    forall (m :: * -> *). HasConstInfo m => QName -> m [IsForced]
    getForcedArgs QName
    f
              [Polarity]
    pol <- Comparison -> QName -> m [Polarity]
    forall (m :: * -> *).
    HasConstInfo m =>
    Comparison -> QName -> m [Polarity]
    getPolarity' Comparison
    cmp QName
    f
              [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 spine comparison of", QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f]
              (Elims -> Elims -> m ()) -> Elims -> Elims -> m ()
    forall {a} {b}. (a -> a -> b) -> a -> a -> b
    app ([Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    [Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
    compareElims [Polarity]
    pol [IsForced]
    fs Type
    fTy (QName -> Elims -> Term
    Def QName
    f [])) Elims
    blkArgs Elims
    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 (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
    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
    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
        Type
    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
        [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
    vcat
          [ TCMT IO Doc
    "inverting injective function" 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
    hsep [QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f, TCMT IO Doc
    ":", Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    fTy]
          , TCMT IO Doc
    "for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <?> TermHead -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty TermHead
    hd
          , 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
    "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, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((Elim -> TCMT IO Doc) -> Elims -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Elim -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Elims
    blkArgs)
          ]                         -- Clauses with unknown heads are also possible candidates
        case [Clause] -> Maybe [Clause] -> [Clause]
    forall a. a -> Maybe a -> a
    fromMaybe [] (Maybe [Clause] -> [Clause]) -> Maybe [Clause] -> [Clause]
    forall a b. (a -> b) -> a -> b
    $ TermHead -> Map TermHead [Clause] -> Maybe [Clause]
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TermHead
    hd Map TermHead [Clause]
    hdMap Maybe [Clause] -> Maybe [Clause] -> Maybe [Clause]
    forall a. Semigroup a => a -> a -> a
    <> TermHead -> Map TermHead [Clause] -> Maybe [Clause]
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TermHead
    UnknownHead Map TermHead [Clause]
    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
              [Term]
    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
              [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.inj.invert" 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
    vcat
                [ TCMT IO Doc
    "meta patterns" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((Term -> TCMT IO Doc) -> [Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Term]
    ms)
                , TCMT IO Doc
    "  perm =" 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 (Permutation -> [Char]
    forall a. Show a => a -> [Char]
    show Permutation
    perm)
                , TCMT IO Doc
    "  tel  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    tel
                , TCMT IO Doc
    "  ps   =" 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 DeBruijnPattern -> TCMT IO Doc)
    -> [Arg DeBruijnPattern] -> [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 DeBruijnPattern -> [Char])
    -> Arg DeBruijnPattern
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg DeBruijnPattern -> [Char]
    forall a. Show a => a -> [Char]
    show) [Arg DeBruijnPattern]
    ps)
                ]
              -- and this is the order the variables occur in the patterns
              let msAux :: [Term]
    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 :: Substitution' Term
    sub   = [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> [Term]
    forall a. [a] -> [a]
    reverse [Term]
    ms)
              Elims
    margs <- ReaderT (Substitution' Term) m Elims
    -> Substitution' Term -> m Elims
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT (StateT [Term] (ReaderT (Substitution' Term) m) Elims
    -> [Term] -> ReaderT (Substitution' Term) m Elims
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT ((Arg DeBruijnPattern
     -> StateT [Term] (ReaderT (Substitution' Term) m) Elim)
    -> [Arg DeBruijnPattern]
    -> StateT [Term] (ReaderT (Substitution' Term) m) Elims
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Arg DeBruijnPattern
    -> StateT [Term] (ReaderT (Substitution' Term) m) Elim
    forall (m :: * -> *).
    (MonadState [Term] m, MonadReader (Substitution' Term) m,
     HasConstInfo m, MonadFail m) =>
    Arg DeBruijnPattern -> m Elim
    metaElim [Arg DeBruijnPattern]
    ps) [Term]
    msAux) Substitution' Term
    sub
              [Char] -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.inj.invert" 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
    vcat
                [ TCMT IO Doc
    "inversion"
                , 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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
                  [ TCMT IO Doc
    "lhs  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Elims -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Elims
    margs
                  , TCMT IO Doc
    "rhs  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Elims -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Elims
    blkArgs
                  , TCMT IO Doc
    "type =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    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.
              [Polarity]
    pol <- [Polarity] -> [Polarity]
    purgeNonvariant ([Polarity] -> [Polarity]) -> m [Polarity] -> m [Polarity]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Comparison -> QName -> m [Polarity]
    forall (m :: * -> *).
    HasConstInfo m =>
    Comparison -> QName -> m [Polarity]
    getPolarity' Comparison
    cmp QName
    f
              [IsForced]
    fs  <- QName -> m [IsForced]
    forall (m :: * -> *). HasConstInfo m => QName -> m [IsForced]
    getForcedArgs QName
    f
              -- The clause might not give as many patterns as there
              -- are arguments (point-free style definitions).
              let blkArgs' :: Elims
    blkArgs' = Nat -> Elims -> Elims
    forall a. Nat -> [a] -> [a]
    take (Elims -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length Elims
    margs) Elims
    blkArgs
              [Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    [Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
    compareElims [Polarity]
    pol [IsForced]
    fs Type
    fTy (QName -> Elims -> Term
    Def QName
    f []) Elims
    margs Elims
    blkArgs'

              -- Check that we made progress.
              Reduced (Blocked' Term Term) Term
    r <- ReduceM (Reduced (Blocked' Term Term) Term)
    -> m (Reduced (Blocked' Term Term) Term)
    forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
    liftReduce (ReduceM (Reduced (Blocked' Term Term) Term)
     -> m (Reduced (Blocked' Term Term) Term))
    -> ReduceM (Reduced (Blocked' Term Term) Term)
    -> m (Reduced (Blocked' Term Term) Term)
    forall a b. (a -> b) -> a -> b
    $ Bool
    -> Term
    -> QName
    -> Elims
    -> ReduceM (Reduced (Blocked' Term Term) Term)
    unfoldDefinitionStep Bool
    False (QName -> Elims -> Term
    Def QName
    f []) QName
    f Elims
    blkArgs
              case Reduced (Blocked' Term Term) Term
    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
    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 (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
    prettyTCM Term
    blk
                    , TCMT IO Doc
    "does not reduce"
                    ]
                  KeepMetas -> m KeepMetas
    forall (m :: * -> *) a. Monad m => a -> m a
    return KeepMetas
    RollBackMetas
      where
        nextMeta :: (MonadState [Term] m, MonadFail m) => m Term
        nextMeta :: forall (m :: * -> *). (MonadState [Term] m, MonadFail m) => m Term
    nextMeta = do
          Term
    m : [Term]
    ms <- m [Term]
    forall s (m :: * -> *). MonadState s m => m s
    get
          [Term] -> m ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put [Term]
    ms
          Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    m

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

        metaElim
          :: (MonadState [Term] m, MonadReader Substitution m, HasConstInfo m, MonadFail m)
          => Arg DeBruijnPattern -> m Elim
        metaElim :: forall (m :: * -> *).
    (MonadState [Term] m, MonadReader (Substitution' Term) m,
     HasConstInfo m, MonadFail 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,
     MonadFail m) =>
    DeBruijnPattern -> m Term
    metaPat DeBruijnPattern
    p

        metaArgs
          :: (MonadState [Term] m, MonadReader Substitution m, MonadFail m)
          => [NamedArg DeBruijnPattern] -> m Args
        metaArgs :: forall (m :: * -> *).
    (MonadState [Term] m, MonadReader (Substitution' Term) m,
     MonadFail 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)
    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)
    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,
     MonadFail 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, MonadFail m)
          => DeBruijnPattern -> m Term
        metaPat :: forall (m :: * -> *).
    (MonadState [Term] m, MonadReader (Substitution' Term) m,
     MonadFail 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, MonadFail m) => m Term
    nextMeta
        metaPat (IApplyP{})      = m Term
    forall (m :: * -> *). (MonadState [Term] m, MonadFail 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,
     MonadFail 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,
     MonadFail m) =>
    NAPs -> m [Arg Term]
    metaArgs NAPs
    args
        metaPat (LitP PatternInfo
    _ Literal
    l)       = Term -> m Term
    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 (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
          InvView
    inv <- Term -> TCMT IO InvView
    forall (m :: * -> *).
    (PureTCM m, MonadError TCErr m) =>
    Term -> m InvView
    functionInverse Term
    blk
          Type
    blkTy Type -> TCMT IO () -> TCM Type
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Comparison
    -> Term
    -> InvView
    -> TermHead
    -> TCMT IO ()
    -> TCMT IO ()
    -> (Term -> TCMT IO ())
    -> TCMT IO ()
    forall (m :: * -> *).
    MonadConversion m =>
    Comparison
    -> Term
    -> InvView
    -> TermHead
    -> m ()
    -> m ()
    -> (Term -> m ())
    -> m ()
    invertFunction Comparison
    CmpEq Term
    blk InvView
    inv TermHead
    PiHead TCMT IO ()
    fallback TCMT IO ()
    err Term -> TCMT IO ()
    forall {m :: * -> *} {p}. Monad m => p -> m ()
    success
        NotBlocked NotBlocked' Term
    _ Type
    t -> Type -> TCM Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    t
      where
        fallback :: TCMT IO ()
    fallback  = () -> TCMT IO ()
    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 (m :: * -> *) a. Monad m => a -> m a
    return ()