    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Records where

    import Control.Monad
    import Control.Monad.Except
    import Control.Monad.Trans.Maybe
    import Control.Monad.Writer

    import Data.Bifunctor
    import qualified Data.List as List
    import Data.Maybe
    import qualified Data.Set as Set
    import qualified Data.HashMap.Strict as HMap

    import Agda.Syntax.Common
    import qualified Agda.Syntax.Concrete.Name as C
    import Agda.Syntax.Concrete (FieldAssignment'(..))
    import Agda.Syntax.Abstract.Name
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Position
    import Agda.Syntax.Scope.Base (isNameInScope)

    import Agda.TypeChecking.Irrelevance
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty as TCM
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Reduce.Monad () --instance only
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Warnings

    import {-# SOURCE #-} Agda.TypeChecking.ProjectionLike (eligibleForProjectionLike)

    import Agda.Utils.Either
    import Agda.Utils.Functor (for, ($>))
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Pretty (prettyShow)
    import Agda.Utils.Singleton
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    mkCon :: ConHead -> ConInfo -> Args -> Term
    mkCon :: ConHead -> ConInfo -> Args -> Term
    mkCon ConHead
    h ConInfo
    info Args
    args = ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    h ConInfo
    info ((Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Args
    args)

    -- | Order the fields of a record construction.
    orderFields
      :: forall a . HasRange a
      => QName             -- ^ Name of record type (for error message).
      -> (Arg C.Name -> a) -- ^ How to fill a missing field.
      -> [Arg C.Name]      -- ^ Field names of the record type.
      -> [(C.Name, a)]     -- ^ Provided fields with content in the record expression.
      -> Writer [RecordFieldWarning] [a]           -- ^ Content arranged in official order.
    orderFields :: forall a.
    HasRange a =>
    QName
    -> (Arg Name -> a)
    -> [Arg Name]
    -> [(Name, a)]
    -> Writer [RecordFieldWarning] [a]
    orderFields QName
    r Arg Name -> a
    fill [Arg Name]
    axs [(Name, a)]
    fs = do
      -- reportSDoc "tc.record" 30 $ vcat
      --   [ "orderFields"
      --   , "  official fields: " <+> sep (map pretty xs)
      --   , "  provided fields: " <+> sep (map pretty ys)
      --   ]
      [(Name, a)]
    -> ([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
    -> WriterT [RecordFieldWarning] Identity ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull [(Name, a)]
    alien     (([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
     -> WriterT [RecordFieldWarning] Identity ())
    -> ([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
    -> WriterT [RecordFieldWarning] Identity ()
    forall a b. (a -> b) -> a -> b
    $ ([(Name, Range)] -> RecordFieldWarning)
    -> [(Name, a)] -> WriterT [RecordFieldWarning] Identity ()
    forall {b} {m :: * -> *} {b} {p :: * -> * -> *} {b} {a}.
    (MonadWriter b m, Singleton b b, Bifunctor p, HasRange b) =>
    ([p a Range] -> b) -> [p a b] -> m ()
    warn (([(Name, Range)] -> RecordFieldWarning)
     -> [(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
    -> ([(Name, Range)] -> RecordFieldWarning)
    -> [(Name, a)]
    -> WriterT [RecordFieldWarning] Identity ()
    forall a b. (a -> b) -> a -> b
    $ QName -> [Name] -> [(Name, Range)] -> RecordFieldWarning
    TooManyFieldsWarning QName
    r [Name]
    missing
      [(Name, a)]
    -> ([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
    -> WriterT [RecordFieldWarning] Identity ()
    forall (m :: * -> *) a.
    (Monad m, Null a) =>
    a -> (a -> m ()) -> m ()
    unlessNull [(Name, a)]
    duplicate (([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
     -> WriterT [RecordFieldWarning] Identity ())
    -> ([(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
    -> WriterT [RecordFieldWarning] Identity ()
    forall a b. (a -> b) -> a -> b
    $ ([(Name, Range)] -> RecordFieldWarning)
    -> [(Name, a)] -> WriterT [RecordFieldWarning] Identity ()
    forall {b} {m :: * -> *} {b} {p :: * -> * -> *} {b} {a}.
    (MonadWriter b m, Singleton b b, Bifunctor p, HasRange b) =>
    ([p a Range] -> b) -> [p a b] -> m ()
    warn (([(Name, Range)] -> RecordFieldWarning)
     -> [(Name, a)] -> WriterT [RecordFieldWarning] Identity ())
    -> ([(Name, Range)] -> RecordFieldWarning)
    -> [(Name, a)]
    -> WriterT [RecordFieldWarning] Identity ()
    forall a b. (a -> b) -> a -> b
    $ [(Name, Range)] -> RecordFieldWarning
    DuplicateFieldsWarning
      [a] -> Writer [RecordFieldWarning] [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([a] -> Writer [RecordFieldWarning] [a])
    -> [a] -> Writer [RecordFieldWarning] [a]
    forall a b. (a -> b) -> a -> b
    $ [Arg Name] -> (Arg Name -> a) -> [a]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [Arg Name]
    axs ((Arg Name -> a) -> [a]) -> (Arg Name -> a) -> [a]
    forall a b. (a -> b) -> a -> b
    $ \ Arg Name
    ax -> a -> Maybe a -> a
    forall a. a -> Maybe a -> a
    fromMaybe (Arg Name -> a
    fill Arg Name
    ax) (Maybe a -> a) -> Maybe a -> a
    forall a b. (a -> b) -> a -> b
    $ Name -> [(Name, a)] -> Maybe a
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup (Arg Name -> Name
    forall e. Arg e -> e
    unArg Arg Name
    ax) [(Name, a)]
    uniq
      where
        ([(Name, a)]
    uniq, [(Name, a)]
    duplicate) = ((Name, a) -> Name) -> [(Name, a)] -> ([(Name, a)], [(Name, a)])
    forall b a. Ord b => (a -> b) -> [a] -> ([a], [a])
    nubAndDuplicatesOn (Name, a) -> Name
    forall a b. (a, b) -> a
    fst [(Name, a)]
    fs   -- separating duplicate fields
        xs :: [Name]
    xs        = (Arg Name -> Name) -> [Arg Name] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Name -> Name
    forall e. Arg e -> e
    unArg [Arg Name]
    axs                       -- official fields (accord. record type)
        missing :: [Name]
    missing   = (Name -> Bool) -> [Name] -> [Name]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (Name -> Bool) -> Name -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Name] -> Name -> Bool
    forall a. Ord a => [a] -> a -> Bool
    hasElem (((Name, a) -> Name) -> [(Name, a)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, a) -> Name
    forall a b. (a, b) -> a
    fst [(Name, a)]
    fs)) [Name]
    xs  -- missing  fields
        alien :: [(Name, a)]
    alien     = ((Name, a) -> Bool) -> [(Name, a)] -> [(Name, a)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> ((Name, a) -> Bool) -> (Name, a) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Name] -> Name -> Bool
    forall a. Ord a => [a] -> a -> Bool
    hasElem [Name]
    xs (Name -> Bool) -> ((Name, a) -> Name) -> (Name, a) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, a) -> Name
    forall a b. (a, b) -> a
    fst) [(Name, a)]
    fs      -- spurious fields
        warn :: ([p a Range] -> b) -> [p a b] -> m ()
    warn [p a Range] -> b
    w    = b -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (b -> m ()) -> ([p a b] -> b) -> [p a b] -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b -> b
    forall el coll. Singleton el coll => el -> coll
    singleton (b -> b) -> ([p a b] -> b) -> [p a b] -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [p a Range] -> b
    w ([p a Range] -> b) -> ([p a b] -> [p a Range]) -> [p a b] -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (p a b -> p a Range) -> [p a b] -> [p a Range]
    forall a b. (a -> b) -> [a] -> [b]
    map ((b -> Range) -> p a b -> p a Range
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second b -> Range
    forall a. HasRange a => a -> Range
    getRange)

    -- | Raise generated 'RecordFieldWarning's as warnings.
    warnOnRecordFieldWarnings :: Writer [RecordFieldWarning] a -> TCM a
    warnOnRecordFieldWarnings :: forall a. Writer [RecordFieldWarning] a -> TCM a
    warnOnRecordFieldWarnings Writer [RecordFieldWarning] a
    comp = do
      let (a
    res, [RecordFieldWarning]
    ws) = Writer [RecordFieldWarning] a -> (a, [RecordFieldWarning])
    forall w a. Writer w a -> (a, w)
    runWriter Writer [RecordFieldWarning] a
    comp
      (RecordFieldWarning -> TCMT IO ())
    -> [RecordFieldWarning] -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Warning -> TCMT IO ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCMT IO ())
    -> (RecordFieldWarning -> Warning)
    -> RecordFieldWarning
    -> TCMT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RecordFieldWarning -> Warning
    RecordFieldWarning) [RecordFieldWarning]
    ws
      a -> TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    res

    -- | Raise generated 'RecordFieldWarning's as errors.
    failOnRecordFieldWarnings :: Writer [RecordFieldWarning] a -> TCM a
    failOnRecordFieldWarnings :: forall a. Writer [RecordFieldWarning] a -> TCM a
    failOnRecordFieldWarnings Writer [RecordFieldWarning] a
    comp = do
      let (a
    res, [RecordFieldWarning]
    ws) = Writer [RecordFieldWarning] a -> (a, [RecordFieldWarning])
    forall w a. Writer w a -> (a, w)
    runWriter Writer [RecordFieldWarning] a
    comp
      (RecordFieldWarning -> TCMT IO Any)
    -> [RecordFieldWarning] -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (TypeError -> TCMT IO Any
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO Any)
    -> (RecordFieldWarning -> TypeError)
    -> RecordFieldWarning
    -> TCMT IO Any
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RecordFieldWarning -> TypeError
    recordFieldWarningToError) [RecordFieldWarning]
    ws
        -- This will raise the first warning (if any) as error.
      a -> TCM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    res

    -- | Order the fields of a record construction.
    --   Raise generated 'RecordFieldWarning's as warnings.
    orderFieldsWarn
      :: forall a . HasRange a
      => QName             -- ^ Name of record type (for error message).
      -> (Arg C.Name -> a) -- ^ How to fill a missing field.
      -> [Arg C.Name]      -- ^ Field names of the record type.
      -> [(C.Name, a)]     -- ^ Provided fields with content in the record expression.
      -> TCM [a]           -- ^ Content arranged in official order.
    orderFieldsWarn :: forall a.
    HasRange a =>
    QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
    orderFieldsWarn QName
    r Arg Name -> a
    fill [Arg Name]
    axs [(Name, a)]
    fs = Writer [RecordFieldWarning] [a] -> TCM [a]
    forall a. Writer [RecordFieldWarning] a -> TCM a
    warnOnRecordFieldWarnings (Writer [RecordFieldWarning] [a] -> TCM [a])
    -> Writer [RecordFieldWarning] [a] -> TCM [a]
    forall a b. (a -> b) -> a -> b
    $ QName
    -> (Arg Name -> a)
    -> [Arg Name]
    -> [(Name, a)]
    -> Writer [RecordFieldWarning] [a]
    forall a.
    HasRange a =>
    QName
    -> (Arg Name -> a)
    -> [Arg Name]
    -> [(Name, a)]
    -> Writer [RecordFieldWarning] [a]
    orderFields QName
    r Arg Name -> a
    fill [Arg Name]
    axs [(Name, a)]
    fs

    -- | Order the fields of a record construction.
    --   Raise generated 'RecordFieldWarning's as errors.
    orderFieldsFail
      :: forall a . HasRange a
      => QName             -- ^ Name of record type (for error message).
      -> (Arg C.Name -> a) -- ^ How to fill a missing field.
      -> [Arg C.Name]      -- ^ Field names of the record type.
      -> [(C.Name, a)]     -- ^ Provided fields with content in the record expression.
      -> TCM [a]           -- ^ Content arranged in official order.
    orderFieldsFail :: forall a.
    HasRange a =>
    QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
    orderFieldsFail QName
    r Arg Name -> a
    fill [Arg Name]
    axs [(Name, a)]
    fs = Writer [RecordFieldWarning] [a] -> TCM [a]
    forall a. Writer [RecordFieldWarning] a -> TCM a
    failOnRecordFieldWarnings (Writer [RecordFieldWarning] [a] -> TCM [a])
    -> Writer [RecordFieldWarning] [a] -> TCM [a]
    forall a b. (a -> b) -> a -> b
    $ QName
    -> (Arg Name -> a)
    -> [Arg Name]
    -> [(Name, a)]
    -> Writer [RecordFieldWarning] [a]
    forall a.
    HasRange a =>
    QName
    -> (Arg Name -> a)
    -> [Arg Name]
    -> [(Name, a)]
    -> Writer [RecordFieldWarning] [a]
    orderFields QName
    r Arg Name -> a
    fill [Arg Name]
    axs [(Name, a)]
    fs

    -- | A record field assignment @record{xs = es}@ might not mention all
    --   visible fields.  @insertMissingFields@ inserts placeholders for
    --   the missing visible fields and returns the values in order
    --   of the fields in the record declaration.
    insertMissingFields
      :: forall a . HasRange a
      => QName                -- ^ Name of record type (for error reporting).
      -> (C.Name -> a)        -- ^ Function to generate a placeholder for missing visible field.
      -> [FieldAssignment' a] -- ^ Given fields.
      -> [Arg C.Name]         -- ^ All record field names with 'ArgInfo'.
      -> Writer [RecordFieldWarning] [NamedArg a]
           -- ^ Given fields enriched by placeholders for missing explicit fields.
    insertMissingFields :: forall a.
    HasRange a =>
    QName
    -> (Name -> a)
    -> [FieldAssignment' a]
    -> [Arg Name]
    -> Writer [RecordFieldWarning] [NamedArg a]
    insertMissingFields QName
    r Name -> a
    placeholder [FieldAssignment' a]
    fs [Arg Name]
    axs = do
      -- Compute the list of given fields, decorated with the ArgInfo from the record def.
      let arg :: Name -> a -> Arg (Named NamedName a)
    arg Name
    x a
    e = Maybe (Arg Name)
    -> Arg (Named NamedName a)
    -> (Arg Name -> Arg (Named NamedName a))
    -> Arg (Named NamedName a)
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe ((Arg Name -> Bool) -> [Arg Name] -> Maybe (Arg Name)
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find ((Name
    x Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Name -> Bool) -> (Arg Name -> Name) -> Arg Name -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Name -> Name
    forall e. Arg e -> e
    unArg) [Arg Name]
    axs) (a -> Arg (Named NamedName a)
    forall a. a -> NamedArg a
    defaultNamedArg a
    e) ((Arg Name -> Arg (Named NamedName a)) -> Arg (Named NamedName a))
    -> (Arg Name -> Arg (Named NamedName a)) -> Arg (Named NamedName a)
    forall a b. (a -> b) -> a -> b
    $ \ Arg Name
    a ->
            Arg Name -> a -> Named NamedName a
    forall c. Arg Name -> c -> Named_ c
    nameIfHidden Arg Name
    a a
    e Named NamedName a -> Arg Name -> Arg (Named NamedName a)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg Name
    a
          givenFields :: [(Name, Maybe (Arg (Named NamedName a)))]
    givenFields = [ (Name
    x, Arg (Named NamedName a) -> Maybe (Arg (Named NamedName a))
    forall a. a -> Maybe a
    Just (Arg (Named NamedName a) -> Maybe (Arg (Named NamedName a)))
    -> Arg (Named NamedName a) -> Maybe (Arg (Named NamedName a))
    forall a b. (a -> b) -> a -> b
    $ Name -> a -> Arg (Named NamedName a)
    arg Name
    x a
    e) | FieldAssignment Name
    x a
    e <- [FieldAssignment' a]
    fs ]

      -- Omitted explicit fields are filled in with placeholders.
      -- Omitted implicit or instance fields
      -- are still left out and inserted later by checkArguments_.
      [Maybe (Arg (Named NamedName a))] -> [Arg (Named NamedName a)]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe (Arg (Named NamedName a))] -> [Arg (Named NamedName a)])
    -> WriterT
         [RecordFieldWarning] Identity [Maybe (Arg (Named NamedName a))]
    -> Writer [RecordFieldWarning] [Arg (Named NamedName a)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName
    -> (Arg Name -> Maybe (Arg (Named NamedName a)))
    -> [Arg Name]
    -> [(Name, Maybe (Arg (Named NamedName a)))]
    -> WriterT
         [RecordFieldWarning] Identity [Maybe (Arg (Named NamedName a))]
    forall a.
    HasRange a =>
    QName
    -> (Arg Name -> a)
    -> [Arg Name]
    -> [(Name, a)]
    -> Writer [RecordFieldWarning] [a]
    orderFields QName
    r Arg Name -> Maybe (Arg (Named NamedName a))
    fill [Arg Name]
    axs [(Name, Maybe (Arg (Named NamedName a)))]
    givenFields
      where
        fill :: Arg C.Name -> Maybe (NamedArg a)
        fill :: Arg Name -> Maybe (Arg (Named NamedName a))
    fill Arg Name
    ax
          | Arg Name -> Bool
    forall a. LensHiding a => a -> Bool
    visible Arg Name
    ax = Arg (Named NamedName a) -> Maybe (Arg (Named NamedName a))
    forall a. a -> Maybe a
    Just (Arg (Named NamedName a) -> Maybe (Arg (Named NamedName a)))
    -> Arg (Named NamedName a) -> Maybe (Arg (Named NamedName a))
    forall a b. (a -> b) -> a -> b
    $ Origin -> Arg (Named NamedName a) -> Arg (Named NamedName a)
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Inserted (Arg (Named NamedName a) -> Arg (Named NamedName a))
    -> Arg (Named NamedName a) -> Arg (Named NamedName a)
    forall a b. (a -> b) -> a -> b
    $ a -> Named NamedName a
    forall a name. a -> Named name a
    unnamed (a -> Named NamedName a)
    -> (Name -> a) -> Name -> Named NamedName a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> a
    placeholder (Name -> Named NamedName a) -> Arg Name -> Arg (Named NamedName a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Name
    ax
          | Bool
    otherwise  = Maybe (Arg (Named NamedName a))
    forall a. Maybe a
    Nothing
        -- Andreas, 2017-04-13, issue #2494
        -- We need to put the field names as argument names for hidden arguments.
        -- Otherwise, insertImplicit does not do the right thing.
        nameIfHidden :: Arg C.Name -> c -> Named_ c
        nameIfHidden :: forall c. Arg Name -> c -> Named_ c
    nameIfHidden Arg Name
    ax
          | Arg Name -> Bool
    forall a. LensHiding a => a -> Bool
    visible Arg Name
    ax = c -> Named NamedName c
    forall a name. a -> Named name a
    unnamed
          | Bool
    otherwise  = NamedName -> c -> Named NamedName c
    forall name a. name -> a -> Named name a
    named (NamedName -> c -> Named NamedName c)
    -> NamedName -> c -> Named NamedName c
    forall a b. (a -> b) -> a -> b
    $ Origin -> Ranged ArgName -> NamedName
    forall a. Origin -> a -> WithOrigin a
    WithOrigin Origin
    Inserted (Ranged ArgName -> NamedName) -> Ranged ArgName -> NamedName
    forall a b. (a -> b) -> a -> b
    $ Range -> ArgName -> Ranged ArgName
    forall a. Range -> a -> Ranged a
    Ranged (Arg Name -> Range
    forall a. HasRange a => a -> Range
    getRange Arg Name
    ax) (ArgName -> Ranged ArgName) -> ArgName -> Ranged ArgName
    forall a b. (a -> b) -> a -> b
    $ Name -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow (Name -> ArgName) -> Name -> ArgName
    forall a b. (a -> b) -> a -> b
    $ Arg Name -> Name
    forall e. Arg e -> e
    unArg Arg Name
    ax

    -- | A record field assignment @record{xs = es}@ might not mention all
    --   visible fields.  @insertMissingFields@ inserts placeholders for
    --   the missing visible fields and returns the values in order
    --   of the fields in the record declaration.
    insertMissingFieldsWarn
      :: forall a . HasRange a
      => QName                -- ^ Name of record type (for error reporting).
      -> (C.Name -> a)        -- ^ Function to generate a placeholder for missing visible field.
      -> [FieldAssignment' a] -- ^ Given fields.
      -> [Arg C.Name]         -- ^ All record field names with 'ArgInfo'.
      -> TCM [NamedArg a]     -- ^ Given fields enriched by placeholders for missing explicit fields.
    insertMissingFieldsWarn :: forall a.
    HasRange a =>
    QName
    -> (Name -> a)
    -> [FieldAssignment' a]
    -> [Arg Name]
    -> TCM [NamedArg a]
    insertMissingFieldsWarn QName
    r Name -> a
    placeholder [FieldAssignment' a]
    fs [Arg Name]
    axs =
      Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a]
    forall a. Writer [RecordFieldWarning] a -> TCM a
    warnOnRecordFieldWarnings (Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a])
    -> Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a]
    forall a b. (a -> b) -> a -> b
    $ QName
    -> (Name -> a)
    -> [FieldAssignment' a]
    -> [Arg Name]
    -> Writer [RecordFieldWarning] [NamedArg a]
    forall a.
    HasRange a =>
    QName
    -> (Name -> a)
    -> [FieldAssignment' a]
    -> [Arg Name]
    -> Writer [RecordFieldWarning] [NamedArg a]
    insertMissingFields QName
    r Name -> a
    placeholder [FieldAssignment' a]
    fs [Arg Name]
    axs

    -- | A record field assignment @record{xs = es}@ might not mention all
    --   visible fields.  @insertMissingFields@ inserts placeholders for
    --   the missing visible fields and returns the values in order
    --   of the fields in the record declaration.
    insertMissingFieldsFail
      :: forall a . HasRange a
      => QName                -- ^ Name of record type (for error reporting).
      -> (C.Name -> a)        -- ^ Function to generate a placeholder for missing visible field.
      -> [FieldAssignment' a] -- ^ Given fields.
      -> [Arg C.Name]         -- ^ All record field names with 'ArgInfo'.
      -> TCM [NamedArg a]     -- ^ Given fields enriched by placeholders for missing explicit fields.
    insertMissingFieldsFail :: forall a.
    HasRange a =>
    QName
    -> (Name -> a)
    -> [FieldAssignment' a]
    -> [Arg Name]
    -> TCM [NamedArg a]
    insertMissingFieldsFail QName
    r Name -> a
    placeholder [FieldAssignment' a]
    fs [Arg Name]
    axs =
      Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a]
    forall a. Writer [RecordFieldWarning] a -> TCM a
    failOnRecordFieldWarnings (Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a])
    -> Writer [RecordFieldWarning] [NamedArg a] -> TCM [NamedArg a]
    forall a b. (a -> b) -> a -> b
    $ QName
    -> (Name -> a)
    -> [FieldAssignment' a]
    -> [Arg Name]
    -> Writer [RecordFieldWarning] [NamedArg a]
    forall a.
    HasRange a =>
    QName
    -> (Name -> a)
    -> [FieldAssignment' a]
    -> [Arg Name]
    -> Writer [RecordFieldWarning] [NamedArg a]
    insertMissingFields QName
    r Name -> a
    placeholder [FieldAssignment' a]
    fs [Arg Name]
    axs

    -- | Get the definition for a record. Throws an exception if the name
    --   does not refer to a record or the record is abstract.
    getRecordDef :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m Defn
    getRecordDef :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
    QName -> m Defn
    getRecordDef QName
    r = m Defn -> (Defn -> m Defn) -> Maybe Defn -> m Defn
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe m Defn
    err Defn -> m Defn
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Defn -> m Defn) -> m (Maybe Defn) -> m Defn
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> m (Maybe Defn)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    r
      where err :: m Defn
    err = TypeError -> m Defn
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m Defn) -> TypeError -> m Defn
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    ShouldBeRecordType (Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    HasCallStack => Sort' Term
    __DUMMY_SORT__ (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    r [])

    -- | Get the record name belonging to a field name.
    getRecordOfField :: QName -> TCM (Maybe QName)
    getRecordOfField :: QName -> TCM (Maybe QName)
    getRecordOfField QName
    d = TCMT IO (Maybe Projection)
    -> TCM (Maybe QName)
    -> (Projection -> TCM (Maybe QName))
    -> TCM (Maybe QName)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> TCMT IO (Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe Projection)
    isProjection QName
    d) (Maybe QName -> TCM (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe QName
    forall a. Maybe a
    Nothing) ((Projection -> TCM (Maybe QName)) -> TCM (Maybe QName))
    -> (Projection -> TCM (Maybe QName)) -> TCM (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $
      \ Projection{ projProper :: Projection -> Maybe QName
    projProper = Maybe QName
    proper, projFromType :: Projection -> Arg QName
    projFromType = Arg QName
    r} ->
        Maybe QName -> TCM (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe QName -> TCM (Maybe QName))
    -> Maybe QName -> TCM (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ Arg QName -> QName
    forall e. Arg e -> e
    unArg Arg QName
    r QName -> Maybe QName -> Maybe QName
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Maybe QName
    proper -- if proper then Just (unArg r) else Nothing

    -- | Get the field names of a record.
    getRecordFieldNames :: (HasConstInfo m, ReadTCState m, MonadError TCErr m)
                        => QName -> m [Dom C.Name]
    getRecordFieldNames :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
    QName -> m [Dom Name]
    getRecordFieldNames QName
    r = Defn -> [Dom Name]
    recordFieldNames (Defn -> [Dom Name]) -> m Defn -> m [Dom Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Defn
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
    QName -> m Defn
    getRecordDef QName
    r

    getRecordFieldNames_ :: (HasConstInfo m, ReadTCState m)
                         => QName -> m (Maybe [Dom C.Name])
    getRecordFieldNames_ :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m (Maybe [Dom Name])
    getRecordFieldNames_ QName
    r = (Defn -> [Dom Name]) -> Maybe Defn -> Maybe [Dom Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Defn -> [Dom Name]
    recordFieldNames (Maybe Defn -> Maybe [Dom Name])
    -> m (Maybe Defn) -> m (Maybe [Dom Name])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe Defn)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    r

    recordFieldNames :: Defn -> [Dom C.Name]
    recordFieldNames :: Defn -> [Dom Name]
    recordFieldNames = (Dom' Term QName -> Dom Name) -> [Dom' Term QName] -> [Dom Name]
    forall a b. (a -> b) -> [a] -> [b]
    map ((QName -> Name) -> Dom' Term QName -> Dom Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Name -> Name
    nameConcrete (Name -> Name) -> (QName -> Name) -> QName -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    qnameName)) ([Dom' Term QName] -> [Dom Name])
    -> (Defn -> [Dom' Term QName]) -> Defn -> [Dom Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Defn -> [Dom' Term QName]
    recFields

    -- | Find all records with at least the given fields.
    findPossibleRecords :: [C.Name] -> TCM [QName]
    findPossibleRecords :: [Name] -> TCM [QName]
    findPossibleRecords [Name]
    fields = do
      [Definition]
    defs  <- HashMap QName Definition -> [Definition]
    forall k v. HashMap k v -> [v]
    HMap.elems (HashMap QName Definition -> [Definition])
    -> TCMT IO (HashMap QName Definition) -> TCMT IO [Definition]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' (HashMap QName Definition) TCState
    -> TCMT IO (HashMap QName Definition)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC ((Signature -> f Signature) -> TCState -> f TCState
    Lens' Signature TCState
    stSignature ((Signature -> f Signature) -> TCState -> f TCState)
    -> ((HashMap QName Definition -> f (HashMap QName Definition))
        -> Signature -> f Signature)
    -> (HashMap QName Definition -> f (HashMap QName Definition))
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature
    Lens' (HashMap QName Definition) Signature
    sigDefinitions)
      [Definition]
    idefs <- HashMap QName Definition -> [Definition]
    forall k v. HashMap k v -> [v]
    HMap.elems (HashMap QName Definition -> [Definition])
    -> TCMT IO (HashMap QName Definition) -> TCMT IO [Definition]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' (HashMap QName Definition) TCState
    -> TCMT IO (HashMap QName Definition)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC ((Signature -> f Signature) -> TCState -> f TCState
    Lens' Signature TCState
    stImports   ((Signature -> f Signature) -> TCState -> f TCState)
    -> ((HashMap QName Definition -> f (HashMap QName Definition))
        -> Signature -> f Signature)
    -> (HashMap QName Definition -> f (HashMap QName Definition))
    -> TCState
    -> f TCState
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (HashMap QName Definition -> f (HashMap QName Definition))
    -> Signature -> f Signature
    Lens' (HashMap QName Definition) Signature
    sigDefinitions)
      ScopeInfo
    scope <- TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
      [QName] -> TCM [QName]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([QName] -> TCM [QName]) -> [QName] -> TCM [QName]
    forall a b. (a -> b) -> a -> b
    $ (QName -> Bool) -> [QName] -> [QName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (QName -> ScopeInfo -> Bool
    `isNameInScope` ScopeInfo
    scope) ([QName] -> [QName]) -> [QName] -> [QName]
    forall a b. (a -> b) -> a -> b
    $ [Definition] -> [QName]
    cands [Definition]
    defs [QName] -> [QName] -> [QName]
    forall a. [a] -> [a] -> [a]
    ++ [Definition] -> [QName]
    cands [Definition]
    idefs
      where
        cands :: [Definition] -> [QName]
    cands [Definition]
    defs = [ Definition -> QName
    defName Definition
    d | Definition
    d <- [Definition]
    defs, Definition -> Bool
    possible Definition
    d ]
        possible :: Definition -> Bool
    possible Definition
    def =
          -- Check whether the given fields are contained
          -- in the fields of record @def@ (if it is a record).
          case Definition -> Defn
    theDef Definition
    def of
            Record{ recFields :: Defn -> [Dom' Term QName]
    recFields = [Dom' Term QName]
    fs } -> Set Name -> Set Name -> Bool
    forall a. Ord a => Set a -> Set a -> Bool
    Set.isSubsetOf Set Name
    given (Set Name -> Bool) -> Set Name -> Bool
    forall a b. (a -> b) -> a -> b
    $
              [Name] -> Set Name
    forall a. Ord a => [a] -> Set a
    Set.fromList ([Name] -> Set Name) -> [Name] -> Set Name
    forall a b. (a -> b) -> a -> b
    $ (Dom' Term QName -> Name) -> [Dom' Term QName] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> Name
    nameConcrete (Name -> Name)
    -> (Dom' Term QName -> Name) -> Dom' Term QName -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Name
    qnameName (QName -> Name)
    -> (Dom' Term QName -> QName) -> Dom' Term QName -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom' Term QName -> QName
    forall t e. Dom' t e -> e
    unDom) [Dom' Term QName]
    fs
            Defn
    _ -> Bool
    False
        given :: Set Name
    given = [Name] -> Set Name
    forall a. Ord a => [a] -> Set a
    Set.fromList [Name]
    fields

    -- | Get the field types of a record.
    getRecordFieldTypes :: QName -> TCM Telescope
    getRecordFieldTypes :: QName -> TCM Telescope
    getRecordFieldTypes QName
    r = Defn -> Telescope
    recTel (Defn -> Telescope) -> TCMT IO Defn -> TCM Telescope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Defn
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
    QName -> m Defn
    getRecordDef QName
    r

    -- | Get the field names belonging to a record type.
    getRecordTypeFields
      :: Type  -- ^ Record type.  Need not be reduced.
      -> TCM [Dom QName]
    getRecordTypeFields :: Type -> TCM [Dom' Term QName]
    getRecordTypeFields Type
    t = do
      Type
    t <- Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t  -- Andreas, 2018-03-03, fix for #2989.
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
        Def QName
    r Elims
    _ -> do
          Defn
    rDef <- Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    r
          case Defn
    rDef of
            Record { recFields :: Defn -> [Dom' Term QName]
    recFields = [Dom' Term QName]
    fields } -> [Dom' Term QName] -> TCM [Dom' Term QName]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Dom' Term QName]
    fields
            Defn
    _ -> TCM [Dom' Term QName]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Term
    _ -> TCM [Dom' Term QName]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Returns the given record type's constructor name (with an empty
    -- range).
    getRecordConstructor :: (HasConstInfo m, ReadTCState m, MonadError TCErr m) => QName -> m ConHead
    getRecordConstructor :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
    QName -> m ConHead
    getRecordConstructor QName
    r = KillRangeT ConHead
    forall a. KillRange a => KillRangeT a
    killRange KillRangeT ConHead -> (Defn -> ConHead) -> Defn -> ConHead
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Defn -> ConHead
    recConHead (Defn -> ConHead) -> m Defn -> m ConHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Defn
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
    QName -> m Defn
    getRecordDef QName
    r

    -- | Check if a name refers to a record.
    --   If yes, return record definition.
    {-# SPECIALIZE isRecord :: QName -> TCM (Maybe Defn) #-}
    {-# SPECIALIZE isRecord :: QName -> ReduceM (Maybe Defn) #-}
    isRecord :: HasConstInfo m => QName -> m (Maybe Defn)
    isRecord :: forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    r = do
      Defn
    def <- Definition -> Defn
    theDef (Definition -> Defn) -> m Definition -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    r
      Maybe Defn -> m (Maybe Defn)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Defn -> m (Maybe Defn)) -> Maybe Defn -> m (Maybe Defn)
    forall a b. (a -> b) -> a -> b
    $ case Defn
    def of
        Record{} -> Defn -> Maybe Defn
    forall a. a -> Maybe a
    Just Defn
    def
        Defn
    _        -> Maybe Defn
    forall a. Maybe a
    Nothing

    -- | Reduce a type and check whether it is a record type.
    --   Succeeds only if type is not blocked by a meta var.
    --   If yes, return its name, parameters, and definition.
    isRecordType :: PureTCM m => Type -> m (Maybe (QName, Args, Defn))
    isRecordType :: forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (QName, Args, Defn))
    isRecordType Type
    t = (Blocked Type -> Maybe (QName, Args, Defn))
    -> ((QName, Args, Defn) -> Maybe (QName, Args, Defn))
    -> Either (Blocked Type) (QName, Args, Defn)
    -> Maybe (QName, Args, Defn)
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (Maybe (QName, Args, Defn)
    -> Blocked Type -> Maybe (QName, Args, Defn)
    forall a b. a -> b -> a
    const Maybe (QName, Args, Defn)
    forall a. Maybe a
    Nothing) (QName, Args, Defn) -> Maybe (QName, Args, Defn)
    forall a. a -> Maybe a
    Just (Either (Blocked Type) (QName, Args, Defn)
     -> Maybe (QName, Args, Defn))
    -> m (Either (Blocked Type) (QName, Args, Defn))
    -> m (Maybe (QName, Args, Defn))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (Either (Blocked Type) (QName, Args, Defn))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Either (Blocked Type) (QName, Args, Defn))
    tryRecordType Type
    t

    -- | Reduce a type and check whether it is a record type.
    --   Succeeds only if type is not blocked by a meta var.
    --   If yes, return its name, parameters, and definition.
    --   If no, return the reduced type (unless it is blocked).
    tryRecordType :: PureTCM m => Type -> m (Either (Blocked Type) (QName, Args, Defn))
    tryRecordType :: forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Either (Blocked Type) (QName, Args, Defn))
    tryRecordType Type
    t = Type
    -> (Blocker
        -> Type -> m (Either (Blocked Type) (QName, Args, Defn)))
    -> (NotBlocked
        -> Type -> m (Either (Blocked Type) (QName, Args, Defn)))
    -> m (Either (Blocked Type) (QName, Args, Defn))
    forall t (m :: * -> *) a.
    (Reduce t, IsMeta t, MonadReduce m) =>
    t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
    ifBlocked Type
    t (\ Blocker
    m Type
    a -> Either (Blocked Type) (QName, Args, Defn)
    -> m (Either (Blocked Type) (QName, Args, Defn))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Blocked Type) (QName, Args, Defn)
     -> m (Either (Blocked Type) (QName, Args, Defn)))
    -> Either (Blocked Type) (QName, Args, Defn)
    -> m (Either (Blocked Type) (QName, Args, Defn))
    forall a b. (a -> b) -> a -> b
    $ Blocked Type -> Either (Blocked Type) (QName, Args, Defn)
    forall a b. a -> Either a b
    Left (Blocked Type -> Either (Blocked Type) (QName, Args, Defn))
    -> Blocked Type -> Either (Blocked Type) (QName, Args, Defn)
    forall a b. (a -> b) -> a -> b
    $ Blocker -> Type -> Blocked Type
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    m Type
    a) ((NotBlocked
      -> Type -> m (Either (Blocked Type) (QName, Args, Defn)))
     -> m (Either (Blocked Type) (QName, Args, Defn)))
    -> (NotBlocked
        -> Type -> m (Either (Blocked Type) (QName, Args, Defn)))
    -> m (Either (Blocked Type) (QName, Args, Defn))
    forall a b. (a -> b) -> a -> b
    $ \ NotBlocked
    nb Type
    t -> do
      let no :: m (Either (Blocked Type) (QName, Args, Defn))
    no = Either (Blocked Type) (QName, Args, Defn)
    -> m (Either (Blocked Type) (QName, Args, Defn))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Blocked Type) (QName, Args, Defn)
     -> m (Either (Blocked Type) (QName, Args, Defn)))
    -> Either (Blocked Type) (QName, Args, Defn)
    -> m (Either (Blocked Type) (QName, Args, Defn))
    forall a b. (a -> b) -> a -> b
    $ Blocked Type -> Either (Blocked Type) (QName, Args, Defn)
    forall a b. a -> Either a b
    Left (Blocked Type -> Either (Blocked Type) (QName, Args, Defn))
    -> Blocked Type -> Either (Blocked Type) (QName, Args, Defn)
    forall a b. (a -> b) -> a -> b
    $ NotBlocked -> Type -> Blocked Type
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked
    nb Type
    t
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
        Def QName
    r Elims
    es -> do
          let vs :: Args
    vs = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
          m (Maybe Defn)
    -> m (Either (Blocked Type) (QName, Args, Defn))
    -> (Defn -> m (Either (Blocked Type) (QName, Args, Defn)))
    -> m (Either (Blocked Type) (QName, Args, Defn))
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> m (Maybe Defn)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    r) m (Either (Blocked Type) (QName, Args, Defn))
    no ((Defn -> m (Either (Blocked Type) (QName, Args, Defn)))
     -> m (Either (Blocked Type) (QName, Args, Defn)))
    -> (Defn -> m (Either (Blocked Type) (QName, Args, Defn)))
    -> m (Either (Blocked Type) (QName, Args, Defn))
    forall a b. (a -> b) -> a -> b
    $ \ Defn
    def -> Either (Blocked Type) (QName, Args, Defn)
    -> m (Either (Blocked Type) (QName, Args, Defn))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Blocked Type) (QName, Args, Defn)
     -> m (Either (Blocked Type) (QName, Args, Defn)))
    -> Either (Blocked Type) (QName, Args, Defn)
    -> m (Either (Blocked Type) (QName, Args, Defn))
    forall a b. (a -> b) -> a -> b
    $ (QName, Args, Defn) -> Either (Blocked Type) (QName, Args, Defn)
    forall a b. b -> Either a b
    Right (QName
    r,Args
    vs,Defn
    def)
        Term
    _ -> m (Either (Blocked Type) (QName, Args, Defn))
    no

    -- | Get the original projection info for name.
    {-# SPECIALIZE origProjection :: QName -> TCM (QName, Definition, Maybe Projection) #-}
    origProjection ::  HasConstInfo m => QName -> m (QName, Definition, Maybe Projection)
    origProjection :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (QName, Definition, Maybe Projection)
    origProjection QName
    f = do
      Definition
    def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
      let proj :: Maybe Projection
    proj     = Defn -> Maybe Projection
    isProjection_ (Defn -> Maybe Projection) -> Defn -> Maybe Projection
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    def
          fallback :: m (QName, Definition, Maybe Projection)
    fallback = (QName, Definition, Maybe Projection)
    -> m (QName, Definition, Maybe Projection)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    f, Definition
    def, Maybe Projection
    proj)
      Maybe Projection
    -> m (QName, Definition, Maybe Projection)
    -> (Projection -> m (QName, Definition, Maybe Projection))
    -> m (QName, Definition, Maybe Projection)
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe Projection
    proj m (QName, Definition, Maybe Projection)
    fallback ((Projection -> m (QName, Definition, Maybe Projection))
     -> m (QName, Definition, Maybe Projection))
    -> (Projection -> m (QName, Definition, Maybe Projection))
    -> m (QName, Definition, Maybe Projection)
    forall a b. (a -> b) -> a -> b
    $
        \ p :: Projection
    p@Projection{ projProper :: Projection -> Maybe QName
    projProper = Maybe QName
    proper, projOrig :: Projection -> QName
    projOrig = QName
    f' } ->
          if Maybe QName -> Bool
    forall a. Maybe a -> Bool
    isNothing Maybe QName
    proper Bool -> Bool -> Bool
    || QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f' then m (QName, Definition, Maybe Projection)
    fallback else do
            Definition
    def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f'
            (QName, Definition, Maybe Projection)
    -> m (QName, Definition, Maybe Projection)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    f', Definition
    def, Defn -> Maybe Projection
    isProjection_ (Defn -> Maybe Projection) -> Defn -> Maybe Projection
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    def)

    -- | @getDefType f t@ computes the type of (possibly projection-(like))
    --   function @f@ whose first argument has type @t@.
    --   The `parameters' for @f@ are extracted from @t@.
    --   @Nothing@ if @f@ is projection(like) but
    --   @t@ is not a data/record/axiom type.
    --
    --   Precondition: @t@ is reduced.
    --
    --   See also: 'Agda.TypeChecking.Datatypes.getConType'
    getDefType :: PureTCM m => QName -> Type -> m (Maybe Type)
    getDefType :: forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
    getDefType QName
    f Type
    t = do
      -- Andreas, Issue #1973: we need to take the original projection
      -- since the parameters from the reduced type t are correct for
      -- the original projection only.
      -- Due to module application, the given (non-original) projection f
      -- may expect less parameters, those corresponding to a unreduced
      -- version of t (which we cannot obtain here).
      (QName
    f, Definition
    def, Maybe Projection
    mp) <- QName -> m (QName, Definition, Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (QName, Definition, Maybe Projection)
    origProjection QName
    f
      let a :: Type
    a = Definition -> Type
    defType Definition
    def
      -- if @f@ is not a projection (like) function, @a@ is the correct type
          fallback :: m (Maybe Type)
    fallback = Maybe Type -> m (Maybe Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Type -> m (Maybe Type)) -> Maybe Type -> m (Maybe Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> Maybe Type
    forall a. a -> Maybe a
    Just Type
    a
      ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.deftype" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "definition f =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName
    "  -- raw: " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow QName
    f)
        , TCMT IO Doc
    "has type   a =" 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
    a
        , TCMT IO Doc
    "principal  t =" 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
        ]
      Maybe Projection
    -> m (Maybe Type)
    -> (Projection -> m (Maybe Type))
    -> m (Maybe Type)
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe Projection
    mp m (Maybe Type)
    fallback ((Projection -> m (Maybe Type)) -> m (Maybe Type))
    -> (Projection -> m (Maybe Type)) -> m (Maybe Type)
    forall a b. (a -> b) -> a -> b
    $
        \ (Projection{ projIndex :: Projection -> Int
    projIndex = Int
    n }) -> if Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    0 then m (Maybe Type)
    fallback else do
          -- otherwise, we have to instantiate @a@ to the "parameters" of @f@
          let npars :: Int
    npars | Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0    = Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                    | Bool
    otherwise = Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1
          ArgName -> Int -> ArgName -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> ArgName -> m ()
    reportSLn ArgName
    "tc.deftype" Int
    20 (ArgName -> m ()) -> ArgName -> m ()
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "projIndex    = " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ Int -> ArgName
    forall a. Show a => a -> ArgName
    show Int
    n
          -- we get the parameters from type @t@
          case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
            Def QName
    d Elims
    es -> do
              -- Andreas, 2013-10-22
              -- we need to check this @Def@ is fully reduced.
              -- If it is stuck due to disabled reductions
              -- (because of failed termination check),
              -- we will produce garbage parameters.
              m Bool -> m (Maybe Type) -> m (Maybe Type) -> m (Maybe Type)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM (QName -> m Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    eligibleForProjectionLike QName
    d) m (Maybe Type)
    failNotElig (m (Maybe Type) -> m (Maybe Type))
    -> m (Maybe Type) -> m (Maybe Type)
    forall a b. (a -> b) -> a -> b
    $ {- else -} do
                -- now we know it is reduced, we can safely take the parameters
                let pars :: Args
    pars = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims (Elims -> Maybe Args) -> Elims -> Maybe Args
    forall a b. (a -> b) -> a -> b
    $ Int -> Elims -> Elims
    forall a. Int -> [a] -> [a]
    take Int
    npars Elims
    es
                ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.deftype" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
                  [ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "head d     = " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow QName
    d
                  , TCMT IO Doc
    "parameters =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep ((Arg Term -> TCMT IO Doc) -> Args -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Args
    pars)
                  ]
                ArgName -> Int -> ArgName -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> ArgName -> m ()
    reportSLn ArgName
    "tc.deftype" Int
    60 (ArgName -> m ()) -> ArgName -> m ()
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "parameters = " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ Args -> ArgName
    forall a. Show a => a -> ArgName
    show Args
    pars
                if Args -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    pars Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    npars then ArgName -> m (Maybe Type)
    failure ArgName
    "does not supply enough parameters"
                else Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> m Type -> m (Maybe Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type
    a Type -> Args -> m Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    Type -> a -> m Type
    `piApplyM` Args
    pars
            Term
    _ -> m (Maybe Type)
    failNotDef
      where
        failNotElig :: m (Maybe Type)
    failNotElig = ArgName -> m (Maybe Type)
    failure ArgName
    "is not eligible for projection-likeness"
        failNotDef :: m (Maybe Type)
    failNotDef  = ArgName -> m (Maybe Type)
    failure ArgName
    "is not a Def."
        failure :: ArgName -> m (Maybe Type)
    failure ArgName
    reason = do
          ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.deftype" Int
    25 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "Def. " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    " is projection(like)"
            , TCMT IO Doc
    "but the type "
            , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
            , ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "of its argument " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    reason
            ]
          Maybe Type -> m (Maybe Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Type
    forall a. Maybe a
    Nothing

    -- | The analogue of 'piApply'.  If @v@ is a value of record type @t@
    --   with field @f@, then @projectTyped v t f@ returns the type of @f v@.
    --   And also the record type (as first result).
    --
    --   Works also for projection-like definitions @f@.
    --   In this case, the first result is not a record type.
    --
    --   Precondition: @t@ is reduced.
    --
    projectTyped
      :: PureTCM m
      => Term        -- ^ Head (record value).
      -> Type        -- ^ Its type.
      -> ProjOrigin
      -> QName       -- ^ Projection.
      -> m (Maybe (Dom Type, Term, Type))
    projectTyped :: forall (m :: * -> *).
    PureTCM m =>
    Term
    -> Type
    -> ProjOrigin
    -> QName
    -> m (Maybe (Dom' Term Type, Term, Type))
    projectTyped Term
    v Type
    t ProjOrigin
    o QName
    f = m (Maybe Type)
    -> m (Maybe (Dom' Term Type, Term, Type))
    -> (Type -> m (Maybe (Dom' Term Type, Term, Type)))
    -> m (Maybe (Dom' Term Type, Term, Type))
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> Type -> m (Maybe Type)
    forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
    getDefType QName
    f Type
    t) (Maybe (Dom' Term Type, Term, Type)
    -> m (Maybe (Dom' Term Type, Term, Type))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Dom' Term Type, Term, Type)
    forall a. Maybe a
    Nothing) ((Type -> m (Maybe (Dom' Term Type, Term, Type)))
     -> m (Maybe (Dom' Term Type, Term, Type)))
    -> (Type -> m (Maybe (Dom' Term Type, Term, Type)))
    -> m (Maybe (Dom' Term Type, Term, Type))
    forall a b. (a -> b) -> a -> b
    $ \ Type
    tf -> do
      Type
    -> (Type -> m (Maybe (Dom' Term Type, Term, Type)))
    -> (Dom' Term Type
        -> Abs Type -> m (Maybe (Dom' Term Type, Term, Type)))
    -> m (Maybe (Dom' Term Type, Term, Type))
    forall (m :: * -> *) a.
    MonadReduce m =>
    Type -> (Type -> m a) -> (Dom' Term Type -> Abs Type -> m a) -> m a
    ifNotPiType Type
    tf (m (Maybe (Dom' Term Type, Term, Type))
    -> Type -> m (Maybe (Dom' Term Type, Term, Type))
    forall a b. a -> b -> a
    const (m (Maybe (Dom' Term Type, Term, Type))
     -> Type -> m (Maybe (Dom' Term Type, Term, Type)))
    -> m (Maybe (Dom' Term Type, Term, Type))
    -> Type
    -> m (Maybe (Dom' Term Type, Term, Type))
    forall a b. (a -> b) -> a -> b
    $ Maybe (Dom' Term Type, Term, Type)
    -> m (Maybe (Dom' Term Type, Term, Type))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Dom' Term Type, Term, Type)
    forall a. Maybe a
    Nothing) {- else -} ((Dom' Term Type
      -> Abs Type -> m (Maybe (Dom' Term Type, Term, Type)))
     -> m (Maybe (Dom' Term Type, Term, Type)))
    -> (Dom' Term Type
        -> Abs Type -> m (Maybe (Dom' Term Type, Term, Type)))
    -> m (Maybe (Dom' Term Type, Term, Type))
    forall a b. (a -> b) -> a -> b
    $ \ Dom' Term Type
    dom Abs Type
    b -> do
      Term
    u <- ProjOrigin -> QName -> Arg Term -> m Term
    forall (m :: * -> *).
    HasConstInfo m =>
    ProjOrigin -> QName -> Arg Term -> m Term
    applyDef ProjOrigin
    o QName
    f (Dom' Term Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom' Term Type
    dom Arg Type -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Term
    v)
      Maybe (Dom' Term Type, Term, Type)
    -> m (Maybe (Dom' Term Type, Term, Type))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Dom' Term Type, Term, Type)
     -> m (Maybe (Dom' Term Type, Term, Type)))
    -> Maybe (Dom' Term Type, Term, Type)
    -> m (Maybe (Dom' Term Type, Term, Type))
    forall a b. (a -> b) -> a -> b
    $ (Dom' Term Type, Term, Type) -> Maybe (Dom' Term Type, Term, Type)
    forall a. a -> Maybe a
    Just (Dom' Term Type
    dom, Term
    u, Abs Type
    b Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    v)

    -- | Typing of an elimination.

    data ElimType
      = ArgT (Dom Type)           -- ^ Type of the argument.
      | ProjT
        { ElimType -> Dom' Term Type
    projTRec   :: Dom Type  -- ^ The type of the record which is eliminated.
        , ElimType -> Type
    projTField :: Type      -- ^ The type of the field.
        }

    instance PrettyTCM ElimType where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => ElimType -> m Doc
    prettyTCM (ArgT Dom' Term Type
    a)    = Dom' Term Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Dom' Term Type
    a
      prettyTCM (ProjT Dom' Term Type
    a Type
    b) =
        m Doc
    "." m Doc -> m Doc -> m Doc
    forall a. Semigroup a => a -> a -> a
    TCM.<> m Doc -> m Doc
    forall (m :: * -> *). Functor m => m Doc -> m Doc
    parens (Dom' Term Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Dom' Term Type
    a m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> m Doc
    "->" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    b)

    -- | Given a head and its type, compute the types of the eliminations.

    typeElims :: Type -> Term -> Elims -> TCM [ElimType]
    typeElims :: Type -> Term -> Elims -> TCM [ElimType]
    typeElims Type
    a Term
    _ [] = [ElimType] -> TCM [ElimType]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
    typeElims Type
    a Term
    self (Elim' Term
    e : Elims
    es) = do
      case Elim' Term
    e of
        -- Andrea 02/08/2017: when going from patterns to elims we
        -- generate an Apply elim even for Path types, because we use VarP
        -- for both, so we have to allow for a Path type here.
        Apply Arg Term
    v -> Type
    -> (Type -> TCM [ElimType])
    -> (Dom' Term Type -> Abs Type -> TCM [ElimType])
    -> TCM [ElimType]
    forall (tcm :: * -> *) a.
    (MonadReduce tcm, HasBuiltins tcm) =>
    Type
    -> (Type -> tcm a)
    -> (Dom' Term Type -> Abs Type -> tcm a)
    -> tcm a
    ifNotPiOrPathType Type
    a Type -> TCM [ElimType]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ {- else -} ((Dom' Term Type -> Abs Type -> TCM [ElimType]) -> TCM [ElimType])
    -> (Dom' Term Type -> Abs Type -> TCM [ElimType]) -> TCM [ElimType]
    forall a b. (a -> b) -> a -> b
    $ \ Dom' Term Type
    a Abs Type
    b -> do
          (Dom' Term Type -> ElimType
    ArgT Dom' Term Type
    a ElimType -> [ElimType] -> [ElimType]
    forall a. a -> [a] -> [a]
    :) ([ElimType] -> [ElimType]) -> TCM [ElimType] -> TCM [ElimType]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Term -> Elims -> TCM [ElimType]
    typeElims (Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp Abs Type
    b (SubstArg Type -> Type) -> SubstArg Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    v) (Term
    self Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [Elim' Term
    e]) Elims
    es
        Proj ProjOrigin
    o QName
    f -> do
          Type
    a <- Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    a
          (Dom' Term Type
    dom, Term
    self, Type
    a) <- (Dom' Term Type, Term, Type)
    -> Maybe (Dom' Term Type, Term, Type)
    -> (Dom' Term Type, Term, Type)
    forall a. a -> Maybe a -> a
    fromMaybe (Dom' Term Type, Term, Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (Dom' Term Type, Term, Type)
     -> (Dom' Term Type, Term, Type))
    -> TCMT IO (Maybe (Dom' Term Type, Term, Type))
    -> TCMT IO (Dom' Term Type, Term, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term
    -> Type
    -> ProjOrigin
    -> QName
    -> TCMT IO (Maybe (Dom' Term Type, Term, Type))
    forall (m :: * -> *).
    PureTCM m =>
    Term
    -> Type
    -> ProjOrigin
    -> QName
    -> m (Maybe (Dom' Term Type, Term, Type))
    projectTyped Term
    self Type
    a ProjOrigin
    o QName
    f
          (Dom' Term Type -> Type -> ElimType
    ProjT Dom' Term Type
    dom Type
    a ElimType -> [ElimType] -> [ElimType]
    forall a. a -> [a] -> [a]
    :) ([ElimType] -> [ElimType]) -> TCM [ElimType] -> TCM [ElimType]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> Term -> Elims -> TCM [ElimType]
    typeElims Type
    a Term
    self Elims
    es
        IApply{} -> TCM [ElimType]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Check if a name refers to an eta expandable record.
    {-# SPECIALIZE isEtaRecord :: QName -> TCM Bool #-}
    {-# SPECIALIZE isEtaRecord :: QName -> ReduceM Bool #-}
    isEtaRecord :: HasConstInfo m => QName -> m Bool
    isEtaRecord :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isEtaRecord QName
    r = Bool -> (Defn -> Bool) -> Maybe Defn -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False ((HasEta' PatternOrCopattern
    forall a. HasEta' a
    YesEta HasEta' PatternOrCopattern -> HasEta' PatternOrCopattern -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (HasEta' PatternOrCopattern -> Bool)
    -> (Defn -> HasEta' PatternOrCopattern) -> Defn -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Defn -> HasEta' PatternOrCopattern
    recEtaEquality) (Maybe Defn -> Bool) -> m (Maybe Defn) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe Defn)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    r

    isEtaCon :: HasConstInfo m => QName -> m Bool
    isEtaCon :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isEtaCon QName
    c = QName -> m (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    c m (Either SigError Definition)
    -> (Either SigError Definition -> m Bool) -> m Bool
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Left (SigUnknown ArgName
    err) -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      Left SigError
    SigAbstract -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
      Right Definition
    def -> case Definition -> Defn
    theDef Definition
    def of
        Constructor {conData :: Defn -> QName
    conData = QName
    r} -> QName -> m Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isEtaRecord QName
    r
        Defn
    _ -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    -- | Going under one of these does not count as a decrease in size for the termination checker.
    isEtaOrCoinductiveRecordConstructor :: HasConstInfo m => QName -> m Bool
    isEtaOrCoinductiveRecordConstructor :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isEtaOrCoinductiveRecordConstructor QName
    c =
      m (Maybe (QName, Defn))
    -> m Bool -> ((QName, Defn) -> m Bool) -> m Bool
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> m (Maybe (QName, Defn))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, Defn))
    isRecordConstructor QName
    c) (Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False) (((QName, Defn) -> m Bool) -> m Bool)
    -> ((QName, Defn) -> m Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    _, Defn
    def) -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $
        Defn -> HasEta' PatternOrCopattern
    recEtaEquality Defn
    def HasEta' PatternOrCopattern -> HasEta' PatternOrCopattern -> Bool
    forall a. Eq a => a -> a -> Bool
    == HasEta' PatternOrCopattern
    forall a. HasEta' a
    YesEta Bool -> Bool -> Bool
    || Defn -> Maybe Induction
    recInduction Defn
    def Maybe Induction -> Maybe Induction -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Induction -> Maybe Induction
    forall a. a -> Maybe a
    Just Induction
    Inductive
          -- If in doubt about coinductivity, then yes.

    -- | Check if a name refers to a record which is not coinductive.  (Projections are then size-preserving)
    isInductiveRecord :: QName -> TCM Bool
    isInductiveRecord :: QName -> TCM Bool
    isInductiveRecord QName
    r = Bool -> (Defn -> Bool) -> Maybe Defn -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False ((Induction -> Maybe Induction
    forall a. a -> Maybe a
    Just Induction
    CoInductive Maybe Induction -> Maybe Induction -> Bool
    forall a. Eq a => a -> a -> Bool
    /=) (Maybe Induction -> Bool)
    -> (Defn -> Maybe Induction) -> Defn -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Defn -> Maybe Induction
    recInduction) (Maybe Defn -> Bool) -> TCMT IO (Maybe Defn) -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO (Maybe Defn)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    r

    -- | Check if a type is an eta expandable record and return the record identifier and the parameters.
    isEtaRecordType :: (HasConstInfo m)
                    => Type -> m (Maybe (QName, Args))
    isEtaRecordType :: forall (m :: * -> *).
    HasConstInfo m =>
    Type -> m (Maybe (QName, Args))
    isEtaRecordType Type
    a = case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    a of
      Def QName
    d Elims
    es -> do
        let vs :: Args
    vs = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
        m Bool
    -> m (Maybe (QName, Args))
    -> m (Maybe (QName, Args))
    -> m (Maybe (QName, Args))
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (QName -> m Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isEtaRecord QName
    d) (Maybe (QName, Args) -> m (Maybe (QName, Args))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (QName, Args) -> m (Maybe (QName, Args)))
    -> Maybe (QName, Args) -> m (Maybe (QName, Args))
    forall a b. (a -> b) -> a -> b
    $ (QName, Args) -> Maybe (QName, Args)
    forall a. a -> Maybe a
    Just (QName
    d, Args
    vs)) (Maybe (QName, Args) -> m (Maybe (QName, Args))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Args)
    forall a. Maybe a
    Nothing)
      Term
    _        -> Maybe (QName, Args) -> m (Maybe (QName, Args))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Args)
    forall a. Maybe a
    Nothing

    -- | Check if a name refers to a record constructor.
    --   If yes, return record definition.
    isRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, Defn))
    isRecordConstructor :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, Defn))
    isRecordConstructor QName
    c = QName -> m (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    c m (Either SigError Definition)
    -> (Either SigError Definition -> m (Maybe (QName, Defn)))
    -> m (Maybe (QName, Defn))
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Left (SigUnknown ArgName
    err)        -> m (Maybe (QName, Defn))
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      Left SigError
    SigAbstract             -> Maybe (QName, Defn) -> m (Maybe (QName, Defn))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Defn)
    forall a. Maybe a
    Nothing
      Right Definition
    def -> case Definition -> Defn
    theDef (Definition -> Defn) -> Definition -> Defn
    forall a b. (a -> b) -> a -> b
    $ Definition
    def of
        Constructor{ conData :: Defn -> QName
    conData = QName
    r } -> (Defn -> (QName, Defn)) -> Maybe Defn -> Maybe (QName, Defn)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (QName
    r,) (Maybe Defn -> Maybe (QName, Defn))
    -> m (Maybe Defn) -> m (Maybe (QName, Defn))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe Defn)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    r
        Defn
    _                          -> Maybe (QName, Defn) -> m (Maybe (QName, Defn))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Defn)
    forall a. Maybe a
    Nothing

    -- | Check if a constructor name is the internally generated record constructor.
    --
    --   Works also for abstract constructors.
    isGeneratedRecordConstructor :: (MonadTCEnv m, HasConstInfo m)
                                 => QName -> m Bool
    isGeneratedRecordConstructor :: forall (m :: * -> *).
    (MonadTCEnv m, HasConstInfo m) =>
    QName -> m Bool
    isGeneratedRecordConstructor QName
    c = m Bool -> m Bool
    forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
    ignoreAbstractMode (m Bool -> m Bool) -> m Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ do
      m (Maybe (QName, Defn))
    -> m Bool -> ((QName, Defn) -> m Bool) -> m Bool
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> m (Maybe (QName, Defn))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, Defn))
    isRecordConstructor QName
    c) (Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False) (((QName, Defn) -> m Bool) -> m Bool)
    -> ((QName, Defn) -> m Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    _, Defn
    def) ->
        case Defn
    def of
          Record{ recNamedCon :: Defn -> Bool
    recNamedCon = Bool
    False } -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
          Defn
    _ -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    -- | Turn off eta for unguarded recursive records.
    --   Projections do not preserve guardedness.
    unguardedRecord :: QName -> PatternOrCopattern -> TCM ()
    unguardedRecord :: QName -> PatternOrCopattern -> TCMT IO ()
    unguardedRecord QName
    q PatternOrCopattern
    pat = (Signature -> Signature) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCMT IO ())
    -> (Signature -> Signature) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Defn -> Defn) -> Definition -> Definition
    updateTheDef ((Defn -> Defn) -> Definition -> Definition)
    -> (Defn -> Defn) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ \case
      r :: Defn
    r@Record{} -> Defn
    r { recEtaEquality' :: EtaEquality
    recEtaEquality' = EtaEquality -> HasEta' PatternOrCopattern -> EtaEquality
    setEtaEquality (Defn -> EtaEquality
    recEtaEquality' Defn
    r) (HasEta' PatternOrCopattern -> EtaEquality)
    -> HasEta' PatternOrCopattern -> EtaEquality
    forall a b. (a -> b) -> a -> b
    $ PatternOrCopattern -> HasEta' PatternOrCopattern
    forall a. a -> HasEta' a
    NoEta PatternOrCopattern
    pat }
      Defn
    _ -> Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Turn on eta for inductive guarded recursive records.
    --   Projections do not preserve guardedness.
    recursiveRecord :: QName -> TCM ()
    recursiveRecord :: QName -> TCMT IO ()
    recursiveRecord QName
    q = do
      Bool
    ok <- TCM Bool
    forall (m :: * -> *). HasOptions m => m Bool
    etaEnabled
      (Signature -> Signature) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCMT IO ())
    -> (Signature -> Signature) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Defn -> Defn) -> Definition -> Definition
    updateTheDef ((Defn -> Defn) -> Definition -> Definition)
    -> (Defn -> Defn) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ \case
        r :: Defn
    r@Record{ recInduction :: Defn -> Maybe Induction
    recInduction = Maybe Induction
    ind, recEtaEquality' :: Defn -> EtaEquality
    recEtaEquality' = EtaEquality
    eta } ->
          Defn
    r { recEtaEquality' :: EtaEquality
    recEtaEquality' = EtaEquality
    eta' }
          where
          eta' :: EtaEquality
    eta' | Bool
    ok, Inferred NoEta{} <- EtaEquality
    eta, Maybe Induction
    ind Maybe Induction -> Maybe Induction -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Induction -> Maybe Induction
    forall a. a -> Maybe a
    Just Induction
    CoInductive = HasEta' PatternOrCopattern -> EtaEquality
    Inferred HasEta' PatternOrCopattern
    forall a. HasEta' a
    YesEta
               | Bool
    otherwise = EtaEquality
    eta
        Defn
    _ -> Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Turn on eta for non-recursive record, unless user declared otherwise.
    nonRecursiveRecord :: QName -> TCM ()
    nonRecursiveRecord :: QName -> TCMT IO ()
    nonRecursiveRecord QName
    q = TCM Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM TCM Bool
    forall (m :: * -> *). HasOptions m => m Bool
    etaEnabled (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
      -- Do nothing if eta is disabled by option.
      (Signature -> Signature) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCMT IO ())
    -> (Signature -> Signature) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    q ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Defn -> Defn) -> Definition -> Definition
    updateTheDef ((Defn -> Defn) -> Definition -> Definition)
    -> (Defn -> Defn) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ \case
        r :: Defn
    r@Record{ recInduction :: Defn -> Maybe Induction
    recInduction = Maybe Induction
    ind, recEtaEquality' :: Defn -> EtaEquality
    recEtaEquality' = Inferred (NoEta PatternOrCopattern
    _) }
          | Maybe Induction
    ind Maybe Induction -> Maybe Induction -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Induction -> Maybe Induction
    forall a. a -> Maybe a
    Just Induction
    CoInductive ->
          Defn
    r { recEtaEquality' :: EtaEquality
    recEtaEquality' = HasEta' PatternOrCopattern -> EtaEquality
    Inferred HasEta' PatternOrCopattern
    forall a. HasEta' a
    YesEta }
        r :: Defn
    r@Record{} -> Defn
    r
        Defn
    _          -> Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Check whether record type is marked as recursive.
    --
    --   Precondition: record type identifier exists in signature.
    isRecursiveRecord :: QName -> TCM Bool
    isRecursiveRecord :: QName -> TCM Bool
    isRecursiveRecord QName
    q = Defn -> Bool
    recRecursive (Defn -> Bool) -> (Signature -> Defn) -> Signature -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> Defn)
    -> (Signature -> Definition) -> Signature -> Defn
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Maybe Definition -> Definition
    forall a. a -> Maybe a -> a
    fromMaybe Definition
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Definition -> Definition)
    -> (Signature -> Maybe Definition) -> Signature -> Definition
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Signature -> Maybe Definition
    lookupDefinition QName
    q (Signature -> Bool) -> TCMT IO Signature -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Signature
    forall (m :: * -> *). ReadTCState m => m Signature
    getSignature

    {- | @etaExpandBoundVar i = (Δ, σ, τ)@

    Precondition: The current context is @Γ = Γ₁, x:R pars, Γ₂@ where
      @|Γ₂| = i@ and @R@ is a eta-expandable record type
      with constructor @c@ and fields @Γ'@.

    Postcondition: @Δ = Γ₁, Γ', Γ₂[c Γ']@ and @Γ ⊢ σ : Δ@ and @Δ ⊢ τ : Γ@.
    -}
    etaExpandBoundVar :: Int -> TCM (Maybe (Telescope, Substitution, Substitution))
    etaExpandBoundVar :: Int -> TCM (Maybe (Telescope, Substitution, Substitution))
    etaExpandBoundVar Int
    i = ((Telescope, Substitution, Substitution, Telescope)
     -> (Telescope, Substitution, Substitution))
    -> Maybe (Telescope, Substitution, Substitution, Telescope)
    -> Maybe (Telescope, Substitution, Substitution)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\ (Telescope
    delta, Substitution
    sigma, Substitution
    tau, Telescope
    _) -> (Telescope
    delta, Substitution
    sigma, Substitution
    tau)) (Maybe (Telescope, Substitution, Substitution, Telescope)
     -> Maybe (Telescope, Substitution, Substitution))
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    -> TCM (Maybe (Telescope, Substitution, Substitution))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
      Int
    -> Telescope
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    expandRecordVar Int
    i (Telescope
     -> TCMT
          IO (Maybe (Telescope, Substitution, Substitution, Telescope)))
    -> TCM Telescope
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCM Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope

    -- | @expandRecordVar i Γ = (Δ, σ, τ, Γ')@
    --
    --   Precondition: @Γ = Γ₁, x:R pars, Γ₂@ where
    --     @|Γ₂| = i@ and @R@ is a eta-expandable record type
    --     with constructor @c@ and fields @Γ'@.
    --
    --   Postcondition: @Δ = Γ₁, Γ', Γ₂[c Γ']@ and @Γ ⊢ σ : Δ@ and @Δ ⊢ τ : Γ@.

    expandRecordVar :: Int -> Telescope -> TCM (Maybe (Telescope, Substitution, Substitution, Telescope))
    expandRecordVar :: Int
    -> Telescope
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    expandRecordVar Int
    i Telescope
    gamma0 = do
      -- Get the context with last variable added last in list.
      let gamma :: [Dom (ArgName, Type)]
    gamma = Telescope -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    gamma0
      -- Convert the de Bruijn index i to a de Bruijn level
          l :: Int
    l     = [Dom (ArgName, Type)] -> Int
    forall a. Sized a => a -> Int
    size [Dom (ArgName, Type)]
    gamma Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i
      -- Extract type of @i@th de Bruijn index.
      -- Γ = Γ₁, x:a, Γ₂
      let ([Dom (ArgName, Type)]
    gamma1, dom :: Dom (ArgName, Type)
    dom@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    ai, unDom :: forall t e. Dom' t e -> e
    unDom = (ArgName
    x, Type
    a)}) : [Dom (ArgName, Type)]
    gamma2) = Int
    -> [Dom (ArgName, Type)]
    -> ([Dom (ArgName, Type)], [Dom (ArgName, Type)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    l [Dom (ArgName, Type)]
    gamma -- TODO:: Defined but not used dom, ai
      -- This must be a eta-expandable record type.
      let failure :: TCMT IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    failure = do
            ArgName -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.meta.assign.proj" Int
    25 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
              TCMT IO Doc
    "failed to eta-expand variable " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty ArgName
    x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
              TCMT IO Doc
    " since its type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    a TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+>
              TCMT IO Doc
    " is not a record type"
            Maybe (Telescope, Substitution, Substitution, Telescope)
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Telescope, Substitution, Substitution, Telescope)
    forall a. Maybe a
    Nothing
      TCMT IO (Maybe (QName, Args, Defn))
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    -> ((QName, Args, Defn)
        -> TCMT
             IO (Maybe (Telescope, Substitution, Substitution, Telescope)))
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Type -> TCMT IO (Maybe (QName, Args, Defn))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (QName, Args, Defn))
    isRecordType Type
    a) TCMT IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    failure (((QName, Args, Defn)
      -> TCMT
           IO (Maybe (Telescope, Substitution, Substitution, Telescope)))
     -> TCMT
          IO (Maybe (Telescope, Substitution, Substitution, Telescope)))
    -> ((QName, Args, Defn)
        -> TCMT
             IO (Maybe (Telescope, Substitution, Substitution, Telescope)))
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    r, Args
    pars, Defn
    def) -> case Defn -> HasEta' PatternOrCopattern
    recEtaEquality Defn
    def of
        NoEta{} -> Maybe (Telescope, Substitution, Substitution, Telescope)
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Telescope, Substitution, Substitution, Telescope)
    forall a. Maybe a
    Nothing
        HasEta' PatternOrCopattern
    YesEta  -> (Telescope, Substitution, Substitution, Telescope)
    -> Maybe (Telescope, Substitution, Substitution, Telescope)
    forall a. a -> Maybe a
    Just ((Telescope, Substitution, Substitution, Telescope)
     -> Maybe (Telescope, Substitution, Substitution, Telescope))
    -> TCMT IO (Telescope, Substitution, Substitution, Telescope)
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
          -- Get the record fields @Γ₁ ⊢ tel@ (@tel = Γ'@).
          -- TODO: compose argInfo ai with tel.
          let tel :: Telescope
    tel = Defn -> Telescope
    recTel Defn
    def Telescope -> Args -> Telescope
    forall t. Apply t => t -> Args -> t
    `apply` Args
    pars
              m :: Int
    m   = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel
              fs :: [Arg QName]
    fs  = (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term QName -> Arg QName
    forall t a. Dom' t a -> Arg a
    argFromDom ([Dom' Term QName] -> [Arg QName])
    -> [Dom' Term QName] -> [Arg QName]
    forall a b. (a -> b) -> a -> b
    $ Defn -> [Dom' Term QName]
    recFields Defn
    def
          -- Construct the record pattern @Γ₁, Γ' ⊢ u := c ys@.
              ys :: Args
    ys  = (Arg QName -> Int -> Arg Term) -> [Arg QName] -> [Int] -> Args
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Arg QName
    f Int
    i -> Arg QName
    f Arg QName -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Int -> Term
    var Int
    i) [Arg QName]
    fs ([Int] -> Args) -> [Int] -> Args
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    m
              u :: Term
    u   = ConHead -> ConInfo -> Args -> Term
    mkCon (Defn -> ConHead
    recConHead Defn
    def) ConInfo
    ConOSystem Args
    ys
          -- @Γ₁, Γ' ⊢ τ₀ : Γ₁, x:_@
              tau0 :: Substitution
    tau0 = Term -> Substitution -> Substitution
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS Term
    u (Substitution -> Substitution) -> Substitution -> Substitution
    forall a b. (a -> b) -> a -> b
    $ Int -> Substitution
    forall a. Int -> Substitution' a
    raiseS Int
    m
          -- @Γ₁, Γ', Γ₂ ⊢ τ₀ : Γ₁, x:_, Γ₂@
              tau :: Substitution
    tau  = Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS ([Dom (ArgName, Type)] -> Int
    forall a. Sized a => a -> Int
    size [Dom (ArgName, Type)]
    gamma2) Substitution
    tau0

          --  Fields are in order first-first.
              zs :: Args
    zs  = [Arg QName] -> (Arg QName -> Arg Term) -> Args
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [Arg QName]
    fs ((Arg QName -> Arg Term) -> Args)
    -> (Arg QName -> Arg Term) -> Args
    forall a b. (a -> b) -> a -> b
    $ (QName -> Term) -> Arg QName -> Arg Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((QName -> Term) -> Arg QName -> Arg Term)
    -> (QName -> Term) -> Arg QName -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ \ QName
    f -> Int -> Elims -> Term
    Var Int
    0 [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    f]
          --  We need to reverse the field sequence to build the substitution.
          -- @Γ₁, x:_ ⊢ σ₀ : Γ₁, Γ'@
              sigma0 :: Substitution
    sigma0 = [Term] -> [Term]
    forall a. [a] -> [a]
    reverse ((Arg Term -> Term) -> Args -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg Args
    zs) [Term] -> Substitution -> Substitution
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# Int -> Substitution
    forall a. Int -> Substitution' a
    raiseS Int
    1
          -- @Γ₁, x:_, Γ₂ ⊢ σ₀ : Γ₁, Γ', Γ₂@
              sigma :: Substitution
    sigma  = Int -> Substitution -> Substitution
    forall a. Int -> Substitution' a -> Substitution' a
    liftS ([Dom (ArgName, Type)] -> Int
    forall a. Sized a => a -> Int
    size [Dom (ArgName, Type)]
    gamma2) Substitution
    sigma0

          -- Construct @Δ@ as telescope.
          -- Note @Γ₁, x:_ ⊢ Γ₂@, thus, @Γ₁, Γ' ⊢ [τ₀]Γ₂@

              -- Use "f(x)" as variable name for the projection f(x).
              s :: ArgName
    s     = ArgName -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow ArgName
    x
              tel' :: Telescope
    tel'  = (ArgName -> ArgName) -> Telescope -> Telescope
    forall a. (ArgName -> ArgName) -> Tele a -> Tele a
    mapAbsNames (\ ArgName
    f -> ArgName -> ArgName
    stringToArgName (ArgName -> ArgName) -> ArgName -> ArgName
    forall a b. (a -> b) -> a -> b
    $ ArgName -> ArgName
    argNameToString ArgName
    f ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    "(" ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    s ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    ")") Telescope
    tel
              delta :: Telescope
    delta = [Dom (ArgName, Type)] -> Telescope
    telFromList ([Dom (ArgName, Type)] -> Telescope)
    -> [Dom (ArgName, Type)] -> Telescope
    forall a b. (a -> b) -> a -> b
    $ [Dom (ArgName, Type)]
    gamma1 [Dom (ArgName, Type)]
    -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
    forall a. [a] -> [a] -> [a]
    ++ Telescope -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    tel' [Dom (ArgName, Type)]
    -> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
    forall a. [a] -> [a] -> [a]
    ++
                        Telescope -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList (Substitution' (SubstArg Telescope) -> Telescope -> Telescope
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Telescope)
    tau0 (Telescope -> Telescope) -> Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ [Dom (ArgName, Type)] -> Telescope
    telFromList [Dom (ArgName, Type)]
    gamma2)
                        -- Andreas, 2017-07-29, issue #2644
                        -- We cannot substitute directly into a ListTel like gamma2,
                        -- we have to convert it to a telescope first, otherwise we get garbage.

          (Telescope, Substitution, Substitution, Telescope)
    -> TCMT IO (Telescope, Substitution, Substitution, Telescope)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope
    delta, Substitution
    sigma, Substitution
    tau, Telescope
    tel)

    -- | Precondition: variable list is ordered descendingly.  Can be empty.
    expandRecordVarsRecursively :: [Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
    expandRecordVarsRecursively :: [Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
    expandRecordVarsRecursively [] Telescope
    gamma = (Telescope, Substitution, Substitution)
    -> TCM (Telescope, Substitution, Substitution)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope
    gamma, Substitution
    forall a. Substitution' a
    idS, Substitution
    forall a. Substitution' a
    idS)
    expandRecordVarsRecursively (Int
    i : [Int]
    is) Telescope
    gamma = do
      TCMT IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    -> TCM (Telescope, Substitution, Substitution)
    -> ((Telescope, Substitution, Substitution, Telescope)
        -> TCM (Telescope, Substitution, Substitution))
    -> TCM (Telescope, Substitution, Substitution)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Int
    -> Telescope
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    expandRecordVar Int
    i Telescope
    gamma) ([Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
    expandRecordVarsRecursively [Int]
    is Telescope
    gamma)
      (((Telescope, Substitution, Substitution, Telescope)
      -> TCM (Telescope, Substitution, Substitution))
     -> TCM (Telescope, Substitution, Substitution))
    -> ((Telescope, Substitution, Substitution, Telescope)
        -> TCM (Telescope, Substitution, Substitution))
    -> TCM (Telescope, Substitution, Substitution)
    forall a b. (a -> b) -> a -> b
    $ \ (Telescope
    gamma1, Substitution
    sigma1, Substitution
    tau1, Telescope
    tel) -> do
        -- Γ ⊢ σ₁ : Γ₁  and  Γ₁ ⊢ τ₁ : Γ
        let n :: Int
    n = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel
            newis :: [Int]
    newis = Int -> [Int] -> [Int]
    forall a. Int -> [a] -> [a]
    take Int
    n ([Int] -> [Int]) -> [Int] -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n
        (Telescope
    gamma2, Substitution
    sigma2, Substitution
    tau2) <- [Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
    expandRecordVarsRecursively ([Int]
    newis [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++ [Int]
    is) Telescope
    gamma1
        -- Γ₁ ⊢ σ₂ : Γ₂  and  Γ₂ ⊢ τ₂ : Γ₁
        (Telescope, Substitution, Substitution)
    -> TCM (Telescope, Substitution, Substitution)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope
    gamma2, Substitution' (SubstArg Substitution)
    -> Substitution -> Substitution
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Substitution)
    sigma1 Substitution
    sigma2, Substitution' (SubstArg Substitution)
    -> Substitution -> Substitution
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Substitution)
    tau2 Substitution
    tau1)

    -- | @curryAt v (Γ (y : R pars) -> B) n =
    --     ( \ v -> λ Γ ys → v Γ (c ys)            {- curry   -}
    --     , \ v -> λ Γ y → v Γ (p1 y) ... (pm y)  {- uncurry -}
    --     , Γ (ys : As) → B[c ys / y]
    --     )@
    --
    --   where @n = size Γ@.
    curryAt :: Type -> Int -> TCM (Term -> Term, Term -> Term, Type)
    curryAt :: Type -> Int -> TCM (Term -> Term, Term -> Term, Type)
    curryAt Type
    t Int
    n = do
      -- first, strip the leading n domains (which remain unchanged)
      TelV Telescope
    gamma Type
    core <- Int -> Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> Type -> m (TelV Type)
    telViewUpTo Int
    n Type
    t
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    core of
        -- There should be at least one domain left
        Pi (dom :: Dom' Term Type
    dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    ai, unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a}) Abs Type
    b -> do
          -- Eta-expand @dom@ along @qs@ into a telescope @tel@, computing a substitution.
          -- For now, we only eta-expand once.
          -- This might trigger another call to @etaExpandProjectedVar@ later.
          -- A more efficient version does all the eta-expansions at once here.
          (QName
    r, Args
    pars, Defn
    def) <- (QName, Args, Defn)
    -> Maybe (QName, Args, Defn) -> (QName, Args, Defn)
    forall a. a -> Maybe a -> a
    fromMaybe (QName, Args, Defn)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (QName, Args, Defn) -> (QName, Args, Defn))
    -> TCMT IO (Maybe (QName, Args, Defn))
    -> TCMT IO (QName, Args, Defn)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCMT IO (Maybe (QName, Args, Defn))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (QName, Args, Defn))
    isRecordType Type
    a
          if | NoEta PatternOrCopattern
    _ <- Defn -> HasEta' PatternOrCopattern
    recEtaEquality Defn
    def -> TCMT IO ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
             | Bool
    otherwise -> () -> TCMT IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          -- TODO: compose argInfo ai with tel.
          let tel :: Telescope
    tel = Defn -> Telescope
    recTel Defn
    def Telescope -> Args -> Telescope
    forall t. Apply t => t -> Args -> t
    `apply` Args
    pars
              m :: Int
    m   = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel
              fs :: [Arg QName]
    fs  = (Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term QName -> Arg QName
    forall t a. Dom' t a -> Arg a
    argFromDom ([Dom' Term QName] -> [Arg QName])
    -> [Dom' Term QName] -> [Arg QName]
    forall a b. (a -> b) -> a -> b
    $ Defn -> [Dom' Term QName]
    recFields Defn
    def
              ys :: Args
    ys  = (Arg QName -> Int -> Arg Term) -> [Arg QName] -> [Int] -> Args
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Arg QName
    f Int
    i -> Arg QName
    f Arg QName -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Int -> Term
    var Int
    i) [Arg QName]
    fs ([Int] -> Args) -> [Int] -> Args
    forall a b. (a -> b) -> a -> b
    $ Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    m
              u :: Term
    u   = ConHead -> ConInfo -> Args -> Term
    mkCon (Defn -> ConHead
    recConHead Defn
    def) ConInfo
    ConOSystem Args
    ys
              b' :: Type
    b'  = Int -> Abs Type -> Abs Type
    forall a. Subst a => Int -> a -> a
    raise Int
    m Abs Type
    b Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    u
              t' :: Type
    t'  = Telescope
    gamma Telescope -> Type -> Type
    `telePi` (Telescope
    tel Telescope -> Type -> Type
    `telePi` Type
    b')
              gammai :: [ArgInfo]
    gammai = (Dom (ArgName, Type) -> ArgInfo)
    -> [Dom (ArgName, Type)] -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom (ArgName, Type) -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo ([Dom (ArgName, Type)] -> [ArgInfo])
    -> [Dom (ArgName, Type)] -> [ArgInfo]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    gamma
              xs :: Args
    xs  = Args -> Args
    forall a. [a] -> [a]
    reverse (Args -> Args) -> Args -> Args
    forall a b. (a -> b) -> a -> b
    $ (ArgInfo -> Int -> Arg Term) -> [ArgInfo] -> [Int] -> Args
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ ArgInfo
    ai Int
    i -> ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    i) [ArgInfo]
    gammai [Int
    m..]
              curry :: Term -> Term
    curry Term
    v = Telescope -> Term -> Term
    teleLam Telescope
    gamma (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Term -> Term
    teleLam Telescope
    tel (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $
                          Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    m) Term
    v Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` (Args
    xs Args -> Args -> Args
    forall a. [a] -> [a] -> [a]
    ++ [ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai Term
    u])
              zs :: Args
    zs  = [Arg QName] -> (Arg QName -> Arg Term) -> Args
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for [Arg QName]
    fs ((Arg QName -> Arg Term) -> Args)
    -> (Arg QName -> Arg Term) -> Args
    forall a b. (a -> b) -> a -> b
    $ (QName -> Term) -> Arg QName -> Arg Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((QName -> Term) -> Arg QName -> Arg Term)
    -> (QName -> Term) -> Arg QName -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ \ QName
    f -> Int -> Elims -> Term
    Var Int
    0 [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    f]
              atel :: Telescope
    atel = Dom (ArgName, Type) -> Telescope
    forall a. SgTel a => a -> Telescope
    sgTel (Dom (ArgName, Type) -> Telescope)
    -> Dom (ArgName, Type) -> Telescope
    forall a b. (a -> b) -> a -> b
    $ (,) (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b) (Type -> (ArgName, Type)) -> Dom' Term Type -> Dom (ArgName, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom' Term Type
    dom
              uncurry :: Term -> Term
    uncurry Term
    v = Telescope -> Term -> Term
    teleLam Telescope
    gamma (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Term -> Term
    teleLam Telescope
    atel (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $
                            Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) Term
    v Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` (Args
    xs Args -> Args -> Args
    forall a. [a] -> [a] -> [a]
    ++ Args
    zs)
          (Term -> Term, Term -> Term, Type)
    -> TCM (Term -> Term, Term -> Term, Type)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> Term
    curry, Term -> Term
    uncurry, Type
    t')
        Term
    _ -> TCM (Term -> Term, Term -> Term, Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    {-| @etaExpand r pars u@ computes the eta expansion of record value @u@
        at record type @r pars@.

        The first argument @r@ should be the name of an eta-expandable record type.
        Given

          @record R : Set where field x : A; y : B; .z : C@

        and @r : R@,

          @etaExpand R [] r = (tel, [R.x r, R.y r, R.z r])@

        where @tel@ is the record telescope instantiated at the parameters @pars@.
    -}
    etaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m)
                    => QName -> Args -> Term -> m (Telescope, Args)
    etaExpandRecord :: forall (m :: * -> *).
    (HasConstInfo m, MonadDebug m, ReadTCState m) =>
    QName -> Args -> Term -> m (Telescope, Args)
    etaExpandRecord = Bool -> QName -> Args -> Term -> m (Telescope, Args)
    forall (m :: * -> *).
    (HasConstInfo m, MonadDebug m, ReadTCState m) =>
    Bool -> QName -> Args -> Term -> m (Telescope, Args)
    etaExpandRecord' Bool
    False

    -- | Eta expand a record regardless of whether it's an eta-record or not.
    forceEtaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m, MonadError TCErr m)
                         => QName -> Args -> Term -> m (Telescope, Args)
    forceEtaExpandRecord :: forall (m :: * -> *).
    (HasConstInfo m, MonadDebug m, ReadTCState m,
     MonadError TCErr m) =>
    QName -> Args -> Term -> m (Telescope, Args)
    forceEtaExpandRecord = Bool -> QName -> Args -> Term -> m (Telescope, Args)
    forall (m :: * -> *).
    (HasConstInfo m, MonadDebug m, ReadTCState m) =>
    Bool -> QName -> Args -> Term -> m (Telescope, Args)
    etaExpandRecord' Bool
    True

    etaExpandRecord' :: (HasConstInfo m, MonadDebug m, ReadTCState m)
                     => Bool -> QName -> Args -> Term -> m (Telescope, Args)
    etaExpandRecord' :: forall (m :: * -> *).
    (HasConstInfo m, MonadDebug m, ReadTCState m) =>
    Bool -> QName -> Args -> Term -> m (Telescope, Args)
    etaExpandRecord' Bool
    forceEta QName
    r Args
    pars Term
    u = do
      Defn
    def <- Defn -> Maybe Defn -> Defn
    forall a. a -> Maybe a -> a
    fromMaybe Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Defn -> Defn) -> m (Maybe Defn) -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe Defn)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    r
      (Telescope
    tel, ConHead
    _, ConInfo
    _, Args
    args) <- Bool
    -> QName
    -> Args
    -> Defn
    -> Term
    -> m (Telescope, ConHead, ConInfo, Args)
    forall (m :: * -> *).
    HasConstInfo m =>
    Bool
    -> QName
    -> Args
    -> Defn
    -> Term
    -> m (Telescope, ConHead, ConInfo, Args)
    etaExpandRecord'_ Bool
    forceEta QName
    r Args
    pars Defn
    def Term
    u
      (Telescope, Args) -> m (Telescope, Args)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope
    tel, Args
    args)

    etaExpandRecord_ :: HasConstInfo m
                     => QName -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
    etaExpandRecord_ :: forall (m :: * -> *).
    HasConstInfo m =>
    QName
    -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
    etaExpandRecord_ = Bool
    -> QName
    -> Args
    -> Defn
    -> Term
    -> m (Telescope, ConHead, ConInfo, Args)
    forall (m :: * -> *).
    HasConstInfo m =>
    Bool
    -> QName
    -> Args
    -> Defn
    -> Term
    -> m (Telescope, ConHead, ConInfo, Args)
    etaExpandRecord'_ Bool
    False

    etaExpandRecord'_ :: HasConstInfo m
                      => Bool -> QName -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
    etaExpandRecord'_ :: forall (m :: * -> *).
    HasConstInfo m =>
    Bool
    -> QName
    -> Args
    -> Defn
    -> Term
    -> m (Telescope, ConHead, ConInfo, Args)
    etaExpandRecord'_ Bool
    forceEta QName
    r Args
    pars Defn
    def Term
    u = do
      let Record{ recConHead :: Defn -> ConHead
    recConHead     = ConHead
    con
                , recFields :: Defn -> [Dom' Term QName]
    recFields      = [Dom' Term QName]
    xs
                , recTel :: Defn -> Telescope
    recTel         = Telescope
    tel
                } = Defn
    def
          tel' :: Telescope
    tel' = Telescope -> Args -> Telescope
    forall t. Apply t => t -> Args -> t
    apply Telescope
    tel Args
    pars
      -- Make sure we do not expand non-eta records (unless forced to):
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Defn -> HasEta' PatternOrCopattern
    recEtaEquality Defn
    def HasEta' PatternOrCopattern -> HasEta' PatternOrCopattern -> Bool
    forall a. Eq a => a -> a -> Bool
    == HasEta' PatternOrCopattern
    forall a. HasEta' a
    YesEta Bool -> Bool -> Bool
    || Bool
    forceEta) m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      case Term
    u of

        -- Already expanded.
        Con ConHead
    con_ ConInfo
    ci Elims
    es -> do
          let args :: Args
    args = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
          -- Andreas, 2019-10-21, issue #4148
          -- @con == con_@ might fail, but their normal forms should be equal.
          m (Maybe QName) -> m () -> m ()
    forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
    whenNothingM (ConHead -> QName
    conName ConHead
    con QName -> QName -> m (Maybe QName)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> QName -> m (Maybe QName)
    `sameDef` ConHead -> QName
    conName ConHead
    con_) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
            ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "impossible" Int
    10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
              [ TCMT IO Doc
    "etaExpandRecord_: the following two constructors should be identical"
              , 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
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "con  = " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ConHead -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow ConHead
    con
              , 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
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "con_ = " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ConHead -> ArgName
    forall a. Pretty a => a -> ArgName
    prettyShow ConHead
    con_
              ]
            m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          (Telescope, ConHead, ConInfo, Args)
    -> m (Telescope, ConHead, ConInfo, Args)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope
    tel', ConHead
    con, ConInfo
    ci, Args
    args)

        -- Not yet expanded.
        Term
    _ -> do
          -- Andreas, < 2016-01-18: Note: recFields are always the original projections,
          -- thus, we can use them in Proj directly.
          let xs' :: Args
    xs' = [Arg QName] -> (Arg QName -> Arg Term) -> Args
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for ((Dom' Term QName -> Arg QName) -> [Dom' Term QName] -> [Arg QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term QName -> Arg QName
    forall t a. Dom' t a -> Arg a
    argFromDom [Dom' Term QName]
    xs) ((Arg QName -> Arg Term) -> Args)
    -> (Arg QName -> Arg Term) -> Args
    forall a b. (a -> b) -> a -> b
    $ (QName -> Term) -> Arg QName -> Arg Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((QName -> Term) -> Arg QName -> Arg Term)
    -> (QName -> Term) -> Arg QName -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ \ QName
    x -> Term
    u Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    x]
          ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.record.eta" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "eta expanding" 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
    u 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
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    r
            , 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
    "tel' =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    tel'
              , TCMT IO Doc
    "args =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Args -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Args
    xs'
              ]
            ]
          (Telescope, ConHead, ConInfo, Args)
    -> m (Telescope, ConHead, ConInfo, Args)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope
    tel', ConHead
    con, ConInfo
    ConOSystem, Args
    xs')

    etaExpandAtRecordType :: Type -> Term -> TCM (Telescope, Term)
    etaExpandAtRecordType :: Type -> Term -> TCM (Telescope, Term)
    etaExpandAtRecordType Type
    t Term
    u = do
      (QName
    r, Args
    pars, Defn
    def) <- (QName, Args, Defn)
    -> Maybe (QName, Args, Defn) -> (QName, Args, Defn)
    forall a. a -> Maybe a -> a
    fromMaybe (QName, Args, Defn)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (QName, Args, Defn) -> (QName, Args, Defn))
    -> TCMT IO (Maybe (QName, Args, Defn))
    -> TCMT IO (QName, Args, Defn)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCMT IO (Maybe (QName, Args, Defn))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (QName, Args, Defn))
    isRecordType Type
    t
      (Telescope
    tel, ConHead
    con, ConInfo
    ci, Args
    args) <- QName
    -> Args
    -> Defn
    -> Term
    -> TCMT IO (Telescope, ConHead, ConInfo, Args)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName
    -> Args -> Defn -> Term -> m (Telescope, ConHead, ConInfo, Args)
    etaExpandRecord_ QName
    r Args
    pars Defn
    def Term
    u
      (Telescope, Term) -> TCM (Telescope, Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Telescope
    tel, ConHead -> ConInfo -> Args -> Term
    mkCon ConHead
    con ConInfo
    ci Args
    args)

    -- | The fields should be eta contracted already.
    --
    --   We can eta contract if all fields @f = ...@ are irrelevant
    --   or all fields @f@ are the projection @f v@ of the same value @v@,
    --   but we need at least one relevant field to find the value @v@.
    --
    --   If all fields are erased, we cannot eta-contract.

    --   Andreas, 2019-11-06, issue #4168: eta-contraction all-erased record
    --   lead to compilation error.

    --   TODO: this can be moved out of TCM.
    --   Andreas, 2018-01-28: attempted just that, but Auto does not
    --   put the conFields there (it does not run in TCM).
    --   If we get rid of Auto, we can do this.  (Tests not involving Auto pass.)

    {-# SPECIALIZE etaContractRecord :: QName -> ConHead -> ConInfo -> Args -> TCM Term #-}
    {-# SPECIALIZE etaContractRecord :: QName -> ConHead -> ConInfo -> Args -> ReduceM Term #-}
    etaContractRecord :: HasConstInfo m => QName -> ConHead -> ConInfo -> Args -> m Term
    etaContractRecord :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> ConHead -> ConInfo -> Args -> m Term
    etaContractRecord QName
    r ConHead
    c ConInfo
    ci Args
    args = if (Arg Term -> Bool) -> Args -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Bool -> Bool
    not (Bool -> Bool) -> (Arg Term -> Bool) -> Arg Term -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Bool
    forall a. LensModality a => a -> Bool
    usableModality) Args
    args then m Term
    fallBack else do
      Just Record{ recFields :: Defn -> [Dom' Term QName]
    recFields = [Dom' Term QName]
    xs } <- QName -> m (Maybe Defn)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    r
      ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.record.eta.contract" Int
    20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "eta contracting record"
        , 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
    "record type r  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    r
          , TCMT IO Doc
    "constructor c  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ConHead -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ConHead
    c
          , TCMT IO Doc
    "field names xs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Dom' Term QName] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty    [Dom' Term QName]
    xs
          , TCMT IO Doc
    "fields    args =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Args -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Args
    args
          ]
        ]
      case Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Args -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    args) ([Dom' Term QName] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Dom' Term QName]
    xs) of
        Ordering
    LT -> m Term
    fallBack       -- Not fully applied
        Ordering
    GT -> m Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- Too many arguments. Impossible.
        Ordering
    EQ -> do
          case (Arg Term -> Dom' Term QName -> Maybe (Maybe Term))
    -> Args -> [Dom' Term QName] -> Maybe [Maybe Term]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM Arg Term -> Dom' Term QName -> Maybe (Maybe Term)
    check Args
    args [Dom' Term QName]
    xs of
            Just [Maybe Term]
    as -> case [Maybe Term] -> [Term]
    forall a. [Maybe a] -> [a]
    catMaybes [Maybe Term]
    as of
              (Term
    a:[Term]
    as) ->
                if (Term -> Bool) -> [Term] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Term
    a Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) [Term]
    as
                  then Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return Term
    a
                  else m Term
    fallBack
              [Term]
    _ -> m Term
    fallBack -- just irrelevant terms
            Maybe [Maybe Term]
    _ -> m Term
    fallBack  -- a Nothing
      where
      fallBack :: m Term
    fallBack = Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ConHead -> ConInfo -> Args -> Term
    mkCon ConHead
    c ConInfo
    ci Args
    args)
      check :: Arg Term -> Dom QName -> Maybe (Maybe Term)
      check :: Arg Term -> Dom' Term QName -> Maybe (Maybe Term)
    check Arg Term
    a Dom' Term QName
    ax = do
      -- @a@ is the constructor argument, @ax@ the corr. record field name
        -- skip irrelevant record fields by returning DontCare
        case (Arg Term -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Arg Term
    a, Term -> Maybe (Elims -> Term, Elims)
    hasElims (Term -> Maybe (Elims -> Term, Elims))
    -> Term -> Maybe (Elims -> Term, Elims)
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a) of
          (Relevance
    Irrelevant, Maybe (Elims -> Term, Elims)
    _)   -> Maybe Term -> Maybe (Maybe Term)
    forall a. a -> Maybe a
    Just Maybe Term
    forall a. Maybe a
    Nothing
          -- if @a@ is the record field name applied to a single argument
          -- then it passes the check
          (Relevance
    _, Just (Elims -> Term
    _, [])) -> Maybe (Maybe Term)
    forall a. Maybe a
    Nothing  -- not a projection
          (Relevance
    _, Just (Elims -> Term
    h, Elim' Term
    e0:Elims
    es0))
            | (Elims
    es, Proj ProjOrigin
    _o QName
    f) <- Elim' Term -> Elims -> (Elims, Elim' Term)
    forall a. a -> [a] -> ([a], a)
    initLast1 Elim' Term
    e0 Elims
    es0
            , Dom' Term QName -> QName
    forall t e. Dom' t e -> e
    unDom Dom' Term QName
    ax QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f -> Maybe Term -> Maybe (Maybe Term)
    forall a. a -> Maybe a
    Just (Maybe Term -> Maybe (Maybe Term))
    -> Maybe Term -> Maybe (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Term -> Maybe Term) -> Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Elims -> Term
    h Elims
    es
          (Relevance, Maybe (Elims -> Term, Elims))
    _                 -> Maybe (Maybe Term)
    forall a. Maybe a
    Nothing

    -- | Is the type a hereditarily singleton record type? May return a
    -- blocking metavariable.
    --
    -- Precondition: The name should refer to a record type, and the
    -- arguments should be the parameters to the type.
    isSingletonRecord :: (PureTCM m, MonadBlock m) => QName -> Args -> m Bool
    isSingletonRecord :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    QName -> Args -> m Bool
    isSingletonRecord QName
    r Args
    ps = Maybe Term -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Term -> Bool) -> m (Maybe Term) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Bool -> QName -> Args -> m (Maybe Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> QName -> Args -> m (Maybe Term)
    isSingletonRecord' Bool
    False QName
    r Args
    ps

    isSingletonRecordModuloRelevance :: (PureTCM m, MonadBlock m)
                                     => QName -> Args -> m Bool
    isSingletonRecordModuloRelevance :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    QName -> Args -> m Bool
    isSingletonRecordModuloRelevance QName
    r Args
    ps = Maybe Term -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Term -> Bool) -> m (Maybe Term) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Bool -> QName -> Args -> m (Maybe Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> QName -> Args -> m (Maybe Term)
    isSingletonRecord' Bool
    True QName
    r Args
    ps

    -- | Return the unique (closed) inhabitant if exists.
    --   In case of counting irrelevance in, the returned inhabitant
    --   contains dummy terms.
    isSingletonRecord' :: forall m. (PureTCM m, MonadBlock m)
                       => Bool -> QName -> Args -> m (Maybe Term)
    isSingletonRecord' :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> QName -> Args -> m (Maybe Term)
    isSingletonRecord' Bool
    regardIrrelevance QName
    r Args
    ps = do
      ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.meta.eta" Int
    30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "Is" 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 (QName -> Elims -> Term
    Def QName
    r (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply Args
    ps) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "a singleton record type?"
      QName -> m (Maybe Defn)
    forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
    isRecord QName
    r m (Maybe Defn) -> (Maybe Defn -> m (Maybe Term)) -> m (Maybe Term)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Maybe Defn
    Nothing  -> Maybe Term -> m (Maybe Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Term
    forall a. Maybe a
    Nothing
        Just Defn
    def -> do
          (Args -> Term) -> Maybe Args -> Maybe Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ConHead -> ConInfo -> Args -> Term
    mkCon (Defn -> ConHead
    recConHead Defn
    def) ConInfo
    ConOSystem) (Maybe Args -> Maybe Term) -> m (Maybe Args) -> m (Maybe Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Telescope -> m (Maybe Args)
    check (Defn -> Telescope
    recTel Defn
    def Telescope -> Args -> Telescope
    forall t. Apply t => t -> Args -> t
    `apply` Args
    ps)
      where
      check :: Telescope -> m (Maybe [Arg Term])
      check :: Telescope -> m (Maybe Args)
    check Telescope
    tel = do
        ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.meta.eta" Int
    30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $
          TCMT IO Doc
    "isSingletonRecord' checking telescope " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    tel
        case Telescope
    tel of
          Telescope
    EmptyTel -> Maybe Args -> m (Maybe Args)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Args -> m (Maybe Args)) -> Maybe Args -> m (Maybe Args)
    forall a b. (a -> b) -> a -> b
    $ Args -> Maybe Args
    forall a. a -> Maybe a
    Just []
          ExtendTel Dom' Term Type
    dom Abs Telescope
    tel -> m Bool -> m (Maybe Args) -> m (Maybe Args) -> m (Maybe Args)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    regardIrrelevance m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` Dom' Term Type -> m Bool
    forall a (m :: * -> *).
    (LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
     MonadBlock m) =>
    a -> m Bool
    isIrrelevantOrPropM Dom' Term Type
    dom)
            {-then-}
              (Dom' Term Type
    -> Abs Telescope -> (Telescope -> m (Maybe Args)) -> m (Maybe Args)
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom' Term Type -> Abs a -> (a -> m b) -> m b
    underAbstraction Dom' Term Type
    dom Abs Telescope
    tel ((Telescope -> m (Maybe Args)) -> m (Maybe Args))
    -> (Telescope -> m (Maybe Args)) -> m (Maybe Args)
    forall a b. (a -> b) -> a -> b
    $ (Maybe Args -> Maybe Args) -> m (Maybe Args) -> m (Maybe Args)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Args -> Args) -> Maybe Args -> Maybe Args
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg (Dom' Term Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom' Term Type
    dom) Term
    HasCallStack => Term
    __DUMMY_TERM__ Arg Term -> Args -> Args
    forall a. a -> [a] -> [a]
    :)) (m (Maybe Args) -> m (Maybe Args))
    -> (Telescope -> m (Maybe Args)) -> Telescope -> m (Maybe Args)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> m (Maybe Args)
    check)
            {-else-} (m (Maybe Args) -> m (Maybe Args))
    -> m (Maybe Args) -> m (Maybe Args)
    forall a b. (a -> b) -> a -> b
    $ do
              Maybe Term
    isSing <- Bool -> Type -> m (Maybe Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> Type -> m (Maybe Term)
    isSingletonType' Bool
    regardIrrelevance (Type -> m (Maybe Term)) -> Type -> m (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ Dom' Term Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom' Term Type
    dom
              case Maybe Term
    isSing of
                Maybe Term
    Nothing  -> Maybe Args -> m (Maybe Args)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Args
    forall a. Maybe a
    Nothing
                (Just Term
    v) -> Dom' Term Type
    -> Abs Telescope -> (Telescope -> m (Maybe Args)) -> m (Maybe Args)
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom' Term Type -> Abs a -> (a -> m b) -> m b
    underAbstraction Dom' Term Type
    dom Abs Telescope
    tel ((Telescope -> m (Maybe Args)) -> m (Maybe Args))
    -> (Telescope -> m (Maybe Args)) -> m (Maybe Args)
    forall a b. (a -> b) -> a -> b
    $ (Maybe Args -> Maybe Args) -> m (Maybe Args) -> m (Maybe Args)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Args -> Args) -> Maybe Args -> Maybe Args
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg (Dom' Term Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom' Term Type
    dom) Term
    v Arg Term -> Args -> Args
    forall a. a -> [a] -> [a]
    :)) (m (Maybe Args) -> m (Maybe Args))
    -> (Telescope -> m (Maybe Args)) -> Telescope -> m (Maybe Args)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> m (Maybe Args)
    check

    -- | Check whether a type has a unique inhabitant and return it.
    --   Can be blocked by a metavar.
    isSingletonType :: (PureTCM m, MonadBlock m) => Type -> m (Maybe Term)
    isSingletonType :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Type -> m (Maybe Term)
    isSingletonType = Bool -> Type -> m (Maybe Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> Type -> m (Maybe Term)
    isSingletonType' Bool
    False

    -- | Check whether a type has a unique inhabitant (irrelevant parts ignored).
    --   Can be blocked by a metavar.
    isSingletonTypeModuloRelevance :: (PureTCM m, MonadBlock m) => Type -> m Bool
    isSingletonTypeModuloRelevance :: forall (m :: * -> *). (PureTCM m, MonadBlock m) => Type -> m Bool
    isSingletonTypeModuloRelevance Type
    t = Maybe Term -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Term -> Bool) -> m (Maybe Term) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Bool -> Type -> m (Maybe Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> Type -> m (Maybe Term)
    isSingletonType' Bool
    True Type
    t

    isSingletonType' :: (PureTCM m, MonadBlock m) => Bool -> Type -> m (Maybe Term)
    isSingletonType' :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> Type -> m (Maybe Term)
    isSingletonType' Bool
    regardIrrelevance Type
    t = do
        TelV Telescope
    tel Type
    t <- Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t
        Type
    t <- Type -> m Type
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked Type
    t
        Telescope -> m (Maybe Term) -> m (Maybe Term)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (m (Maybe Term) -> m (Maybe Term))
    -> m (Maybe Term) -> m (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ do
          Maybe (QName, Args, Defn)
    res <- Type -> m (Maybe (QName, Args, Defn))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (QName, Args, Defn))
    isRecordType Type
    t
          case Maybe (QName, Args, Defn)
    res of
            Just (QName
    r, Args
    ps, Defn
    def) | HasEta' PatternOrCopattern
    YesEta <- Defn -> HasEta' PatternOrCopattern
    recEtaEquality Defn
    def -> do
              (Term -> Term) -> Maybe Term -> Maybe Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Telescope -> Term -> Term
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    tel) (Maybe Term -> Maybe Term) -> m (Maybe Term) -> m (Maybe Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Bool -> QName -> Args -> m (Maybe Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> QName -> Args -> m (Maybe Term)
    isSingletonRecord' Bool
    regardIrrelevance QName
    r Args
    ps
            Maybe (QName, Args, Defn)
    _ -> Maybe Term -> m (Maybe Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Term
    forall a. Maybe a
    Nothing

    -- | Checks whether the given term (of the given type) is beta-eta-equivalent
    --   to a variable. Returns just the de Bruijn-index of the variable if it is,
    --   or nothing otherwise.
    isEtaVar :: forall m. PureTCM m => Term -> Type -> m (Maybe Int)
    isEtaVar :: forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
    isEtaVar Term
    u Type
    a = MaybeT m Int -> m (Maybe Int)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT m Int -> m (Maybe Int)) -> MaybeT m Int -> m (Maybe Int)
    forall a b. (a -> b) -> a -> b
    $ Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
    isEtaVarG Term
    u Type
    a Maybe Int
    forall a. Maybe a
    Nothing []
      where
        -- Checks whether the term u (of type a) is beta-eta-equivalent to
        -- `Var i es`, and returns i if it is. If the argument mi is `Just i'`,
        -- then i and i' are also required to be equal (else Nothing is returned).
        isEtaVarG :: Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
        isEtaVarG :: Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
    isEtaVarG Term
    u Type
    a Maybe Int
    mi [Elim' Int]
    es = do
          (Term
    u, Type
    a) <- (Term, Type) -> MaybeT m (Term, Type)
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Term
    u, Type
    a)
          ArgName -> Int -> TCMT IO Doc -> MaybeT m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.lhs" Int
    80 (TCMT IO Doc -> MaybeT m ()) -> TCMT IO Doc -> MaybeT m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "isEtaVarG" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> 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
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "u  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Term
    u
            , TCMT IO Doc
    "a  = " 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
    a
            , TCMT IO Doc
    "mi = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (Maybe Int -> ArgName
    forall a. Show a => a -> ArgName
    show Maybe Int
    mi)
            , TCMT IO Doc
    "es = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Elim' Int -> TCMT IO Doc) -> [Elim' Int] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Elim' Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Elim' Term -> TCMT IO Doc)
    -> (Elim' Int -> Elim' Term) -> Elim' Int -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Term) -> Elim' Int -> Elim' Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Int -> Term
    var) [Elim' Int]
    es)
            ])
          case (Term
    u, Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    a) of
            (Var Int
    i' Elims
    es', Term
    _) -> do
              Bool -> MaybeT m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> MaybeT m ()) -> Bool -> MaybeT m ()
    forall a b. (a -> b) -> a -> b
    $ Maybe Int
    mi Maybe Int -> Maybe Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Int
    i' Int -> Maybe Int -> Maybe Int
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Maybe Int
    mi)
              Type
    b <- Int -> MaybeT m Type
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Int -> m Type
    typeOfBV Int
    i'
              Term -> Type -> Elims -> [Elim' Int] -> MaybeT m ()
    areEtaVarElims (Int -> Term
    var Int
    i') Type
    b Elims
    es' [Elim' Int]
    es
              Int -> MaybeT m Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    i'
            (Term
    _, Def QName
    d Elims
    pars) -> do
              Bool -> MaybeT m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> MaybeT m ()) -> MaybeT m Bool -> MaybeT m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do QName -> MaybeT m Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isEtaRecord QName
    d
              [QName]
    fs <- (Dom' Term QName -> QName) -> [Dom' Term QName] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term QName -> QName
    forall t e. Dom' t e -> e
    unDom ([Dom' Term QName] -> [QName])
    -> (Definition -> [Dom' Term QName]) -> Definition -> [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Defn -> [Dom' Term QName]
    recFields (Defn -> [Dom' Term QName])
    -> (Definition -> Defn) -> Definition -> [Dom' Term QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> [QName]) -> MaybeT m Definition -> MaybeT m [QName]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> MaybeT m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
              [Int]
    is <- [QName] -> (QName -> MaybeT m Int) -> MaybeT m [Int]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [QName]
    fs ((QName -> MaybeT m Int) -> MaybeT m [Int])
    -> (QName -> MaybeT m Int) -> MaybeT m [Int]
    forall a b. (a -> b) -> a -> b
    $ \QName
    f -> do
                let o :: ProjOrigin
    o = ProjOrigin
    ProjSystem
                (Dom' Term Type
    _, Term
    _, Type
    fa) <- m (Maybe (Dom' Term Type, Term, Type))
    -> MaybeT m (Dom' Term Type, Term, Type)
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (m (Maybe (Dom' Term Type, Term, Type))
     -> MaybeT m (Dom' Term Type, Term, Type))
    -> m (Maybe (Dom' Term Type, Term, Type))
    -> MaybeT m (Dom' Term Type, Term, Type)
    forall a b. (a -> b) -> a -> b
    $ Term
    -> Type
    -> ProjOrigin
    -> QName
    -> m (Maybe (Dom' Term Type, Term, Type))
    forall (m :: * -> *).
    PureTCM m =>
    Term
    -> Type
    -> ProjOrigin
    -> QName
    -> m (Maybe (Dom' Term Type, Term, Type))
    projectTyped Term
    u Type
    a ProjOrigin
    o QName
    f
                Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
    isEtaVarG (Term
    u Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o QName
    f]) Type
    fa Maybe Int
    mi ([Elim' Int]
    es [Elim' Int] -> [Elim' Int] -> [Elim' Int]
    forall a. [a] -> [a] -> [a]
    ++ [ProjOrigin -> QName -> Elim' Int
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o QName
    f])
              case (Maybe Int
    mi, [Int]
    is) of
                (Just Int
    i, [Int]
    _)     -> Int -> MaybeT m Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    i
                (Maybe Int
    Nothing, [])   -> MaybeT m Int
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
                (Maybe Int
    Nothing, Int
    i:[Int]
    is) -> Bool -> MaybeT m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard ((Int -> Bool) -> [Int] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    ==Int
    i) [Int]
    is) MaybeT m () -> MaybeT m Int -> MaybeT m Int
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Int -> MaybeT m Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    i
            (Term
    _, Pi Dom' Term Type
    dom Abs Type
    cod) -> Dom' Term Type -> MaybeT m Int -> MaybeT m Int
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Dom' Term Type
    dom (MaybeT m Int -> MaybeT m Int) -> MaybeT m Int -> MaybeT m Int
    forall a b. (a -> b) -> a -> b
    $ do
              let u' :: Term
    u'  = Int -> Term -> Term
    forall a. Subst a => Int -> a -> a
    raise Int
    1 Term
    u Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [Dom' Term Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom' Term Type
    dom Arg Type -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Int -> Term
    var Int
    0]
                  a' :: Type
    a'  = Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    cod
                  mi' :: Maybe Int
    mi' = (Int -> Int) -> Maybe Int -> Maybe Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) Maybe Int
    mi
                  es' :: [Elim' Int]
    es' = ((Elim' Int -> Elim' Int) -> [Elim' Int] -> [Elim' Int]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Elim' Int -> Elim' Int) -> [Elim' Int] -> [Elim' Int])
    -> ((Int -> Int) -> Elim' Int -> Elim' Int)
    -> (Int -> Int)
    -> [Elim' Int]
    -> [Elim' Int]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Int) -> Elim' Int -> Elim' Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) [Elim' Int]
    es [Elim' Int] -> [Elim' Int] -> [Elim' Int]
    forall a. [a] -> [a] -> [a]
    ++ [Arg Int -> Elim' Int
    forall a. Arg a -> Elim' a
    Apply (Arg Int -> Elim' Int) -> Arg Int -> Elim' Int
    forall a b. (a -> b) -> a -> b
    $ Dom' Term Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom' Term Type
    dom Arg Type -> Int -> Arg Int
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Int
    0]
              (-Int
    1Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +) (Int -> Int) -> MaybeT m Int -> MaybeT m Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
    isEtaVarG Term
    u' Type
    a' Maybe Int
    mi' [Elim' Int]
    es'
            (Term, Term)
    _ -> MaybeT m Int
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

        -- `areEtaVarElims u a es es'` checks whether the given elims es (as applied
        -- to the term u of type a) are beta-eta-equal to either projections or
        -- variables with de Bruijn indices given by es'.
        areEtaVarElims :: Term -> Type -> Elims -> [Elim' Int] -> MaybeT m ()
        areEtaVarElims :: Term -> Type -> Elims -> [Elim' Int] -> MaybeT m ()
    areEtaVarElims Term
    u Type
    a []    []    = () -> MaybeT m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        areEtaVarElims Term
    u Type
    a []    (Elim' Int
    _:[Elim' Int]
    _) = MaybeT m ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (Elim' Term
    _:Elims
    _) []    = MaybeT m ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (Proj ProjOrigin
    o QName
    f : Elims
    es) (Proj ProjOrigin
    _ QName
    f' : [Elim' Int]
    es') = do
          Bool -> MaybeT m ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> MaybeT m ()) -> Bool -> MaybeT m ()
    forall a b. (a -> b) -> a -> b
    $ QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f'
          Type
    a       <- Type -> MaybeT m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    a
          (Dom' Term Type
    _, Term
    _, Type
    fa) <- m (Maybe (Dom' Term Type, Term, Type))
    -> MaybeT m (Dom' Term Type, Term, Type)
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (m (Maybe (Dom' Term Type, Term, Type))
     -> MaybeT m (Dom' Term Type, Term, Type))
    -> m (Maybe (Dom' Term Type, Term, Type))
    -> MaybeT m (Dom' Term Type, Term, Type)
    forall a b. (a -> b) -> a -> b
    $ Term
    -> Type
    -> ProjOrigin
    -> QName
    -> m (Maybe (Dom' Term Type, Term, Type))
    forall (m :: * -> *).
    PureTCM m =>
    Term
    -> Type
    -> ProjOrigin
    -> QName
    -> m (Maybe (Dom' Term Type, Term, Type))
    projectTyped Term
    u Type
    a ProjOrigin
    o QName
    f
          Term -> Type -> Elims -> [Elim' Int] -> MaybeT m ()
    areEtaVarElims (Term
    u Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o QName
    f]) Type
    fa Elims
    es [Elim' Int]
    es'
        -- These two cases can occur only when we're looking at two different
        -- variables (i.e. one of function type and the other of record type) so
        -- it's definitely not the variable we're looking for (or someone is playing
        -- Jedi mind tricks on us)
        areEtaVarElims Term
    u Type
    a (Proj{}  : Elims
    _ ) (Apply Arg Int
    _ : [Elim' Int]
    _  ) = MaybeT m ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (Apply Arg Term
    _ : Elims
    _ ) (Proj{}  : [Elim' Int]
    _  ) = MaybeT m ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (Proj{} : Elims
    _ ) (IApply{} : [Elim' Int]
    _  ) = MaybeT m ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (IApply{} : Elims
    _ ) (Proj{} : [Elim' Int]
    _  ) = MaybeT m ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (Apply  Arg Term
    _ : Elims
    _ ) (IApply{} : [Elim' Int]
    _  ) = MaybeT m ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (IApply{} : Elims
    _ ) (Apply  Arg Int
    _ : [Elim' Int]
    _  ) = MaybeT m ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (IApply{} : Elims
    _) (IApply{} : [Elim' Int]
    _) = MaybeT m ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- TODO Andrea: not actually impossible, should be done like Apply
        areEtaVarElims Term
    u Type
    a (Apply Arg Term
    v : Elims
    es) (Apply Arg Int
    i : [Elim' Int]
    es') = do
          Type
    -> (Type -> MaybeT m ())
    -> (Dom' Term Type -> Abs Type -> MaybeT m ())
    -> MaybeT m ()
    forall (m :: * -> *) a.
    MonadReduce m =>
    Type -> (Type -> m a) -> (Dom' Term Type -> Abs Type -> m a) -> m a
    ifNotPiType Type
    a (MaybeT m () -> Type -> MaybeT m ()
    forall a b. a -> b -> a
    const MaybeT m ()
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero) ((Dom' Term Type -> Abs Type -> MaybeT m ()) -> MaybeT m ())
    -> (Dom' Term Type -> Abs Type -> MaybeT m ()) -> MaybeT m ()
    forall a b. (a -> b) -> a -> b
    $ \Dom' Term Type
    dom Abs Type
    cod -> do
          Int
    _ <- Term -> Type -> Maybe Int -> [Elim' Int] -> MaybeT m Int
    isEtaVarG (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    v) (Dom' Term Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom' Term Type
    dom) (Int -> Maybe Int
    forall a. a -> Maybe a
    Just (Int -> Maybe Int) -> Int -> Maybe Int
    forall a b. (a -> b) -> a -> b
    $ Arg Int -> Int
    forall e. Arg e -> e
    unArg Arg Int
    i) []
          Term -> Type -> Elims -> [Elim' Int] -> MaybeT m ()
    areEtaVarElims (Term
    u Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [(Int -> Term) -> Arg Int -> Arg Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Int -> Term
    var Arg Int
    i]) (Abs Type
    cod Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Int -> Term
    var (Arg Int -> Int
    forall e. Arg e -> e
    unArg Arg Int
    i)) Elims
    es [Elim' Int]
    es'

    -- | Replace projection patterns by the original projections.
    --
    class NormaliseProjP a where
      normaliseProjP :: HasConstInfo m => a -> m a

    instance NormaliseProjP Clause where
      normaliseProjP :: forall (m :: * -> *). HasConstInfo m => Clause -> m Clause
    normaliseProjP Clause
    cl = do
        NAPs
    ps <- NAPs -> m NAPs
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    normaliseProjP (NAPs -> m NAPs) -> NAPs -> m NAPs
    forall a b. (a -> b) -> a -> b
    $ Clause -> NAPs
    namedClausePats Clause
    cl
        Clause -> m Clause
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Clause -> m Clause) -> Clause -> m Clause
    forall a b. (a -> b) -> a -> b
    $ Clause
    cl { namedClausePats :: NAPs
    namedClausePats = NAPs
    ps }

    instance NormaliseProjP a => NormaliseProjP [a] where
      normaliseProjP :: forall (m :: * -> *). HasConstInfo m => [a] -> m [a]
    normaliseProjP = (a -> m a) -> [a] -> m [a]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> m a
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    normaliseProjP

    instance NormaliseProjP a => NormaliseProjP (Arg a) where
      normaliseProjP :: forall (m :: * -> *). HasConstInfo m => Arg a -> m (Arg a)
    normaliseProjP = (a -> m a) -> Arg a -> m (Arg a)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> m a
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    normaliseProjP

    instance NormaliseProjP a => NormaliseProjP (Named_ a) where
      normaliseProjP :: forall (m :: * -> *). HasConstInfo m => Named_ a -> m (Named_ a)
    normaliseProjP = (a -> m a) -> Named_ a -> m (Named_ a)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse a -> m a
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    normaliseProjP

    instance NormaliseProjP (Pattern' x) where
      normaliseProjP :: forall (m :: * -> *).
    HasConstInfo m =>
    Pattern' x -> m (Pattern' x)
    normaliseProjP p :: Pattern' x
    p@VarP{}        = Pattern' x -> m (Pattern' x)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' x
    p
      normaliseProjP p :: Pattern' x
    p@DotP{}        = Pattern' x -> m (Pattern' x)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' x
    p
      normaliseProjP (ConP ConHead
    c ConPatternInfo
    cpi [NamedArg (Pattern' x)]
    ps) = ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c ConPatternInfo
    cpi ([NamedArg (Pattern' x)] -> Pattern' x)
    -> m [NamedArg (Pattern' x)] -> m (Pattern' x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NamedArg (Pattern' x)] -> m [NamedArg (Pattern' x)]
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    normaliseProjP [NamedArg (Pattern' x)]
    ps
      normaliseProjP (DefP PatternInfo
    o QName
    q [NamedArg (Pattern' x)]
    ps) = PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
    forall x.
    PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
    DefP PatternInfo
    o QName
    q ([NamedArg (Pattern' x)] -> Pattern' x)
    -> m [NamedArg (Pattern' x)] -> m (Pattern' x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [NamedArg (Pattern' x)] -> m [NamedArg (Pattern' x)]
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    normaliseProjP [NamedArg (Pattern' x)]
    ps
      normaliseProjP p :: Pattern' x
    p@LitP{}        = Pattern' x -> m (Pattern' x)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' x
    p
      normaliseProjP (ProjP ProjOrigin
    o QName
    d0)    = ProjOrigin -> QName -> Pattern' x
    forall x. ProjOrigin -> QName -> Pattern' x
    ProjP ProjOrigin
    o (QName -> Pattern' x) -> m QName -> m (Pattern' x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getOriginalProjection QName
    d0
      normaliseProjP p :: Pattern' x
    p@IApplyP{}     = Pattern' x -> m (Pattern' x)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' x
    p