    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Records where

    import Prelude hiding (null)

    import Control.Applicative        ( (<|>) )
    import Control.Monad.Except       ( MonadError )
    import Control.Monad.Trans.Maybe  ( MaybeT(MaybeT), runMaybeT )
    import Control.Monad.Writer       ( Writer, runWriter, tell )

    import Data.Bifunctor
    import qualified Data.List as List
    import Data.Maybe
    import Data.Set (Set)
    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.MetaVars (unblockOnAnyMetaIn)
    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 qualified Agda.TypeChecking.Monad.Base.Warning as W
    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.Primitive.Cubical.Base (isCubicalSubtype)
    import {-# SOURCE #-} Agda.TypeChecking.ProjectionLike (eligibleForProjectionLike)

    import Agda.Utils.Empty
    import Agda.Utils.Function (applyWhen)
    import Agda.Utils.Functor (for, ($>), (<&>))
    import Agda.Utils.Lens
    import Agda.Utils.List
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Syntax.Common.Pretty (prettyShow)
    import Agda.Utils.Singleton
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * Tools to build record values

    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) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    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)]
    -> (List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
    -> WriterT [RecordFieldWarning] Identity ()
    forall (m :: * -> *) a.
    Applicative m =>
    [a] -> (List1 a -> m ()) -> m ()
    List1.unlessNull [(Name, a)]
    alien     ((List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
     -> WriterT [RecordFieldWarning] Identity ())
    -> (List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
    -> WriterT [RecordFieldWarning] Identity ()
    forall a b. (a -> b) -> a -> b
    $ (NonEmpty (Name, Range) -> RecordFieldWarning)
    -> List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ()
    forall {b} {m :: * -> *} {b} {p :: * -> * -> *} {b} {f :: * -> *}
           {a}.
    (MonadWriter b m, Singleton b b, Bifunctor p, HasRange b,
     Functor f) =>
    (f (p a Range) -> b) -> f (p a b) -> m ()
    warn ((NonEmpty (Name, Range) -> RecordFieldWarning)
     -> List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
    -> (NonEmpty (Name, Range) -> RecordFieldWarning)
    -> List1 (Name, a)
    -> WriterT [RecordFieldWarning] Identity ()
    forall a b. (a -> b) -> a -> b
    $ QName -> [Name] -> NonEmpty (Name, Range) -> RecordFieldWarning
    W.TooManyFields QName
    r [Name]
    missing
      [(Name, a)]
    -> (List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
    -> WriterT [RecordFieldWarning] Identity ()
    forall (m :: * -> *) a.
    Applicative m =>
    [a] -> (List1 a -> m ()) -> m ()
    List1.unlessNull [(Name, a)]
    duplicate ((List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
     -> WriterT [RecordFieldWarning] Identity ())
    -> (List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
    -> WriterT [RecordFieldWarning] Identity ()
    forall a b. (a -> b) -> a -> b
    $ (NonEmpty (Name, Range) -> RecordFieldWarning)
    -> List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ()
    forall {b} {m :: * -> *} {b} {p :: * -> * -> *} {b} {f :: * -> *}
           {a}.
    (MonadWriter b m, Singleton b b, Bifunctor p, HasRange b,
     Functor f) =>
    (f (p a Range) -> b) -> f (p a b) -> m ()
    warn ((NonEmpty (Name, Range) -> RecordFieldWarning)
     -> List1 (Name, a) -> WriterT [RecordFieldWarning] Identity ())
    -> (NonEmpty (Name, Range) -> RecordFieldWarning)
    -> List1 (Name, a)
    -> WriterT [RecordFieldWarning] Identity ()
    forall a b. (a -> b) -> a -> b
    $ NonEmpty (Name, Range) -> RecordFieldWarning
    W.DuplicateFields
      [a] -> WriterT [RecordFieldWarning] Identity [a]
    forall a. a -> WriterT [RecordFieldWarning] Identity a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([a] -> WriterT [RecordFieldWarning] Identity [a])
    -> [a] -> WriterT [RecordFieldWarning] Identity [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 :: (f (p a Range) -> b) -> f (p a b) -> m ()
    warn f (p a Range) -> b
    w    = b -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (b -> m ()) -> (f (p a b) -> b) -> f (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) -> (f (p a b) -> b) -> f (p a b) -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f (p a Range) -> b
    w (f (p a Range) -> b)
    -> (f (p a b) -> f (p a Range)) -> f (p a b) -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (p a b -> p a Range) -> f (p a b) -> f (p a Range)
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((b -> Range) -> p a b -> p a Range
    forall b c a. (b -> c) -> p a b -> p a c
    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 -> TCMT IO a
    forall a. a -> TCMT IO 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 (ZonkAny 0))
    -> [RecordFieldWarning] -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (TypeError -> TCMT IO (ZonkAny 0)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO (ZonkAny 0))
    -> (RecordFieldWarning -> TypeError)
    -> RecordFieldWarning
    -> TCMT IO (ZonkAny 0)
    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 -> TCMT IO a
    forall a. a -> TCMT IO 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 -> NamedArg a
    arg Name
    x a
    e = Maybe (Arg Name)
    -> NamedArg a -> (Arg Name -> NamedArg a) -> NamedArg 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 -> NamedArg a
    forall a. a -> NamedArg a
    defaultNamedArg a
    e) ((Arg Name -> NamedArg a) -> NamedArg a)
    -> (Arg Name -> NamedArg a) -> NamedArg 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 -> NamedArg a
    forall a b. a -> Arg b -> Arg a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg Name
    a
          givenFields :: [(Name, Maybe (NamedArg a))]
    givenFields = [ (Name
    x, NamedArg a -> Maybe (NamedArg a)
    forall a. a -> Maybe a
    Just (NamedArg a -> Maybe (NamedArg a))
    -> NamedArg a -> Maybe (NamedArg a)
    forall a b. (a -> b) -> a -> b
    $ Name -> a -> NamedArg 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 (NamedArg a)] -> [NamedArg a]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe (NamedArg a)] -> [NamedArg a])
    -> WriterT [RecordFieldWarning] Identity [Maybe (NamedArg a)]
    -> WriterT [RecordFieldWarning] Identity [NamedArg a]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName
    -> (Arg Name -> Maybe (NamedArg a))
    -> [Arg Name]
    -> [(Name, Maybe (NamedArg a))]
    -> WriterT [RecordFieldWarning] Identity [Maybe (NamedArg a)]
    forall a.
    HasRange a =>
    QName
    -> (Arg Name -> a)
    -> [Arg Name]
    -> [(Name, a)]
    -> Writer [RecordFieldWarning] [a]
    orderFields QName
    r Arg Name -> Maybe (NamedArg a)
    fill [Arg Name]
    axs [(Name, Maybe (NamedArg a))]
    givenFields
      where
        fill :: Arg C.Name -> Maybe (NamedArg a)
        fill :: Arg Name -> Maybe (NamedArg a)
    fill Arg Name
    ax
          | Arg Name -> Bool
    forall a. LensHiding a => a -> Bool
    visible Arg Name
    ax = NamedArg a -> Maybe (NamedArg a)
    forall a. a -> Maybe a
    Just (NamedArg a -> Maybe (NamedArg a))
    -> NamedArg a -> Maybe (NamedArg a)
    forall a b. (a -> b) -> a -> b
    $ Origin -> NamedArg a -> NamedArg a
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    Inserted (NamedArg a -> NamedArg a) -> NamedArg a -> NamedArg 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 -> NamedArg a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Arg Name
    ax
          | Bool
    otherwise  = Maybe (NamedArg 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

    ---------------------------------------------------------------------------
    -- * Query information about records from signature

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

    -- | 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 RecordData
    getRecordDef :: forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
    QName -> m RecordData
    getRecordDef QName
    r = m RecordData -> m (Maybe RecordData) -> m RecordData
    forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
    fromMaybeM m RecordData
    err (m (Maybe RecordData) -> m RecordData)
    -> m (Maybe RecordData) -> m RecordData
    forall a b. (a -> b) -> a -> b
    $ QName -> m (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    r
      where err :: m RecordData
    err = TypeError -> m RecordData
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m RecordData) -> TypeError -> m RecordData
    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 a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    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 a b. a -> Maybe b -> Maybe a
    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 = RecordData -> [Dom Name]
    recordFieldNames (RecordData -> [Dom Name]) -> m RecordData -> m [Dom Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m RecordData
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
    QName -> m RecordData
    getRecordDef QName
    r

    recordFieldNames :: RecordData -> [Dom C.Name]
    recordFieldNames :: RecordData -> [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 a b. (a -> b) -> Dom' Term a -> Dom' Term b
    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])
    -> (RecordData -> [Dom' Term QName]) -> RecordData -> [Dom Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RecordData -> [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
      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' TCState (HashMap QName Definition)
    -> TCMT IO (HashMap QName Definition)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC ((Signature -> f Signature) -> TCState -> f TCState
    Lens' TCState Signature
    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' Signature (HashMap QName Definition)
    sigDefinitions)
      idefs <- HMap.elems <$> useTC (stImports   . sigDefinitions)
      scope <- getScope
      return $ filter (`isNameInScope` scope) $ cands defs ++ cands 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 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
      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 unEl t of
        Def QName
    r Elims
    _ -> do
          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 rDef of
            Record { recFields :: Defn -> [Dom' Term QName]
    recFields = [Dom' Term QName]
    fields } -> [Dom' Term QName] -> TCM [Dom' Term QName]
    forall a. a -> TCMT IO a
    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
    -> (RecordData -> ConHead) -> RecordData -> ConHead
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RecordData -> ConHead
    _recConHead (RecordData -> ConHead) -> m RecordData -> m ConHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m RecordData
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
    QName -> m RecordData
    getRecordDef QName
    r

    -- | 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, RecordData))
    isRecordType :: forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (QName, Args, RecordData))
    isRecordType Type
    t = (Blocked Type -> Maybe (QName, Args, RecordData))
    -> ((QName, Args, RecordData) -> Maybe (QName, Args, RecordData))
    -> Either (Blocked Type) (QName, Args, RecordData)
    -> Maybe (QName, Args, RecordData)
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (Maybe (QName, Args, RecordData)
    -> Blocked Type -> Maybe (QName, Args, RecordData)
    forall a b. a -> b -> a
    const Maybe (QName, Args, RecordData)
    forall a. Maybe a
    Nothing) (QName, Args, RecordData) -> Maybe (QName, Args, RecordData)
    forall a. a -> Maybe a
    Just (Either (Blocked Type) (QName, Args, RecordData)
     -> Maybe (QName, Args, RecordData))
    -> m (Either (Blocked Type) (QName, Args, RecordData))
    -> m (Maybe (QName, Args, RecordData))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> m (Either (Blocked Type) (QName, Args, RecordData))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Either (Blocked Type) (QName, Args, RecordData))
    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, RecordData))
    tryRecordType :: forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Either (Blocked Type) (QName, Args, RecordData))
    tryRecordType Type
    t = Type
    -> (Blocker
        -> Type -> m (Either (Blocked Type) (QName, Args, RecordData)))
    -> (NotBlocked
        -> Type -> m (Either (Blocked Type) (QName, Args, RecordData)))
    -> m (Either (Blocked Type) (QName, Args, RecordData))
    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, RecordData)
    -> m (Either (Blocked Type) (QName, Args, RecordData))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Blocked Type) (QName, Args, RecordData)
     -> m (Either (Blocked Type) (QName, Args, RecordData)))
    -> Either (Blocked Type) (QName, Args, RecordData)
    -> m (Either (Blocked Type) (QName, Args, RecordData))
    forall a b. (a -> b) -> a -> b
    $ Blocked Type -> Either (Blocked Type) (QName, Args, RecordData)
    forall a b. a -> Either a b
    Left (Blocked Type -> Either (Blocked Type) (QName, Args, RecordData))
    -> Blocked Type -> Either (Blocked Type) (QName, Args, RecordData)
    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, RecordData)))
     -> m (Either (Blocked Type) (QName, Args, RecordData)))
    -> (NotBlocked
        -> Type -> m (Either (Blocked Type) (QName, Args, RecordData)))
    -> m (Either (Blocked Type) (QName, Args, RecordData))
    forall a b. (a -> b) -> a -> b
    $ \ NotBlocked
    nb Type
    t -> do
      let no :: m (Either (Blocked Type) (QName, Args, RecordData))
    no = Either (Blocked Type) (QName, Args, RecordData)
    -> m (Either (Blocked Type) (QName, Args, RecordData))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Blocked Type) (QName, Args, RecordData)
     -> m (Either (Blocked Type) (QName, Args, RecordData)))
    -> Either (Blocked Type) (QName, Args, RecordData)
    -> m (Either (Blocked Type) (QName, Args, RecordData))
    forall a b. (a -> b) -> a -> b
    $ Blocked Type -> Either (Blocked Type) (QName, Args, RecordData)
    forall a b. a -> Either a b
    Left (Blocked Type -> Either (Blocked Type) (QName, Args, RecordData))
    -> Blocked Type -> Either (Blocked Type) (QName, Args, RecordData)
    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 RecordData)
    -> m (Either (Blocked Type) (QName, Args, RecordData))
    -> (RecordData
        -> m (Either (Blocked Type) (QName, Args, RecordData)))
    -> m (Either (Blocked Type) (QName, Args, RecordData))
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> m (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    r) m (Either (Blocked Type) (QName, Args, RecordData))
    no ((RecordData
      -> m (Either (Blocked Type) (QName, Args, RecordData)))
     -> m (Either (Blocked Type) (QName, Args, RecordData)))
    -> (RecordData
        -> m (Either (Blocked Type) (QName, Args, RecordData)))
    -> m (Either (Blocked Type) (QName, Args, RecordData))
    forall a b. (a -> b) -> a -> b
    $ \ RecordData
    def -> Either (Blocked Type) (QName, Args, RecordData)
    -> m (Either (Blocked Type) (QName, Args, RecordData))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (Blocked Type) (QName, Args, RecordData)
     -> m (Either (Blocked Type) (QName, Args, RecordData)))
    -> Either (Blocked Type) (QName, Args, RecordData)
    -> m (Either (Blocked Type) (QName, Args, RecordData))
    forall a b. (a -> b) -> a -> b
    $ (QName, Args, RecordData)
    -> Either (Blocked Type) (QName, Args, RecordData)
    forall a b. b -> Either a b
    Right (QName
    r,Args
    vs,RecordData
    def)
        Term
    _ -> m (Either (Blocked Type) (QName, Args, RecordData))
    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
      def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
      let proj     = Defn -> Maybe Projection
    isProjection_ (Defn -> Maybe Projection) -> Defn -> Maybe Projection
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    def
          fallback = (QName, Definition, Maybe Projection)
    -> m (QName, Definition, Maybe Projection)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    f, Definition
    def, Maybe Projection
    proj)
      caseMaybe proj fallback $
        \ 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
            def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f'
            return (f', def, isProjection_ $ theDef 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).
      (f, def, mp) <- QName -> m (QName, Definition, Maybe Projection)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (QName, Definition, Maybe Projection)
    origProjection QName
    f
      let a = Definition -> Type
    defType Definition
    def
      -- if @f@ is not a projection (like) function, @a@ is the correct type
          fallback = Maybe Type -> m (Maybe Type)
    forall a. a -> m a
    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
      reportSDoc "tc.deftype" 20 $ vcat
        [ "definition f =" <+> prettyTCM f <+> text ("  -- raw: " ++ prettyShow f)
        , "has type   a =" <+> prettyTCM a
        , "principal  t =" <+> prettyTCM t
        ]
      caseMaybe mp fallback $
        \ (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
    forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
    prettyTCM Args
    pars)
                  ]
                ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.deftype" Int
    60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "parameters = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Args -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Args
    pars
                if Args -> Int
    forall a. [a] -> 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
    forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    Type -> Args -> 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
    forall (m :: * -> *). MonadPretty m => QName -> 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
    forall (m :: * -> *). MonadPretty m => Type -> 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
            ]
          ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.deftype" Int
    60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "raw 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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Type
    t
          Maybe Type -> m (Maybe Type)
    forall a. a -> m a
    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
    $ case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
            Dummy{} -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just Type
    HasCallStack => Type
    __DUMMY_TYPE__
            Term
    _       -> Maybe Type
    forall a. Maybe a
    Nothing

    -- | Apply a projection to an expression with a known type, returning
    --   the type of the projected value.
    --   The given type should either be a record type or a type eligible for
    --   the principal argument of a projection-like function.
    shouldBeProjectible :: (PureTCM m, MonadTCError m, MonadBlock m)
                        => Term -> Type -> ProjOrigin -> QName -> m Type
    -- shouldBeProjectible t f = maybe failure return =<< projectionType t f
    shouldBeProjectible :: forall (m :: * -> *).
    (PureTCM m, MonadTCError m, MonadBlock m) =>
    Term -> Type -> ProjOrigin -> QName -> m Type
    shouldBeProjectible Term
    v Type
    t ProjOrigin
    o QName
    f = do
      t <- Type -> m Type
    forall (m :: * -> *) t.
    (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
    t -> m t
    abortIfBlocked Type
    t
      projectTyped v t o f >>= \case
        Just (Dom' Term Type
    _ , Term
    _ , Type
    ft) -> Type -> m Type
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    ft
        Maybe (Dom' Term Type, Term, Type)
    Nothing -> case Type
    t of
          El Sort' Term
    _ Dummy{} -> Type -> m Type
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    HasCallStack => Type
    __DUMMY_TYPE__
          Type
    _ -> TypeError -> m Type
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m Type) -> TypeError -> m Type
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    ShouldBeRecordType Type
    t
        -- TODO: more accurate error that makes sense also for proj.-like funs.

    -- | 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 a. a -> m a
    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 a. a -> m a
    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
      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)
      return $ Just (dom, u, b `absApp` 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
    forall (m :: * -> *). MonadPretty m => Dom' Term Type -> 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
    <> 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
    forall (m :: * -> *). MonadPretty m => Dom' Term Type -> 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
    forall (m :: * -> *). MonadPretty m => Type -> 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 a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
    typeElims Type
    a Term
    self (Elim
    e : Elims
    es) = do
      case Elim
    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
    e]) Elims
    es
        Proj ProjOrigin
    o QName
    f -> do
          a <- Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    a
          (dom, self, a) <- fromMaybe __IMPOSSIBLE__ <$> projectTyped self a o f
          (ProjT dom a :) <$> typeElims a self es
        IApply{} -> TCM [ElimType]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Given a term with a given type and a list of eliminations, returning the
    --   type of the term applied to the eliminations.
    eliminateType :: (PureTCM m) => m Empty -> Term -> Type -> Elims -> m Type
    eliminateType :: forall (m :: * -> *).
    PureTCM m =>
    m Empty -> Term -> Type -> Elims -> m Type
    eliminateType m Empty
    err = m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
    forall (m :: * -> *).
    PureTCM m =>
    m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
    eliminateType' m Empty
    err ((Elims -> Term) -> Type -> Elims -> m Type)
    -> (Term -> Elims -> Term) -> Term -> Type -> Elims -> m Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    applyE

    eliminateType' :: (PureTCM m) => m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
    eliminateType' :: forall (m :: * -> *).
    PureTCM m =>
    m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
    eliminateType' m Empty
    err Elims -> Term
    hd Type
    t [] = Type -> m Type
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    t
    eliminateType' m Empty
    err Elims -> Term
    hd Type
    t (Elim
    e : Elims
    es) = case Elim
    e of
      Apply Arg Term
    v -> do
        t' <- m Empty -> Type -> Arg Term -> m Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> a -> m Type
    forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> Arg Term -> m Type
    piApplyM' m Empty
    err Type
    t Arg Term
    v
        eliminateType' err (hd . (e:)) t' es
      Proj ProjOrigin
    o QName
    f -> Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t m Type -> (Type -> m (Maybe Type)) -> m (Maybe Type)
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= QName -> Type -> m (Maybe Type)
    forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
    getDefType QName
    f m (Maybe Type) -> (Maybe Type -> m Type) -> m Type
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just Type
    a -> Type
    -> (Type -> m Type)
    -> (Dom' Term Type -> Abs Type -> m Type)
    -> m Type
    forall (m :: * -> *) a.
    MonadReduce m =>
    Type -> (Type -> m a) -> (Dom' Term Type -> Abs Type -> m a) -> m a
    ifNotPiType Type
    a (\Type
    _ -> Empty -> Type
    forall a. Empty -> a
    absurd (Empty -> Type) -> m Empty -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Empty
    err) ((Dom' Term Type -> Abs Type -> m Type) -> m Type)
    -> (Dom' Term Type -> Abs Type -> m Type) -> m Type
    forall a b. (a -> b) -> a -> b
    $ \Dom' Term Type
    _ Abs Type
    c ->
          m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
    forall (m :: * -> *).
    PureTCM m =>
    m Empty -> (Elims -> Term) -> Type -> Elims -> m Type
    eliminateType' m Empty
    err (Elims -> Term
    hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Elim
    eElim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :)) (Abs Type
    c Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` (Elims -> Term
    hd [])) Elims
    es
        Maybe Type
    Nothing -> Empty -> Type
    forall a. Empty -> a
    absurd (Empty -> Type) -> m Empty -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Empty
    err
      IApply Term
    _ Term
    _ Term
    r -> do
        t' <- m Empty -> Type -> Term -> m Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> a -> m Type
    forall (m :: * -> *).
    (MonadReduce m, HasBuiltins m) =>
    m Empty -> Type -> Term -> m Type
    piApplyM' m Empty
    err Type
    t Term
    r
        eliminateType' err (hd . (e:)) t' es

    -- | Check if a name refers to an eta expandable record.
    --
    -- The answer is no for a record type with an erased constructor
    -- unless the current quantity is \"erased\".
    {-# 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 = do
      QName -> m (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    r m (Maybe RecordData) -> (Maybe RecordData -> m Bool) -> m Bool
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Just RecordData
    r | RecordData -> Bool
    isEtaRecordDef RecordData
    r -> do
         constructorQ <- Definition -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity (Definition -> Quantity) -> m Definition -> m Quantity
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo (ConHead -> QName
    conName (RecordData -> ConHead
    _recConHead RecordData
    r))
         currentQ     <- viewTC eQuantity
         return $ constructorQ `moreQuantity` currentQ
        Maybe RecordData
    _ -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    isEtaRecordDef :: RecordData -> Bool
    isEtaRecordDef :: RecordData -> Bool
    isEtaRecordDef RecordData
    r = RecordData -> HasEta
    _recEtaEquality RecordData
    r HasEta -> HasEta -> Bool
    forall a. Eq a => a -> a -> Bool
    == HasEta
    forall a. HasEta' a
    YesEta

    {-# SPECIALIZE isEtaCon :: QName -> TCM Bool #-}
    isEtaCon :: HasConstInfo m => QName -> m Bool
    isEtaCon :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isEtaCon QName
    c = Maybe (QName, RecordData) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (QName, RecordData) -> Bool)
    -> m (Maybe (QName, RecordData)) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe (QName, RecordData))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, RecordData))
    isEtaRecordConstructor QName
    c

    -- | 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, RecordData))
    -> m Bool -> ((QName, RecordData) -> 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, RecordData))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, RecordData))
    isRecordConstructor QName
    c) (Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False) (((QName, RecordData) -> m Bool) -> m Bool)
    -> ((QName, RecordData) -> m Bool) -> m Bool
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    _, RecordData
    def) ->
        Bool -> m Bool
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (RecordData -> Bool
    isEtaRecordDef RecordData
    def) m Bool -> m Bool -> m Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `or2M`
          Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RecordData -> Maybe Induction
    _recInduction RecordData
    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 :: HasConstInfo m => QName -> m Bool
    isInductiveRecord :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isInductiveRecord QName
    r = Bool -> (RecordData -> Bool) -> Maybe RecordData -> 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)
    -> (RecordData -> Maybe Induction) -> RecordData -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RecordData -> Maybe Induction
    _recInduction) (Maybe RecordData -> Bool) -> m (Maybe RecordData) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    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 a. a -> m a
    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 a. a -> m a
    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 a. a -> m a
    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, RecordData))
    isRecordConstructor :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, RecordData))
    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, RecordData)))
    -> m (Maybe (QName, RecordData))
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Left (SigUnknown ArgName
    err)     -> m (Maybe (QName, RecordData))
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      Left SigError
    SigCubicalNotErasure -> m (Maybe (QName, RecordData))
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      Left SigError
    SigAbstract          -> Maybe (QName, RecordData) -> m (Maybe (QName, RecordData))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, RecordData)
    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 } -> (RecordData -> (QName, RecordData))
    -> Maybe RecordData -> Maybe (QName, RecordData)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (QName
    r,) (Maybe RecordData -> Maybe (QName, RecordData))
    -> m (Maybe RecordData) -> m (Maybe (QName, RecordData))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    r
        Defn
    _                          -> Maybe (QName, RecordData) -> m (Maybe (QName, RecordData))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, RecordData)
    forall a. Maybe a
    Nothing

    isEtaRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, RecordData))
    isEtaRecordConstructor :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, RecordData))
    isEtaRecordConstructor QName
    c = QName -> m (Maybe (QName, RecordData))
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe (QName, RecordData))
    isRecordConstructor QName
    c m (Maybe (QName, RecordData))
    -> (Maybe (QName, RecordData) -> m (Maybe (QName, RecordData)))
    -> m (Maybe (QName, RecordData))
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Maybe (QName, RecordData)
    Nothing -> Maybe (QName, RecordData) -> m (Maybe (QName, RecordData))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, RecordData)
    forall a. Maybe a
    Nothing
      Just (QName
    d, RecordData
    def) -> if RecordData -> Bool
    isEtaRecordDef RecordData
    def then Maybe (QName, RecordData) -> m (Maybe (QName, RecordData))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (QName, RecordData) -> m (Maybe (QName, RecordData)))
    -> Maybe (QName, RecordData) -> m (Maybe (QName, RecordData))
    forall a b. (a -> b) -> a -> b
    $ (QName, RecordData) -> Maybe (QName, RecordData)
    forall a. a -> Maybe a
    Just (QName
    d, RecordData
    def) else Maybe (QName, RecordData) -> m (Maybe (QName, RecordData))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, RecordData)
    forall a. Maybe a
    Nothing

    -- | 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 = QName -> (EtaEquality -> EtaEquality) -> TCMT IO ()
    forall (m :: * -> *).
    MonadTCState m =>
    QName -> (EtaEquality -> EtaEquality) -> m ()
    modifyRecEta QName
    q \ EtaEquality
    eta -> EtaEquality -> HasEta -> EtaEquality
    setEtaEquality EtaEquality
    eta (HasEta -> EtaEquality) -> HasEta -> EtaEquality
    forall a b. (a -> b) -> a -> b
    $ PatternOrCopattern -> HasEta
    forall a. a -> HasEta' a
    NoEta PatternOrCopattern
    pat

    -- | Turn on eta for non-recursive and inductive guarded recursive records,
    --   unless user declared otherwise.
    --   Projections do not preserve guardedness.
    updateEtaForRecord :: QName -> TCM ()
    updateEtaForRecord :: QName -> TCMT IO ()
    updateEtaForRecord QName
    q = TCMT IO Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM TCMT IO 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 we need to switch on eta for record q?
      switchEta <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q TCMT IO Definition -> (Definition -> Defn) -> TCMT IO Defn
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> Definition -> Defn
    theDef TCMT IO Defn -> (Defn -> Bool) -> TCMT IO Bool
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \case
        Record{ recInduction :: Defn -> Maybe Induction
    recInduction = Maybe Induction
    ind, recEtaEquality' :: Defn -> EtaEquality
    recEtaEquality' = EtaEquality
    eta }
          | 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 -> Bool
    True
          | Bool
    otherwise -> Bool
    False
        Defn
    _ -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      when switchEta $ modifyRecEta q $ const $ Inferred YesEta

    -- | Turn on eta for inductive guarded recursive records.
    --   Projections do not preserve guardedness.
    recursiveRecord :: QName -> TCM ()
    recursiveRecord :: QName -> TCMT IO ()
    recursiveRecord = QName -> TCMT IO ()
    updateEtaForRecord

    -- | Turn on eta for non-recursive record, unless user declared otherwise.
    nonRecursiveRecord :: QName -> TCM ()
    nonRecursiveRecord :: QName -> TCMT IO ()
    nonRecursiveRecord = QName -> TCMT IO ()
    updateEtaForRecord

    -- | Check whether record type is marked as recursive.
    --
    --   Precondition: record type identifier exists in signature.
    isRecursiveRecord :: QName -> TCM Bool
    isRecursiveRecord :: QName -> TCMT IO Bool
    isRecursiveRecord QName
    q =
      TCMT IO Signature
    forall (m :: * -> *). ReadTCState m => m Signature
    getSignature TCMT IO Signature
    -> (Signature -> Maybe Definition) -> TCMT IO (Maybe Definition)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> QName -> Signature -> Maybe Definition
    lookupDefinition QName
    q TCMT IO (Maybe Definition)
    -> (Maybe Definition -> Maybe Defn) -> TCMT IO (Maybe Defn)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> (Definition -> Defn) -> Maybe Definition -> Maybe Defn
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Definition -> Defn
    theDef TCMT IO (Maybe Defn) -> (Maybe Defn -> Bool) -> TCMT IO Bool
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \case
        Just (RecordDefn RecordData
    r) -> RecordData -> Bool
    recRecursive_ RecordData
    r
        Maybe Defn
    _ -> Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    {- | @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 a b. (a -> b) -> Maybe a -> Maybe b
    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))
    forall (m :: * -> *).
    PureTCM m =>
    Int
    -> Telescope
    -> m (Maybe (Telescope, Substitution, Substitution, Telescope))
    expandRecordVar Int
    i (Telescope
     -> TCMT
          IO (Maybe (Telescope, Substitution, Substitution, Telescope)))
    -> TCMT IO Telescope
    -> TCMT
         IO (Maybe (Telescope, Substitution, Substitution, Telescope))
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (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 :: PureTCM m => Int -> Telescope -> m (Maybe (Telescope, Substitution, Substitution, Telescope))
    expandRecordVar :: forall (m :: * -> *).
    PureTCM m =>
    Int
    -> Telescope
    -> m (Maybe (Telescope, Substitution, Substitution, Telescope))
    expandRecordVar Int
    i Telescope
    gamma0 = do
      -- Get the context with last variable added last in list.
      let gamma :: [Dom' Term (ArgName, Type)]
    gamma = Telescope -> [Dom' Term (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' Term (ArgName, Type)] -> Int
    forall a. Sized a => a -> Int
    size [Dom' Term (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' Term (ArgName, Type)]
    gamma1, dom :: Dom' Term (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' Term (ArgName, Type)]
    gamma2) = Int
    -> [Dom' Term (ArgName, Type)]
    -> ([Dom' Term (ArgName, Type)], [Dom' Term (ArgName, Type)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    l [Dom' Term (ArgName, Type)]
    gamma -- TODO:: Defined but not used dom, ai
      -- This must be a eta-expandable record type.
      let failure :: m (Maybe (Telescope, Substitution, Substitution, Telescope))
    failure = do
            ArgName -> Int -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Int -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.meta.assign.proj" Int
    25 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    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
    forall (m :: * -> *). MonadPretty m => Type -> 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)
    -> m (Maybe (Telescope, Substitution, Substitution, Telescope))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Telescope, Substitution, Substitution, Telescope)
    forall a. Maybe a
    Nothing
      m (Maybe (QName, Args, RecordData))
    -> m (Maybe (Telescope, Substitution, Substitution, Telescope))
    -> ((QName, Args, RecordData)
        -> m (Maybe (Telescope, Substitution, Substitution, Telescope)))
    -> m (Maybe (Telescope, Substitution, Substitution, Telescope))
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Type -> m (Maybe (QName, Args, RecordData))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (QName, Args, RecordData))
    isRecordType Type
    a) m (Maybe (Telescope, Substitution, Substitution, Telescope))
    failure (((QName, Args, RecordData)
      -> m (Maybe (Telescope, Substitution, Substitution, Telescope)))
     -> m (Maybe (Telescope, Substitution, Substitution, Telescope)))
    -> ((QName, Args, RecordData)
        -> m (Maybe (Telescope, Substitution, Substitution, Telescope)))
    -> m (Maybe (Telescope, Substitution, Substitution, Telescope))
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    r, Args
    pars, RecordData
    def) -> case RecordData -> Bool
    isEtaRecordDef RecordData
    def of
        Bool
    False -> Maybe (Telescope, Substitution, Substitution, Telescope)
    -> m (Maybe (Telescope, Substitution, Substitution, Telescope))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Telescope, Substitution, Substitution, Telescope)
    forall a. Maybe a
    Nothing
        Bool
    True  -> (Telescope, Substitution, Substitution, Telescope)
    -> Maybe (Telescope, Substitution, Substitution, Telescope)
    forall a. a -> Maybe a
    Just ((Telescope, Substitution, Substitution, Telescope)
     -> Maybe (Telescope, Substitution, Substitution, Telescope))
    -> m (Telescope, Substitution, Substitution, Telescope)
    -> m (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 = RecordData -> Telescope
    _recTel RecordData
    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
    $ RecordData -> [Dom' Term QName]
    _recFields RecordData
    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 (RecordData -> ConHead
    _recConHead RecordData
    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' Term (ArgName, Type)] -> Int
    forall a. Sized a => a -> Int
    size [Dom' Term (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 a b. (a -> b) -> Arg a -> Arg b
    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
    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' Term (ArgName, Type)] -> Int
    forall a. Sized a => a -> Int
    size [Dom' Term (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' Term (ArgName, Type)] -> Telescope
    telFromList ([Dom' Term (ArgName, Type)] -> Telescope)
    -> [Dom' Term (ArgName, Type)] -> Telescope
    forall a b. (a -> b) -> a -> b
    $ [Dom' Term (ArgName, Type)]
    gamma1 [Dom' Term (ArgName, Type)]
    -> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
    forall a. [a] -> [a] -> [a]
    ++ Telescope -> [Dom' Term (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    tel' [Dom' Term (ArgName, Type)]
    -> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
    forall a. [a] -> [a] -> [a]
    ++
                        Telescope -> [Dom' Term (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' Term (ArgName, Type)] -> Telescope
    telFromList [Dom' Term (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)
    -> m (Telescope, Substitution, Substitution, Telescope)
    forall a. a -> m a
    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 a. a -> TCMT IO a
    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))
    forall (m :: * -> *).
    PureTCM m =>
    Int
    -> Telescope
    -> m (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
        (gamma2, sigma2, tau2) <- [Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
    expandRecordVarsRecursively ([Int]
    newis [Int] -> [Int] -> [Int]
    forall a. [a] -> [a] -> [a]
    ++ [Int]
    is) Telescope
    gamma1
        -- Γ₁ ⊢ σ₂ : Γ₂  and  Γ₂ ⊢ τ₂ : Γ₁
        return (gamma2, applySubst sigma1 sigma2, applySubst tau2 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 gamma core <- Int -> Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Int -> Type -> m (TelV Type)
    telViewUpTo Int
    n Type
    t
      case unEl 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.
          (r, pars, def) <- (QName, Args, RecordData)
    -> Maybe (QName, Args, RecordData) -> (QName, Args, RecordData)
    forall a. a -> Maybe a -> a
    fromMaybe (QName, Args, RecordData)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (QName, Args, RecordData) -> (QName, Args, RecordData))
    -> TCMT IO (Maybe (QName, Args, RecordData))
    -> TCMT IO (QName, Args, RecordData)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCMT IO (Maybe (QName, Args, RecordData))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (QName, Args, RecordData))
    isRecordType Type
    a
          if | NoEta _ <- _recEtaEquality def -> __IMPOSSIBLE__
             | otherwise -> return ()
          -- TODO: compose argInfo ai with tel.
          let tel = RecordData -> Telescope
    _recTel RecordData
    def Telescope -> Args -> Telescope
    forall t. Apply t => t -> Args -> t
    `apply` Args
    pars
              m   = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel
              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
    $ RecordData -> [Dom' Term QName]
    _recFields RecordData
    def
              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   = ConHead -> ConInfo -> Args -> Term
    mkCon (KillRangeT ConHead
    forall a. KillRange a => KillRangeT a
    killRange KillRangeT ConHead -> KillRangeT ConHead
    forall a b. (a -> b) -> a -> b
    $ RecordData -> ConHead
    _recConHead RecordData
    def) ConInfo
    ConOSystem Args
    ys
              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'  = Telescope
    gamma Telescope -> Type -> Type
    `telePi` (Telescope
    tel Telescope -> Type -> Type
    `telePi` Type
    b')
              gammai = (Dom' Term (ArgName, Type) -> ArgInfo)
    -> [Dom' Term (ArgName, Type)] -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term (ArgName, Type) -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo ([Dom' Term (ArgName, Type)] -> [ArgInfo])
    -> [Dom' Term (ArgName, Type)] -> [ArgInfo]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom' Term (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Telescope
    gamma
              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
    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
    n Int -> 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  = [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 a b. (a -> b) -> Arg a -> Arg b
    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
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    f]
              atel = Dom' Term (ArgName, Type) -> Telescope
    forall a. SgTel a => a -> Telescope
    sgTel (Dom' Term (ArgName, Type) -> Telescope)
    -> Dom' Term (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' Term (ArgName, Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom' Term Type
    dom
              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)
          return (curry, uncurry, 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       -- ^ Name of record type.
      -> Args        -- ^ Parameters applied to record type.
      -> Term        -- ^ Term to eta-expand.
      -> m (Telescope, Args)
         -- ^ Field types instantiated to parameters, field values.
    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       -- ^ Name of record type.
      -> Args        -- ^ Parameters applied to record type.
      -> Term        -- ^ Term to eta-expand.
      -> m (Telescope, Args)
         -- ^ Field types instantiated to parameters, field values.
    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

    -- | Eta-expand a value at the given record type (must match).
    etaExpandRecord' :: (HasConstInfo m, MonadDebug m, ReadTCState m)
      => Bool        -- ^ Force expansion, overriding '_recEtaEquality'?
      -> QName       -- ^ Name of record type.
      -> Args        -- ^ Parameters applied to record type.
      -> Term        -- ^ Term to eta-expand.
      -> m (Telescope, Args)
         -- ^ Field types instantiated to parameters, field values.
    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
      def <- RecordData -> Maybe RecordData -> RecordData
    forall a. a -> Maybe a -> a
    fromMaybe RecordData
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe RecordData -> RecordData)
    -> m (Maybe RecordData) -> m RecordData
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    r
      (tel, _, _, args) <- etaExpandRecord'_ forceEta r pars def u
      return (tel, args)

    -- | Eta-expand a value at the given eta record type (must match).
    etaExpandRecord_ :: HasConstInfo m
      => QName       -- ^ Name of record type.
      -> Args        -- ^ Parameters applied to record type.
      -> RecordData  -- ^ Definition of record type.
      -> Term        -- ^ Term to eta-expand.
      -> m (Telescope, ConHead, ConInfo, Args)
         -- ^ Field types instantiated to parameters, disassembled constructor term.
    etaExpandRecord_ :: forall (m :: * -> *).
    HasConstInfo m =>
    QName
    -> Args
    -> RecordData
    -> Term
    -> m (Telescope, ConHead, ConInfo, Args)
    etaExpandRecord_ = Bool
    -> QName
    -> Args
    -> RecordData
    -> Term
    -> m (Telescope, ConHead, ConInfo, Args)
    forall (m :: * -> *).
    HasConstInfo m =>
    Bool
    -> QName
    -> Args
    -> RecordData
    -> Term
    -> m (Telescope, ConHead, ConInfo, Args)
    etaExpandRecord'_ Bool
    False

    -- | Eta-expand a value at the given record type (must match).
    etaExpandRecord'_ :: HasConstInfo m
      => Bool        -- ^ Force expansion, overriding '_recEtaEquality'?
      -> QName       -- ^ Name of record type.
      -> Args        -- ^ Parameters applied to record type.
      -> RecordData  -- ^ Definition of record type.
      -> Term        -- ^ Term to eta-expand.
      -> m (Telescope, ConHead, ConInfo, Args)
         -- ^ Field types instantiated to parameters, disassembled constructor term.
    etaExpandRecord'_ :: forall (m :: * -> *).
    HasConstInfo m =>
    Bool
    -> QName
    -> Args
    -> RecordData
    -> Term
    -> m (Telescope, ConHead, ConInfo, Args)
    etaExpandRecord'_ Bool
    forceEta QName
    r Args
    pars
        def :: RecordData
    def@RecordData{ _recConHead :: RecordData -> ConHead
    _recConHead = ConHead
    con, _recFields :: RecordData -> [Dom' Term QName]
    _recFields = [Dom' Term QName]
    xs, _recTel :: RecordData -> Telescope
    _recTel = Telescope
    tel }
        Term
    u = do
      let 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (RecordData -> HasEta
    _recEtaEquality RecordData
    def HasEta -> HasEta -> Bool
    forall a. Eq a => a -> a -> Bool
    == HasEta
    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 a. a -> m a
    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 a b. (a -> b) -> Arg a -> Arg b
    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
    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
    forall (m :: * -> *). MonadPretty m => Term -> 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
    forall (m :: * -> *). MonadPretty m => QName -> 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
    forall (m :: * -> *). MonadPretty m => Telescope -> 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
    forall (m :: * -> *). MonadPretty m => Args -> m Doc
    prettyTCM Args
    xs'
              ]
            ]
          (Telescope, ConHead, ConInfo, Args)
    -> m (Telescope, ConHead, ConInfo, Args)
    forall a. a -> m a
    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
      (r, pars, def) <- (QName, Args, RecordData)
    -> Maybe (QName, Args, RecordData) -> (QName, Args, RecordData)
    forall a. a -> Maybe a -> a
    fromMaybe (QName, Args, RecordData)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (QName, Args, RecordData) -> (QName, Args, RecordData))
    -> TCMT IO (Maybe (QName, Args, RecordData))
    -> TCMT IO (QName, Args, RecordData)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCMT IO (Maybe (QName, Args, RecordData))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (QName, Args, RecordData))
    isRecordType Type
    t
      (tel, con, ci, args) <- etaExpandRecord_ r pars def u
      return (tel, mkCon con ci 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
      RecordData{ _recFields = xs } <- RecordData -> Maybe RecordData -> RecordData
    forall a. a -> Maybe a -> a
    fromMaybe RecordData
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe RecordData -> RecordData)
    -> m (Maybe RecordData) -> m RecordData
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    r
      reportSDoc "tc.record.eta.contract" 20 $ vcat
        [ "eta contracting record"
        , nest 2 $ vcat
          [ "record type r  =" <+> prettyTCM r
          , "constructor c  =" <+> prettyTCM c
          , "field names xs =" <+> pretty    xs
          , "fields    args =" <+> prettyTCM args
          ]
        ]
      case compare (length args) (length 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 a. a -> m a
    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 a. a -> m a
    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
          (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
    e0:Elims
    es0))
            | (Elims
    es, Proj ProjOrigin
    _o QName
    f) <- Elim -> Elims -> (Elims, Elim)
    forall a. a -> [a] -> ([a], a)
    initLast1 Elim
    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

    {-# SPECIALIZE isSingletonRecord :: QName -> Args -> TCM Bool #-}
    -- | 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   -- ^ Name of record type to check.
      -> Args    -- ^ Parameters given to the record type.
      -> 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 -> Set QName -> m (Maybe Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> QName -> Args -> Set QName -> m (Maybe Term)
    isSingletonRecord' Bool
    False QName
    r Args
    ps Set QName
    forall a. Monoid a => a
    mempty

    isSingletonRecordModuloRelevance :: (PureTCM m, MonadBlock m)
      => QName   -- ^ Name of record type to check.
      -> Args    -- ^ Parameters given to the record type.
      -> 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 -> Set QName -> m (Maybe Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> QName -> Args -> Set QName -> m (Maybe Term)
    isSingletonRecord' Bool
    True QName
    r Args
    ps Set QName
    forall a. Monoid a => a
    mempty

    -- | 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            -- ^ Should disregard irrelevant fields?
      -> QName           -- ^ Name of record type to check.
      -> Args            -- ^ Parameters given to the record type.
      -> Set QName       -- ^ Non-terminating record types we already encountered.
                         --   These are considered as non-singletons,
                         --   otherwise we would construct an infinite inhabitant (in an infinite time...).
      -> m (Maybe Term)  -- ^ The unique inhabitant, if any.  May contain dummy terms in irrelevant positions.
    isSingletonRecord' :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> QName -> Args -> Set QName -> m (Maybe Term)
    isSingletonRecord' Bool
    regardIrrelevance QName
    r Args
    ps Set QName
    rs = 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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ 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
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (QName -> Elims -> Term
    Def QName
    r (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    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?"
        , TCMT IO Doc
    "  already visited:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep ((QName -> TCMT IO Doc) -> [QName] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM ([QName] -> [TCMT IO Doc]) -> [QName] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ Set QName -> [QName]
    forall a. Set a -> [a]
    Set.toList Set QName
    rs)
        ]
      -- Andreas, 2022-03-10, issue #5823
      -- We need to make sure we are not infinitely unfolding records, so we only expand each once,
      -- and keep track of the recursive ones we have already seen.
      if QName
    r QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set QName
    rs then m (Maybe Term)
    forall {a}. m (Maybe a)
    no else do
        m (Maybe RecordData)
    -> m (Maybe Term)
    -> (RecordData -> m (Maybe Term))
    -> m (Maybe Term)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (QName -> m (Maybe RecordData)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe RecordData)
    isRecord QName
    r) m (Maybe Term)
    forall {a}. m (Maybe a)
    no ((RecordData -> m (Maybe Term)) -> m (Maybe Term))
    -> (RecordData -> m (Maybe Term)) -> m (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ \ RecordData
    def -> do
          -- We might not know yet whether a record type is recursive because the positivity checker hasn't run yet.
          -- In this case, we pessimistically consider the record type to be recursive (@True@).
          let recursive :: Bool
    recursive = Bool -> ([QName] -> Bool) -> Maybe [QName] -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True (Bool -> Bool
    not (Bool -> Bool) -> ([QName] -> Bool) -> [QName] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [QName] -> Bool
    forall a. Null a => a -> Bool
    null) (Maybe [QName] -> Bool) -> Maybe [QName] -> Bool
    forall a b. (a -> b) -> a -> b
    $ RecordData -> Maybe [QName]
    _recMutual RecordData
    def
          -- Andreas, 2022-03-23, issue #5823
          -- We may pass through terminating record types as often as we want.
          -- If the termination checker has not run yet, we pessimistically consider the record type
          -- to be non-terminating.
          let nonTerminating :: Bool
    nonTerminating = Bool -> (Bool -> Bool) -> Maybe Bool -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True Bool -> Bool
    not (Maybe Bool -> Bool) -> Maybe Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ RecordData -> Maybe Bool
    _recTerminates RecordData
    def
          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] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep [ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    r, TCMT IO Doc
    "is recursive      :", Bool -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Bool -> m Doc
    prettyTCM Bool
    recursive      ]
            , [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep [ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    r, TCMT IO Doc
    "is non-terminating:", Bool -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Bool -> m Doc
    prettyTCM Bool
    nonTerminating ]
            ]
          (Args -> Term) -> Maybe Args -> Maybe Term
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ConHead -> ConInfo -> Args -> Term
    mkCon (RecordData -> ConHead
    _recConHead RecordData
    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
    <$> do
            Set QName -> Telescope -> m (Maybe Args)
    check (Bool -> (Set QName -> Set QName) -> Set QName -> Set QName
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen (Bool
    recursive Bool -> Bool -> Bool
    && Bool
    nonTerminating) (QName -> Set QName -> Set QName
    forall a. Ord a => a -> Set a -> Set a
    Set.insert QName
    r) Set QName
    rs) (Telescope -> m (Maybe Args)) -> Telescope -> m (Maybe Args)
    forall a b. (a -> b) -> a -> b
    $ RecordData -> Telescope
    _recTel RecordData
    def Telescope -> Args -> Telescope
    forall t. Apply t => t -> Args -> t
    `apply` Args
    ps
      where
      -- Check that all entries of the constructor telescope are singletons.
      check :: Set QName -> Telescope -> m (Maybe [Arg Term])
      check :: Set QName -> Telescope -> m (Maybe Args)
    check Set QName
    rs 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
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM Telescope
    tel
        case Telescope
    tel of
          Telescope
    EmptyTel -> m (Maybe Args)
    forall {a}. m (Maybe [a])
    yes
          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 a. a -> m a
    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 a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Args -> Args) -> Maybe Args -> Maybe Args
    forall a b. (a -> b) -> Maybe a -> Maybe b
    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
    . Set QName -> Telescope -> m (Maybe Args)
    check Set QName
    rs)
            {-else-} (m (Maybe Args) -> m (Maybe Args))
    -> m (Maybe Args) -> m (Maybe Args)
    forall a b. (a -> b) -> a -> b
    $ do
              m (Maybe Term)
    -> m (Maybe Args) -> (Term -> m (Maybe Args)) -> m (Maybe Args)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Bool -> Type -> Set QName -> m (Maybe Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> Type -> Set QName -> m (Maybe Term)
    isSingletonType' Bool
    regardIrrelevance (Dom' Term Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom' Term Type
    dom) Set QName
    rs) m (Maybe Args)
    forall {a}. m (Maybe a)
    no ((Term -> m (Maybe Args)) -> m (Maybe Args))
    -> (Term -> m (Maybe Args)) -> m (Maybe Args)
    forall a b. (a -> b) -> a -> b
    $ \ Term
    v -> do
                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 a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Args -> Args) -> Maybe Args -> Maybe Args
    forall a b. (a -> b) -> Maybe a -> Maybe b
    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
    . Set QName -> Telescope -> m (Maybe Args)
    check Set QName
    rs
      no :: m (Maybe a)
    no  = Maybe a -> m (Maybe a)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing
      yes :: m (Maybe [a])
    yes = Maybe [a] -> m (Maybe [a])
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe [a] -> m (Maybe [a])) -> Maybe [a] -> m (Maybe [a])
    forall a b. (a -> b) -> a -> b
    $ [a] -> Maybe [a]
    forall a. a -> Maybe a
    Just []

    -- | 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 Type
    t = Bool -> Type -> Set QName -> m (Maybe Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> Type -> Set QName -> m (Maybe Term)
    isSingletonType' Bool
    False Type
    t Set QName
    forall a. Monoid a => a
    mempty

    -- | 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 -> Set QName -> m (Maybe Term)
    forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> Type -> Set QName -> m (Maybe Term)
    isSingletonType' Bool
    True Type
    t Set QName
    forall a. Monoid a => a
    mempty

    isSingletonType'
      :: forall m. (PureTCM m, MonadBlock m)
      => Bool            -- ^ Should disregard irrelevant fields?
      -> Type            -- ^ Type to check.
      -> Set QName       -- ^ Non-terminating record typess we already encountered.
                         --   These are considered as non-singletons,
                         --   otherwise we would construct an infinite inhabitant (in an infinite time...).
      -> m (Maybe Term)  -- ^ The unique inhabitant, if any.  May contain dummy terms in irrelevant positions.
    isSingletonType' :: forall (m :: * -> *).
    (PureTCM m, MonadBlock m) =>
    Bool -> Type -> Set QName -> m (Maybe Term)
    isSingletonType' Bool
    regardIrrelevance Type
    t Set QName
    rs = do
        TelV tel t <- Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t
        t <- abortIfBlocked t
        addContext tel $ do
          let
            -- Easy case: η for records.
            record :: m (Maybe Term)
            record = MaybeT m Term -> m (Maybe Term)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT m Term -> m (Maybe Term))
    -> MaybeT m Term -> m (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ do
              (r, ps, def) <- m (Maybe (QName, Args, RecordData))
    -> MaybeT m (QName, Args, RecordData)
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (m (Maybe (QName, Args, RecordData))
     -> MaybeT m (QName, Args, RecordData))
    -> m (Maybe (QName, Args, RecordData))
    -> MaybeT m (QName, Args, RecordData)
    forall a b. (a -> b) -> a -> b
    $ Type -> m (Maybe (QName, Args, RecordData))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (QName, Args, RecordData))
    isRecordType Type
    t
              guard $ isEtaRecordDef def
              abstract tel <$> MaybeT (isSingletonRecord' regardIrrelevance r ps rs)

            -- Slightly harder case: η for Sub {level} tA phi elt.
            -- tA : Type level, phi : I, elt : Partial phi tA.
            subtype :: m (Maybe Term)
            subtype = MaybeT m Term -> m (Maybe Term)
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT m Term -> m (Maybe Term))
    -> MaybeT m Term -> m (Maybe Term)
    forall a b. (a -> b) -> a -> b
    $ do
              (level, tA, phi, elt) <- m (Maybe (Term, Term, Term, Term))
    -> MaybeT m (Term, Term, Term, Term)
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (m (Maybe (Term, Term, Term, Term))
     -> MaybeT m (Term, Term, Term, Term))
    -> m (Maybe (Term, Term, Term, Term))
    -> MaybeT m (Term, Term, Term, Term)
    forall a b. (a -> b) -> a -> b
    $ Type -> m (Maybe (Term, Term, Term, Term))
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (Term, Term, Term, Term))
    isCubicalSubtype Type
    t
              subin <- MaybeT $ getBuiltinName' builtinSubIn
              itIsOne <- MaybeT $ getBuiltinName' builtinIsOne
              phiV <- intervalView phi
              case phiV of
                -- If phi = i1, then inS (elt 1=1) is the only inhabitant.
                IntervalView
    IOne -> do
                  let
                    argH :: e -> Arg e
    argH = ArgInfo -> e -> Arg e
    forall e. ArgInfo -> e -> Arg e
    Arg (ArgInfo -> e -> Arg e) -> ArgInfo -> e -> Arg e
    forall a b. (a -> b) -> a -> b
    $ Hiding -> ArgInfo -> ArgInfo
    forall a. LensHiding a => Hiding -> a -> a
    setHiding Hiding
    Hidden ArgInfo
    defaultArgInfo
                    it :: Term
    it = Term
    elt Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (QName -> Elims -> Term
    Def QName
    itIsOne [])]
                  Term -> MaybeT m Term
    forall a. a -> MaybeT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (QName -> Elims -> Term
    Def QName
    subin [] Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [Term -> Arg Term
    forall a. a -> Arg a
    argH Term
    level, Term -> Arg Term
    forall a. a -> Arg a
    argH Term
    tA, Term -> Arg Term
    forall a. a -> Arg a
    argH Term
    phi, Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    it])
                -- Otherwise we're blocked
                OTerm Term
    phi' -> Blocker -> MaybeT m Term
    forall a. Blocker -> MaybeT m a
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
    patternViolation (Term -> Blocker
    forall t. AllMetas t => t -> Blocker
    unblockOnAnyMetaIn Term
    phi')
                -- This fails the MaybeT: we're not looking at a
                -- definitional singleton.
                IntervalView
    _ -> ArgName -> MaybeT m Term
    forall a. ArgName -> MaybeT m a
    forall (m :: * -> *) a. MonadFail m => ArgName -> m a
    fail ArgName
    ""

          (<|>) <$> record <*> subtype

    {-# SPECIALIZE isEtaVar :: Term -> Type -> TCM (Maybe Int) #-}
    -- | 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
          (u, a) <- (Term, Type) -> MaybeT m (Term, Type)
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Term
    u, Type
    a)
          reportSDoc "tc.lhs" 80 $ "isEtaVarG" <+> nest 2 (vcat
            [ "u  = " <+> prettyTCM u
            , "a  = " <+> prettyTCM a
            , "mi = " <+> text (show mi)
            , "es = " <+> prettyList_ (map (prettyTCM . fmap var) es)
            ])
          case (u, unEl a) of
            (Var Int
    i' Elims
    es', Term
    _) -> do
              Bool -> MaybeT m ()
    forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
    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 a b. a -> Maybe b -> Maybe a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Maybe Int
    mi)
              b <- Int -> MaybeT m Type
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
    typeOfBV Int
    i'
              areEtaVarElims (var i') b es' es
              return i'
            (Term
    _, Def QName
    d Elims
    pars) -> do
              Bool -> MaybeT m ()
    forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
    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
              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
              is <- forM fs $ \QName
    f -> do
                let o :: ProjOrigin
    o = ProjOrigin
    ProjSystem
                (_, _, 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
                isEtaVarG (u `applyE` [Proj o f]) fa mi (es ++ [Proj o f])
              case (mi, is) of
                (Just Int
    i, [Int]
    _)     -> Int -> MaybeT m Int
    forall a. a -> MaybeT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    i
                (Maybe Int
    Nothing, [])   -> MaybeT m Int
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
                (Maybe Int
    Nothing, Int
    i:[Int]
    is) -> Bool -> MaybeT m ()
    forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
    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 a b. MaybeT m a -> MaybeT m b -> MaybeT m b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Int -> MaybeT m Int
    forall a. a -> MaybeT m a
    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
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Dom' Term Type -> 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 a b. (a -> b) -> Maybe a -> Maybe b
    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 a b. (a -> b) -> [a] -> [b]
    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 a b. (a -> b) -> Elim' a -> Elim' b
    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
    1 Int -> 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 a. MaybeT m a
    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 a. a -> MaybeT m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        areEtaVarElims Term
    u Type
    a []    (Elim' Int
    _:[Elim' Int]
    _) = MaybeT m ()
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (Elim
    _:Elims
    _) []    = MaybeT m ()
    forall a. MaybeT m a
    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 b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
    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'
          a       <- Type -> MaybeT m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    a
          (_, _, fa) <- MaybeT $ projectTyped u a o f
          areEtaVarElims (u `applyE` [Proj o f]) fa es 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 a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (Apply Arg Term
    _ : Elims
    _ ) (Proj{}  : [Elim' Int]
    _  ) = MaybeT m ()
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (Proj{} : Elims
    _ ) (IApply{} : [Elim' Int]
    _  ) = MaybeT m ()
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (IApply{} : Elims
    _ ) (Proj{} : [Elim' Int]
    _  ) = MaybeT m ()
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (Apply  Arg Term
    _ : Elims
    _ ) (IApply{} : [Elim' Int]
    _  ) = MaybeT m ()
    forall a. MaybeT m a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
        areEtaVarElims Term
    u Type
    a (IApply{} : Elims
    _ ) (Apply  Arg Int
    _ : [Elim' Int]
    _  ) = MaybeT m ()
    forall a. MaybeT m a
    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 a. MaybeT m a
    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
          _ <- 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) []
          areEtaVarElims (u `apply` [fmap var i]) (cod `absApp` var (unArg i)) es 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
        ps <- NAPs -> m NAPs
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    forall (m :: * -> *). HasConstInfo m => NAPs -> m NAPs
    normaliseProjP (NAPs -> m NAPs) -> NAPs -> m NAPs
    forall a b. (a -> b) -> a -> b
    $ Clause -> NAPs
    namedClausePats Clause
    cl
        return $ cl { namedClausePats = 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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse a -> m a
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    forall (m :: * -> *). 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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Arg a -> f (Arg b)
    traverse a -> m a
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    forall (m :: * -> *). 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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Named NamedName a -> f (Named NamedName b)
    traverse a -> m a
    forall a (m :: * -> *).
    (NormaliseProjP a, HasConstInfo m) =>
    a -> m a
    forall (m :: * -> *). 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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' x
    p
      normaliseProjP p :: Pattern' x
    p@DotP{}        = Pattern' x -> m (Pattern' x)
    forall a. a -> m a
    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
    forall (m :: * -> *).
    HasConstInfo m =>
    [NamedArg (Pattern' x)] -> m [NamedArg (Pattern' x)]
    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
    forall (m :: * -> *).
    HasConstInfo m =>
    [NamedArg (Pattern' x)] -> m [NamedArg (Pattern' x)]
    normaliseProjP [NamedArg (Pattern' x)]
    ps
      normaliseProjP p :: Pattern' x
    p@LitP{}        = Pattern' x -> m (Pattern' x)
    forall a. a -> m a
    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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pattern' x
    p