    {-# LANGUAGE NondecreasingIndentation   #-}

    module Agda.TypeChecking.Rules.Record where

    import Prelude hiding (null)

    import Control.Monad
    import Data.Maybe
    import qualified Data.Set as Set

    import Agda.Interaction.Options

    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern
    import Agda.Syntax.Position
    import qualified Agda.Syntax.Info as Info

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Primitive
    import Agda.TypeChecking.Rewriting.Confluence
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Positivity.Occurrence
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Polarity
    import Agda.TypeChecking.Warnings
    import Agda.TypeChecking.Irrelevance
    import Agda.TypeChecking.CompiledClause (hasProjectionPatterns)
    import Agda.TypeChecking.CompiledClause.Compile

    import Agda.TypeChecking.Rules.Data ( getGeneralizedParameters, bindGeneralizedParameters, bindParameters, fitsIn, forceSort,
                                          defineCompData, defineTranspOrHCompForFields )
    import Agda.TypeChecking.Rules.Term ( isType_ )
    import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkDecl)

    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Permutation
    import Agda.Utils.POMonoid
    import Agda.Utils.Pretty (render)
    import qualified Agda.Utils.Pretty as P
    import Agda.Utils.Size
    import Agda.Utils.WithDefault

    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * Records
    ---------------------------------------------------------------------------

    -- | @checkRecDef i name con ps contel fields@
    --
    --     [@name@]    Record type identifier.
    --
    --     [@con@]     Maybe constructor name and info.
    --
    --     [@ps@]      Record parameters.
    --
    --     [@contel@]  Approximate type of constructor (@fields@ -> Set).
    --                 Does not include record parameters.
    --
    --     [@fields@]  List of field signatures.
    --
    checkRecDef
      :: A.DefInfo                 -- ^ Position and other info.
      -> QName                     -- ^ Record type identifier.
      -> UniverseCheck             -- ^ Check universes?
      -> A.RecordDirectives        -- ^ (Co)Inductive, (No)Eta, (Co)Pattern, Constructor?
      -> A.DataDefParams           -- ^ Record parameters.
      -> A.Expr                    -- ^ Approximate type of constructor (@fields@ -> Set).
                                   --   Does not include record parameters.
      -> [A.Field]                 -- ^ Field signatures.
      -> TCM ()
    checkRecDef :: DefInfo
    -> QName
    -> UniverseCheck
    -> RecordDirectives
    -> DataDefParams
    -> Expr
    -> [Field]
    -> TCM ()
    checkRecDef DefInfo
    i QName
    name UniverseCheck
    uc (RecordDirectives Maybe (Ranged Induction)
    ind Maybe HasEta0
    eta0 Maybe Range
    pat Maybe QName
    con) (A.DataDefParams Set Name
    gpars [LamBinding]
    ps) Expr
    contel [Field]
    fields =
      Call -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> QName -> [LamBinding] -> [Field] -> Call
    CheckRecDef (QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    name) QName
    name [LamBinding]
    ps [Field]
    fields) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "checking record def" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    name
          , 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
    "ps ="     TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList ((LamBinding -> TCMT IO Doc) -> [LamBinding] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map LamBinding -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA [LamBinding]
    ps)
          , 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
    "contel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Expr -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Expr
    contel
          , 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
    "fields =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Constr Field] -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA ((Field -> Constr Field) -> [Field] -> [Constr Field]
    forall a b. (a -> b) -> [a] -> [b]
    map Field -> Constr Field
    forall a. a -> Constr a
    Constr [Field]
    fields)
          ]
        -- get type of record
        Definition
    def <- Definition -> TCMT IO Definition
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    Definition -> m Definition
    instantiateDef (Definition -> TCMT IO Definition)
    -> TCMT IO Definition -> TCMT IO Definition
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    name
        Type
    t   <- Type -> TCMT IO Type
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull (Type -> TCMT IO Type) -> Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type
    defType Definition
    def
        let npars :: Int
    npars =
              case Definition -> Defn
    theDef Definition
    def of
                DataOrRecSig Int
    n -> Int
    n
                Defn
    _              -> Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        [Maybe Name]
    parNames <- Set Name -> QName -> TCM [Maybe Name]
    getGeneralizedParameters Set Name
    gpars QName
    name

        [Maybe Name] -> Type -> (Telescope -> Type -> TCM ()) -> TCM ()
    forall a.
    [Maybe Name] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
    bindGeneralizedParameters [Maybe Name]
    parNames Type
    t ((Telescope -> Type -> TCM ()) -> TCM ())
    -> (Telescope -> Type -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Telescope
    gtel Type
    t0 ->
         Int
    -> [LamBinding] -> Type -> (Telescope -> Type -> TCM ()) -> TCM ()
    forall a.
    Int
    -> [LamBinding] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
    bindParameters (Int
    npars Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [Maybe Name] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Maybe Name]
    parNames) [LamBinding]
    ps Type
    t0 ((Telescope -> Type -> TCM ()) -> TCM ())
    -> (Telescope -> Type -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ Telescope
    ptel Type
    t0 -> do

          let tel :: Telescope
    tel = Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    gtel Telescope
    ptel

          -- Generate type of constructor from field telescope @contel@,
          -- which is the approximate constructor type (target missing).

          -- Check and evaluate field types.
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec" Int
    15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "checking fields"
          Type
    contype <- TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    workOnTypes (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Type
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Expr -> TCMT IO Type
    isType_ Expr
    contel
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "contype = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    contype ]

          -- compute the field telescope (does not include record parameters)
          let TelV Telescope
    ftel Type
    _ = Type -> TelV Type
    telView' Type
    contype

          -- Compute correct type of constructor

          -- t = tel -> t0 where t0 must be a sort s
          TelV Telescope
    idxTel Type
    s <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t0
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Telescope -> Bool
    forall a. Null a => a -> Bool
    null Telescope
    idxTel) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    ShouldBeASort Type
    t0
          Sort
    s <- Type -> TCM Sort
    forceSort Type
    s

          -- needed for impredicative Prop (not implemented yet)
          -- ftel <- return $
          --   if s == Prop
          --   then telFromList $ map (setRelevance Irrelevant) $ telToList ftel
          --   else ftel

          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec" Int
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            Telescope
    gamma <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope  -- the record params (incl. module params)
            TCMT IO Doc
    "gamma = " 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 (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    gamma)

          -- record type (name applied to parameters)
          Type
    rect <- Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> ([Arg Term] -> Term) -> [Arg Term] -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Elims -> Term
    Def QName
    name (Elims -> Term) -> ([Arg Term] -> Elims) -> [Arg Term] -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply ([Arg Term] -> Type) -> TCMT IO [Arg Term] -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO [Arg Term]
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
    getContextArgs

          -- Put in @rect@ as correct target of constructor type.
          -- Andreas, 2011-05-10 use telePi_ instead of telePi to preserve
          -- even names of non-dependent fields in constructor type (Issue 322).
          let contype :: Type
    contype = Telescope -> Type -> Type
    telePi_ Telescope
    ftel (Int -> Type -> Type
    forall a. Subst a => Int -> a -> a
    raise (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    ftel) Type
    rect)
            -- NB: contype does not contain the parameter telescope

          -- Obtain name of constructor (if present).
          (Bool
    hasNamedCon, QName
    conName) <- case Maybe QName
    con of
            Just QName
    c  -> (Bool, QName) -> TCMT IO (Bool, QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    True, QName
    c)
            Maybe QName
    Nothing -> do
              ModuleName
    m <- KillRangeT ModuleName
    forall a. KillRange a => KillRangeT a
    killRange KillRangeT ModuleName -> TCMT IO ModuleName -> TCMT IO ModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
              -- Andreas, 2020-06-01, AIM XXXII
              -- Using prettyTCM here jinxes the printer, see PR #4699.
              -- r <- prettyTCM name
              let r :: Doc
    r = Name -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (Name -> Doc) -> Name -> Doc
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    name
              QName
    c <- ModuleName -> Name -> QName
    qualify ModuleName
    m (Name -> QName) -> TCMT IO Name -> TCMT IO QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> TCMT IO Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ (Doc -> [Char]
    render Doc
    r [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ".constructor")
              (Bool, QName) -> TCMT IO (Bool, QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    False, QName
    c)

          -- Add record type to signature.
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec" Int
    15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "adding record type to signature"

          Bool
    etaenabled <- TCMT IO Bool
    forall (m :: * -> *). HasOptions m => m Bool
    etaEnabled

          let getName :: A.Declaration -> [Dom QName]
              getName :: Field -> [Dom' Term QName]
    getName (A.Field DefInfo
    _ QName
    x Arg Expr
    arg)    = [QName
    x QName -> Dom' Term Expr -> Dom' Term QName
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg Expr -> Dom' Term Expr
    forall a. Arg a -> Dom a
    domFromArg Arg Expr
    arg]
              getName (A.ScopedDecl ScopeInfo
    _ [Field
    f]) = Field -> [Dom' Term QName]
    getName Field
    f
              getName Field
    _                    = []

              setTactic :: Dom' t e -> Dom' t e -> Dom' t e
    setTactic Dom' t e
    dom Dom' t e
    f = Dom' t e
    f { domTactic :: Maybe t
    domTactic = Dom' t e -> Maybe t
    forall t e. Dom' t e -> Maybe t
    domTactic Dom' t e
    dom }

              fs :: [Dom' Term QName]
    fs = (Dom ([Char], Type) -> Dom' Term QName -> Dom' Term QName)
    -> [Dom ([Char], Type)] -> [Dom' Term QName] -> [Dom' Term QName]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Dom ([Char], Type) -> Dom' Term QName -> Dom' Term QName
    forall {t} {e} {t} {e}. Dom' t e -> Dom' t e -> Dom' t e
    setTactic (Telescope -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    ftel) ([Dom' Term QName] -> [Dom' Term QName])
    -> [Dom' Term QName] -> [Dom' Term QName]
    forall a b. (a -> b) -> a -> b
    $ (Field -> [Dom' Term QName]) -> [Field] -> [Dom' Term QName]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Field -> [Dom' Term QName]
    getName [Field]
    fields

              -- indCo is what the user wrote: inductive/coinductive/Nothing.
              -- We drop the Range.
              indCo :: Maybe Induction
    indCo = Ranged Induction -> Induction
    forall a. Ranged a -> a
    rangedThing (Ranged Induction -> Induction)
    -> Maybe (Ranged Induction) -> Maybe Induction
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (Ranged Induction)
    ind
              -- A constructor is inductive unless declared coinductive.
              conInduction :: Induction
    conInduction = Induction -> Maybe Induction -> Induction
    forall a. a -> Maybe a -> a
    fromMaybe Induction
    Inductive Maybe Induction
    indCo
              -- Andreas, 2016-09-20, issue #2197.
              -- Eta is inferred by the positivity checker.
              -- We should turn it off until it is proven to be safe.
              haveEta :: EtaEquality
    haveEta      = EtaEquality
    -> (HasEta -> EtaEquality) -> Maybe HasEta -> EtaEquality
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (HasEta -> EtaEquality
    Inferred (HasEta -> EtaEquality) -> HasEta -> EtaEquality
    forall a b. (a -> b) -> a -> b
    $ PatternOrCopattern -> HasEta
    forall a. a -> HasEta' a
    NoEta PatternOrCopattern
    patCopat) HasEta -> EtaEquality
    Specified Maybe HasEta
    eta
              -- haveEta      = maybe (Inferred $ conInduction == Inductive && etaenabled) Specified eta
              con :: ConHead
    con = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead QName
    conName (PatternOrCopattern -> DataOrRecord
    IsRecord PatternOrCopattern
    patCopat) Induction
    conInduction ([Arg QName] -> ConHead) -> [Arg QName] -> ConHead
    forall a b. (a -> b) -> a -> b
    $ (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]
    fs

              -- A record is irrelevant if all of its fields are.
              -- In this case, the associated module parameter will be irrelevant.
              -- See issue 392.
              -- Unless it's been declared coinductive or no-eta-equality (#2607).
              recordRelevance :: Relevance
    recordRelevance
                | Just NoEta{} <- Maybe HasEta
    eta         = Relevance
    Relevant
                | Induction
    CoInductive <- Induction
    conInduction = Relevance
    Relevant
                | Bool
    otherwise                   = [Relevance] -> Relevance
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum ([Relevance] -> Relevance) -> [Relevance] -> Relevance
    forall a b. (a -> b) -> a -> b
    $ Relevance
    Irrelevant Relevance -> [Relevance] -> [Relevance]
    forall a. a -> [a] -> [a]
    : (Dom ([Char], Type) -> Relevance)
    -> [Dom ([Char], Type)] -> [Relevance]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom ([Char], Type) -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance (Telescope -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    ftel)

          -- Andreas, 2017-01-26, issue #2436
          -- Disallow coinductive records with eta-equality
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Induction
    conInduction Induction -> Induction -> Bool
    forall a. Eq a => a -> a -> Bool
    == Induction
    CoInductive Bool -> Bool -> Bool
    && EtaEquality -> HasEta
    theEtaEquality EtaEquality
    haveEta HasEta -> HasEta -> Bool
    forall a. Eq a => a -> a -> Bool
    == HasEta
    forall a. HasEta' a
    YesEta) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
              [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "Agda doesn't like coinductive records with eta-equality."
                  , TCMT IO Doc
    "If you must, use pragma"
                  , TCMT IO Doc
    "{-# ETA" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    name TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "#-}"
                  ]
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "record constructor is " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ConHead -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ConHead
    con

          -- Jesper, 2021-05-26: Warn when declaring coinductive record
          -- but neither --guardedness nor --sized-types is enabled.
          Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Induction
    conInduction Induction -> Induction -> Bool
    forall a. Eq a => a -> a -> Bool
    == Induction
    CoInductive) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            Bool
    guardedness <- WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    optGuardedness (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
            Bool
    sizedTypes  <- WithDefault 'False -> Bool
    forall (b :: Bool). KnownBool b => WithDefault b -> Bool
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    optSizedTypes  (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Bool
    guardedness Bool -> Bool -> Bool
    || Bool
    sizedTypes) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> TCM ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCM ()) -> Warning -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Warning
    NoGuardednessFlag QName
    name

          -- Add the record definition.

          -- Andreas, 2016-06-17, Issue #2018:
          -- Do not rely on @addConstant@ to put in the record parameters,
          -- as they might be renamed in the context.
          -- By putting them ourselves (e.g. by using the original type @t@)
          -- we make sure we get the original names!
          let npars :: Int
    npars = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel
              telh :: Telescope
    telh  = (Dom Type -> Dom Type) -> Telescope -> Telescope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Dom Type -> Dom Type
    forall a. (LensHiding a, LensRelevance a) => a -> a
    hideAndRelParams Telescope
    tel
          Impossible -> Int -> TCM () -> TCM ()
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible Int
    npars (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
    addConstant' QName
    name ArgInfo
    defaultArgInfo QName
    name Type
    t (Defn -> TCM ()) -> Defn -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                Record :: Int
    -> Maybe Clause
    -> ConHead
    -> Bool
    -> [Dom' Term QName]
    -> Telescope
    -> Maybe [QName]
    -> EtaEquality
    -> PatternOrCopattern
    -> Maybe Induction
    -> IsAbstract
    -> CompKit
    -> Defn
    Record
                  { recPars :: Int
    recPars           = Int
    npars
                  , recClause :: Maybe Clause
    recClause         = Maybe Clause
    forall a. Maybe a
    Nothing
                  , recConHead :: ConHead
    recConHead        = ConHead
    con
                  , recNamedCon :: Bool
    recNamedCon       = Bool
    hasNamedCon
                  , recFields :: [Dom' Term QName]
    recFields         = [Dom' Term QName]
    fs
                  , recTel :: Telescope
    recTel            = Telescope
    telh Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    ftel
                  , recAbstr :: IsAbstract
    recAbstr          = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    i
                  , recEtaEquality' :: EtaEquality
    recEtaEquality'   = EtaEquality
    haveEta
                  , recPatternMatching :: PatternOrCopattern
    recPatternMatching= PatternOrCopattern
    patCopat
                  , recInduction :: Maybe Induction
    recInduction      = Maybe Induction
    indCo
                      -- We retain the original user declaration [(co)inductive]
                      -- in case the record turns out to be recursive.
                  -- Determined by positivity checker:
                  , recMutual :: Maybe [QName]
    recMutual         = Maybe [QName]
    forall a. Maybe a
    Nothing
                  , recComp :: CompKit
    recComp           = CompKit
    emptyCompKit -- filled in later
                  }

            -- Add record constructor to signature
            QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
    addConstant' QName
    conName ArgInfo
    defaultArgInfo QName
    conName
                (Telescope
    telh Telescope -> Type -> Type
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Type
    contype) (Defn -> TCM ()) -> Defn -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                Constructor :: Int
    -> Int
    -> ConHead
    -> QName
    -> IsAbstract
    -> Induction
    -> CompKit
    -> Maybe [QName]
    -> [IsForced]
    -> Maybe [Bool]
    -> Defn
    Constructor
                  { conPars :: Int
    conPars   = Int
    npars
                  , conArity :: Int
    conArity  = [Dom' Term QName] -> Int
    forall a. Sized a => a -> Int
    size [Dom' Term QName]
    fs
                  , conSrcCon :: ConHead
    conSrcCon = ConHead
    con
                  , conData :: QName
    conData   = QName
    name
                  , conAbstr :: IsAbstract
    conAbstr  = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    i
                  , conInd :: Induction
    conInd    = Induction
    conInduction
                  , conComp :: CompKit
    conComp   = CompKit
    emptyCompKit  -- filled in later
                  , conProj :: Maybe [QName]
    conProj   = Maybe [QName]
    forall a. Maybe a
    Nothing       -- filled in later
                  , conForced :: [IsForced]
    conForced = []
                  , conErased :: Maybe [Bool]
    conErased = Maybe [Bool]
    forall a. Maybe a
    Nothing
                  }

          -- Declare the constructor as eligible for instance search
          case DefInfo -> IsInstance
    forall t. DefInfo' t -> IsInstance
    Info.defInstance DefInfo
    i of
            InstanceDef Range
    r -> Range -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Range
    r (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              -- Andreas, 2020-01-28, issue #4360:
              -- Use addTypedInstance instead of addNamedInstance
              -- to detect unusable instances.
              QName -> Type -> TCM ()
    addTypedInstance QName
    conName Type
    contype
              -- addNamedInstance conName name
            IsInstance
    NotInstanceDef -> () -> TCM ()
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

          -- Check that the fields fit inside the sort
          Int
    _ <- UniverseCheck -> [IsForced] -> Type -> Sort -> TCM Int
    fitsIn UniverseCheck
    uc [] Type
    contype Sort
    s

          {- Andreas, 2011-04-27 WRONG because field types are checked again
             and then non-stricts should not yet be irrelevant

          -- make record parameters hidden and non-stricts irrelevant
          -- ctx <- (reverse . map hideAndRelParams . take (size tel)) <$> getContext
          -}

    {- Andreas, 2013-09-13 DEBUGGING the debug printout
          reportSDoc "tc.rec" 80 $ sep
            [ "current module record telescope"
            , nest 2 $ (prettyTCM =<< getContextTelescope)
            ]
          reportSDoc "tc.rec" 80 $ sep
            [ "current module record telescope"
            , nest 2 $ (text . show =<< getContextTelescope)
            ]
          reportSDoc "tc.rec" 80 $ sep
            [ "current module record telescope"
            , nest 2 $ (inTopContext . prettyTCM =<< getContextTelescope)
            ]
          reportSDoc "tc.rec" 80 $ sep
            [ "current module record telescope"
            , nest 2 $ do
               tel <- getContextTelescope
               text (show tel) $+$ do
               inTopContext $ do
                 prettyTCM tel $+$ do
                   telA <- reify tel
                   text (show telA) $+$ do
                   ctx <- getContextTelescope
                   "should be empty:" <+> prettyTCM ctx
            ]
    -}

          let info :: ArgInfo
    info = Relevance -> ArgInfo -> ArgInfo
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    recordRelevance ArgInfo
    defaultArgInfo
              addRecordVar :: TCM () -> TCM ()
    addRecordVar =
                Dom Type -> TCM () -> TCM ()
    forall (m :: * -> *) b.
    (MonadAddContext m, MonadFresh NameId m) =>
    Dom Type -> m b -> m b
    addRecordNameContext (ArgInfo -> Dom Type -> Dom Type
    forall a. LensArgInfo a => ArgInfo -> a -> a
    setArgInfo ArgInfo
    info (Dom Type -> Dom Type) -> Dom Type -> Dom Type
    forall a b. (a -> b) -> a -> b
    $ Type -> Dom Type
    forall a. a -> Dom a
    defaultDom Type
    rect)

          let m :: ModuleName
    m = QName -> ModuleName
    qnameToMName QName
    name  -- Name of record module.

          -- Andreas, 2016-02-09 setting all parameters hidden in the record
          -- section telescope changes the semantics, see e.g.
          -- test/Succeed/RecordInParModule.
          -- Ulf, 2016-03-02 but it's the right thing to do (#1759)
          (forall e. Dom e -> Dom e) -> TCM () -> TCM ()
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (forall e. Dom e -> Dom e) -> tcm a -> tcm a
    modifyContextInfo forall a. LensHiding a => a -> a
    forall e. Dom e -> Dom e
    hideOrKeepInstance (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    addRecordVar (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

            -- Add the record section.

            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.def" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
              [ TCMT IO Doc
    "record section:"
              , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                [ ModuleName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ModuleName
    m 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 (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc)
    -> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope)
                , [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    m Doc -> t (m Doc) -> [m Doc]
    punctuate TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc
    comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
    forall a b. (a -> b) -> a -> b
    $ (Field -> TCMT IO Doc) -> [Field] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> (Field -> Doc) -> Field -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Arg QName] -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty ([Arg QName] -> Doc) -> (Field -> [Arg QName]) -> Field -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (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])
    -> (Field -> [Dom' Term QName]) -> Field -> [Arg QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Field -> [Dom' Term QName]
    getName) [Field]
    fields
                ]
              ]
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.def" Int
    15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
              [ TCMT IO Doc
    "field tel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible Int
    1 (Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    ftel)
              ]
            ModuleName -> TCM ()
    addSection ModuleName
    m

          -- Andreas, 2016-02-09, Issue 1815 (see also issue 1759).
          -- For checking the record declarations, hide the record parameters
          -- and the parameters of the parent modules.
          (forall e. Dom e -> Dom e) -> TCM () -> TCM ()
    forall (tcm :: * -> *) a.
    MonadTCEnv tcm =>
    (forall e. Dom e -> Dom e) -> tcm a -> tcm a
    modifyContextInfo forall a. LensHiding a => a -> a
    forall e. Dom e -> Dom e
    hideOrKeepInstance (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCM () -> TCM ()
    addRecordVar (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

            -- Check the types of the fields and the other record declarations.
            ModuleName -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
    withCurrentModule ModuleName
    m (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

              -- Andreas, 2013-09-13, 2016-01-06.
              -- Argument telescope for the projections: all parameters are hidden.
              -- This means parameters of the parent modules and of the current
              -- record type.
              -- See test/Succeed/ProjectionsTakeModuleTelAsParameters.agda.
              Telescope
    tel' <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
              ModuleName -> TCM ()
    setModuleCheckpoint ModuleName
    m
              ModuleName
    -> QName
    -> Bool
    -> ConHead
    -> Telescope
    -> Telescope
    -> [Field]
    -> TCM ()
    checkRecordProjections ModuleName
    m QName
    name Bool
    hasNamedCon ConHead
    con Telescope
    tel' Telescope
    ftel [Field]
    fields

          -- we define composition here so that the projections are already in the signature.
          Impossible -> Int -> TCM () -> TCM ()
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible Int
    npars (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
            QName
    -> ConHead
    -> Telescope
    -> [Arg QName]
    -> Telescope
    -> Type
    -> TCM ()
    addCompositionForRecord QName
    name ConHead
    con Telescope
    tel ((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]
    fs) Telescope
    ftel Type
    rect

          -- The confluence checker needs to know what symbols match against
          -- the constructor.
          (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    conName ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ \Definition
    def ->
            Definition
    def { defMatchable :: Set QName
    defMatchable = [QName] -> Set QName
    forall a. Ord a => [a] -> Set a
    Set.fromList ([QName] -> Set QName) -> [QName] -> Set QName
    forall a b. (a -> b) -> a -> b
    $ (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]
    fs }

          () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      where
      -- Andreas, 2020-04-19, issue #4560
      -- If the user declared the record constructor as @pattern@,
      -- then switch on pattern matching for no-eta-equality.
      -- Default is no pattern matching, but definition by copatterns instead.
      patCopat :: PatternOrCopattern
    patCopat = PatternOrCopattern
    -> (Range -> PatternOrCopattern)
    -> Maybe Range
    -> PatternOrCopattern
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe PatternOrCopattern
    CopatternMatching (PatternOrCopattern -> Range -> PatternOrCopattern
    forall a b. a -> b -> a
    const PatternOrCopattern
    PatternMatching) Maybe Range
    pat
      eta :: Maybe HasEta
    eta      = (PatternOrCopattern
    patCopat PatternOrCopattern -> HasEta0 -> HasEta
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) (HasEta0 -> HasEta) -> Maybe HasEta0 -> Maybe HasEta
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe HasEta0
    eta0

    addCompositionForRecord
      :: QName       -- ^ Datatype name.
      -> ConHead
      -> Telescope   -- ^ @Γ@ parameters.
      -> [Arg QName] -- ^ Projection names.
      -> Telescope   -- ^ @Γ ⊢ Φ@ field types.
      -> Type        -- ^ @Γ ⊢ T@ target type.
      -> TCM ()
    addCompositionForRecord :: QName
    -> ConHead
    -> Telescope
    -> [Arg QName]
    -> Telescope
    -> Type
    -> TCM ()
    addCompositionForRecord QName
    name ConHead
    con Telescope
    tel [Arg QName]
    fs Telescope
    ftel Type
    rect = do
      Telescope
    cxt <- TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
      TCM () -> TCM ()
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

        -- Record has no fields: attach composition data to record constructor
        if [Arg QName] -> Bool
    forall a. Null a => a -> Bool
    null [Arg QName]
    fs then do
          CompKit
    kit <- QName
    -> ConHead
    -> Telescope
    -> [QName]
    -> Telescope
    -> Type
    -> Boundary
    -> TCM CompKit
    defineCompData QName
    name ConHead
    con (Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    cxt Telescope
    tel) [] Telescope
    ftel Type
    rect []
          (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition (ConHead -> QName
    conName ConHead
    con) ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Defn -> Defn) -> Definition -> Definition
    updateTheDef ((Defn -> Defn) -> Definition -> Definition)
    -> (Defn -> Defn) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ \case
            r :: Defn
    r@Constructor{} -> Defn
    r { conComp :: CompKit
    conComp = CompKit
    kit, conProj :: Maybe [QName]
    conProj = [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just [] }  -- no projections
            Defn
    _ -> Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- Record has fields: attach composition data to record type
        else do
          -- If record has irrelevant fields but irrelevant projections are disabled,
          -- we cannot generate composition data.
          CompKit
    kit <- TCMT IO Bool -> TCM CompKit -> TCM CompKit -> TCM CompKit
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Arg QName -> Bool) -> [Arg QName] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Arg QName -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant [Arg QName]
    fs)
                      TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` do Bool -> Bool
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optIrrelevantProjections (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions)
            {-then-} (CompKit -> TCM CompKit
    forall (m :: * -> *) a. Monad m => a -> m a
    return CompKit
    emptyCompKit)
            {-else-} (QName
    -> Telescope -> Telescope -> [Arg QName] -> Type -> TCM CompKit
    defineCompKitR QName
    name (Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    cxt Telescope
    tel) Telescope
    ftel [Arg QName]
    fs Type
    rect)
          (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    name ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Defn -> Defn) -> Definition -> Definition
    updateTheDef ((Defn -> Defn) -> Definition -> Definition)
    -> (Defn -> Defn) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ \case
            r :: Defn
    r@Record{} -> Defn
    r { recComp :: CompKit
    recComp = CompKit
    kit }
            Defn
    _          -> Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    defineCompKitR ::
        QName          -- ^ some name, e.g. record name
      -> Telescope   -- ^ param types Δ
      -> Telescope   -- ^ fields' types Δ ⊢ Φ
      -> [Arg QName] -- ^ fields' names
      -> Type        -- ^ record type Δ ⊢ T
      -> TCM CompKit
    defineCompKitR :: QName
    -> Telescope -> Telescope -> [Arg QName] -> Type -> TCM CompKit
    defineCompKitR QName
    name Telescope
    params Telescope
    fsT [Arg QName]
    fns Type
    rect = do
      [Maybe Term]
    required <- ([Char] -> TCMT IO (Maybe Term))
    -> [[Char]] -> TCMT IO [Maybe Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM [Char] -> TCMT IO (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
    getTerm'
            [ [Char]
    builtinInterval
            , [Char]
    builtinIZero
            , [Char]
    builtinIOne
            , [Char]
    builtinIMin
            , [Char]
    builtinIMax
            , [Char]
    builtinINeg
            , [Char]
    builtinPOr
            , [Char]
    builtinItIsOne
            ]
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.cxt" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    params
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.cxt" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    fsT
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.cxt" Int
    30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Type
    rect
      if Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ (Maybe Term -> Bool) -> [Maybe Term] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Maybe Term -> Bool
    forall a. Maybe a -> Bool
    isJust [Maybe Term]
    required then CompKit -> TCM CompKit
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CompKit -> TCM CompKit) -> CompKit -> TCM CompKit
    forall a b. (a -> b) -> a -> b
    $ CompKit
    emptyCompKit else do
        Maybe QName
    transp <- [[Char]] -> TCMT IO (Maybe QName) -> TCMT IO (Maybe QName)
    forall {m :: * -> *} {t :: * -> *} {a}.
    (Traversable t, HasBuiltins m) =>
    t [Char] -> m (Maybe a) -> m (Maybe a)
    whenDefined [[Char]
    builtinTrans]              (TranspOrHComp
    -> QName
    -> Telescope
    -> Telescope
    -> [Arg QName]
    -> Type
    -> TCMT IO (Maybe QName)
    defineTranspOrHCompR TranspOrHComp
    DoTransp QName
    name Telescope
    params Telescope
    fsT [Arg QName]
    fns Type
    rect)
        Maybe QName
    hcomp  <- [[Char]] -> TCMT IO (Maybe QName) -> TCMT IO (Maybe QName)
    forall {m :: * -> *} {t :: * -> *} {a}.
    (Traversable t, HasBuiltins m) =>
    t [Char] -> m (Maybe a) -> m (Maybe a)
    whenDefined [[Char]
    builtinTrans,[Char]
    builtinHComp] (TranspOrHComp
    -> QName
    -> Telescope
    -> Telescope
    -> [Arg QName]
    -> Type
    -> TCMT IO (Maybe QName)
    defineTranspOrHCompR TranspOrHComp
    DoHComp QName
    name Telescope
    params Telescope
    fsT [Arg QName]
    fns Type
    rect)
        CompKit -> TCM CompKit
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CompKit -> TCM CompKit) -> CompKit -> TCM CompKit
    forall a b. (a -> b) -> a -> b
    $ CompKit :: Maybe QName -> Maybe QName -> CompKit
    CompKit
          { nameOfTransp :: Maybe QName
    nameOfTransp = Maybe QName
    transp
          , nameOfHComp :: Maybe QName
    nameOfHComp  = Maybe QName
    hcomp
          }
      where
        whenDefined :: t [Char] -> m (Maybe a) -> m (Maybe a)
    whenDefined t [Char]
    xs m (Maybe a)
    m = do
          t (Maybe Term)
    xs <- ([Char] -> m (Maybe Term)) -> t [Char] -> m (t (Maybe Term))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM [Char] -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
    getTerm' t [Char]
    xs
          if (Maybe Term -> Bool) -> t (Maybe Term) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Maybe Term -> Bool
    forall a. Maybe a -> Bool
    isJust t (Maybe Term)
    xs then m (Maybe a)
    m else Maybe a -> m (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing

    defineTranspOrHCompR ::
      TranspOrHComp
      -> QName       -- ^ some name, e.g. record name
      -> Telescope   -- ^ param types Δ
      -> Telescope   -- ^ fields' types Δ ⊢ Φ
      -> [Arg QName] -- ^ fields' names
      -> Type        -- ^ record type Δ ⊢ T
      -> TCM (Maybe QName)
    defineTranspOrHCompR :: TranspOrHComp
    -> QName
    -> Telescope
    -> Telescope
    -> [Arg QName]
    -> Type
    -> TCMT IO (Maybe QName)
    defineTranspOrHCompR TranspOrHComp
    cmd QName
    name Telescope
    params Telescope
    fsT [Arg QName]
    fns Type
    rect = do
      let project :: Term -> QName -> Term
    project = (\ Term
    t QName
    fn -> Term
    t Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    fn])
      Maybe (QName, Telescope, Type, [Dom Type], [Term])
    stuff <- (((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
     -> (QName, Telescope, Type, [Dom Type], [Term]))
    -> Maybe
         ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
    -> Maybe (QName, Telescope, Type, [Dom Type], [Term])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
    -> (QName, Telescope, Type, [Dom Type], [Term])
    forall a b. (a, b) -> a
    fst (Maybe ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
     -> Maybe (QName, Telescope, Type, [Dom Type], [Term]))
    -> TCMT
         IO
         (Maybe
            ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
    -> TCMT IO (Maybe (QName, Telescope, Type, [Dom Type], [Term]))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TranspOrHComp
    -> Maybe Term
    -> (Term -> QName -> Term)
    -> QName
    -> Telescope
    -> Telescope
    -> [Arg QName]
    -> Type
    -> TCMT
         IO
         (Maybe
            ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
    defineTranspOrHCompForFields TranspOrHComp
    cmd Maybe Term
    forall a. Maybe a
    Nothing Term -> QName -> Term
    project QName
    name Telescope
    params Telescope
    fsT [Arg QName]
    fns Type
    rect

      Maybe (QName, Telescope, Type, [Dom Type], [Term])
    -> TCMT IO (Maybe QName)
    -> ((QName, Telescope, Type, [Dom Type], [Term])
        -> TCMT IO (Maybe QName))
    -> TCMT IO (Maybe QName)
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe (QName, Telescope, Type, [Dom Type], [Term])
    stuff (Maybe QName -> TCMT IO (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe QName
    forall a. Maybe a
    Nothing) (((QName, Telescope, Type, [Dom Type], [Term])
      -> TCMT IO (Maybe QName))
     -> TCMT IO (Maybe QName))
    -> ((QName, Telescope, Type, [Dom Type], [Term])
        -> TCMT IO (Maybe QName))
    -> TCMT IO (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ \ (QName
    theName, Telescope
    gamma, Type
    rtype, [Dom Type]
    clause_types, [Term]
    bodies) -> do
      -- phi = 1 clause
      Clause
    c' <- do
               Term
    io <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIOne
               Just QName
    io_name <- [Char] -> TCMT IO (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
    getBuiltinName' [Char]
    builtinIOne
               Term
    one <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primItIsOne
               Type
    tInterval <- TCMT IO Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType
               let
                  (Int
    ix,Term
    rhs) =
                    case TranspOrHComp
    cmd of
                      -- TranspRArgs = phi : I, a0 : ..
                      -- Γ = Δ^I , CompRArgs
                      -- pats = ... | phi = i1
                      -- body = a0
                      TranspOrHComp
    DoTransp -> (Int
    1,Int -> Elims -> Term
    Var Int
    0 [])
                      -- HCompRArgs = phi : I, u : .., a0 : ..
                      -- Γ = Δ, CompRArgs
                      -- pats = ... | phi = i1
                      -- body = u i1 itIsOne
                      TranspOrHComp
    DoHComp  -> (Int
    2,Int -> Elims -> Term
    Var Int
    1 [] Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    io, Relevance -> Arg Term -> Arg Term
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    Irrelevant (Arg Term -> Arg Term) -> Arg Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    one])

                  p :: Pattern' DBPatVar
    p = ConHead
    -> ConPatternInfo
    -> [NamedArg (Pattern' DBPatVar)]
    -> Pattern' DBPatVar
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead QName
    io_name DataOrRecord
    IsData Induction
    Inductive [])
                           (ConPatternInfo
    noConPatternInfo { conPType :: Maybe (Arg Type)
    conPType = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just (ArgInfo -> Type -> Arg Type
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    defaultArgInfo Type
    tInterval)
                                             , conPFallThrough :: Bool
    conPFallThrough = Bool
    True })
                             []

                  -- gamma, rtype

                  s :: Substitution' (Pattern' DBPatVar)
    s = Int -> Pattern' DBPatVar -> Substitution' (Pattern' DBPatVar)
    forall a. DeBruijn a => Int -> a -> Substitution' a
    singletonS Int
    ix Pattern' DBPatVar
    p

                  pats :: [NamedArg DeBruijnPattern]
                  pats :: [NamedArg (Pattern' DBPatVar)]
    pats = Substitution' (Pattern' DBPatVar)
    Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
    s Substitution' (SubstArg [NamedArg (Pattern' DBPatVar)])
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Telescope -> [NamedArg (Pattern' DBPatVar)]
    forall a. DeBruijn a => Telescope -> [NamedArg a]
    teleNamedArgs Telescope
    gamma

                  t :: Type
                  t :: Type
    t = Substitution' (Pattern' DBPatVar)
    s Substitution' (Pattern' DBPatVar) -> Type -> Type
    forall a.
    TermSubst a =>
    Substitution' (Pattern' DBPatVar) -> a -> a
    `applyPatSubst` Type
    rtype

                  gamma' :: Telescope
                  gamma' :: Telescope
    gamma' = [[Char]] -> [Dom Type] -> Telescope
    unflattenTel ([[Char]]
    ns0 [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ [[Char]]
    ns1) ([Dom Type] -> Telescope) -> [Dom Type] -> Telescope
    forall a b. (a -> b) -> a -> b
    $ Substitution' (Pattern' DBPatVar)
    s Substitution' (Pattern' DBPatVar) -> [Dom Type] -> [Dom Type]
    forall a.
    TermSubst a =>
    Substitution' (Pattern' DBPatVar) -> a -> a
    `applyPatSubst` ([Dom Type]
    g0 [Dom Type] -> [Dom Type] -> [Dom Type]
    forall a. [a] -> [a] -> [a]
    ++ [Dom Type]
    g1)
                   where
                    ([Dom Type]
    g0,Dom Type
    _:[Dom Type]
    g1) = Int -> [Dom Type] -> ([Dom Type], [Dom Type])
    forall a. Int -> [a] -> ([a], [a])
    splitAt (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    gamma Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    ix) ([Dom Type] -> ([Dom Type], [Dom Type]))
    -> [Dom Type] -> ([Dom Type], [Dom Type])
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Telescope
    gamma
                    ([[Char]]
    ns0,[Char]
    _:[[Char]]
    ns1) = Int -> [[Char]] -> ([[Char]], [[Char]])
    forall a. Int -> [a] -> ([a], [a])
    splitAt (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    gamma Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    ix) ([[Char]] -> ([[Char]], [[Char]]))
    -> [[Char]] -> ([[Char]], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [[Char]]
    teleNames Telescope
    gamma

                  c :: Clause
    c = Clause :: Range
    -> Range
    -> Telescope
    -> [NamedArg (Pattern' DBPatVar)]
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Bool
    -> Maybe Bool
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Clause
    Clause { clauseTel :: Telescope
    clauseTel       = Telescope
    gamma'
                             , clauseType :: Maybe (Arg Type)
    clauseType      = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> Arg Type
    forall e. e -> Arg e
    argN Type
    t
                             , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
    namedClausePats = [NamedArg (Pattern' DBPatVar)]
    pats
                             , clauseFullRange :: Range
    clauseFullRange = Range
    forall a. Range' a
    noRange
                             , clauseLHSRange :: Range
    clauseLHSRange  = Range
    forall a. Range' a
    noRange
                             , clauseCatchall :: Bool
    clauseCatchall  = Bool
    False
                             , clauseBody :: Maybe Term
    clauseBody      = Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Term -> Maybe Term) -> Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Term
    rhs
                             , clauseExact :: Maybe Bool
    clauseExact       = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
                             , clauseRecursive :: Maybe Bool
    clauseRecursive   = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False  -- definitely non-recursive!
                             , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
                             , clauseEllipsis :: ExpandedEllipsis
    clauseEllipsis  = ExpandedEllipsis
    NoEllipsis
                             }
               [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "trans.rec.face" Int
    17 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Clause -> [Char]
    forall a. Show a => a -> [Char]
    show Clause
    c
               Clause -> TCMT IO Clause
    forall (m :: * -> *) a. Monad m => a -> m a
    return Clause
    c
      [Clause]
    cs <- [(Arg QName, Dom Type, Term)]
    -> ((Arg QName, Dom Type, Term) -> TCMT IO Clause)
    -> TCMT IO [Clause]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM ([Arg QName]
    -> [Dom Type] -> [Term] -> [(Arg QName, Dom Type, Term)]
    forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
    zip3 [Arg QName]
    fns [Dom Type]
    clause_types [Term]
    bodies) (((Arg QName, Dom Type, Term) -> TCMT IO Clause)
     -> TCMT IO [Clause])
    -> ((Arg QName, Dom Type, Term) -> TCMT IO Clause)
    -> TCMT IO [Clause]
    forall a b. (a -> b) -> a -> b
    $ \ (Arg QName
    fname, Dom Type
    clause_ty, Term
    body) -> do
              let
                  pats :: [NamedArg (Pattern' DBPatVar)]
    pats = Telescope -> [NamedArg (Pattern' DBPatVar)]
    forall a. DeBruijn a => Telescope -> [NamedArg a]
    teleNamedArgs Telescope
    gamma [NamedArg (Pattern' DBPatVar)]
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a. [a] -> [a] -> [a]
    ++ [Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar)
    forall a. a -> NamedArg a
    defaultNamedArg (Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar))
    -> Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar)
    forall a b. (a -> b) -> a -> b
    $ ProjOrigin -> QName -> Pattern' DBPatVar
    forall x. ProjOrigin -> QName -> Pattern' x
    ProjP ProjOrigin
    ProjSystem (QName -> Pattern' DBPatVar) -> QName -> Pattern' DBPatVar
    forall a b. (a -> b) -> a -> b
    $ Arg QName -> QName
    forall e. Arg e -> e
    unArg Arg QName
    fname]
                  c :: Clause
    c = Clause :: Range
    -> Range
    -> Telescope
    -> [NamedArg (Pattern' DBPatVar)]
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Bool
    -> Maybe Bool
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Clause
    Clause { clauseTel :: Telescope
    clauseTel       = Telescope
    gamma
                             , clauseType :: Maybe (Arg Type)
    clauseType      = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> Arg Type
    forall e. e -> Arg e
    argN (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    clause_ty)
                             , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
    namedClausePats = [NamedArg (Pattern' DBPatVar)]
    pats
                             , clauseFullRange :: Range
    clauseFullRange = Range
    forall a. Range' a
    noRange
                             , clauseLHSRange :: Range
    clauseLHSRange  = Range
    forall a. Range' a
    noRange
                             , clauseCatchall :: Bool
    clauseCatchall  = Bool
    False
                             , clauseBody :: Maybe Term
    clauseBody      = Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    body
                             , clauseExact :: Maybe Bool
    clauseExact       = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
                             , clauseRecursive :: Maybe Bool
    clauseRecursive   = Maybe Bool
    forall a. Maybe a
    Nothing
                                 -- Andreas 2020-02-06 TODO
                                 -- Or: Just False;  is it known to be non-recursive?
                             , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
                             , clauseEllipsis :: ExpandedEllipsis
    clauseEllipsis  = ExpandedEllipsis
    NoEllipsis
                             }
              [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "trans.rec" Int
    17 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Clause -> [Char]
    forall a. Show a => a -> [Char]
    show Clause
    c
              [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "trans.rec" Int
    16 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "type =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (Maybe (Arg Type) -> [Char]
    forall a. Show a => a -> [Char]
    show (Clause -> Maybe (Arg Type)
    clauseType Clause
    c))
              [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "trans.rec" Int
    15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Type -> TCMT IO Doc) -> Type -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Type -> Type
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    gamma (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    clause_ty)
              [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "trans.rec" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "body =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Telescope -> Term -> Term
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    gamma Term
    body)
              Clause -> TCMT IO Clause
    forall (m :: * -> *) a. Monad m => a -> m a
    return Clause
    c
      QName -> [Clause] -> TCM ()
    addClauses QName
    theName ([Clause] -> TCM ()) -> [Clause] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Clause
    c' Clause -> [Clause] -> [Clause]
    forall a. a -> [a] -> [a]
    : [Clause]
    cs
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "trans.rec" Int
    15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "compiling clauses for " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Show a => a -> [Char]
    show QName
    theName
      (Maybe SplitTree
    mst, Bool
    _, CompiledClauses
    cc) <- TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (Maybe (QName, Type)
    -> [Clause] -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    compileClauses Maybe (QName, Type)
    forall a. Maybe a
    Nothing [Clause]
    cs)
      Maybe SplitTree -> (SplitTree -> TCM ()) -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust Maybe SplitTree
    mst ((SplitTree -> TCM ()) -> TCM ())
    -> (SplitTree -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> SplitTree -> TCM ()
    setSplitTree QName
    theName
      QName -> CompiledClauses -> TCM ()
    setCompiledClauses QName
    theName CompiledClauses
    cc
      [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "trans.rec" Int
    15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "compiled"
      Maybe QName -> TCMT IO (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe QName -> TCMT IO (Maybe QName))
    -> Maybe QName -> TCMT IO (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    theName

    {-| @checkRecordProjections m r q tel ftel fs@.

        [@m@    ]  name of the generated module

        [@r@    ]  name of the record type

        [@con@  ]  name of the record constructor

        [@tel@  ]  parameters and record variable r ("self")

        [@ftel@ ]  telescope of fields

        [@fs@   ]  the fields to be checked
    -}
    checkRecordProjections ::
      ModuleName -> QName -> Bool -> ConHead -> Telescope -> Telescope ->
      [A.Declaration] -> TCM ()
    checkRecordProjections :: ModuleName
    -> QName
    -> Bool
    -> ConHead
    -> Telescope
    -> Telescope
    -> [Field]
    -> TCM ()
    checkRecordProjections ModuleName
    m QName
    r Bool
    hasNamedCon ConHead
    con Telescope
    tel Telescope
    ftel [Field]
    fs = do
        Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
    checkProjs Telescope
    forall a. Tele a
    EmptyTel Telescope
    ftel [] [Field]
    fs
      where

        checkProjs :: Telescope -> Telescope -> [Term] -> [A.Declaration] -> TCM ()

        checkProjs :: Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
    checkProjs Telescope
    _ Telescope
    _ [Term]
    _ [] = () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

        checkProjs Telescope
    ftel1 Telescope
    ftel2 [Term]
    vs (A.ScopedDecl ScopeInfo
    scope [Field]
    fs' : [Field]
    fs) =
          ScopeInfo -> TCM ()
    setScope ScopeInfo
    scope TCM () -> TCM () -> TCM ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
    checkProjs Telescope
    ftel1 Telescope
    ftel2 [Term]
    vs ([Field]
    fs' [Field] -> [Field] -> [Field]
    forall a. [a] -> [a] -> [a]
    ++ [Field]
    fs)

        -- Case: projection.
        checkProjs Telescope
    ftel1 (ExtendTel (dom :: Dom Type
    dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    ai,unDom :: forall t e. Dom' t e -> e
    unDom = Type
    t}) Abs Telescope
    ftel2) [Term]
    vs (A.Field DefInfo
    info QName
    x Arg Expr
    _ : [Field]
    fs) =
          Call -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> QName -> Type -> Call
    CheckProjection (DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    info) QName
    x Type
    t) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          -- Andreas, 2012-06-07:
          -- Issue 387: It is wrong to just type check field types again
          -- because then meta variables are created again.
          -- Instead, we take the field type t from the field telescope.
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Int
    5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "checking projection" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    x
            , 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
    "top   =" 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 (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc)
    -> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope)
              , TCMT IO Doc
    "tel   =" 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 (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc)
    -> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope
    tel)
              ]
            ]
          -- Andreas, 2021-05-11, issue #5378
          -- The impossible is sometimes possible, so splitting out this part...
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Int
    5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
              [ TCMT IO Doc
    "ftel1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible Int
    1 (Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    ftel1)
              , TCMT IO Doc
    "t     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible Int
    1 (Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    ftel1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t)
              , TCMT IO Doc
    "ftel2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Impossible -> Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible Int
    1 (Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    ftel1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Dom Type
    -> Abs Telescope -> (Telescope -> TCMT IO Doc) -> TCMT IO Doc
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction Dom Type
    dom Abs Telescope
    ftel2 Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM)
              ]
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Int
    55 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
              [ TCMT IO Doc
    "ftel1 (raw) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Telescope
    ftel1
              , TCMT IO Doc
    "t     (raw) =" 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
              , TCMT IO Doc
    "ftel2 (raw) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Abs Telescope -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Abs Telescope
    ftel2
              ]
          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Int
    5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
              [ TCMT IO Doc
    "vs    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Semigroup (m Doc), Foldable t) =>
    t (m Doc) -> m Doc
    prettyList_ ((Term -> TCMT IO Doc) -> [Term] -> [TCMT IO Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Term]
    vs)
              , TCMT IO Doc
    "abstr =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (IsAbstract -> [Char]) -> IsAbstract -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IsAbstract -> [Char]
    forall a. Show a => a -> [Char]
    show) (DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    info)
              , TCMT IO Doc
    "quant =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (Quantity -> [Char]) -> Quantity -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Quantity -> [Char]
    forall a. Show a => a -> [Char]
    show) (ArgInfo -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity ArgInfo
    ai)
              , TCMT IO Doc
    "coh   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ([Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text ([Char] -> TCMT IO Doc)
    -> (Cohesion -> [Char]) -> Cohesion -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Cohesion -> [Char]
    forall a. Show a => a -> [Char]
    show) (ArgInfo -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion ArgInfo
    ai)
              ]

          -- Cohesion check:
          -- For a field `@c π : A` we would create a projection `π : .., (@(c^-1) r : R as) -> A`
          -- So we want to check that `@.., (c^-1 . c) x : A |- x : A` is allowed by the modalities.
          --
          -- Alternatively we could create a projection `.. |- π r :c A`
          -- but that would require support for a `t :c A` judgment.
          if UnderComposition Cohesion -> Bool
    forall a. LeftClosedPOMonoid a => a -> Bool
    hasLeftAdjoint (Cohesion -> UnderComposition Cohesion
    forall t. t -> UnderComposition t
    UnderComposition (ArgInfo -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion ArgInfo
    ai))
            then Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (ArgInfo -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion ArgInfo
    ai Cohesion -> Cohesion -> Bool
    forall a. Eq a => a -> a -> Bool
    == Cohesion
    Continuous)
                        -- Andrea TODO: properly update the context/type of the projection when we add Sharp
                        TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            else [Char] -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    [Char] -> m a
    genericError ([Char] -> TCM ()) -> [Char] -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Cannot have record fields with modality " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Cohesion -> [Char]
    forall a. Show a => a -> [Char]
    show (ArgInfo -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion ArgInfo
    ai)

          -- The telescope tel includes the variable of record type as last one
          -- e.g. for cartesion product it is
          --
          --   tel = {A' : Set} {B' : Set} (r : Prod A' B')

          -- create the projection functions (instantiate the type with the values
          -- of the previous fields)

          -- The type of the projection function should be
          --  {Δ} -> (r : R Δ) -> t
          -- where Δ are the parameters of R

          {- what are the contexts?

              Δ , ftel₁              ⊢ t
              Δ , (r : R Δ)          ⊢ parallelS vs : ftel₁
              Δ , (r : R Δ) , ftel₁  ⊢ t' = raiseFrom (size ftel₁) 1 t
              Δ , (r : R Δ)          ⊢ t'' = applySubst (parallelS vs) t'
                                     ⊢ finalt = telePi tel t''
          -}
          let t' :: Type
    t'       = Int -> Int -> Type -> Type
    forall a. Subst a => Int -> Int -> a -> a
    raiseFrom (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    ftel1) Int
    1 Type
    t
              t'' :: Type
    t''      = Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst ([Term] -> Substitution
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS [Term]
    vs) Type
    t'
              finalt :: Type
    finalt   = Telescope -> Type -> Type
    telePi ([Char] -> Telescope -> Telescope
    forall a. [Char] -> Tele a -> Tele a
    replaceEmptyName [Char]
    "r" Telescope
    tel) Type
    t''
              projname :: QName
    projname = ModuleName -> Name -> QName
    qualify ModuleName
    m (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    x
              projcall :: ProjOrigin -> Term
    projcall ProjOrigin
    o = Int -> Elims -> Term
    Var Int
    0 [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o QName
    projname]
              rel :: Relevance
    rel      = ArgInfo -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance ArgInfo
    ai
              -- the recursive call
              recurse :: TCM ()
    recurse  = Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
    checkProjs (Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    ftel1 (Telescope -> Telescope) -> Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Abs Telescope -> Telescope
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    dom
                                     (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Telescope -> Abs Telescope
    forall a. [Char] -> a -> Abs a
    Abs (Name -> [Char]
    nameToArgName (Name -> [Char]) -> Name -> [Char]
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    projname) Telescope
    forall a. Tele a
    EmptyTel)
                                    (Abs Telescope -> Telescope
    forall a. Subst a => Abs a -> a
    absBody Abs Telescope
    ftel2) (ProjOrigin -> Term
    projcall ProjOrigin
    ProjSystem Term -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    : [Term]
    vs) [Field]
    fs

          [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Int
    25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "finalt=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do
            TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    finalt

          -- -- Andreas, 2012-02-20 do not add irrelevant projections if
          -- -- disabled by --no-irrelevant-projections
          -- ifM (return (rel == Irrelevant) `and2M` do not . optIrrelevantProjections <$> pragmaOptions) recurse $ do
          -- Andreas, 2018-06-09 issue #2170
          -- Always create irrelevant projections (because the scope checker accepts irrelevant fields).
          -- If --no-irrelevant-projections, then their use should be disallowed by the type checker for expressions.
          do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
              [ TCMT IO Doc
    "adding projection"
              , 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
    $ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    projname 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
    <+> TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    finalt)
              ]

            -- The body should be
            --  P.xi {tel} (r _ .. x .. _) = x
            -- Ulf, 2011-08-22: actually we're dropping the parameters from the
            -- projection functions so the body is now
            --  P.xi (r _ .. x .. _) = x
            -- Andreas, 2012-01-12: irrelevant projections get translated to
            --  P.xi (r _ .. x .. _) = irrAxiom {level of t} {t} x
            -- PROBLEM: because of dropped parameters, cannot refer to t
            -- 2012-04-02: DontCare instead of irrAxiom

            -- compute body modification for irrelevant projections
            let bodyMod :: Term -> Term
    bodyMod = case Relevance
    rel of
                  Relevance
    Relevant   -> Term -> Term
    forall a. a -> a
    id
                  Relevance
    NonStrict  -> Term -> Term
    forall a. a -> a
    id
                  Relevance
    Irrelevant -> Term -> Term
    dontCare

            let -- Andreas, 2010-09-09: comment for existing code
                -- split the telescope into parameters (ptel) and the type or the record
                -- (rt) which should be  R ptel
                telList :: [Dom ([Char], Type)]
    telList = Telescope -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    tel
                ([Dom ([Char], Type)]
    ptelList,[Dom ([Char], Type)
    rt]) = Int
    -> [Dom ([Char], Type)]
    -> ([Dom ([Char], Type)], [Dom ([Char], Type)])
    forall a. Int -> [a] -> ([a], [a])
    splitAt (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) [Dom ([Char], Type)]
    telList
                ptel :: Telescope
    ptel   = [Dom ([Char], Type)] -> Telescope
    telFromList [Dom ([Char], Type)]
    ptelList
                cpo :: PatOrigin
    cpo    = if Bool
    hasNamedCon then PatOrigin
    PatOCon else PatOrigin
    PatORec
                cpi :: ConPatternInfo
    cpi    = ConPatternInfo :: PatternInfo
    -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
    ConPatternInfo { conPInfo :: PatternInfo
    conPInfo   = PatOrigin -> [Name] -> PatternInfo
    PatternInfo PatOrigin
    cpo []
                                        , conPRecord :: Bool
    conPRecord = Bool
    True
                                        , conPFallThrough :: Bool
    conPFallThrough = Bool
    False
                                        , conPType :: Maybe (Arg Type)
    conPType   = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom (Dom Type -> Arg Type) -> Dom Type -> Arg Type
    forall a b. (a -> b) -> a -> b
    $ (([Char], Type) -> Type) -> Dom ([Char], Type) -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Char], Type) -> Type
    forall a b. (a, b) -> b
    snd Dom ([Char], Type)
    rt
                                        , conPLazy :: Bool
    conPLazy   = Bool
    True }
                conp :: NamedArg (Pattern' DBPatVar)
    conp   = Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar)
    forall a. a -> NamedArg a
    defaultNamedArg (Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar))
    -> Pattern' DBPatVar -> NamedArg (Pattern' DBPatVar)
    forall a b. (a -> b) -> a -> b
    $ ConHead
    -> ConPatternInfo
    -> [NamedArg (Pattern' DBPatVar)]
    -> Pattern' DBPatVar
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    con ConPatternInfo
    cpi ([NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar)
    -> [NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [NamedArg (Pattern' DBPatVar)]
    forall a. DeBruijn a => Telescope -> [NamedArg a]
    teleNamedArgs Telescope
    ftel
                body :: Maybe Term
    body   = Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Term -> Maybe Term) -> Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Term
    bodyMod (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var (Abs Telescope -> Int
    forall a. Sized a => a -> Int
    size Abs Telescope
    ftel2)
                cltel :: Telescope
    cltel  = Telescope
    ptel Telescope -> Telescope -> Telescope
    forall t. Abstract t => Telescope -> t -> t
    `abstract` Telescope
    ftel
                cltype :: Maybe (Arg Type)
    cltype = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Type -> Arg Type
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Type -> Arg Type) -> Type -> Arg Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Type -> Type
    forall a. Subst a => Int -> a -> a
    raise (Int
    1 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Abs Telescope -> Int
    forall a. Sized a => a -> Int
    size Abs Telescope
    ftel2) Type
    t
                clause :: Clause
    clause = Clause :: Range
    -> Range
    -> Telescope
    -> [NamedArg (Pattern' DBPatVar)]
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Bool
    -> Maybe Bool
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Clause
    Clause { clauseLHSRange :: Range
    clauseLHSRange  = DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    info
                                , clauseFullRange :: Range
    clauseFullRange = DefInfo -> Range
    forall a. HasRange a => a -> Range
    getRange DefInfo
    info
                                , clauseTel :: Telescope
    clauseTel       = Telescope -> Telescope
    forall a. KillRange a => KillRangeT a
    killRange Telescope
    cltel
                                , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
    namedClausePats = [NamedArg (Pattern' DBPatVar)
    conp]
                                , clauseBody :: Maybe Term
    clauseBody      = Maybe Term
    body
                                , clauseType :: Maybe (Arg Type)
    clauseType      = Maybe (Arg Type)
    cltype
                                , clauseCatchall :: Bool
    clauseCatchall  = Bool
    False
                                , clauseExact :: Maybe Bool
    clauseExact       = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
                                , clauseRecursive :: Maybe Bool
    clauseRecursive   = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
                                , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
                                , clauseEllipsis :: ExpandedEllipsis
    clauseEllipsis  = ExpandedEllipsis
    NoEllipsis
                                }

            let projection :: Projection
    projection = Projection :: Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> Projection
    Projection
                  { projProper :: Maybe QName
    projProper   = QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    r
                  , projOrig :: QName
    projOrig     = QName
    projname
                  -- name of the record type:
                  , projFromType :: Arg QName
    projFromType = QName -> Arg QName
    forall e. e -> Arg e
    defaultArg QName
    r
                  -- index of the record argument (in the type),
                  -- start counting with 1:
                  , projIndex :: Int
    projIndex    = Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel -- which is @size ptel + 1@
                  , projLams :: ProjLams
    projLams     = [Arg [Char]] -> ProjLams
    ProjLams ([Arg [Char]] -> ProjLams) -> [Arg [Char]] -> ProjLams
    forall a b. (a -> b) -> a -> b
    $ (Dom ([Char], Type) -> Arg [Char])
    -> [Dom ([Char], Type)] -> [Arg [Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (Dom' Term [Char] -> Arg [Char]
    forall t a. Dom' t a -> Arg a
    argFromDom (Dom' Term [Char] -> Arg [Char])
    -> (Dom ([Char], Type) -> Dom' Term [Char])
    -> Dom ([Char], Type)
    -> Arg [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (([Char], Type) -> [Char])
    -> Dom ([Char], Type) -> Dom' Term [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Char], Type) -> [Char]
    forall a b. (a, b) -> a
    fst) [Dom ([Char], Type)]
    telList
                  }

            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Int
    70 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
              [ TCMT IO Doc
    "adding projection"
              , 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
    $ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    projname TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Clause -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Clause
    clause
              ]
            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Int
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
              [ TCMT IO Doc
    "adding projection"
              , 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
    $ QNamed Clause -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (QName -> Clause -> QNamed Clause
    forall a. QName -> a -> QNamed a
    QNamed QName
    projname Clause
    clause)
              ]

                  -- Record patterns should /not/ be translated when the
                  -- projection functions are defined. Record pattern
                  -- translation is defined in terms of projection
                  -- functions.
            (Maybe SplitTree
    mst, Bool
    _, CompiledClauses
    cc) <- Maybe (QName, Type)
    -> [Clause] -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    compileClauses Maybe (QName, Type)
    forall a. Maybe a
    Nothing [Clause
    clause]

            [Char] -> Int -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Int -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.cc" Int
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "compiled clauses of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    projname
                  , 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
    $ [Char] -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text (CompiledClauses -> [Char]
    forall a. Show a => a -> [Char]
    show CompiledClauses
    cc)
                  ]

            Impossible -> Int -> TCM () -> TCM ()
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Int -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              Language
    lang <- TCMT IO Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
              QName -> Definition -> TCM ()
    addConstant QName
    projname (Definition -> TCM ()) -> Definition -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
    defaultDefn ArgInfo
    ai QName
    projname (Type -> Type
    forall a. KillRange a => KillRangeT a
    killRange Type
    finalt) Language
    lang
                  Defn
    emptyFunction
                    { funClauses :: [Clause]
    funClauses        = [Clause
    clause]
                    , funCompiled :: Maybe CompiledClauses
    funCompiled       = CompiledClauses -> Maybe CompiledClauses
    forall a. a -> Maybe a
    Just CompiledClauses
    cc
                    , funSplitTree :: Maybe SplitTree
    funSplitTree      = Maybe SplitTree
    mst
                    , funProjection :: Maybe Projection
    funProjection     = Projection -> Maybe Projection
    forall a. a -> Maybe a
    Just Projection
    projection
                    , funMutual :: Maybe [QName]
    funMutual         = [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just []  -- Projections are not mutually recursive with anything
                    , funTerminates :: Maybe Bool
    funTerminates     = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
                    })
                  { defArgOccurrences :: [Occurrence]
    defArgOccurrences = [Occurrence
    StrictPos]
                  , defCopatternLHS :: Bool
    defCopatternLHS   = CompiledClauses -> Bool
    hasProjectionPatterns CompiledClauses
    cc
                  }
              [QName] -> TCM ()
    forall (m :: * -> *).
    (HasOptions m, HasConstInfo m, HasBuiltins m, MonadTCEnv m,
     MonadTCState m, MonadReduce m, MonadAddContext m, MonadTCError m,
     MonadDebug m, MonadPretty m) =>
    [QName] -> m ()
    computePolarity [QName
    projname]

            case DefInfo -> IsInstance
    forall t. DefInfo' t -> IsInstance
    Info.defInstance DefInfo
    info of
              -- fields do not have an @instance@ keyword!?
              InstanceDef Range
    _r -> QName -> Type -> TCM ()
    addTypedInstance QName
    projname Type
    t
              IsInstance
    NotInstanceDef -> () -> TCM ()
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

            TCM ()
    recurse

        -- Case: definition.
        checkProjs Telescope
    ftel1 Telescope
    ftel2 [Term]
    vs (Field
    d : [Field]
    fs) = do
          Field -> TCM ()
    checkDecl Field
    d
          Telescope -> Telescope -> [Term] -> [Field] -> TCM ()
    checkProjs Telescope
    ftel1 Telescope
    ftel2 [Term]
    vs [Field]
    fs