{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation   #-}

module Agda.TypeChecking.Rules.Record where

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

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.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.Record.Cubical (addCompositionForRecord)

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

import Agda.Utils.Function ( applyWhen )
import Agda.Utils.List
import Agda.Utils.List1 (pattern (:|) )
import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Utils.Size
import Agda.Utils.POMonoid (hasLeftAdjoint)

import Agda.Utils.Impossible
import qualified Agda.Utils.List1 as List1

---------------------------------------------------------------------------
-- * 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.
  -> PositivityCheck           -- ^ Report positivity errors for this record type?
  -> UniverseCheck             -- ^ Check universes?
  -> ForceRecordEta            -- ^ @{-# ETA_EQUALITY #-}@ pragma attached to this record definition?
  -> 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' Expr
-> QName
-> PositivityCheck
-> UniverseCheck
-> ForceRecordEta
-> RecordDirectives
-> DataDefParams
-> Expr
-> [Declaration]
-> TCM ()
checkRecDef DefInfo' Expr
i QName
name PositivityCheck
pc UniverseCheck
uc ForceRecordEta
forceEta (RecordDirectives Maybe (Ranged Induction)
ind Maybe (Ranged HasEta0)
eta0 Maybe (Range' SrcFile)
pat RecordConName
con) (A.DataDefParams Set Name
gpars [LamBinding]
ps) Expr
contel0 [Declaration]
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 Int
n DataOrRecord_
IsRecord_ -> Int
n
            Defn
_ -> Int
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'' Term Term
t0 ->
     Int
-> [LamBinding]
-> Type'' Term Term
-> (Telescope -> Type'' Term Term -> TCM ())
-> TCM ()
forall a.
Int
-> [LamBinding]
-> Type'' Term Term
-> (Telescope -> Type'' Term Term -> TCM a)
-> TCM a
bindParameters (Int
npars Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Maybe Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Maybe Name]
parNames) [LamBinding]
ps Type'' Term Term
t0 ((Telescope -> Type'' Term Term -> TCM ()) -> TCM ())
-> (Telescope -> Type'' Term Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Telescope
ptel Type'' Term Term
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.
      ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.rec" Int
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'' Term Term) -> TCMT IO (Type'' Term Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCMT IO (Type'' Term Term) -> TCMT IO (Type'' Term Term))
-> TCMT IO (Type'' Term Term) -> TCMT IO (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TCMT IO (Type'' Term Term)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Type'' Term Term -> TCMT IO (Type'' Term Term))
-> TCMT IO (Type'' Term Term) -> TCMT IO (Type'' Term Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCMT IO (Type'' Term Term)
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'' Term Term -> Type'' Term Term
telePi_ Telescope
ftel (Int -> Type'' Term Term -> Type'' Term Term
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
ftel) Type'' Term Term
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"

      let getName :: A.Declaration -> [Dom QName]
          getName = \case
            A.Field DefInfo' Expr
_ 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 ]
            A.ScopedDecl ScopeInfo
_ (Declaration
f :| []) -> Declaration -> [Dom' Term QName]
getName Declaration
f
            Declaration
_ -> []

          setTactic Dom' t e
dom Dom' t e
f = Dom' t e
f Dom' t e -> (Dom' t e -> Dom' t e) -> Dom' t e
forall a b. a -> (a -> b) -> b
& (Maybe t -> Identity (Maybe t)) -> Dom' t e -> Identity (Dom' t e)
forall t e (f :: * -> *).
Functor f =>
(Maybe t -> f (Maybe t)) -> Dom' t e -> f (Dom' t e)
dTactic ((Maybe t -> Identity (Maybe t))
 -> Dom' t e -> Identity (Dom' t e))
-> Maybe t -> Dom' t e -> Dom' t e
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (Dom' t e
dom Dom' t e -> Getting (Maybe t) (Dom' t e) (Maybe t) -> Maybe t
forall s a. s -> Getting a s a -> a
^. Getting (Maybe t) (Dom' t e) (Maybe t)
forall t e (f :: * -> *).
Functor f =>
(Maybe t -> f (Maybe t)) -> Dom' t e -> f (Dom' t e)
dTactic)
          fs = (Dom' Term (ArgName, Type'' Term Term)
 -> Dom' Term QName -> Dom' Term QName)
-> [Dom' Term (ArgName, Type'' Term Term)]
-> [Dom' Term QName]
-> [Dom' Term QName]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' Dom' Term (ArgName, Type'' Term Term)
-> Dom' Term QName -> Dom' Term QName
forall {t} {e} {e}. Dom' t e -> Dom' t e -> Dom' t e
setTactic (Telescope -> [Dom' Term (ArgName, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
ftel) ([Dom' Term QName] -> [Dom' Term QName])
-> [Dom' Term QName] -> [Dom' Term QName]
forall a b. (a -> b) -> a -> b
$ (Declaration -> [Dom' Term QName])
-> [Declaration] -> [Dom' Term QName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Declaration -> [Dom' Term QName]
getName [Declaration]
fields

          -- 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
-> (Range' SrcFile -> PatternOrCopattern)
-> Maybe (Range' SrcFile)
-> PatternOrCopattern
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PatternOrCopattern
CopatternMatching (PatternOrCopattern -> Range' SrcFile -> PatternOrCopattern
forall a b. a -> b -> a
const PatternOrCopattern
PatternMatching) Maybe (Range' SrcFile)
pat
          eta      = ((PatternOrCopattern
patCopat PatternOrCopattern -> HasEta0 -> HasEta' PatternOrCopattern
forall a b. a -> HasEta' b -> HasEta' a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) (HasEta0 -> HasEta' PatternOrCopattern)
-> (Ranged HasEta0 -> HasEta0)
-> Ranged HasEta0
-> HasEta' PatternOrCopattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranged HasEta0 -> HasEta0
forall a. Ranged a -> a
rangedThing) (Ranged HasEta0 -> HasEta' PatternOrCopattern)
-> Maybe (Ranged HasEta0) -> Maybe (HasEta' PatternOrCopattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Ranged HasEta0)
eta0
          -- 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
          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' PatternOrCopattern)
eta         = Relevance
relevant
            | Induction
CoInductive <- Induction
conInduction = Relevance
relevant
            | [Dom' Term (ArgName, Type'' Term Term)] -> Bool
forall a. Null a => a -> Bool
null (Telescope -> [Dom' Term (ArgName, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (ArgName, 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' Term (ArgName, Type'' Term Term) -> Relevance)
-> [Dom' Term (ArgName, Type'' Term Term)] -> [Relevance]
forall a b. (a -> b) -> [a] -> [b]
map' Dom' Term (ArgName, Type'' Term Term) -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance (Telescope -> [Dom' Term (ArgName, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
ftel)

      reportSDoc "tc.rec" 30 $ "record constructor is " <+> prettyTCM con

      -- Compute eta status from record directives and options.
      let noEta = PatternOrCopattern -> HasEta' PatternOrCopattern
forall a. a -> HasEta' a
NoEta PatternOrCopattern
patCopat
      etaenabled <- etaEnabled
      haveEta <- case forceEta of
        -- We force eta-equality since we have an ETA_EQUALITY pragma.
        ForceRecordEta
YesForceRecordEta -> case Maybe (HasEta' PatternOrCopattern)
eta of
          Just (NoEta PatternOrCopattern
_)             -> TypeError -> TCMT IO EtaEquality
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO EtaEquality)
-> TypeError -> TCMT IO EtaEquality
forall a b. (a -> b) -> a -> b
$ TypeError
EtaPragmaVsNoEtaEquality
          Maybe (HasEta' PatternOrCopattern)
_                          -> EtaEquality -> TCMT IO EtaEquality
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EtaEquality -> TCMT IO EtaEquality)
-> EtaEquality -> TCMT IO EtaEquality
forall a b. (a -> b) -> a -> b
$ HasEta' PatternOrCopattern -> EtaProvenance -> EtaEquality
EtaEquality HasEta' PatternOrCopattern
forall a. HasEta' a
YesEta EtaProvenance
EtaFromPragma
        -- We do not have an ETA_EQUALITY pragma, so we first look at possible eta-equality directives
        -- and then at the defaults.
        ForceRecordEta
NoForceRecordEta -> case (Maybe (HasEta' PatternOrCopattern)
eta, Induction
conInduction, Bool
etaenabled) of
          (Maybe (HasEta' PatternOrCopattern)
Nothing, Induction
Inductive, Bool
True) -> EtaEquality -> TCMT IO EtaEquality
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EtaEquality -> TCMT IO EtaEquality)
-> EtaEquality -> TCMT IO EtaEquality
forall a b. (a -> b) -> a -> b
$ HasEta' PatternOrCopattern -> EtaProvenance -> EtaEquality
EtaEquality HasEta' PatternOrCopattern
forall a. HasEta' a
YesEta EtaProvenance
EtaFromOption
          (Maybe (HasEta' PatternOrCopattern)
Nothing, Induction
_, Bool
_)            -> EtaEquality -> TCMT IO EtaEquality
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EtaEquality -> TCMT IO EtaEquality)
-> EtaEquality -> TCMT IO EtaEquality
forall a b. (a -> b) -> a -> b
$ HasEta' PatternOrCopattern -> EtaProvenance -> EtaEquality
EtaEquality HasEta' PatternOrCopattern
noEta  EtaProvenance
EtaFromOption
          (Just noEta :: HasEta' PatternOrCopattern
noEta@NoEta{}, Induction
_, Bool
_) -> EtaEquality -> TCMT IO EtaEquality
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EtaEquality -> TCMT IO EtaEquality)
-> EtaEquality -> TCMT IO EtaEquality
forall a b. (a -> b) -> a -> b
$ HasEta' PatternOrCopattern -> EtaProvenance -> EtaEquality
EtaEquality HasEta' PatternOrCopattern
noEta  EtaProvenance
EtaFromDirective
          (Just HasEta' PatternOrCopattern
YesEta, Induction
Inductive,Bool
_) -> EtaEquality -> TCMT IO EtaEquality
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EtaEquality -> TCMT IO EtaEquality)
-> EtaEquality -> TCMT IO EtaEquality
forall a b. (a -> b) -> a -> b
$ HasEta' PatternOrCopattern -> EtaProvenance -> EtaEquality
EtaEquality HasEta' PatternOrCopattern
forall a. HasEta' a
YesEta EtaProvenance
EtaFromDirective
          (Just HasEta' PatternOrCopattern
YesEta, Induction
CoInductive, Bool
_)     -> HasEta' PatternOrCopattern -> EtaProvenance -> EtaEquality
EtaEquality HasEta' PatternOrCopattern
noEta  EtaProvenance
EtaFromOption EtaEquality -> TCM () -> TCMT IO EtaEquality
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ do
            -- Andreas, 2017-01-26, issue #2436
            -- Disallow coinductive records with eta-equality
            -- Andreas, 2024-06-14, PR #7300
            -- Just make this a deadcode warning.
            Maybe (Ranged HasEta0) -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Maybe (Ranged HasEta0)
eta0 (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
CoinductiveEtaRecord QName
name

      -- Warn about 'pattern' directive if eta is on.
      case (haveEta, pat) of
        (EtaEquality HasEta' PatternOrCopattern
YesEta EtaProvenance
_, Just Range' SrcFile
r) -> Range' SrcFile -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range' SrcFile
r (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
$ ArgName -> Warning
UselessPatternDeclarationForRecord ArgName
"eta"
        (EtaEquality, Maybe (Range' SrcFile))
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

      -- 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 -> Int
forall a. Sized a => a -> Int
size Telescope
tel
          telh  = (Dom (Type'' Term Term) -> Dom (Type'' Term Term))
-> 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'' Term Term) -> Dom (Type'' Term Term)
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
              , recPositivityCheck= pc
              , 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 (analysis running always, independently of recPositivityCheck):
              , 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.
          KwRange -> QName -> Type'' Term Term -> TCM ()
addTypedInstance KwRange
r QName
conName Type'' Term Term
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
        ]
-}

      -- Make a note of what variable is the 'self' variable in the telescope.
      let info = Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
RecordSelf (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo
forall a b. (a -> b) -> a -> b
$ Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
recordRelevance ArgInfo
defaultArgInfo
          addRecordVar = Dom (Type'' Term Term) -> TCM () -> TCM ()
forall (m :: * -> *) b.
(MonadAddContext m, MonadFresh NameId m) =>
Dom (Type'' Term Term) -> m b -> m b
addRecordNameContext (ArgInfo -> Dom (Type'' Term Term) -> Dom (Type'' Term Term)
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info (Dom (Type'' Term Term) -> Dom (Type'' Term Term))
-> Dom (Type'' Term Term) -> Dom (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> Dom (Type'' Term Term)
forall a. a -> Dom a
defaultDom Type'' Term Term
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 <- fromMaybe __IMPOSSIBLE__ . cxLookup 0 <$> getContext
            return $ contextToTel $ CxExtend r params
          cp <- viewTC eCurrentCheckpoint
          setModuleCheckpoint m cp
          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 }


{-| @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
-> [Declaration]
-> TCM ()
checkRecordProjections ModuleName
m QName
r Bool
hasNamedCon ConHead
con Telescope
tel Telescope
ftel [Declaration]
fs = do
    Telescope -> Telescope -> [Term] -> [Declaration] -> TCM ()
checkProjs Telescope
forall a. Tele a
EmptyTel Telescope
ftel [] [Declaration]
fs
  where

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

    checkProjs :: Telescope -> Telescope -> [Term] -> [Declaration] -> 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 NonEmpty Declaration
fs' : [Declaration]
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] -> [Declaration] -> TCM ()
checkProjs Telescope
ftel1 Telescope
ftel2 [Term]
vs (NonEmpty Declaration -> [Item (NonEmpty Declaration)]
forall l. IsList l => l -> [Item l]
List1.toList NonEmpty Declaration
fs' [Declaration] -> [Declaration] -> [Declaration]
forall a. [a] -> [a] -> [a]
++! [Declaration]
fs)

    -- Case: projection.
    checkProjs Telescope
ftel1 (ExtendTel (dom :: Dom (Type'' Term Term)
dom@(Dom (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom -> Type'' Term Term
t)) Abs Telescope
ftel2) [Term]
vs (A.Field DefInfo' Expr
info QName
x Arg Expr
_ : [Declaration]
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' SrcFile -> QName -> Type'' Term Term -> Call
CheckProjection (DefInfo' Expr -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange DefInfo' Expr
info) QName
x Type'' Term Term
t) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      let ai :: ArgInfo
ai = Dom (Type'' Term Term)
dom Dom (Type'' Term Term)
-> Getting ArgInfo (Dom (Type'' Term Term)) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom (Type'' Term Term)) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo
      -- 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.
      ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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
forall (m :: * -> *). MonadPretty m => QName -> 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
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...
      ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.rec.proj.escapeContext" Int
45 (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
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 -> 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
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'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
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
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'' Term Term)
-> Abs Telescope -> (Telescope -> TCMT IO Doc) -> TCMT IO Doc
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom (Type'' Term Term) -> Abs a -> (a -> m b) -> m b
underAbstraction Dom (Type'' Term Term)
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)
          ]
      ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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
<+> Int -> TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a. MonadTCM tcm => Int -> tcm a -> tcm a
unsafeEscapeContext Int
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
<+> Int -> TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a. MonadTCM tcm => Int -> tcm a -> tcm a
unsafeEscapeContext Int
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'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
t)
          , TCMT IO Doc
"ftel2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a. MonadTCM tcm => Int -> tcm a -> tcm a
unsafeEscapeContext Int
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'' Term Term)
-> Abs Telescope -> (Telescope -> TCMT IO Doc) -> TCMT IO Doc
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom (Type'' Term Term) -> Abs a -> (a -> m b) -> m b
underAbstraction Dom (Type'' Term Term)
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)
          ]
      ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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'' Term Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type'' Term Term
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
          ]
      ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"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
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
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (IsAbstract -> ArgName) -> IsAbstract -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsAbstract -> ArgName
forall a. Show a => a -> ArgName
show) (DefInfo' Expr -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo' Expr
info)
          , TCMT IO Doc
"quant =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (Quantity -> ArgName) -> Quantity -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quantity -> ArgName
forall a. Show a => a -> ArgName
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
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (Cohesion -> ArgName) -> Cohesion -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cohesion -> ArgName
forall a. Show a => a -> ArgName
show) (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai)
          ]

      -- Cohesion check:
      -- For a field `@c π : A`, if c has a left adjoint, we create a projection
      -- `@(c^-1) π : .., (@(c^-1 . c) r : R as) -> A`
      -- So we want to check that `@.., (c^-1 . c) x : A |- x : A` is allowed by the modalities.
      --
      -- Currently only sharp and continuous have left adjoints under composition.
      -- This check happens at scope checking time, so we should only be left
      -- with annotations with left adjoints here
      tel <- 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 Telescope -> TCMT IO Telescope
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Telescope -> TCMT IO Telescope) -> Telescope -> TCMT IO Telescope
forall a b. (a -> b) -> a -> b
$ ASetter
  Telescope
  Telescope
  [Dom' Term (ArgName, Type'' Term Term)]
  [Dom' Term (ArgName, Type'' Term Term)]
-> ([Dom' Term (ArgName, Type'' Term Term)]
    -> [Dom' Term (ArgName, Type'' Term Term)])
-> Telescope
-> Telescope
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  Telescope
  Telescope
  [Dom' Term (ArgName, Type'' Term Term)]
  [Dom' Term (ArgName, Type'' Term Term)]
Lens' Telescope [Dom' Term (ArgName, Type'' Term Term)]
listTel ((Dom' Term (ArgName, Type'' Term Term)
 -> Dom' Term (ArgName, Type'' Term Term))
-> [Dom' Term (ArgName, Type'' Term Term)]
-> [Dom' Term (ArgName, Type'' Term Term)]
forall a b. (a -> b) -> [a] -> [b]
map' (Cohesion
-> Dom' Term (ArgName, Type'' Term Term)
-> Dom' Term (ArgName, Type'' Term Term)
forall a. LensCohesion a => Cohesion -> a -> a
inverseApplyCohesion (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai))) Telescope
tel
          else TCMT IO Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__

      -- 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).
      unless (getModalPolarity ai `samePolarity` (withStandardLock MixedPolarity)) $
        -- Andreas, 2025-05-03, already checked in ConcreteToAbstract.checkFieldArgInfo
        __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'       = Int -> Int -> Type'' Term Term -> Type'' Term Term
forall a. Subst a => Int -> Int -> a -> a
raiseFrom (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
ftel1) Int
1 Type'' Term Term
t
          t''      = Substitution' (SubstArg (Type'' Term Term))
-> Type'' Term Term -> Type'' Term Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst ([Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS [Term]
vs) Type'' Term Term
t'
          finalt   = Telescope -> Type'' Term Term -> Type'' Term Term
telePi Telescope
tel Type'' Term Term
t''
          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
o = Int -> Elims -> Term
Var Int
0 [ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
projname]
          rel      = ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai
          -- the recursive call
          recurse  = Telescope -> Telescope -> [Term] -> [Declaration] -> 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'' Term Term) -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom (Type'' Term Term)
dom
                                 (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ ArgName -> Telescope -> Abs Telescope
forall a. ArgName -> a -> Abs a
Abs (Name -> ArgName
nameToArgName (Name -> ArgName) -> Name -> ArgName
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) [Declaration]
fs

      reportSDoc "tc.rec.proj" 25 $ nest 2 $ "finalt=" <+> do
        inTopContext $ prettyTCM 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
        reportSDoc "tc.rec.proj" 10 $ sep
          [ "adding projection"
          , nest 2 $ prettyTCM projname <+> ":" <+> inTopContext (prettyTCM 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 = 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 = Telescope -> [Dom' Term (ArgName, Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel
            (ptelList,[rt]) = splitAt' (size tel - 1) telList
            ptel   = [Dom' Term (ArgName, Type'' Term Term)] -> Telescope
telFromList [Dom' Term (ArgName, Type'' Term Term)]
ptelList
            cpo    = if Bool
hasNamedCon then PatOrigin
PatOCon else PatOrigin
PatORec
            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'' Term Term))
conPType   = Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term))
forall a. a -> Maybe a
Just (Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term)))
-> Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ Dom (Type'' Term Term) -> Arg (Type'' Term Term)
forall t a. Dom' t a -> Arg a
argFromDom (Dom (Type'' Term Term) -> Arg (Type'' Term Term))
-> Dom (Type'' Term Term) -> Arg (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ ((ArgName, Type'' Term Term) -> Type'' Term Term)
-> Dom' Term (ArgName, Type'' Term Term) -> Dom (Type'' Term Term)
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName, Type'' Term Term) -> Type'' Term Term
forall a b. (a, b) -> b
snd Dom' Term (ArgName, Type'' Term Term)
rt
                                    , conPLazy :: Bool
conPLazy   = Bool
True }
            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   = 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
ptel Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ftel
            cltype = Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term))
forall a. a -> Maybe a
Just (Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term)))
-> Arg (Type'' Term Term) -> Maybe (Arg (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Type'' Term Term -> Arg (Type'' Term Term)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Type'' Term Term -> Arg (Type'' Term Term))
-> Type'' Term Term -> Arg (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Int -> Type'' Term Term -> Type'' Term Term
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'' Term Term
t
            clause = Clause { clauseLHSRange :: Range' SrcFile
clauseLHSRange  = DefInfo' Expr -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange DefInfo' Expr
info
                            , clauseFullRange :: Range' SrcFile
clauseFullRange = DefInfo' Expr -> Range' SrcFile
forall a. HasRange a => a -> Range' SrcFile
getRange DefInfo' Expr
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'' Term Term))
clauseType      = Maybe (Arg (Type'' Term Term))
cltype
                            , clauseCatchall :: Catchall
clauseCatchall  = Catchall
forall a. Null a => a
empty
                            , clauseRecursive :: ClauseRecursive
clauseRecursive   = ClauseRecursive
NotRecursive
                            , 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
              { 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 a. a -> Arg a
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 ArgName] -> ProjLams
ProjLams ([Arg ArgName] -> ProjLams) -> [Arg ArgName] -> ProjLams
forall a b. (a -> b) -> a -> b
$ (Dom' Term (ArgName, Type'' Term Term) -> Arg ArgName)
-> [Dom' Term (ArgName, Type'' Term Term)] -> [Arg ArgName]
forall a b. (a -> b) -> [a] -> [b]
map' (Dom' Term ArgName -> Arg ArgName
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term ArgName -> Arg ArgName)
-> (Dom' Term (ArgName, Type'' Term Term) -> Dom' Term ArgName)
-> Dom' Term (ArgName, Type'' Term Term)
-> Arg ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ArgName, Type'' Term Term) -> ArgName)
-> Dom' Term (ArgName, Type'' Term Term) -> Dom' Term ArgName
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName, Type'' Term Term) -> ArgName
forall a b. (a, b) -> a
fst) [Dom' Term (ArgName, Type'' Term Term)]
telList
              }

        reportSDoc "tc.rec.proj" 70 $ sep
          [ "adding projection"
          , nest 2 $ prettyTCM projname <+> pretty clause
          ]
        reportSDoc "tc.rec.proj" 10 $ sep
          [ "adding projection"
          , nest 2 $ prettyTCM (QNamed projname 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) <- compileClauses Nothing [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
kwr -> KwRange -> QName -> Type'' Term Term -> TCM ()
addTypedInstance KwRange
kwr QName
projname Type'' Term Term
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 (Declaration
d : [Declaration]
fs) = do
      Declaration -> TCM ()
checkDecl Declaration
d
      Telescope -> Telescope -> [Term] -> [Declaration] -> TCM ()
checkProjs Telescope
ftel1 Telescope
ftel2 [Term]
vs [Declaration]
fs