    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Dropping initial arguments (``parameters'') from a function which can be
    --   easily reconstructed from its principal argument.
    --
    --   A function which has such parameters is called ``projection-like''.
    --
    --   The motivation for this optimization comes from the use of nested records.
    --
    --   First, let us look why proper projections need not store the parameters:
    --   The type of a projection @f@ is of the form
    --   @
    --      f : Γ → R Γ → C
    --   @
    --   where @R@ is the record type and @C@ is the type of the field @f@.
    --   Given a projection application
    --   @
    --      p pars u
    --   @
    --   we know that the type of the principal argument @u@ is
    --   @
    --      u : R pars
    --   @
    --   thus, the parameters @pars@ are redundant in the projection application
    --   if we can always infer the type of @u@.
    --   For projections, this is case, because the principal argument @u@ must be
    --   neutral; otherwise, if it was a record value, we would have a redex,
    --   yet Agda maintains a β-normal form.
    --
    --   The situation for projections can be generalized to ``projection-like''
    --   functions @f@.  Conditions:
    --
    --     1. The type of @f@ is of the form @f : Γ → D Γ → ...@ for some
    --        type constructor @D@ which can never reduce.
    --
    --     2. For every reduced welltyped application @f pars u ...@,
    --        the type of @u@ is inferable.
    --
    --   This then allows @pars@ to be dropped always.
    --
    --   Condition 2 is approximated by a bunch of criteria, for details see function
    --   'makeProjection'.
    --
    --   Typical projection-like functions are compositions of projections
    --   which arise from nested records.
    --
    --   Notes:
    --
    --     1. This analysis could be dualized to ``constructor-like'' functions
    --        whose parameters are reconstructable from the target type.
    --        But such functions would need to be fully applied.
    --
    --     2. A more general analysis of which arguments are reconstructible
    --        can be found in
    --
    --          Jason C. Reed, Redundancy elimination for LF
    --          LFTMP 2004.

    module Agda.TypeChecking.ProjectionLike where

    import qualified Data.Map as Map
    import Data.Monoid (Any(..), getAny)

    import Agda.Interaction.Options

    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Free (runFree, IgnoreSorts(..))
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Positivity
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Reduce (reduce, abortIfBlocked)
    import Agda.TypeChecking.Telescope

    import Agda.TypeChecking.DropArgs

    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Permutation
    import Agda.Syntax.Common.Pretty ( prettyShow )
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    -- | View for a @Def f (Apply a : es)@ where @isRelevantProjection f@.
    --   Used for projection-like @f@s.
    data ProjectionView
      = ProjectionView
        { ProjectionView -> QName
    projViewProj  :: QName
        , ProjectionView -> Arg Term
    projViewSelf  :: Arg Term
        , ProjectionView -> Elims
    projViewSpine :: Elims
        }
        -- ^ A projection or projection-like function, applied to its
        --   principal argument
      | LoneProjectionLike QName ArgInfo
        -- ^ Just a lone projection-like function, missing its principal
        --   argument (from which we could infer the parameters).
      | NoProjection Term
        -- ^ Not a projection or projection-like thing.

    -- | Semantics of 'ProjectionView'.
    unProjView :: ProjectionView -> Term
    unProjView :: ProjectionView -> Term
    unProjView ProjectionView
    pv =
      case ProjectionView
    pv of
        ProjectionView QName
    f Arg Term
    a Elims
    es   -> QName -> Elims -> Term
    Def QName
    f (Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Arg Term
    a Elim' Term -> Elims -> Elims
    forall a. a -> [a] -> [a]
    : Elims
    es)
        LoneProjectionLike QName
    f ArgInfo
    ai -> QName -> Elims -> Term
    Def QName
    f []
        NoProjection Term
    v          -> Term
    v

    -- | Top-level 'ProjectionView' (no reduction).
    {-# SPECIALIZE projView :: Term -> TCM ProjectionView #-}
    projView :: HasConstInfo m => Term -> m ProjectionView
    projView :: forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
    projView Term
    v = do
      let fallback :: m ProjectionView
    fallback = ProjectionView -> m ProjectionView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProjectionView -> m ProjectionView)
    -> ProjectionView -> m ProjectionView
    forall a b. (a -> b) -> a -> b
    $ Term -> ProjectionView
    NoProjection Term
    v
      case Term
    v of
        Def QName
    f Elims
    es -> m (Maybe Projection)
    -> m ProjectionView
    -> (Projection -> m ProjectionView)
    -> m ProjectionView
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> m (Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isRelevantProjection QName
    f) m ProjectionView
    fallback ((Projection -> m ProjectionView) -> m ProjectionView)
    -> (Projection -> m ProjectionView) -> m ProjectionView
    forall a b. (a -> b) -> a -> b
    $ \ Projection
    isP -> do
          if Projection -> Int
    projIndex Projection
    isP Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0 then m ProjectionView
    fallback else do
            case Elims
    es of
              []           -> ProjectionView -> m ProjectionView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProjectionView -> m ProjectionView)
    -> ProjectionView -> m ProjectionView
    forall a b. (a -> b) -> a -> b
    $ QName -> ArgInfo -> ProjectionView
    LoneProjectionLike QName
    f (ArgInfo -> ProjectionView) -> ArgInfo -> ProjectionView
    forall a b. (a -> b) -> a -> b
    $ Projection -> ArgInfo
    projArgInfo Projection
    isP
              Apply Arg Term
    a : Elims
    es -> ProjectionView -> m ProjectionView
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ProjectionView -> m ProjectionView)
    -> ProjectionView -> m ProjectionView
    forall a b. (a -> b) -> a -> b
    $ QName -> Arg Term -> Elims -> ProjectionView
    ProjectionView QName
    f Arg Term
    a Elims
    es
              -- Since a projection is a function, it cannot be projected itself.
              Proj{}  : Elims
    _  -> m ProjectionView
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              -- The principal argument of a projection-like cannot be the interval?
              IApply{} : Elims
    _ -> m ProjectionView
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        Term
    _ -> m ProjectionView
    fallback

    {-# SPECIALIZE reduceProjectionLike :: Term -> TCM Term #-}
    -- | Reduce away top-level projection like functions.
    --   (Also reduces projections, but they should not be there,
    --   since Internal is in lambda- and projection-beta-normal form.)
    --
    reduceProjectionLike :: PureTCM m => Term -> m Term
    reduceProjectionLike :: forall (m :: * -> *). PureTCM m => Term -> m Term
    reduceProjectionLike Term
    v = do
      -- Andreas, 2013-11-01 make sure we do not reduce a constructor
      -- because that could be folded back into a literal by reduce.
      pv <- Term -> m ProjectionView
    forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
    projView Term
    v
      case pv of
        ProjectionView{} -> m Term -> m Term
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    onlyReduceProjections (m Term -> m Term) -> m Term -> m Term
    forall a b. (a -> b) -> a -> b
    $ Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v
                                -- ordinary reduce, only different for Def's
        ProjectionView
    _                -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v

    data ProjEliminator = EvenLone | ButLone | NoPostfix
      deriving ProjEliminator -> ProjEliminator -> Bool
    (ProjEliminator -> ProjEliminator -> Bool)
    -> (ProjEliminator -> ProjEliminator -> Bool) -> Eq ProjEliminator
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ProjEliminator -> ProjEliminator -> Bool
    == :: ProjEliminator -> ProjEliminator -> Bool
    $c/= :: ProjEliminator -> ProjEliminator -> Bool
    /= :: ProjEliminator -> ProjEliminator -> Bool
    Eq

    {-# SPECIALIZE elimView :: ProjEliminator -> Term -> TCM Term #-}
    -- | Turn prefix projection-like function application into postfix ones.
    --   This does just one layer, such that the top spine contains
    --   the projection-like functions as projections.
    --   Used in 'compareElims' in @TypeChecking.Conversion@
    --   and in "Agda.TypeChecking.CheckInternal".
    --
    --   If the 'Bool' is 'True', a lone projection like function will be
    --   turned into a lambda-abstraction, expecting the principal argument.
    --   If the 'Bool' is 'False', it will be returned unaltered.
    --
    --   No precondition.
    --   Preserves constructorForm, since it really does only something
    --   on (applications of) projection-like functions.
    elimView :: PureTCM m => ProjEliminator -> Term -> m Term
    elimView :: forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
    elimView ProjEliminator
    pe Term
    v = do
      [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.conv.elim" Int
    60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "elimView of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
      v <- Term -> m Term
    forall (m :: * -> *). PureTCM m => Term -> m Term
    reduceProjectionLike Term
    v
      reportSDoc "tc.conv.elim" 65 $
        "elimView (projections reduced) of " <+> prettyTCM v
      case pe of
        ProjEliminator
    NoPostfix -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
        ProjEliminator
    _         -> do
          pv <- Term -> m ProjectionView
    forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
    projView Term
    v
          case pv of
            NoProjection{}        -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
            LoneProjectionLike QName
    f ArgInfo
    ai
              | ProjEliminator
    pe ProjEliminator -> ProjEliminator -> Bool
    forall a. Eq a => a -> a -> Bool
    == ProjEliminator
    EvenLone  -> 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
    $ ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    ai (Abs Term -> Term) -> Abs Term -> Term
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Term -> Abs Term
    forall a. [Char] -> a -> Abs a
    Abs [Char]
    "r" (Term -> Abs Term) -> Term -> Abs Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Elims -> Term
    Var Int
    0 [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjPrefix QName
    f]
              | Bool
    otherwise     -> Term -> m Term
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
            ProjectionView QName
    f Arg Term
    a Elims
    es -> (Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` (ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjPrefix QName
    f Elim' Term -> Elims -> Elims
    forall a. a -> [a] -> [a]
    : Elims
    es)) (Term -> Term) -> m Term -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ProjEliminator -> Term -> m Term
    forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
    elimView ProjEliminator
    pe (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a)

    {-# SPECIALIZE eligibleForProjectionLike :: QName -> TCM Bool #-}
    -- | Which @Def@types are eligible for the principle argument
    --   of a projection-like function?
    eligibleForProjectionLike :: (HasConstInfo m) => QName -> m Bool
    eligibleForProjectionLike :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    eligibleForProjectionLike QName
    d = Defn -> Bool
    eligible (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> Bool) -> m Definition -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
      where
      eligible :: Defn -> Bool
    eligible = \case
        Datatype{} -> Bool
    True
        Record{}   -> Bool
    True
        Axiom{}    -> Bool
    True
        DataOrRecSig{}     -> Bool
    True
        GeneralizableVar{} -> Bool
    False
        Function{}    -> Bool
    False
        Primitive{}   -> Bool
    False
        PrimitiveSort{} -> Bool
    False
        Constructor{} -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        AbstractDefn Defn
    d -> Defn -> Bool
    eligible Defn
    d
          -- Andreas, 2017-08-14, issue #2682:
          -- Abstract records still export the projections.
          -- Andreas, 2016-10-11 AIM XXIV
          -- Projection-like at abstract types violates the parameter reconstructibility property.
          -- See test/Fail/AbstractTypeProjectionLike.

    -- | Turn a definition into a projection if it looks like a projection.
    --
    -- Conditions for projection-likeness of @f@:
    --
    --   1. The type of @f@ must be of the shape @Γ → D Γ → C@ for @D@
    --      a name (@Def@) which is 'eligibleForProjectionLike':
    --      @data@ / @record@ / @postulate@.
    --
    --   2. The application of f should only get stuck if the principal argument
    --      is inferable (neutral).  Thus:
    --
    --      a. @f@ cannot have absurd clauses (which are stuck even if the principal
    --         argument is a constructor).
    --
    --      b. @f@ cannot be abstract as it does not reduce outside abstract blocks
    --         (always stuck).
    --
    --      c. @f@ cannot match on other arguments than the principal argument.
    --
    --      d. @f@ cannot match deeply.
    --
    --      e. @f@s body may not mention the parameters.
    --
    --      f. A rhs of @f@ cannot be a record expression, since this will be
    --         translated to copatterns by recordExpressionsToCopatterns.
    --         Thus, an application of @f@ waiting for a projection
    --         can be stuck even when the principal argument is a constructor.
    --
    --      g. @f@ cannot be an irrelevant definition (Andreas, 2022-03-07, #5809),
    --         as those are not reduced.
    --
    -- For internal reasons:
    --
    --   3. @f@ cannot be constructor headed
    --
    --   4. @f@ cannot be recursive, since we have not implemented a function
    --      which goes through the bodies of the @f@ and the mutually recursive
    --      functions and drops the parameters from all applications of @f@.
    --
    -- Examples for these reasons: see test/Succeed/NotProjectionLike.agda

    makeProjection :: QName -> TCM ()
    makeProjection :: QName -> TCM ()
    makeProjection QName
    x = TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (PragmaOptions -> Bool
    optProjectionLike (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
     TCM () -> TCM ()
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
      [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    70 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Considering " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    x [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " for projection likeness"
      defn <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
      let t = Definition -> Type
    defType Definition
    defn
      reportSDoc "tc.proj.like" 20 $ sep
        [ "Checking for projection likeness "
        , prettyTCM x <+> " : " <+> prettyTCM t
        ]
      if isIrrelevant defn then
        reportSDoc "tc.proj.like" 30 $ "  projection-like functions cannot be irrelevant"
      else case theDef defn of
        Function{funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cls}
          | (Clause -> Bool) -> [Clause] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Maybe Term -> Bool
    forall a. Maybe a -> Bool
    isNothing (Maybe Term -> Bool) -> (Clause -> Maybe Term) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Maybe Term
    clauseBody) [Clause]
    cls ->
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  projection-like functions cannot have absurd clauses"
          | (Clause -> Bool) -> [Clause] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Bool -> (Term -> Bool) -> Maybe Term -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Term -> Bool
    isRecordExpression (Maybe Term -> Bool) -> (Clause -> Maybe Term) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Maybe Term
    clauseBody) [Clause]
    cls ->
            [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  projection-like functions cannot have record rhss"
        -- Constructor-headed functions can't be projection-like (at the moment). The reason
        -- for this is that invoking constructor-headedness will circumvent the inference of
        -- the dropped arguments.
        -- Nor can abstract definitions be projection-like since they won't reduce
        -- outside the abstract block.
        def :: Defn
    def@Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Left ProjectionLikenessMissing
    MaybeProjection, funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cls,
                     funSplitTree :: Defn -> Maybe SplitTree
    funSplitTree = Maybe SplitTree
    st0, funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Maybe CompiledClauses
    cc0, funInv :: Defn -> FunctionInverse
    funInv = FunctionInverse
    NotInjective,
                     funMutual :: Defn -> Maybe [QName]
    funMutual = Just [], -- Andreas, 2012-09-28: only consider non-mutual funs
                     funOpaque :: Defn -> IsOpaque
    funOpaque = IsOpaque
    TransparentDef} | Bool -> Bool
    not (Defn
    def Defn -> Lens' Defn Bool -> Bool
    forall o i. o -> Lens' o i -> i
    ^. (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    funAbstract) -> do
          ps0 <- ((Arg QName, Int) -> TCMT IO Bool)
    -> [(Arg QName, Int)] -> TCMT IO [(Arg QName, Int)]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM (Arg QName, Int) -> TCMT IO Bool
    validProj ([(Arg QName, Int)] -> TCMT IO [(Arg QName, Int)])
    -> [(Arg QName, Int)] -> TCMT IO [(Arg QName, Int)]
    forall a b. (a -> b) -> a -> b
    $ [Term] -> Type -> [(Arg QName, Int)]
    candidateArgs [] Type
    t
          reportSLn "tc.proj.like" 30 $ if null ps0 then "  no candidates found"
                                                    else "  candidates: " ++ prettyShow ps0
          unless (null ps0) $ do
            -- Andreas 2012-09-26: only consider non-recursive functions for proj.like.
            -- Issue 700: problems with recursive funs. in term.checker and reduction
            ifM recursive (reportSLn "tc.proj.like" 30 $ "  recursive functions are not considered for projection-likeness") $ do
              {- else -}
              case lastMaybe (filter (checkOccurs cls . snd) ps0) of
                Maybe (Arg QName, Int)
    Nothing -> [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.proj.like" Int
    50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
                  [ TCMT IO Doc
    "occurs check failed"
                  , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "clauses =" 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
    vcat ((Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Clause -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [Clause]
    cls) ]
                Just (Arg QName
    d, Int
    n) -> do
                  -- Yes, we are projection-like!
                  [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.proj.like" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
                    [ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " : " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
                    , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                      [ TCMT IO Doc
    "is projection like in argument",  Int -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Int -> m Doc
    prettyTCM Int
    n, TCMT IO Doc
    "for type", QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM (Arg QName -> QName
    forall e. Arg e -> e
    unArg Arg QName
    d) ]
                    ]
                  [Char] -> Int -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadTCM m, MonadDebug m) =>
    [Char] -> Int -> m ()
    __CRASH_WHEN__ [Char]
    "tc.proj.like.crash" Int
    1000

                  let cls' :: [Clause]
    cls' = (Clause -> Clause) -> [Clause] -> [Clause]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int -> Clause -> Clause
    forall a. DropArgs a => Int -> a -> a
    dropArgs Int
    n) [Clause]
    cls
                      cc :: Maybe CompiledClauses
    cc   = Int -> Maybe CompiledClauses -> Maybe CompiledClauses
    forall a. DropArgs a => Int -> a -> a
    dropArgs Int
    n Maybe CompiledClauses
    cc0
                      st :: Maybe SplitTree
    st   = Int -> Maybe SplitTree -> Maybe SplitTree
    forall a. DropArgs a => Int -> a -> a
    dropArgs Int
    n Maybe SplitTree
    st0
                  [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    60 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines
                    [ [Char]
    "  rewrote clauses to"
                    , [Char]
    "    " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Maybe CompiledClauses -> [Char]
    forall a. Show a => a -> [Char]
    show Maybe CompiledClauses
    cc
                    ]

                  -- Andreas, 2013-10-20 build parameter dropping function
                  let pIndex :: Int
    pIndex = Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1
                      tel :: [Dom ([Char], Type)]
    tel = Int -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
    forall a. Int -> [a] -> [a]
    take Int
    pIndex ([Dom ([Char], Type)] -> [Dom ([Char], Type)])
    -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList (Tele (Dom Type) -> [Dom ([Char], Type)])
    -> Tele (Dom Type) -> [Dom ([Char], Type)]
    forall a b. (a -> b) -> a -> b
    $ TelV Type -> Tele (Dom Type)
    forall a. TelV a -> Tele (Dom a)
    theTel (TelV Type -> Tele (Dom Type)) -> TelV Type -> Tele (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> TelV Type
    telView' Type
    t
                  Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ([Dom ([Char], Type)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Dom ([Char], Type)]
    tel Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    pIndex) TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                  let projection :: Projection
    projection = Projection
                        { projProper :: Maybe QName
    projProper   = Maybe QName
    forall a. Maybe a
    Nothing
                        , projOrig :: QName
    projOrig     = QName
    x
                        , projFromType :: Arg QName
    projFromType = Arg QName
    d
                        , projIndex :: Int
    projIndex    = Int
    pIndex
                        , projLams :: ProjLams
    projLams     = [Arg [Char]] -> ProjLams
    ProjLams ([Arg [Char]] -> ProjLams) -> [Arg [Char]] -> ProjLams
    forall a b. (a -> b) -> a -> b
    $ (Dom ([Char], Type) -> Arg [Char])
    -> [Dom ([Char], Type)] -> [Arg [Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (Dom' Term [Char] -> Arg [Char]
    forall t a. Dom' t a -> Arg a
    argFromDom (Dom' Term [Char] -> Arg [Char])
    -> (Dom ([Char], Type) -> Dom' Term [Char])
    -> Dom ([Char], Type)
    -> Arg [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (([Char], Type) -> [Char])
    -> Dom ([Char], Type) -> Dom' Term [Char]
    forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Char], Type) -> [Char]
    forall a b. (a, b) -> a
    fst) [Dom ([Char], Type)]
    tel
                        }
                  let newDef :: Defn
    newDef = Defn
    def
                               { funProjection     = Right projection
                               , funClauses        = cls'
                               , funSplitTree      = st
                               , funCompiled       = cc
                               , funInv            = dropArgs n $ funInv def
                               }
                  QName -> Definition -> TCM ()
    addConstant QName
    x (Definition -> TCM ()) -> Definition -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Definition
    defn { defPolarity       = drop n $ defPolarity defn
                                       , defArgOccurrences = drop n $ defArgOccurrences defn
                                       , defDisplay        = []
                                       , theDef            = newDef
                                       }
        Function{funInv :: Defn -> FunctionInverse
    funInv = Inverse{}} ->
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  injective functions can't be projections"
        d :: Defn
    d@Function{} | Defn
    d Defn -> Lens' Defn Bool -> Bool
    forall o i. o -> Lens' o i -> i
    ^. (Bool -> f Bool) -> Defn -> f Defn
    Lens' Defn Bool
    funAbstract ->
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  abstract functions can't be projections"
        Function{funOpaque :: Defn -> IsOpaque
    funOpaque = OpaqueDef OpaqueId
    _} ->
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  opaque functions can't be projections"
        Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right{}} ->
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  already projection like"
        Function{funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Left ProjectionLikenessMissing
    NeverProjection} ->
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  the user has asked for it not to be projection-like"
        Function{funMutual :: Defn -> Maybe [QName]
    funMutual = Just (QName
    _:[QName]
    _)} ->
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  mutual functions can't be projections"
        Function{funMutual :: Defn -> Maybe [QName]
    funMutual = Maybe [QName]
    Nothing} ->
          [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  mutuality check has not run yet"
        Function{} -> TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- match is complete, but GHC does not see this (because of d^.funAbstract)
        Axiom{}        -> [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  not a function, but Axiom"
        DataOrRecSig{} -> [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  not a function, but DataOrRecSig"
        GeneralizableVar{} -> [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  not a function, but GeneralizableVar"
        AbstractDefn{} -> [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  not a function, but AbstractDefn"
        Constructor{}  -> [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  not a function, but Constructor"
        Datatype{}     -> [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  not a function, but Datatype"
        Primitive{}    -> [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  not a function, but Primitive"
        PrimitiveSort{} -> [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  not a function, but PrimitiveSort"
        Record{}       -> [Char] -> Int -> [Char] -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> [Char] -> m ()
    reportSLn [Char]
    "tc.proj.like" Int
    30 ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  not a function, but Record"
      where
        -- If the user wrote a record expression as rhs,
        -- the recordExpressionsToCopatterns translation will turn this into copatterns,
        -- violating the conditions of projection-likeness.
        -- Andreas, 2019-07-11, issue #3843.
        isRecordExpression :: Term -> Bool
        isRecordExpression :: Term -> Bool
    isRecordExpression = \case
          Con ConHead
    _ ConOrigin
    ConORec Elims
    _ -> Bool
    True
          Term
    _ -> Bool
    False
        -- @validProj (d,n)@ checks whether the head @d@ of the type of the
        -- @n@th argument is injective in all args (i.d. being name of data/record/axiom).
        validProj :: (Arg QName, Int) -> TCM Bool
        validProj :: (Arg QName, Int) -> TCMT IO Bool
    validProj (Arg QName
    _, Int
    0) = Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        validProj (Arg QName
    d, Int
    _) = QName -> TCMT IO Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    eligibleForProjectionLike (Arg QName -> QName
    forall e. Arg e -> e
    unArg Arg QName
    d)

        -- NOTE: If the following definition turns out to be slow, then
        -- one could perhaps reuse information computed by the termination
        -- and/or positivity checkers.
        recursive :: TCMT IO Bool
    recursive = do
          occs <- QName -> TCM (Map Item Integer)
    computeOccurrences QName
    x
          case Map.lookup (ADef x) occs of
            Just Integer
    n | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    1 -> Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True -- recursive occurrence
            Maybe Integer
    _               -> Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

        checkOccurs :: t Clause -> Int -> Bool
    checkOccurs t Clause
    cls Int
    n = (Clause -> Bool) -> t Clause -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Int -> Clause -> Bool
    nonOccur Int
    n) t Clause
    cls

        nonOccur :: Int -> Clause -> Bool
    nonOccur Int
    n Clause
    cl =
            (Int -> [Int] -> [Int]
    forall a. Int -> [a] -> [a]
    take Int
    n [Int]
    p [Int] -> [Int] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Int
    0..Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]) Bool -> Bool -> Bool
    &&
            Int -> [NamedArg DeBruijnPattern] -> Bool
    forall {x}. Int -> [NamedArg (Pattern' x)] -> Bool
    onlyMatch Int
    n [NamedArg DeBruijnPattern]
    ps Bool -> Bool -> Bool
    &&  -- projection-like functions are only allowed to match on the eliminatee
                              -- otherwise we may end up projecting from constructor applications, in
                              -- which case we can't reconstruct the dropped parameters
            Int -> Int -> Maybe Term -> Bool
    forall {t}. Free t => Int -> Int -> t -> Bool
    checkBody Int
    m Int
    n Maybe Term
    b
          where
            Perm Int
    _ [Int]
    p = 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
            ps :: [NamedArg DeBruijnPattern]
    ps       = Clause -> [NamedArg DeBruijnPattern]
    namedClausePats Clause
    cl
            b :: Maybe Term
    b        = Clause -> Maybe Term
    compiledClauseBody Clause
    cl  -- Renumbers variables to match order in patterns
                                              -- and includes dot patterns as variables.
            m :: Int
    m        = [Arg (Either DBPatVar Term)] -> Int
    forall a. Sized a => a -> Int
    size ([Arg (Either DBPatVar Term)] -> Int)
    -> [Arg (Either DBPatVar Term)] -> Int
    forall a b. (a -> b) -> a -> b
    $ (NamedArg DeBruijnPattern -> [Arg (Either DBPatVar Term)])
    -> [NamedArg DeBruijnPattern] -> [Arg (Either DBPatVar Term)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap NamedArg DeBruijnPattern
    -> [Arg (Either (PatternVarOut (NamedArg DeBruijnPattern)) Term)]
    NamedArg DeBruijnPattern -> [Arg (Either DBPatVar Term)]
    forall a.
    PatternVars a =>
    a -> [Arg (Either (PatternVarOut a) Term)]
    patternVars [NamedArg DeBruijnPattern]
    ps  -- This also counts dot patterns!

        onlyMatch :: Int -> [NamedArg (Pattern' x)] -> Bool
    onlyMatch Int
    n [NamedArg (Pattern' x)]
    ps = (NamedArg (Pattern' x) -> Bool) -> [NamedArg (Pattern' x)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Pattern' x -> Bool
    shallowMatch (Pattern' x -> Bool)
    -> (NamedArg (Pattern' x) -> Pattern' x)
    -> NamedArg (Pattern' x)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg (Pattern' x) -> Pattern' x
    forall a. NamedArg a -> a
    namedArg) (Int -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
    forall a. Int -> [a] -> [a]
    take Int
    1 [NamedArg (Pattern' x)]
    ps1) Bool -> Bool -> Bool
    &&
                         [NamedArg (Pattern' x)] -> Bool
    forall {x}. [NamedArg (Pattern' x)] -> Bool
    noMatches ([NamedArg (Pattern' x)]
    ps0 [NamedArg (Pattern' x)]
    -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [NamedArg (Pattern' x)] -> [NamedArg (Pattern' x)]
    forall a. Int -> [a] -> [a]
    drop Int
    1 [NamedArg (Pattern' x)]
    ps1)
          where
            ([NamedArg (Pattern' x)]
    ps0, [NamedArg (Pattern' x)]
    ps1) = Int
    -> [NamedArg (Pattern' x)]
    -> ([NamedArg (Pattern' x)], [NamedArg (Pattern' x)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    n [NamedArg (Pattern' x)]
    ps
            shallowMatch :: Pattern' x -> Bool
    shallowMatch (ConP ConHead
    _ ConPatternInfo
    _ [NamedArg (Pattern' x)]
    ps) = [NamedArg (Pattern' x)] -> Bool
    forall {x}. [NamedArg (Pattern' x)] -> Bool
    noMatches [NamedArg (Pattern' x)]
    ps
            shallowMatch Pattern' x
    _             = Bool
    True
            noMatches :: [NamedArg (Pattern' x)] -> Bool
    noMatches = (NamedArg (Pattern' x) -> Bool) -> [NamedArg (Pattern' x)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Pattern' x -> Bool
    forall {x}. Pattern' x -> Bool
    noMatch (Pattern' x -> Bool)
    -> (NamedArg (Pattern' x) -> Pattern' x)
    -> NamedArg (Pattern' x)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg (Pattern' x) -> Pattern' x
    forall a. NamedArg a -> a
    namedArg)
            noMatch :: Pattern' x -> Bool
    noMatch ConP{} = Bool
    False
            noMatch DefP{} = Bool
    False
            noMatch LitP{} = Bool
    False
            noMatch ProjP{}= Bool
    False
            noMatch VarP{} = Bool
    True
            noMatch DotP{} = Bool
    True
            noMatch IApplyP{} = Bool
    True

        -- Make sure non of the parameters occurs in the body of the function.
        checkBody :: Int -> Int -> t -> Bool
    checkBody Int
    m Int
    n t
    b = Bool -> Bool
    not (Bool -> Bool) -> (Any -> Bool) -> Any -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Any -> Bool
    getAny (Any -> Bool) -> Any -> Bool
    forall a b. (a -> b) -> a -> b
    $ SingleVar Any -> IgnoreSorts -> t -> Any
    forall a c t.
    (IsVarSet a c, Free t) =>
    SingleVar c -> IgnoreSorts -> t -> c
    runFree SingleVar Any
    badVar IgnoreSorts
    IgnoreNot t
    b
          where badVar :: SingleVar Any
    badVar Int
    x = Bool -> Any
    Any (Bool -> Any) -> Bool -> Any
    forall a b. (a -> b) -> a -> b
    $ Int
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    x Bool -> Bool -> Bool
    && Int
    x Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    m

        -- @candidateArgs [var 0,...,var(n-1)] t@ adds @(n,d)@ to the output,
        -- if @t@ is a function-type with domain @t 0 .. (n-1)@
        -- (the domain of @t@ is the type of the arg @n@).
        --
        -- This means that from the type of arg @n@ all previous arguments
        -- can be computed by a simple matching.
        -- (Provided the @d@ is data/record/postulate, checked in @validProj@).
        --
        -- E.g. f : {x : _}(y : _){z : _} -> D x y z -> ...
        -- will return (D,3) as a candidate (amongst maybe others).
        --
        candidateArgs :: [Term] -> Type -> [(Arg QName, Int)]
        candidateArgs :: [Term] -> Type -> [(Arg QName, Int)]
    candidateArgs [Term]
    vs Type
    t =
          case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
            Pi Dom Type
    a Abs Type
    b
              | Def QName
    d Elims
    es <- Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> Type -> Term
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a,
                Just [Arg Term]
    us  <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es,
                [Term]
    vs [Term] -> [Term] -> Bool
    forall a. Eq a => a -> a -> Bool
    == (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]
    us -> (QName
    d QName -> Arg Type -> Arg QName
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Dom Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom Type
    a, [Term] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Term]
    vs) (Arg QName, Int) -> [(Arg QName, Int)] -> [(Arg QName, Int)]
    forall a. a -> [a] -> [a]
    : Abs Type -> [(Arg QName, Int)]
    candidateRec Abs Type
    b
              | Bool
    otherwise          -> Abs Type -> [(Arg QName, Int)]
    candidateRec Abs Type
    b
            Term
    _                      -> []
          where
            candidateRec :: Abs Type -> [(Arg QName, Int)]
    candidateRec NoAbs{}   = []
            candidateRec (Abs [Char]
    x Type
    t) = [Term] -> Type -> [(Arg QName, Int)]
    candidateArgs (Int -> Term
    var ([Term] -> Int
    forall a. Sized a => a -> Int
    size [Term]
    vs) Term -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    : [Term]
    vs) Type
    t

    {-# SPECIALIZE inferNeutral :: Term -> TCM Type #-}
    -- | Infer type of a neutral term.
    --   See also @infer@ in @Agda.TypeChecking.CheckInternal@, which has a very similar
    --   logic but also type checks all arguments.
    inferNeutral :: (PureTCM m, MonadBlock m) => Term -> m Type
    inferNeutral :: forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Type
    inferNeutral Term
    u = do
      [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.infer" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "inferNeutral" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u
      case Term
    u of
        Var Int
    i Elims
    es -> do
          a <- Int -> m Type
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
    typeOfBV Int
    i
          loop a (Var i) es
        Def QName
    f Elims
    es -> do
          m (Maybe Projection) -> (Projection -> m ()) -> m ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM (QName -> m (Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isRelevantProjection QName
    f) ((Projection -> m ()) -> m ()) -> (Projection -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \Projection
    _ -> m ()
    forall (m :: * -> *) a. MonadDebug m => m a
    nonInferable
          a <- 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
          loop a (Def f) es
        MetaV MetaId
    x Elims
    es -> do -- we assume meta instantiations to be well-typed
          a <- MetaId -> m Type
    forall (m :: * -> *). ReadTCState m => MetaId -> m Type
    metaType MetaId
    x
          loop a (MetaV x) es
        Term
    _ -> m Type
    forall (m :: * -> *) a. MonadDebug m => m a
    nonInferable
      where
        nonInferable :: MonadDebug m => m a
        nonInferable :: forall (m :: * -> *) a. MonadDebug m => m a
    nonInferable = [Char] -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__ ([Char] -> m a) -> [Char] -> m a
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines
          [ [Char]
    "inferNeutral: non-inferable term:"
          , [Char]
    "  " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Term -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Term
    u
          ]
        loop :: (PureTCM m, MonadBlock m) => Type -> (Elims -> Term) -> Elims -> m Type
        loop :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Type -> (Elims -> Term) -> Elims -> m Type
    loop Type
    t Elims -> Term
    hd [] = Type -> m Type
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    t
        loop Type
    t Elims -> Term
    hd (Elim' Term
    e:Elims
    es) = do
          t' <- case Elim' Term
    e of
            Apply (Arg ArgInfo
    ai Term
    v) ->
              Type
    -> (Dom Type -> Abs Type -> m Type) -> (Type -> m Type) -> m Type
    forall (m :: * -> *) a.
    MonadReduce m =>
    Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
    ifPiType Type
    t (\Dom Type
    _ Abs Type
    b -> Type -> m Type
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> m Type) -> Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ Abs Type
    b Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    v) Type -> m Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            IApply Term
    x Term
    y Term
    r ->
              Type
    -> (Dom Type -> Abs Type -> m Type) -> (Type -> m Type) -> m Type
    forall (m :: * -> *) a.
    PureTCM m =>
    Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
    ifPath Type
    t (\Dom Type
    _ Abs Type
    b -> Type -> m Type
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> m Type) -> Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ Abs Type
    b Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    r) Type -> m Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            Proj ProjOrigin
    o QName
    f -> do
              -- @projectTyped@ expects the type to be reduced.
              t <- Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t
              ifJustM (projectTyped (hd []) t o f) (\(Dom Type
    _,Term
    _,Type
    t') -> Type -> m Type
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    t') __IMPOSSIBLE__
          loop t' (hd . (e:)) es

    {-# SPECIALIZE computeDefType :: QName -> Elims -> TCM Type #-}
    -- | Compute the head type of a Def application. For projection-like functions
    --   this requires inferring the type of the principal argument.
    computeDefType :: (PureTCM m, MonadBlock m) => QName -> Elims -> m Type
    computeDefType :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    QName -> Elims -> m Type
    computeDefType QName
    f Elims
    es = do
      def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
      -- To compute the type @a@ of a projection-like @f@,
      -- we have to infer the type of its first argument.
      let defaultResult = Type -> m Type
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> m Type) -> Type -> m Type
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type
    defType Definition
    def
      -- Find a first argument to @f@.
      case es of
        Elims
    _ | Definition -> Int
    projectionArgs Definition
    def Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0 -> m Type
    defaultResult
        (Apply Arg Term
    arg : Elims
    _) -> do
          -- Infer its type.
          [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.infer" Int
    30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "inferring type of internal arg: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM Arg Term
    arg
          -- Jesper, 2023-02-06: infer crashes on non-inferable terms,
          -- e.g. applications of projection-like functions. Hence we bring them
          -- into postfix form.
          targ <- Term -> m Type
    forall (m :: * -> *). (PureTCM m, MonadBlock m) => Term -> m Type
    inferNeutral (Term -> m Type) -> m Term -> m Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ProjEliminator -> Term -> m Term
    forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
    elimView ProjEliminator
    EvenLone (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg)
          reportSDoc "tc.infer" 30 $
            "inferred type: " <+> prettyTCM targ
          -- getDefType wants the argument type reduced.
          -- Andreas, 2016-02-09, Issue 1825: The type of arg might be
          -- a meta-variable, e.g. in interactive development.
          -- In this case, we postpone.
          targ <- abortIfBlocked targ
          fromMaybeM __IMPOSSIBLE__ $ getDefType f targ
        Elims
    _ -> m Type
    defaultResult