    -- | 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 Control.Monad

    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.Reduce (reduce)

    import Agda.TypeChecking.DropArgs

    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Permutation
    import Agda.Utils.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 (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 (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 (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

    -- | 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.
      ProjectionView
    pv <- Term -> m ProjectionView
    forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
    projView Term
    v
      case ProjectionView
    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 (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
    /= :: ProjEliminator -> ProjEliminator -> Bool
    $c/= :: ProjEliminator -> ProjEliminator -> Bool
    == :: ProjEliminator -> ProjEliminator -> Bool
    $c== :: ProjEliminator -> ProjEliminator -> Bool
    Eq

    -- | 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
    30 (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
    prettyTCM Term
    v
      Term
    v <- Term -> m Term
    forall (m :: * -> *). PureTCM m => Term -> m Term
    reduceProjectionLike Term
    v
      [Char] -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.conv.elim" Int
    40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "elimView (projections reduced) 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
    prettyTCM Term
    v
      case ProjEliminator
    pe of
        ProjEliminator
    NoPostfix -> Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
        ProjEliminator
    _         -> do
          ProjectionView
    pv <- Term -> m ProjectionView
    forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
    projView Term
    v
          case ProjectionView
    pv of
            NoProjection{}        -> Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    v
            LoneProjectionLike QName
    f ArgInfo
    ai
              | ProjEliminator
    peProjEliminator -> ProjEliminator -> Bool
    forall a. Eq a => a -> a -> Bool
    ==ProjEliminator
    EvenLone  -> 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
    $ 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 (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)

    -- | 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"
      Definition
    defn <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
      let t :: Type
    t = Definition -> Type
    defType Definition
    defn
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.proj.like" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
        [ TCMT IO Doc
    "Checking for projection likeness "
        , QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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
    prettyTCM Type
    t
        ]
      if Definition -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Definition
    defn then
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.proj.like" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "  projection-like functions cannot be irrelevant"
      else case Definition -> Defn
    theDef Definition
    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 -> Maybe Projection
    funProjection = Maybe Projection
    Nothing, 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
                     funAbstr :: Defn -> IsAbstract
    funAbstr = IsAbstract
    ConcreteDef} -> do
          [(Arg QName, Int)]
    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
          [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
    $ if [(Arg QName, Int)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Arg QName, Int)]
    ps0 then [Char]
    "  no candidates found"
                                                    else [Char]
    "  candidates: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [(Arg QName, Int)] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [(Arg QName, Int)]
    ps0
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([(Arg QName, Int)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(Arg QName, Int)]
    ps0) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            -- Andreas 2012-09-26: only consider non-recursive functions for proj.like.
            -- Issue 700: problems with recursive funs. in term.checker and reduction
            TCMT IO Bool -> TCM () -> TCM () -> TCM ()
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM TCMT IO Bool
    recursive ([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]
    "  recursive functions are not considered for projection-likeness") (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              {- else -}
              case [(Arg QName, Int)] -> Maybe (Arg QName, Int)
    forall a. [a] -> Maybe a
    lastMaybe (((Arg QName, Int) -> Bool)
    -> [(Arg QName, Int)] -> [(Arg QName, Int)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ([Clause] -> Int -> Bool
    forall {t :: * -> *}. Foldable t => t Clause -> Int -> Bool
    checkOccurs [Clause]
    cls (Int -> Bool)
    -> ((Arg QName, Int) -> Int) -> (Arg QName, Int) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg QName, Int) -> Int
    forall a b. (a, b) -> b
    snd) [(Arg QName, Int)]
    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
    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
    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
    prettyTCM Int
    n, TCMT IO Doc
    "for type", QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Dom ([Char], Type)] -> 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 :: Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> 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 (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 :: Maybe Projection
    funProjection     = Projection -> Maybe Projection
    forall a. a -> Maybe a
    Just Projection
    projection
                               , funClauses :: [Clause]
    funClauses        = [Clause]
    cls'
                               , funSplitTree :: Maybe SplitTree
    funSplitTree      = Maybe SplitTree
    st
                               , funCompiled :: Maybe CompiledClauses
    funCompiled       = Maybe CompiledClauses
    cc
                               , funInv :: FunctionInverse
    funInv            = Int -> FunctionInverse -> FunctionInverse
    forall a. DropArgs a => Int -> a -> a
    dropArgs Int
    n (FunctionInverse -> FunctionInverse)
    -> FunctionInverse -> FunctionInverse
    forall a b. (a -> b) -> a -> b
    $ Defn -> FunctionInverse
    funInv Defn
    def
                               }
                  QName -> Definition -> TCM ()
    addConstant QName
    x (Definition -> TCM ()) -> Definition -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Definition
    defn { defPolarity :: [Polarity]
    defPolarity       = Int -> [Polarity] -> [Polarity]
    forall a. Int -> [a] -> [a]
    drop Int
    n ([Polarity] -> [Polarity]) -> [Polarity] -> [Polarity]
    forall a b. (a -> b) -> a -> b
    $ Definition -> [Polarity]
    defPolarity Definition
    defn
                                       , defArgOccurrences :: [Occurrence]
    defArgOccurrences = Int -> [Occurrence] -> [Occurrence]
    forall a. Int -> [a] -> [a]
    drop Int
    n ([Occurrence] -> [Occurrence]) -> [Occurrence] -> [Occurrence]
    forall a b. (a -> b) -> a -> b
    $ Definition -> [Occurrence]
    defArgOccurrences Definition
    defn
                                       , defDisplay :: [LocalDisplayForm]
    defDisplay        = []
                                       , theDef :: Defn
    theDef            = Defn
    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"
        Function{funAbstr :: Defn -> IsAbstract
    funAbstr = IsAbstract
    AbstractDef} ->
          [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{funProjection :: Defn -> Maybe Projection
    funProjection = Just{}} ->
          [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{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"
        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 (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
          Map Item Integer
    occs <- QName -> TCM (Map Item Integer)
    computeOccurrences QName
    x
          case Item -> Map Item Integer -> Maybe Integer
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup (QName -> Item
    ADef QName
    x) Map Item Integer
    occs of
            Just Integer
    n | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    1 -> Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True -- recursive occurrence
            Maybe Integer
    _               -> Bool -> TCMT IO Bool
    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 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 (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 (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