    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation   #-}

    module Agda.TypeChecking.Rules.Record where

    import Prelude hiding (null, not, (&&), (||))

    import Data.Maybe
    import qualified Data.Set as Set

    import Agda.Interaction.Options

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

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Primitive
    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.CompiledClause (hasProjectionPatterns)
    import Agda.TypeChecking.CompiledClause.Compile
    import Agda.TypeChecking.InstanceArguments

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

    import Agda.Utils.Boolean
    import Agda.Utils.Function ( applyWhen )
    import Agda.Utils.Lens
    import Agda.Utils.List (headWithDefault)
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import qualified Agda.Syntax.Common.Pretty as P
    import Agda.Utils.Size

    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@ -> dummy).
    --                 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@ -> dummy).
                                   --   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 (Ranged HasEta0)
    eta0 Maybe Range
    pat RecordConName
    con) (A.DataDefParams Set Name
    gpars [LamBinding]
    ps) Expr
    contel0 [Field]
    fields = do

      -- Andreas, 2022-10-06, issue #6165:
      -- The target type of the constructor is a meaningless dummy expression which does not type-check.
      -- We replace it by Set/Type (builtinSet) which is still incorrect but type-checks.
      -- It will be fixed after type-checking.
      aType <- QName -> Expr
    A.Def (QName -> Expr) -> (Maybe QName -> QName) -> Maybe QName -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> Expr) -> TCMT IO (Maybe QName) -> TCMT IO Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> TCMT IO (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinSet
      let contel = PiView -> Expr
    A.unPiView (PiView -> Expr) -> (Expr -> PiView) -> Expr -> Expr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (\ (A.PiView [(ExprInfo, Telescope1)]
    tels Expr
    _) -> [(ExprInfo, Telescope1)] -> Expr -> PiView
    A.PiView [(ExprInfo, Telescope1)]
    tels Expr
    aType) (PiView -> PiView) -> (Expr -> PiView) -> Expr -> PiView
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Expr -> PiView
    A.piView (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ Expr
    contel0

      traceCall (CheckRecDef (getRange name) name ps fields) $ do
        reportSDoc "tc.rec" 10 $ vcat
          [ "checking record def" <+> prettyTCM name
          , nest 2 $ "ps ="     <+> prettyList (map prettyA ps)
          , nest 2 $ "contel =" <+> prettyA contel
          , nest 2 $ "fields =" <+> prettyA (map Constr fields)
          ]
        -- get type of record
        def <- instantiateDef =<< getConstInfo name
        t   <- instantiateFull $ defType def
        let npars =
              case Definition -> Defn
    theDef Definition
    def of
                DataOrRecSig Nat
    n -> Nat
    n
                Defn
    _              -> Nat
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- If the record type is erased, then hard compile-time mode is
        -- entered.
        setHardCompileTimeModeIfErased' def $ do

        parNames <- getGeneralizedParameters gpars name

        bindGeneralizedParameters parNames t $ \ Telescope
    gtel Type
    t0 ->
         Nat
    -> [LamBinding] -> Type -> (Telescope -> Type -> TCM ()) -> TCM ()
    forall a.
    Nat
    -> [LamBinding] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
    bindParameters (Nat
    npars Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - [Maybe Name] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    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] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec" Nat
    15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "checking fields"
          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
          reportSDoc "tc.rec" 20 $ vcat
            [ "contype = " <+> prettyTCM contype ]

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

          -- Compute correct type of constructor

          -- t = tel -> t0 where t0 must be a sort s
          TelV idxTel s <- telView t0
          unless (null idxTel) $ typeError $ ShouldBeASort t0
          s <- forceSort s

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

          reportSDoc "tc.rec" 20 $ do
            gamma <- getContextTelescope  -- the record params (incl. module params)
            "gamma = " <+> inTopContext (prettyTCM gamma)

          -- record type (name applied to parameters)
          rect <- El s . Def name . map Apply <$> 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 = Telescope -> Type -> Type
    telePi_ Telescope
    ftel (Nat -> Type -> Type
    forall a. Subst a => Nat -> a -> a
    raise (Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    ftel) Type
    rect)
            -- NB: contype does not contain the parameter telescope

          -- Obtain name of constructor (if present).
          (hasNamedCon, conName) <- case con of
            A.NamedRecCon QName
    c -> (Bool, QName) -> TCMT IO (Bool, QName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    True, QName
    c)
            A.FreshRecCon QName
    c -> (Bool, QName) -> TCMT IO (Bool, QName)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    False, QName
    c)

          -- Add record type to signature.
          reportSDoc "tc.rec" 15 $ "adding record type to signature"

          etaenabled <- etaEnabled

          let getName :: A.Declaration -> [Dom QName]
              getName (A.Field DefInfo
    _ QName
    x Arg Expr
    arg)    = [QName
    x QName -> Dom' Term Expr -> Dom' Term QName
    forall a b. a -> Dom' Term b -> Dom' Term a
    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 Dom' t e
    f = Dom' t e
    f { domTactic = domTactic dom }

              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 = 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 -> 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.
              noEta    = HasEta -> EtaEquality
    Inferred (HasEta -> EtaEquality) -> HasEta -> EtaEquality
    forall a b. (a -> b) -> a -> b
    $ PatternOrCopattern -> HasEta
    forall a. a -> HasEta' a
    NoEta PatternOrCopattern
    patCopat
              haveEta0 = EtaEquality
    -> (HasEta -> EtaEquality) -> Maybe HasEta -> EtaEquality
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe EtaEquality
    noEta HasEta -> EtaEquality
    Specified Maybe HasEta
    eta
              con = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead QName
    conName (PatternOrCopattern -> DataOrRecord
    forall p. p -> DataOrRecord' p
    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
                | Just NoEta{} <- Maybe HasEta
    eta         = Relevance
    relevant
                | Induction
    CoInductive <- Induction
    conInduction = Relevance
    relevant
                | [Dom ([Char], Type)] -> Bool
    forall a. Null a => a -> Bool
    null (Telescope -> [Dom ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    ftel)       = Relevance
    relevant    -- #6270: eta unit types don't need to be irrelevant
                | Bool
    otherwise                   = [Relevance] -> Relevance
    forall a. Ord a => [a] -> a
    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
          -- Andreas, 2024-06-14, PR #7300
          -- Just make this a deadcode warning.
          haveEta <-
            if (conInduction == CoInductive && theEtaEquality haveEta0 == YesEta) then do
              noEta <$ do
                setCurrentRange eta0 $ warning $ CoinductiveEtaRecord name
            else pure haveEta0
          reportSDoc "tc.rec" 30 $ "record constructor is " <+> prettyTCM con

          -- 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 = Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    tel
              telh  = (Dom Type -> Dom Type) -> Telescope -> Telescope
    forall a b. (a -> b) -> Tele a -> Tele b
    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
          escapeContext impossible npars $ do
            addConstant' name defaultArgInfo t $
                Record
                  { recPars           = npars
                  , recClause         = Nothing
                  , recConHead        = con
                  , recNamedCon       = hasNamedCon
                  , recFields         = fs
                  , recTel            = telh `abstract` ftel
                  , recAbstr          = Info.defAbstract i
                  , recEtaEquality'   = haveEta
                  , recPatternMatching= patCopat
                  , recInduction      = indCo
                      -- We retain the original user declaration [(co)inductive]
                      -- in case the record turns out to be recursive.
                  -- Determined by positivity checker:
                  , recMutual         = Nothing
                  -- Determined by the termination checker:
                  , recTerminates     = Nothing
                  , recComp           = emptyCompKit -- filled in later
                  }

            erasure <- optErasure <$> pragmaOptions
            -- Add record constructor to signature
            addConstant' conName defaultArgInfo
                 -- If --erasure is used, then the parameters are erased
                 -- in the constructor's type.
                (applyWhen erasure (fmap $ applyQuantity zeroQuantity) telh
                 `abstract` contype) $
                Constructor
                  { conPars   = npars
                  , conArity  = size fs
                  , conSrcCon = con
                  , conData   = name
                  , conAbstr  = Info.defAbstract i
                  , conComp   = emptyCompKit  -- filled in later
                  , conProj   = Nothing       -- filled in later
                  , conForced = []
                  , conErased = Nothing
                  , conErasure = erasure
                  , conInline  = False
                  }

          -- Declare the constructor as eligible for instance search
          case Info.defInstance i of
            InstanceDef KwRange
    r -> KwRange -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange KwRange
    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 a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

          -- Check that the fields fit inside the sort
          _ <- fitsIn IsRecord_ conName uc [] contype s

          -- Check that the sort admits record declarations.
          checkDataSort name 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 = Relevance -> ArgInfo -> ArgInfo
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    recordRelevance ArgInfo
    defaultArgInfo
              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 = QName -> ModuleName
    qnameToMName QName
    name  -- Name of record module.

          eraseRecordParameters <- optEraseRecordParameters <$> pragmaOptions
          let maybeErase :: forall a. LensQuantity a => a -> a
              maybeErase | Bool
    eraseRecordParameters = Quantity -> a -> a
    forall a. LensQuantity a => Quantity -> a -> a
    setQuantity Quantity
    zeroQuantity
                         | Bool
    otherwise             = a -> a
    forall a. a -> a
    id

          -- 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)
          modifyContextInfo (hideOrKeepInstance . maybeErase) $ addRecordVar $ do

            -- Add the record section.

            reportSDoc "tc.rec.def" 10 $ sep
              [ "record section:"
              , nest 2 $ sep
                [ prettyTCM m <+> (inTopContext . prettyTCM =<< getContextTelescope)
                , fsep $ punctuate comma $ map (return . P.pretty . map argFromDom . getName) fields
                ]
              ]
            reportSDoc "tc.rec.def" 15 $ nest 2 $ vcat
              [ "field tel =" <+> escapeContext impossible 1 (prettyTCM ftel)
              ]
            addSection 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.
          modifyContextInfo (hideOrKeepInstance . maybeErase) $ do
            -- If --erasure is used, then the parameters are erased in the
            -- types of the projections.
            erasure <- optErasure <$> pragmaOptions
            params  <- applyWhen erasure (fmap $ applyQuantity zeroQuantity) <$> getContext

            -- Check the types of the fields and the other record declarations.
            addRecordVar $ withCurrentModule m $ 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.
              tel' <- do
                r <- headWithDefault __IMPOSSIBLE__ <$> getContext
                return $ contextToTel $ r : params
              setModuleCheckpoint m
              checkRecordProjections m name hasNamedCon con tel' ftel fields

          -- we define composition here so that the projections are already in the signature.
          whenM cubicalCompatibleOption do
            escapeContext impossible npars do
              addCompositionForRecord name haveEta con tel (map argFromDom fs) ftel rect

          -- The confluence checker needs to know what symbols match against
          -- the constructor.
          modifySignature $ updateDefinition conName $ \Definition
    def ->
            Definition
    def { defMatchable = Set.fromList $ map unDom fs }

      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 a b. a -> HasEta' b -> HasEta' a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$) (HasEta0 -> HasEta)
    -> (Ranged HasEta0 -> HasEta0) -> Ranged HasEta0 -> HasEta
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Ranged HasEta0 -> HasEta0
    forall a. Ranged a -> a
    rangedThing) (Ranged HasEta0 -> HasEta)
    -> Maybe (Ranged HasEta0) -> Maybe HasEta
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (Ranged HasEta0)
    eta0

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

        -- Record has no fields: attach composition data to record constructor
        if null fs then do
          kit <- defineCompData name con (abstract cxt tel) [] ftel rect empty
          modifySignature $ updateDefinition (conName con) $ updateTheDef $ \case
            r :: Defn
    r@Constructor{} -> Defn
    r { conComp = kit, conProj = Just [] }  -- no projections
            Defn
    _ -> Defn
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        -- No-eta record with pattern matching (i.e., withOUT copattern
        -- matching): define composition as for a data type, attach it to
        -- the record.
        else if theEtaEquality eta == NoEta PatternMatching then do
          kit <- defineCompData name con (abstract cxt tel) (unArg <$> fs) ftel rect empty
          modifySignature $ updateDefinition name $ updateTheDef $ \case
            r :: Defn
    r@Record{} -> Defn
    r { recComp = kit }
            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.
          kit <- ifM (return (any isIrrelevant fs)
                      `and2M` do not . optIrrelevantProjections <$> pragmaOptions)
            {-then-} (return emptyCompKit)
            {-else-} (defineCompKitR name (abstract cxt tel) ftel fs rect)
          modifySignature $ updateDefinition name $ updateTheDef $ \case
            r :: Defn
    r@Record{} -> Defn
    r { recComp = 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
      required <- (SomeBuiltin -> TCMT IO (Maybe Term))
    -> [SomeBuiltin] -> TCMT IO [Maybe Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM SomeBuiltin -> TCMT IO (Maybe Term)
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    a -> m (Maybe Term)
    getTerm'
            [ BuiltinId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin BuiltinId
    builtinInterval
            , BuiltinId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin BuiltinId
    builtinIZero
            , BuiltinId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin BuiltinId
    builtinIOne
            , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    builtinIMin
            , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    builtinIMax
            , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    builtinINeg
            , PrimitiveId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin PrimitiveId
    builtinPOr
            , BuiltinId -> SomeBuiltin
    forall a. IsBuiltin a => a -> SomeBuiltin
    someBuiltin BuiltinId
    builtinItIsOne
            ]
      reportSDoc "tc.rec.cxt" 30 $ prettyTCM params
      reportSDoc "tc.rec.cxt" 30 $ prettyTCM fsT
      reportSDoc "tc.rec.cxt" 30 $ pretty rect
      if not $ all isJust required then return $ emptyCompKit else do
        transp <- whenDefined [builtinTrans]              (defineKanOperationR DoTransp name params fsT fns rect)
        hcomp  <- whenDefined [builtinTrans,builtinHComp] (defineKanOperationR DoHComp name params fsT fns rect)
        return $ CompKit
          { nameOfTransp = transp
          , nameOfHComp  = hcomp
          }
      where
        whenDefined :: t a -> m (Maybe a) -> m (Maybe a)
    whenDefined t a
    xs m (Maybe a)
    m = do
          xs <- (a -> m (Maybe Term)) -> t a -> m (t (Maybe Term))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
    mapM a -> m (Maybe Term)
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    a -> m (Maybe Term)
    getTerm' t a
    xs
          if all isJust xs then m else return Nothing

    defineKanOperationR
      :: Command
      -> QName       -- ^ some name, e.g. record name
      -> Telescope   -- ^ param types Δ
      -> Telescope   -- ^ fields' types Δ ⊢ Φ
      -> [Arg QName] -- ^ fields' names
      -> Type        -- ^ record type Δ ⊢ T
      -> TCM (Maybe QName)
    defineKanOperationR :: Command
    -> QName
    -> Telescope
    -> Telescope
    -> [Arg QName]
    -> Type
    -> TCMT IO (Maybe QName)
    defineKanOperationR Command
    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
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    fn])
      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 a b. (a -> b) -> Maybe a -> Maybe b
    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
    <$> Command
    -> Maybe Term
    -> (Term -> QName -> Term)
    -> QName
    -> Telescope
    -> Telescope
    -> [Arg QName]
    -> Type
    -> TCMT
         IO
         (Maybe
            ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
    defineKanOperationForFields Command
    cmd Maybe Term
    forall a. Maybe a
    Nothing Term -> QName -> Term
    project QName
    name Telescope
    params Telescope
    fsT [Arg QName]
    fns Type
    rect

      caseMaybe stuff (return Nothing) $ \ (QName
    theName, Telescope
    gamma, Type
    rtype, [Dom Type]
    clause_types, [Term]
    bodies) -> do
      -- phi = 1 clause
      c' <- do
               io <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIOne
               Just io_name <- getBuiltinName' builtinIOne
               one <- primItIsOne
               tInterval <- primIntervalType
               let
                  (ix,rhs) =
                    case cmd of
                      -- TranspRArgs = phi : I, a0 : ..
                      -- Γ = Δ^I , CompRArgs
                      -- pats = ... | phi = i1
                      -- body = a0
                      Command
    DoTransp -> (Nat
    1,Nat -> Elims -> Term
    Var Nat
    0 [])
                      -- HCompRArgs = phi : I, u : .., a0 : ..
                      -- Γ = Δ, CompRArgs
                      -- pats = ... | phi = i1
                      -- body = u i1 itIsOne
                      Command
    DoHComp  -> (Nat
    2,Nat -> Elims -> Term
    Var Nat
    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 = 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
    forall p. DataOrRecord' p
    IsData Induction
    Inductive [])
                           (ConPatternInfo
    noConPatternInfo { conPType = Just (Arg defaultArgInfo tInterval)
                                             , conPFallThrough = True })
                             []

                  -- gamma, rtype

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

                  pats :: [NamedArg DeBruijnPattern]
                  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 t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
    teleNamedArgs Telescope
    gamma

                  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' = [[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) = Nat -> [Dom Type] -> ([Dom Type], [Dom Type])
    forall a. Nat -> [a] -> ([a], [a])
    splitAt (Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    gamma Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    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) = Nat -> [[Char]] -> ([[Char]], [[Char]])
    forall a. Nat -> [a] -> ([a], [a])
    splitAt (Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    gamma Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    ix) ([[Char]] -> ([[Char]], [[Char]]))
    -> [[Char]] -> ([[Char]], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [[Char]]
    teleNames Telescope
    gamma

                  c = Clause { clauseFullRange :: Range
    clauseFullRange = Range
    forall a. Range' a
    noRange
                             , clauseLHSRange :: Range
    clauseLHSRange  = Range
    forall a. Range' a
    noRange
                             , clauseTel :: Telescope
    clauseTel       = Telescope
    gamma'
                             , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
    namedClausePats = [NamedArg (Pattern' DBPatVar)]
    pats
                             , 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
                             , 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
                             , clauseCatchall :: Catchall
    clauseCatchall    = Catchall
    forall a. Null a => a
    empty
                             , 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
                             , clauseWhereModule :: Maybe ModuleName
    clauseWhereModule = Maybe ModuleName
    forall a. Maybe a
    Nothing
                             }
               reportSDoc "trans.rec.face" 17 $ text $ show c
               return c
      cs <- forM (zip3 fns clause_types bodies) $ \ (Arg QName
    fname, Dom Type
    clause_ty, Term
    body) -> do
              let
                  pats :: [NamedArg (Pattern' DBPatVar)]
    pats = Telescope -> [NamedArg (Pattern' DBPatVar)]
    forall a t. DeBruijn a => Tele (Dom t) -> [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 { clauseFullRange :: Range
    clauseFullRange = Range
    forall a. Range' a
    noRange
                             , clauseLHSRange :: Range
    clauseLHSRange  = Range
    forall a. Range' a
    noRange
                             , clauseTel :: Telescope
    clauseTel       = Telescope
    gamma
                             , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
    namedClausePats = [NamedArg (Pattern' DBPatVar)]
    pats
                             , clauseBody :: Maybe Term
    clauseBody      = Term -> Maybe Term
    forall a. a -> Maybe a
    Just Term
    body
                             , 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)
                             , clauseCatchall :: Catchall
    clauseCatchall    = Catchall
    forall a. Null a => a
    empty
                             , 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
                             , clauseWhereModule :: Maybe ModuleName
    clauseWhereModule = Maybe ModuleName
    forall a. Maybe a
    Nothing
                             }
              [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "trans.rec" Nat
    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] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "trans.rec" Nat
    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] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "trans.rec" Nat
    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
    forall (m :: * -> *). MonadPretty m => Type -> 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] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "trans.rec" Nat
    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
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Telescope -> Term -> Term
    forall t. Abstract t => Telescope -> t -> t
    abstract Telescope
    gamma Term
    body)
              Clause -> TCMT IO Clause
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Clause
    c
      addClauses theName $ c' : cs
      reportSDoc "trans.rec" 15 $ text $ "compiling clauses for " ++ show theName
      (mst, _, cc) <- inTopContext (compileClauses Nothing cs)
      whenJust mst $ setSplitTree theName
      setCompiledClauses theName cc
      reportSDoc "trans.rec" 15 $ text $ "compiled"
      return $ Just 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 (perhaps erased) 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 a. a -> TCMT IO a
    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 a b. TCMT IO a -> TCMT IO b -> TCMT IO b
    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 a. Call -> TCMT IO a -> TCMT IO a
    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] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Nat
    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
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    x
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    forall (m :: * -> *). MonadPretty m => Telescope -> 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 :: * -> *). 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
    forall (m :: * -> *). MonadPretty m => Telescope -> 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] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Nat
    5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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 -> Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Nat -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible Nat
    1 (Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Telescope -> 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 -> Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Nat -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible Nat
    1 (Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> 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
    forall (m :: * -> *). MonadPretty m => Type -> 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 -> Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Nat -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible Nat
    1 (Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> 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
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM)
              ]
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Nat
    55 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Nat
    5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    forall (m :: * -> *). MonadPretty m => Term -> 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)
              ]

          Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (ArgInfo -> Cohesion
    forall a. LensCohesion a => a -> Cohesion
    getCohesion ArgInfo
    ai Cohesion -> Cohesion -> Bool
    forall a. Eq a => a -> a -> Bool
    == Cohesion
    Continuous) TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          -- Andreas, 2025-05-03, moved check to ConcreteToAbstract.checkFieldArgInfo.
          -- -- 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 hasLeftAdjoint (UnderComposition (getCohesion ai))
          --   then unless (getCohesion ai == Continuous)
          --               -- Atm, only Continuous has a left adjoint.
          --               -- Andrea TODO: properly update the context/type of the projection when we add Sharp
          --               __IMPOSSIBLE__
          --   else typeError $ InvalidFieldModality (getCohesion ai)

          -- For now, we forbid any polarity annotations on record fields (we would need to do as above,
          -- and eta-equality or projection existence would be in danger).
          Bool -> TCM () -> TCM ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless (ArgInfo -> PolarityModality
    forall a. LensModalPolarity a => a -> PolarityModality
    getModalPolarity ArgInfo
    ai PolarityModality -> PolarityModality -> Bool
    `samePolarity` (ModalPolarity -> PolarityModality
    withStandardLock ModalPolarity
    MixedPolarity)) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            -- Andreas, 2025-05-03, already checked in ConcreteToAbstract.checkFieldArgInfo
            TCM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          -- 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'       = Nat -> Nat -> Type -> Type
    forall a. Subst a => Nat -> Nat -> a -> a
    raiseFrom (Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    ftel1) Nat
    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 = Nat -> Elims -> Term
    Var Nat
    0 [ProjOrigin -> QName -> Elim
    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] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Nat
    25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    forall (m :: * -> *). MonadPretty m => Type -> 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] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Nat
    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"
              , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    forall (m :: * -> *). MonadPretty m => QName -> 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
    forall (m :: * -> *). MonadPretty m => Type -> 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 = Bool -> (Term -> Term) -> Term -> Term
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen (Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    rel) 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]) = Nat
    -> [Dom ([Char], Type)]
    -> ([Dom ([Char], Type)], [Dom ([Char], Type)])
    forall a. Nat -> [a] -> ([a], [a])
    splitAt (Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Telescope
    tel Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    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 { 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 a b. (a -> b) -> Dom' Term a -> Dom' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Char], Type) -> 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 t. DeBruijn a => Tele (Dom t) -> [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
    $ Nat -> Term
    var (Abs Telescope -> Nat
    forall a. Sized a => a -> Nat
    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
    $ Nat -> Type -> Type
    forall a. Subst a => Nat -> a -> a
    raise (Nat
    1 Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Abs Telescope -> Nat
    forall a. Sized a => a -> Nat
    size Abs Telescope
    ftel2) Type
    t
                clause :: Clause
    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 :: Catchall
    clauseCatchall  = Catchall
    forall a. Null a => a
    empty
                                , 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
                                , clauseWhereModule :: Maybe ModuleName
    clauseWhereModule = Maybe ModuleName
    forall a. Maybe a
    Nothing
                                }

            let projection :: Projection
    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 :: Nat
    projIndex    = Telescope -> Nat
    forall a. Sized a => a -> Nat
    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 a b. (a -> b) -> Dom' Term a -> Dom' Term b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Char], Type) -> [Char]
    forall a b. (a, b) -> a
    fst) [Dom ([Char], Type)]
    telList
                  }

            [Char] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Nat
    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"
              , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    forall (m :: * -> *). MonadPretty m => QName -> 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] -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.rec.proj" Nat
    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"
              , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    forall (m :: * -> *). MonadPretty m => QNamed Clause -> 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.
            (mst, _, cc) <- Maybe (QName, Type)
    -> [Clause] -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    compileClauses Maybe (QName, Type)
    forall a. Maybe a
    Nothing [Clause
    clause]

            reportSDoc "tc.cc" 60 $ do
              sep [ "compiled clauses of " <+> prettyTCM projname
                  , nest 2 $ text (show cc)
                  ]

            escapeContext impossible (size tel) $ do
              lang <- getLanguage
              fun  <- emptyFunctionData
              let -- It should be fine to mark a field with @ω in an
                  -- erased record type: the field will be non-erased, but
                  -- the projection will be erased. The following code
                  -- ensures that the use of addConstant does not trigger
                  -- a PlentyInHardCompileTimeMode warning.
                  ai' = ((Quantity -> Quantity) -> ArgInfo -> ArgInfo)
    -> ArgInfo -> (Quantity -> Quantity) -> ArgInfo
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (Quantity -> Quantity) -> ArgInfo -> ArgInfo
    forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
    mapQuantity ArgInfo
    ai ((Quantity -> Quantity) -> ArgInfo)
    -> (Quantity -> Quantity) -> ArgInfo
    forall a b. (a -> b) -> a -> b
    $ \case
                          Quantityω QωOrigin
    _ -> QωOrigin -> Quantity
    Quantityω QωOrigin
    QωInferred
                          Quantity
    q           -> Quantity
    q
              addConstant projname $
                (defaultDefn ai' projname (killRange finalt) lang $ FunctionDefn $
                 set funProj_ True $
                  fun
                    { _funClauses        = [clause]
                    , _funCompiled       = Just cc
                    , _funSplitTree      = mst
                    , _funProjection     = Right projection
                    , _funMutual         = Just []  -- Projections are not mutually recursive with anything
                    , _funTerminates     = Just True
                    })
                  { defArgOccurrences = [StrictPos]
                  , defCopatternLHS   = hasProjectionPatterns cc
                  }
              computePolarity [projname]

            addContext ftel1 case Info.defInstance info of
              -- Instance projections have to be added with their types "qua
              -- local variable" (i.e. the type you'd get were you to open
              -- the record module), but this type has to be treated in the
              -- context ftel1 otherwise it's nonsense
              InstanceDef KwRange
    _r -> QName -> Type -> TCM ()
    addTypedInstance QName
    projname Type
    t
              IsInstance
    NotInstanceDef -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

            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