    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Rules.Data where

    import Prelude hiding (null)

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

    import Data.Set (Set)
    import qualified Data.Set as Set

    import qualified Agda.Syntax.Abstract as A
    import qualified Agda.Syntax.Concrete.Name as C
    import Agda.Syntax.Abstract.Views (deepUnscope)
    import Agda.Syntax.Internal
    import Agda.Syntax.Common
    import Agda.Syntax.Position
    import qualified Agda.Syntax.Info as Info
    import Agda.Syntax.Scope.Monad

    import {-# SOURCE #-} Agda.TypeChecking.CompiledClause.Compile
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Conversion
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Generalize
    import Agda.TypeChecking.Implicit
    import Agda.TypeChecking.MetaVars
    import Agda.TypeChecking.Names
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Positivity.Occurrence (Occurrence(StrictPos))
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Primitive hiding (Nat)
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Forcing
    import Agda.TypeChecking.Irrelevance
    import Agda.TypeChecking.Telescope

    import {-# SOURCE #-} Agda.TypeChecking.Rules.Term ( isType_ )

    import Agda.Utils.List
    import Agda.Utils.List1 (List1, pattern (:|))
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import qualified Agda.Utils.Pretty as P
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * Datatypes
    ---------------------------------------------------------------------------

    -- | Type check a datatype definition. Assumes that the type has already been
    --   checked.
    checkDataDef :: A.DefInfo -> QName -> UniverseCheck -> A.DataDefParams -> [A.Constructor] -> TCM ()
    checkDataDef :: DefInfo
    -> QName
    -> UniverseCheck
    -> DataDefParams
    -> [Constructor]
    -> TCM ()
    checkDataDef DefInfo
    i QName
    name UniverseCheck
    uc (A.DataDefParams Set Name
    gpars [LamBinding]
    ps) [Constructor]
    cs =
        Call -> TCM () -> TCM ()
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (Range -> QName -> [LamBinding] -> [Constructor] -> Call
    CheckDataDef (QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    name) QName
    name [LamBinding]
    ps [Constructor]
    cs) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

            -- Add the datatype module
            ModuleName -> TCM ()
    addSection (QName -> ModuleName
    qnameToMName QName
    name)

            -- Look up the type of the datatype.
            Definition
    def <- Definition -> TCMT IO Definition
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    Definition -> m Definition
    instantiateDef (Definition -> TCMT IO Definition)
    -> TCMT IO Definition -> TCMT IO Definition
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    name
            Type
    t   <- Type -> TCMT IO Type
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull (Type -> TCMT IO Type) -> Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type
    defType Definition
    def
            let npars :: Nat
    npars =
                  case Definition -> Defn
    theDef Definition
    def of
                    DataOrRecSig Nat
    n -> Nat
    n
                    Defn
    _              -> Nat
    forall a. HasCallStack => a
    __IMPOSSIBLE__

            -- Make sure the shape of the type is visible
            let unTelV :: TelV Type -> Type
    unTelV (TelV Tele (Dom Type)
    tel Type
    a) = Tele (Dom Type) -> Type -> Type
    telePi Tele (Dom Type)
    tel Type
    a
            Type
    t <- TelV Type -> Type
    unTelV (TelV Type -> Type) -> TCMT IO (TelV Type) -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t

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

            -- Top level free vars
            Nat
    freeVars <- TCMT IO Nat
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
    getContextSize

            -- The parameters are in scope when checking the constructors.
            Defn
    dataDef <- [Maybe Name]
    -> Type -> (Tele (Dom Type) -> Type -> TCM Defn) -> TCM Defn
    forall a.
    [Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
    bindGeneralizedParameters [Maybe Name]
    parNames Type
    t ((Tele (Dom Type) -> Type -> TCM Defn) -> TCM Defn)
    -> (Tele (Dom Type) -> Type -> TCM Defn) -> TCM Defn
    forall a b. (a -> b) -> a -> b
    $ \ Tele (Dom Type)
    gtel Type
    t0 ->
                       Nat
    -> [LamBinding]
    -> Type
    -> (Tele (Dom Type) -> Type -> TCM Defn)
    -> TCM Defn
    forall a.
    Nat
    -> [LamBinding]
    -> Type
    -> (Tele (Dom Type) -> Type -> TCM a)
    -> TCM a
    bindParameters (Nat
    npars Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - [Maybe Name] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Maybe Name]
    parNames) [LamBinding]
    ps Type
    t0 ((Tele (Dom Type) -> Type -> TCM Defn) -> TCM Defn)
    -> (Tele (Dom Type) -> Type -> TCM Defn) -> TCM Defn
    forall a b. (a -> b) -> a -> b
    $ \ Tele (Dom Type)
    ptel Type
    t0 -> do

                -- Parameters are always hidden in constructors
                let tel :: Tele (Dom Type)
    tel  = Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    gtel Tele (Dom Type)
    ptel
                    tel' :: Tele (Dom Type)
    tel' = Dom Type -> Dom Type
    forall a. (LensHiding a, LensRelevance a) => a -> a
    hideAndRelParams (Dom Type -> Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Tele (Dom Type)
    tel
                -- let tel' = hideTel tel

                -- The type we get from bindParameters is Θ -> s where Θ is the type of
                -- the indices. We count the number of indices and return s.
                -- We check that s is a sort.
                let TelV Tele (Dom Type)
    ixTel Type
    s0 = Type -> TelV Type
    telView' Type
    t0
                    nofIxs :: Nat
    nofIxs = Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    ixTel

                Sort
    s <- TCMT IO Sort -> TCMT IO Sort
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    workOnTypes (TCMT IO Sort -> TCMT IO Sort) -> TCMT IO Sort -> TCMT IO Sort
    forall a b. (a -> b) -> a -> b
    $ do
                  -- Andreas, 2016-11-02 issue #2290
                  -- Trying to unify the sort with a fresh sort meta which is
                  -- defined outside the index telescope is the most robust way
                  -- to check independence of the indices.
                  -- However, it might give the dreaded "Cannot instantiate meta..."
                  -- error which we replace by a more understandable error
                  -- in case of a suspected dependency.
                  Sort
    s <- TCMT IO Sort
    newSortMetaBelowInf
                  TCM () -> (TCErr -> TCM ()) -> TCM ()
    forall a. TCM a -> (TCErr -> TCM a) -> TCM a
    catchError_ (Tele (Dom Type) -> TCM () -> TCM ()
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    ixTel (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> TCM ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    equalType Type
    s0 (Type -> TCM ()) -> Type -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Nat -> Type -> Type
    forall a. Subst a => Nat -> a -> a
    raise Nat
    nofIxs (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Sort -> Type
    sort Sort
    s) ((TCErr -> TCM ()) -> TCM ()) -> (TCErr -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ TCErr
    err ->
                      if (Nat -> Bool) -> [Nat] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Nat -> Type -> Bool
    forall a. Free a => Nat -> a -> Bool
    `freeIn` Type
    s0) [Nat
    0..Nat
    nofIxs Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1] then TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                         [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep [ TCMT IO Doc
    "The sort of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    name
                              , TCMT IO Doc
    "cannot depend on its indices in the type"
                              , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t0
                              ]
                      else TCErr -> TCM ()
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError TCErr
    err
                  Sort -> TCMT IO Sort
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Sort
    s

                -- when `--without-K`, all the indices should fit in the
                -- sort of the datatype (see #3420).
                let s' :: Sort
    s' = case Sort
    s of
                      Prop Level
    l -> Level -> Sort
    forall t. Level' t -> Sort' t
    Type Level
    l
                      Sort
    _      -> Sort
    s
                -- Andreas, 2019-07-16, issue #3916:
                -- NoUniverseCheck should also disable the index sort check!
                Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (UniverseCheck
    uc UniverseCheck -> UniverseCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == UniverseCheck
    NoUniverseCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                  TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM TCMT IO Bool
    forall (m :: * -> *). HasOptions m => m Bool
    withoutKOption (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Sort -> Tele (Dom Type) -> TCM ()
    checkIndexSorts Sort
    s' Tele (Dom Type)
    ixTel

                ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.data.sort" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
                  [ TCMT IO Doc
    "checking datatype" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    name
                  , 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
    "type (parameters instantiated):   " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t0
                    , TCMT IO Doc
    "type (full):   " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
                    , TCMT IO Doc
    "sort:   " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Sort -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Sort
    s
                    , TCMT IO Doc
    "indices:" 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 (Nat -> ArgName
    forall a. Show a => a -> ArgName
    show Nat
    nofIxs)
                    , TCMT IO Doc
    "gparams:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text ([Maybe Name] -> ArgName
    forall a. Show a => a -> ArgName
    show [Maybe Name]
    parNames)
                    , TCMT IO Doc
    "params: " 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 ([LamBinding] -> ArgName
    forall a. Show a => a -> ArgName
    show ([LamBinding] -> ArgName) -> [LamBinding] -> ArgName
    forall a b. (a -> b) -> a -> b
    $ [LamBinding] -> [LamBinding]
    forall a. ExprLike a => a -> a
    deepUnscope [LamBinding]
    ps)
                    ]
                  ]
                let npars :: Nat
    npars = Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel

                -- Change the datatype from an axiom to a datatype with no constructors.
                let dataDef :: Defn
    dataDef = Datatype :: Nat
    -> Nat
    -> Maybe Clause
    -> [QName]
    -> Sort
    -> Maybe [QName]
    -> IsAbstract
    -> [QName]
    -> Defn
    Datatype
                      { dataPars :: Nat
    dataPars       = Nat
    npars
                      , dataIxs :: Nat
    dataIxs        = Nat
    nofIxs
                      , dataClause :: Maybe Clause
    dataClause     = Maybe Clause
    forall a. Maybe a
    Nothing
                      , dataCons :: [QName]
    dataCons       = []     -- Constructors are added later
                      , dataSort :: Sort
    dataSort       = Sort
    s
                      , dataAbstr :: IsAbstract
    dataAbstr      = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    i
                      , dataMutual :: Maybe [QName]
    dataMutual     = Maybe [QName]
    forall a. Maybe a
    Nothing
                      , dataPathCons :: [QName]
    dataPathCons   = []     -- Path constructors are added later
                      }

                Impossible -> Nat -> TCM () -> TCM ()
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Nat -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible Nat
    npars (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
                  QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
    addConstant' QName
    name ArgInfo
    defaultArgInfo QName
    name Type
    t Defn
    dataDef
                    -- polarity and argOcc.s determined by the positivity checker

                -- Check the types of the constructors
                [Maybe QName]
    pathCons <- [Constructor]
    -> (Constructor -> TCMT IO (Maybe QName)) -> TCMT IO [Maybe QName]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Constructor]
    cs ((Constructor -> TCMT IO (Maybe QName)) -> TCMT IO [Maybe QName])
    -> (Constructor -> TCMT IO (Maybe QName)) -> TCMT IO [Maybe QName]
    forall a b. (a -> b) -> a -> b
    $ \ Constructor
    c -> do
                  IsPathCons
    isPathCons <- QName
    -> UniverseCheck
    -> Tele (Dom Type)
    -> Nat
    -> Sort
    -> Constructor
    -> TCM IsPathCons
    checkConstructor QName
    name UniverseCheck
    uc Tele (Dom Type)
    tel' Nat
    nofIxs Sort
    s Constructor
    c
                  Maybe QName -> TCMT IO (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe QName -> TCMT IO (Maybe QName))
    -> Maybe QName -> TCMT IO (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ if IsPathCons
    isPathCons IsPathCons -> IsPathCons -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsPathCons
    PathCons then QName -> Maybe QName
    forall a. a -> Maybe a
    Just (Constructor -> QName
    A.axiomName Constructor
    c) else Maybe QName
    forall a. Maybe a
    Nothing

                -- Return the data definition
                Defn -> TCM Defn
    forall (m :: * -> *) a. Monad m => a -> m a
    return Defn
    dataDef{ dataPathCons :: [QName]
    dataPathCons = [Maybe QName] -> [QName]
    forall a. [Maybe a] -> [a]
    catMaybes [Maybe QName]
    pathCons }

            let cons :: [QName]
    cons   = (Constructor -> QName) -> [Constructor] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Constructor -> QName
    A.axiomName [Constructor]
    cs  -- get constructor names

            -- Add the datatype to the signature with its constructors.
            -- It was previously added without them.
            QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
    addConstant' QName
    name ArgInfo
    defaultArgInfo QName
    name Type
    t (Defn -> TCM ()) -> Defn -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                Defn
    dataDef{ dataCons :: [QName]
    dataCons = [QName]
    cons }

    -- | Ensure that the type is a sort.
    --   If it is not directly a sort, compare it to a 'newSortMetaBelowInf'.
    forceSort :: Type -> TCM Sort
    forceSort :: Type -> TCMT IO Sort
    forceSort Type
    t = Term -> TCMT IO Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t) TCMT IO Term -> (Term -> TCMT IO Sort) -> TCMT IO Sort
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Sort Sort
    s -> Sort -> TCMT IO Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s
      Term
    _      -> do
        Sort
    s <- TCMT IO Sort
    newSortMetaBelowInf
        Type -> Type -> TCM ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    equalType Type
    t (Sort -> Type
    sort Sort
    s)
        Sort -> TCMT IO Sort
    forall (m :: * -> *) a. Monad m => a -> m a
    return Sort
    s

    -- | Type check a constructor declaration. Checks that the constructor targets
    --   the datatype and that it fits inside the declared sort.
    --   Returns the non-linear parameters.
    checkConstructor
      :: QName         -- ^ Name of data type.
      -> UniverseCheck -- ^ Check universes?
      -> Telescope     -- ^ Parameter telescope.
      -> Nat           -- ^ Number of indices of the data type.
      -> Sort          -- ^ Sort of the data type.
      -> A.Constructor -- ^ Constructor declaration (type signature).
      -> TCM IsPathCons
    checkConstructor :: QName
    -> UniverseCheck
    -> Tele (Dom Type)
    -> Nat
    -> Sort
    -> Constructor
    -> TCM IsPathCons
    checkConstructor QName
    d UniverseCheck
    uc Tele (Dom Type)
    tel Nat
    nofIxs Sort
    s (A.ScopedDecl ScopeInfo
    scope [Constructor
    con]) = do
      ScopeInfo -> TCM ()
    setScope ScopeInfo
    scope
      QName
    -> UniverseCheck
    -> Tele (Dom Type)
    -> Nat
    -> Sort
    -> Constructor
    -> TCM IsPathCons
    checkConstructor QName
    d UniverseCheck
    uc Tele (Dom Type)
    tel Nat
    nofIxs Sort
    s Constructor
    con
    checkConstructor QName
    d UniverseCheck
    uc Tele (Dom Type)
    tel Nat
    nofIxs Sort
    s con :: Constructor
    con@(A.Axiom KindOfName
    _ DefInfo
    i ArgInfo
    ai Maybe [Occurrence]
    Nothing QName
    c Expr
    e) =
        Call -> TCM IsPathCons -> TCM IsPathCons
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (QName -> Tele (Dom Type) -> Sort -> Constructor -> Call
    CheckConstructor QName
    d Tele (Dom Type)
    tel Sort
    s Constructor
    con) (TCM IsPathCons -> TCM IsPathCons)
    -> TCM IsPathCons -> TCM IsPathCons
    forall a b. (a -> b) -> a -> b
    $ do
    {- WRONG
          -- Andreas, 2011-04-26: the following happens to the right of ':'
          -- we may use irrelevant arguments in a non-strict way in types
          t' <- workOnTypes $ do
    -}
            QName -> Expr -> TCM ()
    forall {m :: * -> *} {a} {a}.
    (MonadDebug m, PrettyTCM a, PrettyTCM a) =>
    a -> a -> m ()
    debugEnter QName
    c Expr
    e
            -- check that we are relevant
            case ArgInfo -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance ArgInfo
    ai of
              Relevance
    Relevant   -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
              Relevance
    Irrelevant -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TypeError
    GenericError (ArgName -> TypeError) -> ArgName -> TypeError
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "Irrelevant constructors are not supported"
              Relevance
    NonStrict  -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TypeError
    GenericError (ArgName -> TypeError) -> ArgName -> TypeError
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "Shape-irrelevant constructors are not supported"
            case ArgInfo -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity ArgInfo
    ai of
              Quantityω{} -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
              Quantity0{} -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
              Quantity1{} -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TypeError
    GenericError (ArgName -> TypeError) -> ArgName -> TypeError
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "Quantity-restricted constructors are not supported"
            -- check that the type of the constructor is well-formed
            (Type
    t, IsPathCons
    isPathCons) <- ArgInfo -> TCMT IO (Type, IsPathCons) -> TCMT IO (Type, IsPathCons)
    forall (tcm :: * -> *) q a.
    (MonadTCEnv tcm, LensQuantity q) =>
    q -> tcm a -> tcm a
    applyQuantityToContext ArgInfo
    ai (TCMT IO (Type, IsPathCons) -> TCMT IO (Type, IsPathCons))
    -> TCMT IO (Type, IsPathCons) -> TCMT IO (Type, IsPathCons)
    forall a b. (a -> b) -> a -> b
    $
                               Expr -> QName -> TCMT IO (Type, IsPathCons)
    checkConstructorType Expr
    e QName
    d

            -- compute which constructor arguments are forced (only point constructors)
            [IsForced]
    forcedArgs <- if IsPathCons
    isPathCons IsPathCons -> IsPathCons -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsPathCons
    PointCons
                          then QName -> Type -> TCM [IsForced]
    computeForcingAnnotations QName
    c Type
    t
                          else [IsForced] -> TCM [IsForced]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
            -- check that the sort (universe level) of the constructor type
            -- is contained in the sort of the data type
            -- (to avoid impredicative existential types)
            Sort -> TCM ()
    forall {m :: * -> *} {a}. (MonadDebug m, PrettyTCM a) => a -> m ()
    debugFitsIn Sort
    s
            -- To allow propositional squash, we turn @Prop ℓ@ into @Set ℓ@
            -- for the purpose of checking the type of the constructors.
            let s' :: Sort
    s' = case Sort
    s of
                  Prop Level
    l -> Level -> Sort
    forall t. Level' t -> Sort' t
    Type Level
    l
                  Sort
    _      -> Sort
    s
            Nat
    arity <- Call -> TCMT IO Nat -> TCMT IO Nat
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
    traceCall (QName -> Type -> Sort -> Call
    CheckConstructorFitsIn QName
    c Type
    t Sort
    s') (TCMT IO Nat -> TCMT IO Nat) -> TCMT IO Nat -> TCMT IO Nat
    forall a b. (a -> b) -> a -> b
    $
                     ArgInfo -> TCMT IO Nat -> TCMT IO Nat
    forall (tcm :: * -> *) q a.
    (MonadTCEnv tcm, LensQuantity q) =>
    q -> tcm a -> tcm a
    applyQuantityToContext ArgInfo
    ai (TCMT IO Nat -> TCMT IO Nat) -> TCMT IO Nat -> TCMT IO Nat
    forall a b. (a -> b) -> a -> b
    $
                     UniverseCheck -> [IsForced] -> Type -> Sort -> TCMT IO Nat
    fitsIn UniverseCheck
    uc [IsForced]
    forcedArgs Type
    t Sort
    s'
            -- this may have instantiated some metas in s, so we reduce
            Sort
    s <- Sort -> TCMT IO Sort
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Sort
    s
            QName -> Type -> TCM ()
    forall {m :: * -> *} {a} {a}.
    (MonadDebug m, PrettyTCM a, PrettyTCM a) =>
    a -> a -> m ()
    debugAdd QName
    c Type
    t

            (TelV Tele (Dom Type)
    fields Type
    _, Boundary
    boundary) <- Nat -> Type -> TCMT IO (TelV Type, Boundary)
    forall (m :: * -> *).
    PureTCM m =>
    Nat -> Type -> m (TelV Type, Boundary)
    telViewUpToPathBoundaryP (-Nat
    1) Type
    t

            -- We assume that the current context matches the parameters
            -- of the datatype in an empty context (c.f. getContextSize above).
            Tele (Dom Type)
    params <- TCMT IO (Tele (Dom Type))
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m) =>
    m (Tele (Dom Type))
    getContextTelescope

            (ConHead
    con, CompKit
    comp, Maybe [QName]
    projNames) <- do
                -- Name for projection of ith field of constructor c is just c-i
                [QName]
    names <- [Nat] -> (Nat -> TCMT IO QName) -> TCMT IO [QName]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Nat
    0 .. Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    fields Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1] ((Nat -> TCMT IO QName) -> TCMT IO [QName])
    -> (Nat -> TCMT IO QName) -> TCMT IO [QName]
    forall a b. (a -> b) -> a -> b
    $ \ Nat
    i ->
                  ArgName -> TCMT IO QName
    freshAbstractQName'_ (ArgName -> TCMT IO QName) -> ArgName -> TCMT IO QName
    forall a b. (a -> b) -> a -> b
    $ Name -> ArgName
    forall a. Pretty a => a -> ArgName
    P.prettyShow (QName -> Name
    A.qnameName QName
    c) ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    "-" ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ Nat -> ArgName
    forall a. Show a => a -> ArgName
    show Nat
    i

                -- nofIxs == 0 means the data type can be reconstructed
                -- by appling the QName d to the parameters.
                let dataT :: Type
    dataT = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    d (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    params

                ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.data.con.comp" Nat
    5 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ 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
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
                  [ TCMT IO Doc
    "params =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Tele (Dom Type)
    params
                  , TCMT IO Doc
    "dataT  =" 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
    dataT
                  , TCMT IO Doc
    "fields =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Tele (Dom Type) -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Tele (Dom Type)
    fields
                  , TCMT IO Doc
    "names  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [QName] -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty [QName]
    names
                  ]

                let con :: ConHead
    con = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead QName
    c DataOrRecord
    IsData Induction
    Inductive ([Arg QName] -> ConHead) -> [Arg QName] -> ConHead
    forall a b. (a -> b) -> a -> b
    $ (QName -> Arg (ArgName, Type) -> Arg QName)
    -> [QName] -> [Arg (ArgName, Type)] -> [Arg QName]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith QName -> Arg (ArgName, Type) -> Arg QName
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    (<$) [QName]
    names ([Arg (ArgName, Type)] -> [Arg QName])
    -> [Arg (ArgName, Type)] -> [Arg QName]
    forall a b. (a -> b) -> a -> b
    $ (Dom' Term (ArgName, Type) -> Arg (ArgName, Type))
    -> [Dom' Term (ArgName, Type)] -> [Arg (ArgName, Type)]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term (ArgName, Type) -> Arg (ArgName, Type)
    forall t a. Dom' t a -> Arg a
    argFromDom ([Dom' Term (ArgName, Type)] -> [Arg (ArgName, Type)])
    -> [Dom' Term (ArgName, Type)] -> [Arg (ArgName, Type)]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom' Term (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    fields

                QName
    -> ConHead
    -> Tele (Dom Type)
    -> [QName]
    -> Tele (Dom Type)
    -> Type
    -> TCM ()
    defineProjections QName
    d ConHead
    con Tele (Dom Type)
    params [QName]
    names Tele (Dom Type)
    fields Type
    dataT
                -- Cannot compose indexed inductive types yet.
                CompKit
    comp <- if Nat
    nofIxs Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Nat
    0 Bool -> Bool -> Bool
    || (DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    i IsAbstract -> IsAbstract -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsAbstract
    AbstractDef)
                        then CompKit -> TCMT IO CompKit
    forall (m :: * -> *) a. Monad m => a -> m a
    return CompKit
    emptyCompKit
                        else TCMT IO CompKit -> TCMT IO CompKit
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO CompKit -> TCMT IO CompKit)
    -> TCMT IO CompKit -> TCMT IO CompKit
    forall a b. (a -> b) -> a -> b
    $ QName
    -> ConHead
    -> Tele (Dom Type)
    -> [QName]
    -> Tele (Dom Type)
    -> Type
    -> Boundary
    -> TCMT IO CompKit
    defineCompData QName
    d ConHead
    con Tele (Dom Type)
    params [QName]
    names Tele (Dom Type)
    fields Type
    dataT Boundary
    boundary
                (ConHead, CompKit, Maybe [QName])
    -> TCMT IO (ConHead, CompKit, Maybe [QName])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ConHead
    con, CompKit
    comp, [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just [QName]
    names)

            -- add parameters to constructor type and put into signature
            Impossible -> Nat -> TCM () -> TCM ()
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Nat -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do

              QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
    addConstant' QName
    c ArgInfo
    ai QName
    c (Tele (Dom Type) -> Type -> Type
    telePi Tele (Dom Type)
    tel Type
    t) (Defn -> TCM ()) -> Defn -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Constructor :: Nat
    -> Nat
    -> ConHead
    -> QName
    -> IsAbstract
    -> Induction
    -> CompKit
    -> Maybe [QName]
    -> [IsForced]
    -> Maybe [Bool]
    -> Defn
    Constructor
                  { conPars :: Nat
    conPars   = Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel
                  , conArity :: Nat
    conArity  = Nat
    arity
                  , conSrcCon :: ConHead
    conSrcCon = ConHead
    con
                  , conData :: QName
    conData   = QName
    d
                  , conAbstr :: IsAbstract
    conAbstr  = DefInfo -> IsAbstract
    forall t. DefInfo' t -> IsAbstract
    Info.defAbstract DefInfo
    i
                  , conInd :: Induction
    conInd    = Induction
    Inductive
                  , conComp :: CompKit
    conComp   = CompKit
    comp
                  , conProj :: Maybe [QName]
    conProj   = Maybe [QName]
    projNames
                  , conForced :: [IsForced]
    conForced = [IsForced]
    forcedArgs
                  , conErased :: Maybe [Bool]
    conErased = Maybe [Bool]
    forall a. Maybe a
    Nothing  -- computed during compilation to treeless
                  }

            -- Add the constructor to the instance table, if needed
            case DefInfo -> IsInstance
    forall t. DefInfo' t -> IsInstance
    Info.defInstance DefInfo
    i of
              InstanceDef Range
    _r -> QName -> TCM () -> TCM ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange QName
    c (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
                -- Including the range of the @instance@ keyword, like
                -- @(getRange (r,c))@, does not produce good results.
                -- Andreas, 2020-01-28, issue #4360:
                -- Use addTypedInstance instead of addNamedInstance
                -- to detect unusable instances.
                QName -> Type -> TCM ()
    addTypedInstance QName
    c Type
    t
                -- addNamedInstance c d
              IsInstance
    NotInstanceDef -> () -> TCM ()
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

            IsPathCons -> TCM IsPathCons
    forall (m :: * -> *) a. Monad m => a -> m a
    return IsPathCons
    isPathCons

      where
        -- Issue 3362: we need to do the `constructs` call inside the
        -- generalization, so unpack the A.Generalize
        checkConstructorType :: Expr -> QName -> TCMT IO (Type, IsPathCons)
    checkConstructorType (A.ScopedExpr ScopeInfo
    s Expr
    e) QName
    d = ScopeInfo
    -> TCMT IO (Type, IsPathCons) -> TCMT IO (Type, IsPathCons)
    forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
    withScope_ ScopeInfo
    s (TCMT IO (Type, IsPathCons) -> TCMT IO (Type, IsPathCons))
    -> TCMT IO (Type, IsPathCons) -> TCMT IO (Type, IsPathCons)
    forall a b. (a -> b) -> a -> b
    $ Expr -> QName -> TCMT IO (Type, IsPathCons)
    checkConstructorType Expr
    e QName
    d
        checkConstructorType Expr
    e QName
    d = do
          let check :: Nat -> Expr -> TCMT IO (Type, IsPathCons)
    check Nat
    k Expr
    e = do
                Type
    t <- 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
    $ Expr -> TCMT IO Type
    isType_ Expr
    e
                -- check that the type of the constructor ends in the data type
                Nat
    n <- TCMT IO Nat
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
    getContextSize
                Type -> QName -> Nat -> TCM ()
    forall {m :: * -> *} {a} {a} {a}.
    (MonadDebug m, PrettyTCM a, PrettyTCM a, Show a) =>
    a -> a -> a -> m ()
    debugEndsIn Type
    t QName
    d (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    k)
                IsPathCons
    isPathCons <- Nat -> Nat -> Type -> QName -> TCM IsPathCons
    constructs (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    k) Nat
    k Type
    t QName
    d
                (Type, IsPathCons) -> TCMT IO (Type, IsPathCons)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type
    t, IsPathCons
    isPathCons)

          case Expr
    e of
            A.Generalized Set QName
    s Expr
    e -> do
              ([Maybe QName]
    _, Type
    t, IsPathCons
    isPathCons) <- Set QName
    -> TCMT IO (Type, IsPathCons)
    -> TCM ([Maybe QName], Type, IsPathCons)
    forall a.
    Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
    generalizeType' Set QName
    s (Nat -> Expr -> TCMT IO (Type, IsPathCons)
    check Nat
    1 Expr
    e)
              (Type, IsPathCons) -> TCMT IO (Type, IsPathCons)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type
    t, IsPathCons
    isPathCons)
            Expr
    _ -> Nat -> Expr -> TCMT IO (Type, IsPathCons)
    check Nat
    0 Expr
    e

        debugEnter :: a -> a -> m ()
    debugEnter a
    c a
    e =
          ArgName -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.data.con" Nat
    5 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "checking constructor" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    c 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
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    e
            ]
        debugEndsIn :: a -> a -> a -> m ()
    debugEndsIn a
    t a
    d a
    n =
          ArgName -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.data.con" Nat
    15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "checking that"
                  , 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
    $ a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    t
                  , TCMT IO Doc
    "ends in" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    d
                  ]
            , 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
    "nofPars =" 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 (a -> ArgName
    forall a. Show a => a -> ArgName
    show a
    n)
            ]
        debugFitsIn :: a -> m ()
    debugFitsIn a
    s =
          ArgName -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.data.con" Nat
    15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "checking that the type fits in"
            , 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
    $ a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    s
            ]
        debugAdd :: a -> a -> m ()
    debugAdd a
    c a
    t =
          ArgName -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.data.con" Nat
    5 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "adding constructor" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    c 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
    <+> a -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    t
            ]
    checkConstructor QName
    _ UniverseCheck
    _ Tele (Dom Type)
    _ Nat
    _ Sort
    _ Constructor
    _ = TCM IsPathCons
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- constructors are axioms

    defineCompData :: QName      -- datatype name
                   -> ConHead
                   -> Telescope  -- Γ parameters
                   -> [QName]    -- projection names
                   -> Telescope  -- Γ ⊢ Φ field types
                   -> Type       -- Γ ⊢ T target type
                   -> Boundary   -- [(i,t_i,b_i)],  Γ.Φ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : B_i
                   -> TCM CompKit
    defineCompData :: QName
    -> ConHead
    -> Tele (Dom Type)
    -> [QName]
    -> Tele (Dom Type)
    -> Type
    -> Boundary
    -> TCMT IO CompKit
    defineCompData QName
    d ConHead
    con Tele (Dom Type)
    params [QName]
    names Tele (Dom Type)
    fsT Type
    t Boundary
    boundary = do
      [Maybe Term]
    required <- (ArgName -> TCMT IO (Maybe Term))
    -> [ArgName] -> TCMT IO [Maybe Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ArgName -> TCMT IO (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
    getTerm'
        [ ArgName
    builtinInterval
        , ArgName
    builtinIZero
        , ArgName
    builtinIOne
        , ArgName
    builtinIMin
        , ArgName
    builtinIMax
        , ArgName
    builtinINeg
        , ArgName
    builtinPOr
        , ArgName
    builtinItIsOne
        ]
      if Bool -> Bool
    not ((Maybe Term -> Bool) -> [Maybe Term] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Maybe Term -> Bool
    forall a. Maybe a -> Bool
    isJust [Maybe Term]
    required) then CompKit -> TCMT IO CompKit
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CompKit -> TCMT IO CompKit) -> CompKit -> TCMT IO CompKit
    forall a b. (a -> b) -> a -> b
    $ CompKit
    emptyCompKit else do
        Maybe QName
    hcomp  <- Bool -> [ArgName] -> TCMT IO (Maybe QName) -> TCMT IO (Maybe QName)
    forall {m :: * -> *} {t :: * -> *} {a}.
    (Traversable t, HasBuiltins m) =>
    Bool -> t ArgName -> m (Maybe a) -> m (Maybe a)
    whenDefined (Boundary -> Bool
    forall a. Null a => a -> Bool
    null Boundary
    boundary) [ArgName
    builtinHComp,ArgName
    builtinTrans] (TranspOrHComp
    -> QName
    -> ConHead
    -> Tele (Dom Type)
    -> [QName]
    -> Tele (Dom Type)
    -> Type
    -> Boundary
    -> TCMT IO (Maybe QName)
    defineTranspOrHCompD TranspOrHComp
    DoHComp  QName
    d ConHead
    con Tele (Dom Type)
    params [QName]
    names Tele (Dom Type)
    fsT Type
    t Boundary
    boundary)
        Maybe QName
    transp <- Bool -> [ArgName] -> TCMT IO (Maybe QName) -> TCMT IO (Maybe QName)
    forall {m :: * -> *} {t :: * -> *} {a}.
    (Traversable t, HasBuiltins m) =>
    Bool -> t ArgName -> m (Maybe a) -> m (Maybe a)
    whenDefined Bool
    True            [ArgName
    builtinTrans]              (TranspOrHComp
    -> QName
    -> ConHead
    -> Tele (Dom Type)
    -> [QName]
    -> Tele (Dom Type)
    -> Type
    -> Boundary
    -> TCMT IO (Maybe QName)
    defineTranspOrHCompD TranspOrHComp
    DoTransp QName
    d ConHead
    con Tele (Dom Type)
    params [QName]
    names Tele (Dom Type)
    fsT Type
    t Boundary
    boundary)
        CompKit -> TCMT IO CompKit
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CompKit -> TCMT IO CompKit) -> CompKit -> TCMT IO CompKit
    forall a b. (a -> b) -> a -> b
    $ CompKit :: Maybe QName -> Maybe QName -> CompKit
    CompKit
          { nameOfTransp :: Maybe QName
    nameOfTransp = Maybe QName
    transp
          , nameOfHComp :: Maybe QName
    nameOfHComp  = Maybe QName
    hcomp
          }
      where
        -- Δ^I, i : I |- sub Δ : Δ
        sub :: a -> Substitution' Term
    sub a
    tel = [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS [ Nat -> Term
    var Nat
    n Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    defaultArgInfo (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Nat -> Term
    var Nat
    0] | Nat
    n <- [Nat
    1..a -> Nat
    forall a. Sized a => a -> Nat
    size a
    tel] ]
        withArgInfo :: Tele (Dom t) -> [b] -> [Arg b]
    withArgInfo Tele (Dom t)
    tel = (ArgInfo -> b -> Arg b) -> [ArgInfo] -> [b] -> [Arg b]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith ArgInfo -> b -> Arg b
    forall e. ArgInfo -> e -> Arg e
    Arg ((Dom' Term (ArgName, t) -> ArgInfo)
    -> [Dom' Term (ArgName, t)] -> [ArgInfo]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term (ArgName, t) -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo ([Dom' Term (ArgName, t)] -> [ArgInfo])
    -> (Tele (Dom t) -> [Dom' Term (ArgName, t)])
    -> Tele (Dom t)
    -> [ArgInfo]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Tele (Dom t) -> [Dom' Term (ArgName, t)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList (Tele (Dom t) -> [ArgInfo]) -> Tele (Dom t) -> [ArgInfo]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom t)
    tel)

        defineTranspOrHCompD :: TranspOrHComp
    -> QName
    -> ConHead
    -> Tele (Dom Type)
    -> [QName]
    -> Tele (Dom Type)
    -> Type
    -> Boundary
    -> TCMT IO (Maybe QName)
    defineTranspOrHCompD TranspOrHComp
    cmd QName
    d ConHead
    con Tele (Dom Type)
    params [QName]
    names Tele (Dom Type)
    fsT Type
    t Boundary
    boundary = do
          let project :: Term -> QName -> Term
    project = (\ Term
    t QName
    p -> Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    apply (QName -> Elims -> Term
    Def QName
    p []) [Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    t])
          Maybe
      ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
       Substitution' Term)
    stuff <- TranspOrHComp
    -> Maybe Term
    -> (Term -> QName -> Term)
    -> QName
    -> Tele (Dom Type)
    -> Tele (Dom Type)
    -> [Arg QName]
    -> Type
    -> TCM
         (Maybe
            ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
             Substitution' Term))
    defineTranspOrHCompForFields TranspOrHComp
    cmd
                     (Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Boundary -> Bool
    forall a. Null a => a -> Bool
    null Boundary
    boundary) Maybe () -> Maybe Term -> Maybe Term
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Term -> Maybe Term
    forall a. a -> Maybe a
    Just (ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    con ConInfo
    ConOSystem (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Boundary -> Elims
    forall a.
    DeBruijn a =>
    Tele (Dom Type) -> Boundary' (a, a) -> [Elim' a]
    teleElims Tele (Dom Type)
    fsT Boundary
    boundary))
                     Term -> QName -> Term
    project QName
    d Tele (Dom Type)
    params Tele (Dom Type)
    fsT ((QName -> Arg QName) -> [QName] -> [Arg QName]
    forall a b. (a -> b) -> [a] -> [b]
    map QName -> Arg QName
    forall e. e -> Arg e
    argN [QName]
    names) Type
    t
          Maybe
      ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
       Substitution' Term)
    -> TCMT IO (Maybe QName)
    -> (((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
         Substitution' Term)
        -> TCMT IO (Maybe QName))
    -> TCMT IO (Maybe QName)
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe
      ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
       Substitution' Term)
    stuff (Maybe QName -> TCMT IO (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe QName
    forall a. Maybe a
    Nothing) ((((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
       Substitution' Term)
      -> TCMT IO (Maybe QName))
     -> TCMT IO (Maybe QName))
    -> (((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
         Substitution' Term)
        -> TCMT IO (Maybe QName))
    -> TCMT IO (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ \ ((QName
    theName, Tele (Dom Type)
    gamma , Type
    ty, [Dom Type]
    _cl_types , [Term]
    bodies), Substitution' Term
    theSub) -> do

          Term
    iz <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIZero
          Term
    body <- do
            case TranspOrHComp
    cmd of
              TranspOrHComp
    DoHComp -> Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    con ConInfo
    ConOSystem ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Term] -> [Arg Term]
    forall {t} {b}. Tele (Dom t) -> [b] -> [Arg b]
    withArgInfo Tele (Dom Type)
    fsT [Term]
    bodies)
              TranspOrHComp
    DoTransp | Boundary -> Bool
    forall a. Null a => a -> Bool
    null Boundary
    boundary -> Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    con ConInfo
    ConOSystem ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Term] -> [Arg Term]
    forall {t} {b}. Tele (Dom t) -> [b] -> [Arg b]
    withArgInfo Tele (Dom Type)
    fsT [Term]
    bodies)
                       | Bool
    otherwise -> do
                Term
    io <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIOne
                Term
    tIMax <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIMax
                Term
    tIMin <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIMin
                Term
    tINeg <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primINeg
                Term
    tPOr  <- Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> TCMT IO (Maybe Term) -> TCMT IO Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ArgName -> TCMT IO (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
    getTerm' ArgName
    builtinPOr
                Term
    tHComp <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primHComp
                -- Δ = params
                -- Δ ⊢ Φ = fsT
                -- (δ : Δ) ⊢ T = R δ
                -- (δ : Δ) ⊢ con : Φ → R δ  -- no indexing
                -- boundary = [(i,t_i,u_i)]
                -- Δ.Φ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : B_i
                -- Δ.Φ | PiPath Φ boundary (R δ) |- teleElims fsT boundary : R δ
                -- Γ = ((δ : Δ^I), φ, us : Φ[δ 0]) = gamma
                -- Γ ⊢ ty = R (δ i1)
                -- (γ : Γ) ⊢ cl_types = (flatten Φ)[n ↦ f_n (transpR γ)]
                -- Γ ⊢ bodies : Φ[δ i1]
                -- Γ ⊢ t : ty
                -- Γ, i : I ⊢ theSub : Δ.Φ
                let

                  -- Δ.Φ ⊢ u = Con con ConOSystem $ teleElims fsT boundary : R δ
                  u :: Term
    u = ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    con ConInfo
    ConOSystem (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> Boundary -> Elims
    forall a.
    DeBruijn a =>
    Tele (Dom Type) -> Boundary' (a, a) -> [Elim' a]
    teleElims Tele (Dom Type)
    fsT Boundary
    boundary
                  -- Γ ⊢ u
                  the_u :: Term
    the_u = Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    fsT) Substitution' Term
    d0 Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Term
    u
                    where
                      -- δ : Δ^I, φ : F ⊢ [δ 0] : Δ
                      d0 :: Substitution
                      d0 :: Substitution' Term
    d0 = Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS Nat
    1 -- Δ^I, φ : F ⊢ Δ
                                 (Term -> Substitution' Term -> Substitution' Term
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS Term
    iz Substitution' Term
    forall a. Substitution' a
    IdS Substitution' Term -> Substitution' Term -> Substitution' Term
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Tele (Dom Type) -> Substitution' Term
    forall {a}. Sized a => a -> Substitution' Term
    sub Tele (Dom Type)
    params) -- Δ^I ⊢ Δ
                                           -- Δ^I , i:I ⊢ sub params : Δ
                  the_phi :: Term
    the_phi = Nat -> Term -> Term
    forall a. Subst a => Nat -> a -> a
    raise (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    fsT) (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Nat -> Term
    var Nat
    0
                  -- Γ ⊢ sigma : Δ.Φ
                  -- sigma = [δ i1,bodies]
                  sigma :: Substitution' Term
    sigma = [Term] -> [Term]
    forall a. [a] -> [a]
    reverse [Term]
    bodies [Term] -> Substitution' Term -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# Substitution' Term
    d1
                   where
                    -- δ i1
                    d1 :: Substitution
                    d1 :: Substitution' Term
    d1 = Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    gamma Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    params) -- Γ ⊢ Δ
                           (Term -> Substitution' Term -> Substitution' Term
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS Term
    io Substitution' Term
    forall a. Substitution' a
    IdS Substitution' Term -> Substitution' Term -> Substitution' Term
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Tele (Dom Type) -> Substitution' Term
    forall {a}. Sized a => a -> Substitution' Term
    sub Tele (Dom Type)
    params) -- Δ^I ⊢ Δ
                                     -- Δ^I , i:I ⊢ sub params : Δ

                  -- Δ.Φ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : R δ
                  bs :: Boundary
    bs = Tele (Dom Type) -> Boundary -> Boundary
    fullBoundary Tele (Dom Type)
    fsT Boundary
    boundary
                  -- ψ = sigma `applySubst` map (\ i → i ∨ ~ i) . map fst $ boundary
                  -- Γ ⊢ t : R (δ i1)
                  w1' :: Term
    w1' = ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    con ConInfo
    ConOSystem (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ Substitution' Term
    Substitution' (SubstArg Elims)
    sigma Substitution' (SubstArg Elims) -> Elims -> Elims
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Tele (Dom Type) -> Boundary -> Elims
    forall a.
    DeBruijn a =>
    Tele (Dom Type) -> Boundary' (a, a) -> [Elim' a]
    teleElims Tele (Dom Type)
    fsT Boundary
    boundary
                  -- (δ, φ, u0) : Γ ⊢
                  -- w1 = hcomp (\ i → R (δ i1))
                  --            (\ i → [ ψ ↦ α (~ i), φ ↦ u0])
                  --            w1'
                  imax :: NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    imax NamesT (TCMT IO) Term
    x NamesT (TCMT IO) Term
    y = Term -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tIMax NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    x NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    y
                  ineg :: NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    ineg NamesT (TCMT IO) Term
    r = Term -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tINeg NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    r
                  lvlOfType :: Type -> Term
    lvlOfType = (\ (Type Level
    l) -> Level -> Term
    Level Level
    l) (Sort -> Term) -> (Type -> Sort) -> Type -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort
                  pOr :: NamesT (TCMT IO) Type
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    pOr NamesT (TCMT IO) Type
    la NamesT (TCMT IO) Term
    i NamesT (TCMT IO) Term
    j NamesT (TCMT IO) Term
    u0 NamesT (TCMT IO) Term
    u1 = Term -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tPOr NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (Type -> Term
    lvlOfType (Type -> Term) -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) Type
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    i NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    j
                                               NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> ArgName
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
    -> NamesT (TCMT IO) Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam ArgName
    "o" (\ NamesT (TCMT IO) Term
    _ -> Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) Type
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    u0 NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    u1
                  absAp :: m (Abs r) -> m (SubstArg r) -> m r
    absAp m (Abs r)
    x m (SubstArg r)
    y = (Abs r -> SubstArg r -> r) -> m (Abs r) -> m (SubstArg r) -> m r
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 Abs r -> SubstArg r -> r
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp m (Abs r)
    x m (SubstArg r)
    y

                  mkFace :: (Term, (Term, Term)) -> TCMT IO (Abs (Term, Term))
    mkFace (Term
    r,(Term
    u1,Term
    u2)) = [ArgName]
    -> NamesT (TCMT IO) (Abs (Term, Term))
    -> TCMT IO (Abs (Term, Term))
    forall (m :: * -> *) a. [ArgName] -> NamesT m a -> m a
    runNamesT [] (NamesT (TCMT IO) (Abs (Term, Term)) -> TCMT IO (Abs (Term, Term)))
    -> NamesT (TCMT IO) (Abs (Term, Term))
    -> TCMT IO (Abs (Term, Term))
    forall a b. (a -> b) -> a -> b
    $ do
                    -- Γ
                    NamesT (TCMT IO) Term
    phi <- Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open Term
    the_phi  -- (δ , φ , us) ⊢ φ
                    -- Γ ⊢ ty = Abs i. R (δ i)
                    NamesT (TCMT IO) (Abs Type)
    ty <- Abs Type -> NamesT (TCMT IO) (NamesT (TCMT IO) (Abs Type))
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open (ArgName -> Type -> Abs Type
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    "i" (Type -> Abs Type) -> Type -> Abs Type
    forall a b. (a -> b) -> a -> b
    $ (Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    1 (Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    gamma Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    params)) Substitution' Term -> Substitution' Term -> Substitution' Term
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Tele (Dom Type) -> Substitution' Term
    forall {a}. Sized a => a -> Substitution' Term
    sub Tele (Dom Type)
    params) Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Type
    t)

                    ArgName
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) (Term, Term))
    -> NamesT (TCMT IO) (Abs (Term, Term))
    forall (m :: * -> *) b a.
    (MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
    ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
    bind ArgName
    "i" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) (Term, Term))
     -> NamesT (TCMT IO) (Abs (Term, Term)))
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) (Term, Term))
    -> NamesT (TCMT IO) (Abs (Term, Term))
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    i -> do
                      -- Γ, i
                      [NamesT (TCMT IO) Term
    r,NamesT (TCMT IO) Term
    u1,NamesT (TCMT IO) Term
    u2] <- (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
    -> [Term] -> NamesT (TCMT IO) [NamesT (TCMT IO) Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
    -> (Term -> Term)
    -> Term
    -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg Term)
    theSub) [Term
    r,Term
    u1,Term
    u2]
                      Term
    psi <- NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    imax NamesT (TCMT IO) Term
    r (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    ineg NamesT (TCMT IO) Term
    r)
                      let
                        -- Γ, i ⊢ squeeze u = primTrans (\ j -> ty [i := i ∨ j]) (φ ∨ i) u
                        squeeze :: NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    squeeze NamesT (TCMT IO) Term
    u = TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primTrans
                                              NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> ArgName
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
    -> NamesT (TCMT IO) Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam ArgName
    "j" (\ NamesT (TCMT IO) Term
    j -> Type -> Term
    lvlOfType (Type -> Term) -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) (Abs Type)
    ty NamesT (TCMT IO) (Abs Type)
    -> NamesT (TCMT IO) (SubstArg Type) -> NamesT (TCMT IO) Type
    forall {m :: * -> *} {r}.
    (Monad m, Subst r) =>
    m (Abs r) -> m (SubstArg r) -> m r
    `absAp` (NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    imax NamesT (TCMT IO) Term
    i NamesT (TCMT IO) Term
    j))
                                              NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> ArgName
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
    -> NamesT (TCMT IO) Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam ArgName
    "j" (\ NamesT (TCMT IO) Term
    j -> Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) (Abs Type)
    ty NamesT (TCMT IO) (Abs Type)
    -> NamesT (TCMT IO) (SubstArg Type) -> NamesT (TCMT IO) Type
    forall {m :: * -> *} {r}.
    (Monad m, Subst r) =>
    m (Abs r) -> m (SubstArg r) -> m r
    `absAp` (NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    imax NamesT (TCMT IO) Term
    i NamesT (TCMT IO) Term
    j))
                                              NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (NamesT (TCMT IO) Term
    phi NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    `imax` NamesT (TCMT IO) Term
    i)
                                              NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    u
                      Term
    alpha <- NamesT (TCMT IO) Type
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    pOr (NamesT (TCMT IO) (Abs Type)
    ty NamesT (TCMT IO) (Abs Type)
    -> NamesT (TCMT IO) (SubstArg Type) -> NamesT (TCMT IO) Type
    forall {m :: * -> *} {r}.
    (Monad m, Subst r) =>
    m (Abs r) -> m (SubstArg r) -> m r
    `absAp` NamesT (TCMT IO) Term
    NamesT (TCMT IO) (SubstArg Type)
    i)
                                  (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    ineg NamesT (TCMT IO) Term
    r)
                                  NamesT (TCMT IO) Term
    r
                               (ArgName
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
    -> NamesT (TCMT IO) Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam ArgName
    "o" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
     -> NamesT (TCMT IO) Term)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
    -> NamesT (TCMT IO) Term
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    _ -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    squeeze NamesT (TCMT IO) Term
    u1) (ArgName
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
    -> NamesT (TCMT IO) Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam ArgName
    "o" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
     -> NamesT (TCMT IO) Term)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
    -> NamesT (TCMT IO) Term
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    _ -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    squeeze NamesT (TCMT IO) Term
    u2)
                      (Term, Term) -> NamesT (TCMT IO) (Term, Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Term, Term) -> NamesT (TCMT IO) (Term, Term))
    -> (Term, Term) -> NamesT (TCMT IO) (Term, Term)
    forall a b. (a -> b) -> a -> b
    $ (Term
    psi, Term
    alpha)

                -- Γ ⊢ Abs i. [(ψ_n,α_n : [ψ] → R (δ i))]
                [Abs (Term, Term)]
    faces <- ((Term, (Term, Term)) -> TCMT IO (Abs (Term, Term)))
    -> Boundary -> TCMT IO [Abs (Term, Term)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Term, (Term, Term)) -> TCMT IO (Abs (Term, Term))
    mkFace Boundary
    bs

                [ArgName] -> NamesT (TCMT IO) Term -> TCMT IO Term
    forall (m :: * -> *) a. [ArgName] -> NamesT m a -> m a
    runNamesT [] (NamesT (TCMT IO) Term -> TCMT IO Term)
    -> NamesT (TCMT IO) Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ do
                    -- Γ
                    NamesT (TCMT IO) Term
    w1' <- Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open Term
    w1'
                    NamesT (TCMT IO) Term
    phi <- Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open Term
    the_phi
                    NamesT (TCMT IO) Term
    u   <- Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open Term
    the_u
                    -- R (δ i1)
                    NamesT (TCMT IO) Type
    ty <- Type -> NamesT (TCMT IO) (NamesT (TCMT IO) Type)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open Type
    ty
                    [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
    faces <- (Abs (Term, Term)
     -> NamesT
          (TCMT IO) (NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term)))
    -> [Abs (Term, Term)]
    -> NamesT
         (TCMT IO) [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (\ Abs (Term, Term)
    x -> (NamesT (TCMT IO) Term
     -> NamesT (TCMT IO) (Abs Term)
     -> (NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term)))
    -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
    -> NamesT (TCMT IO) (NamesT (TCMT IO) (Abs Term))
    -> NamesT
         (TCMT IO) (NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 (,) (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open (Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
    -> (Abs Term -> Term)
    -> Abs Term
    -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Impossible -> Abs Term -> Term
    forall a. Subst a => Impossible -> Abs a -> a
    noabsApp Impossible
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Abs Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term))
    -> Abs Term -> NamesT (TCMT IO) (NamesT (TCMT IO) Term)
    forall a b. (a -> b) -> a -> b
    $ ((Term, Term) -> Term) -> Abs (Term, Term) -> Abs Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Term, Term) -> Term
    forall a b. (a, b) -> a
    fst Abs (Term, Term)
    x) (Abs Term -> NamesT (TCMT IO) (NamesT (TCMT IO) (Abs Term))
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open (Abs Term -> NamesT (TCMT IO) (NamesT (TCMT IO) (Abs Term)))
    -> Abs Term -> NamesT (TCMT IO) (NamesT (TCMT IO) (Abs Term))
    forall a b. (a -> b) -> a -> b
    $ ((Term, Term) -> Term) -> Abs (Term, Term) -> Abs Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Term, Term) -> Term
    forall a b. (a, b) -> b
    snd Abs (Term, Term)
    x)) [Abs (Term, Term)]
    faces
                    let
                      thePsi :: NamesT (TCMT IO) Term
    thePsi = (NamesT (TCMT IO) Term
     -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
    -> [NamesT (TCMT IO) Term] -> NamesT (TCMT IO) Term
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldl1 NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    imax (((NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))
     -> NamesT (TCMT IO) Term)
    -> [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
    -> [NamesT (TCMT IO) Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))
    -> NamesT (TCMT IO) Term
    forall a b. (a, b) -> a
    fst [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
    faces)
                      hcomp :: NamesT (TCMT IO) Type
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    hcomp NamesT (TCMT IO) Type
    ty NamesT (TCMT IO) Term
    phi NamesT (TCMT IO) Term
    sys NamesT (TCMT IO) Term
    a0 = Term -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tHComp NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (Type -> Term
    lvlOfType (Type -> Term) -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) Type
    ty)
                                                        NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) Type
    ty)
                                                        NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT (TCMT IO) Term
    phi
                                                        NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    sys
                                                        NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    a0
                    let
                     sys :: NamesT (TCMT IO) Term
    sys = ArgName
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
    -> NamesT (TCMT IO) Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam ArgName
    "i" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
     -> NamesT (TCMT IO) Term)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
    -> NamesT (TCMT IO) Term
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    i -> do
                      let
                        recurse :: [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
    -> NamesT (TCMT IO) Term
    recurse [(NamesT (TCMT IO) Term
    psi,NamesT (TCMT IO) (Abs Term)
    alpha)] = NamesT (TCMT IO) (Abs Term)
    alpha NamesT (TCMT IO) (Abs Term)
    -> NamesT (TCMT IO) (SubstArg Term) -> NamesT (TCMT IO) Term
    forall {m :: * -> *} {r}.
    (Monad m, Subst r) =>
    m (Abs r) -> m (SubstArg r) -> m r
    `absAp` (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    ineg NamesT (TCMT IO) Term
    i)
                        recurse ((NamesT (TCMT IO) Term
    psi,NamesT (TCMT IO) (Abs Term)
    alpha):[(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
    xs) = NamesT (TCMT IO) Type
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    pOr NamesT (TCMT IO) Type
    ty
                                                       NamesT (TCMT IO) Term
    psi  NamesT (TCMT IO) Term
    theOr
                                                       (NamesT (TCMT IO) (Abs Term)
    alpha NamesT (TCMT IO) (Abs Term)
    -> NamesT (TCMT IO) (SubstArg Term) -> NamesT (TCMT IO) Term
    forall {m :: * -> *} {r}.
    (Monad m, Subst r) =>
    m (Abs r) -> m (SubstArg r) -> m r
    `absAp` (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    ineg NamesT (TCMT IO) Term
    i)) ([(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
    -> NamesT (TCMT IO) Term
    recurse [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
    xs)
                          where
                            theOr :: NamesT (TCMT IO) Term
    theOr = (NamesT (TCMT IO) Term
     -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
    -> [NamesT (TCMT IO) Term] -> NamesT (TCMT IO) Term
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldl1 NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    imax (((NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))
     -> NamesT (TCMT IO) Term)
    -> [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
    -> [NamesT (TCMT IO) Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))
    -> NamesT (TCMT IO) Term
    forall a b. (a, b) -> a
    fst [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
    xs)
                        recurse [] = NamesT (TCMT IO) Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                        sys_alpha :: NamesT (TCMT IO) Term
    sys_alpha = [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
    -> NamesT (TCMT IO) Term
    recurse [(NamesT (TCMT IO) Term, NamesT (TCMT IO) (Abs Term))]
    faces
                      NamesT (TCMT IO) Type
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    pOr NamesT (TCMT IO) Type
    ty
                                                       NamesT (TCMT IO) Term
    thePsi    NamesT (TCMT IO) Term
    phi
                                                       NamesT (TCMT IO) Term
    sys_alpha (ArgName
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
    -> NamesT (TCMT IO) Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam ArgName
    "o" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
     -> NamesT (TCMT IO) Term)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
    -> NamesT (TCMT IO) Term
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    _ -> NamesT (TCMT IO) Term
    u)
                    NamesT (TCMT IO) Type
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term
    hcomp NamesT (TCMT IO) Type
    ty (NamesT (TCMT IO) Term
    thePsi NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    `imax` NamesT (TCMT IO) Term
    phi) NamesT (TCMT IO) Term
    sys NamesT (TCMT IO) Term
    w1'

          let

            -- δ : Δ^I, φ : F ⊢ [δ 0] : Δ
            d0 :: Substitution
            d0 :: Substitution' Term
    d0 = Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS Nat
    1 -- Δ^I, φ : F ⊢ Δ
                           (Term -> Substitution' Term -> Substitution' Term
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS Term
    iz Substitution' Term
    forall a. Substitution' a
    IdS Substitution' Term -> Substitution' Term -> Substitution' Term
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Tele (Dom Type) -> Substitution' Term
    forall {a}. Sized a => a -> Substitution' Term
    sub Tele (Dom Type)
    params) -- Δ^I ⊢ Δ
                                     -- Δ^I , i:I ⊢ sub params : Δ

            -- Δ.Φ ⊢ u = Con con ConOSystem $ teleElims fsT boundary : R δ
    --        u = Con con ConOSystem $ teleElims fsT boundary
            up :: Pattern' DBPatVar
    up = ConHead
    -> ConPatternInfo
    -> [NamedArg (Pattern' DBPatVar)]
    -> Pattern' DBPatVar
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    con (PatternInfo
    -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
    ConPatternInfo PatternInfo
    defaultPatternInfo Bool
    False Bool
    False Maybe (Arg Type)
    forall a. Maybe a
    Nothing Bool
    False) ([NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar)
    -> [NamedArg (Pattern' DBPatVar)] -> Pattern' DBPatVar
    forall a b. (a -> b) -> a -> b
    $
                   Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' DBPatVar)]
    forall a.
    DeBruijn a =>
    Tele (Dom Type) -> Boundary -> [NamedArg (Pattern' a)]
    telePatterns (Substitution' Term
    Substitution' (SubstArg (Tele (Dom Type)))
    d0 Substitution' (SubstArg (Tele (Dom Type)))
    -> Tele (Dom Type) -> Tele (Dom Type)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Tele (Dom Type)
    fsT) (Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    fsT) Substitution' Term
    d0 Substitution' (SubstArg Boundary) -> Boundary -> Boundary
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Boundary
    boundary)
    --        gamma' = telFromList $ take (size gamma - 1) $ telToList gamma

            -- (δ , φ , fs : Φ[d0]) ⊢ u[liftS Φ d0]
            -- (δ , φ, u) : Γ ⊢ body
            -- Δ ⊢ Φ = fsT
            -- (δ , φ , fs : Φ[d0]) ⊢ u[liftS Φ d0] `consS` raiseS Φ : Γ
    --        (tel',theta) = (abstract gamma' (d0 `applySubst` fsT), (liftS (size fsT) d0 `applySubst` u) `consS` raiseS (size fsT))

          let
            pats :: [NamedArg (Pattern' DBPatVar)]
    pats | Boundary -> Bool
    forall a. Null a => a -> Bool
    null Boundary
    boundary = Tele (Dom Type) -> [NamedArg (Pattern' DBPatVar)]
    forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
    teleNamedArgs Tele (Dom Type)
    gamma
                 | Bool
    otherwise     = Nat
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a. Nat -> [a] -> [a]
    take (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    gamma Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    fsT) (Tele (Dom Type) -> [NamedArg (Pattern' DBPatVar)]
    forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
    teleNamedArgs Tele (Dom Type)
    gamma) [NamedArg (Pattern' DBPatVar)]
    -> [NamedArg (Pattern' DBPatVar)] -> [NamedArg (Pattern' DBPatVar)]
    forall a. [a] -> [a] -> [a]
    ++ [Named NamedName (Pattern' DBPatVar) -> NamedArg (Pattern' DBPatVar)
    forall e. e -> Arg e
    argN (Named NamedName (Pattern' DBPatVar)
     -> NamedArg (Pattern' DBPatVar))
    -> Named NamedName (Pattern' DBPatVar)
    -> NamedArg (Pattern' DBPatVar)
    forall a b. (a -> b) -> a -> b
    $ Pattern' DBPatVar -> Named NamedName (Pattern' DBPatVar)
    forall a name. a -> Named name a
    unnamed (Pattern' DBPatVar -> Named NamedName (Pattern' DBPatVar))
    -> Pattern' DBPatVar -> Named NamedName (Pattern' DBPatVar)
    forall a b. (a -> b) -> a -> b
    $ Pattern' DBPatVar
    up]
            clause :: Clause
    clause = Clause :: Range
    -> Range
    -> Tele (Dom Type)
    -> [NamedArg (Pattern' DBPatVar)]
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Bool
    -> Maybe Bool
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Clause
    Clause
              { clauseTel :: Tele (Dom Type)
    clauseTel         = Tele (Dom Type)
    gamma
              , clauseType :: Maybe (Arg Type)
    clauseType        = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just (Arg Type -> Maybe (Arg Type))
    -> (Type -> Arg Type) -> Type -> Maybe (Arg Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Arg Type
    forall e. e -> Arg e
    argN (Type -> Maybe (Arg Type)) -> Type -> Maybe (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ Type
    ty
              , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
    namedClausePats   = [NamedArg (Pattern' DBPatVar)]
    pats
              , clauseFullRange :: Range
    clauseFullRange   = Range
    forall a. Range' a
    noRange
              , clauseLHSRange :: Range
    clauseLHSRange    = Range
    forall a. Range' a
    noRange
              , clauseCatchall :: Bool
    clauseCatchall    = Bool
    False
              , clauseBody :: Maybe Term
    clauseBody        = Term -> Maybe Term
    forall a. a -> Maybe a
    Just (Term -> Maybe Term) -> Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Term
    body
              , clauseExact :: Maybe Bool
    clauseExact       = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
              , clauseRecursive :: Maybe Bool
    clauseRecursive   = Maybe Bool
    forall a. Maybe a
    Nothing
                  -- Andreas 2020-02-06 TODO
                  -- Or: Just False;  is it known to be non-recursive?
              , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
              , clauseEllipsis :: ExpandedEllipsis
    clauseEllipsis    = ExpandedEllipsis
    NoEllipsis
              }
            cs :: [Clause]
    cs = [Clause
    clause]
          QName -> [Clause] -> TCM ()
    addClauses QName
    theName [Clause]
    cs
          (Maybe SplitTree
    mst, Bool
    _, CompiledClauses
    cc) <- TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (Maybe (QName, Type)
    -> [Clause] -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    compileClauses Maybe (QName, Type)
    forall a. Maybe a
    Nothing [Clause]
    cs)
          Maybe SplitTree -> (SplitTree -> TCM ()) -> TCM ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust Maybe SplitTree
    mst ((SplitTree -> TCM ()) -> TCM ())
    -> (SplitTree -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> SplitTree -> TCM ()
    setSplitTree QName
    theName
          QName -> CompiledClauses -> TCM ()
    setCompiledClauses QName
    theName CompiledClauses
    cc
          QName -> Bool -> TCM ()
    setTerminates QName
    theName Bool
    True
          Maybe QName -> TCMT IO (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe QName -> TCMT IO (Maybe QName))
    -> Maybe QName -> TCMT IO (Maybe QName)
    forall a b. (a -> b) -> a -> b
    $ QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    theName

        whenDefined :: Bool -> t ArgName -> m (Maybe a) -> m (Maybe a)
    whenDefined Bool
    False t ArgName
    _ m (Maybe a)
    _ = Maybe a -> m (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing
        whenDefined Bool
    True t ArgName
    xs m (Maybe a)
    m = do
          t (Maybe Term)
    xs <- (ArgName -> m (Maybe Term)) -> t ArgName -> m (t (Maybe Term))
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ArgName -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe Term)
    getTerm' t ArgName
    xs
          if (Maybe Term -> Bool) -> t (Maybe Term) -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Maybe Term -> Bool
    forall a. Maybe a -> Bool
    isJust t (Maybe Term)
    xs then m (Maybe a)
    m else Maybe a -> m (Maybe a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe a
    forall a. Maybe a
    Nothing

    -- Andrea: TODO handle Irrelevant fields somehow.
    -- | Define projections for non-indexed data types (families don't work yet).
    --   Of course, these projections are partial functions in general.
    --
    --   Precondition: we are in the context Γ of the data type parameters.
    defineProjections :: QName      -- datatype name
                      -> ConHead
                      -> Telescope  -- Γ parameters
                      -> [QName]    -- projection names
                      -> Telescope  -- Γ ⊢ Φ field types
                      -> Type       -- Γ ⊢ T target type
                      -> TCM ()
    defineProjections :: QName
    -> ConHead
    -> Tele (Dom Type)
    -> [QName]
    -> Tele (Dom Type)
    -> Type
    -> TCM ()
    defineProjections QName
    dataName ConHead
    con Tele (Dom Type)
    params [QName]
    names Tele (Dom Type)
    fsT Type
    t = do
      let
        -- Γ , (d : T) ⊢ Φ[n ↦ proj n d]
        fieldTypes :: [Dom Type]
    fieldTypes = ([ QName -> Elims -> Term
    Def QName
    f [] Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Term -> Arg Term
    forall e. e -> Arg e
    argN (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Nat -> Term
    var Nat
    0] | QName
    f <- [QName] -> [QName]
    forall a. [a] -> [a]
    reverse [QName]
    names ] [Term] -> Substitution' Term -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS Nat
    1) Substitution' (SubstArg [Dom Type]) -> [Dom Type] -> [Dom Type]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst`
                        Tele (Dom Type) -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Tele (Dom Type)
    fsT  -- Γ , Φ ⊢ Φ
        -- ⊢ Γ , (d : T)
        projTel :: Tele (Dom Type)
    projTel    = Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    params (Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Type -> Dom Type
    forall a. a -> Dom a
    defaultDom Type
    t) (ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    "d" Tele (Dom Type)
    forall a. Tele a
    EmptyTel))
        np :: Nat
    np         = Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    params

      [(Nat, QName, Dom Type)]
    -> ((Nat, QName, Dom Type) -> TCM ()) -> TCM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ ([Nat] -> [QName] -> [Dom Type] -> [(Nat, QName, Dom Type)]
    forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
    zip3 (Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom ([Dom Type] -> Nat
    forall a. Sized a => a -> Nat
    size [Dom Type]
    fieldTypes)) [QName]
    names [Dom Type]
    fieldTypes) (((Nat, QName, Dom Type) -> TCM ()) -> TCM ())
    -> ((Nat, QName, Dom Type) -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ (Nat
    i,QName
    projName,Dom Type
    ty) -> do
        let
          projType :: Dom Type
    projType = Tele (Dom Type) -> Type -> Type
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    projTel (Type -> Type) -> Dom Type -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Dom Type
    ty
          cpi :: ConPatternInfo
    cpi    = PatternInfo
    -> Bool -> Bool -> Maybe (Arg Type) -> Bool -> ConPatternInfo
    ConPatternInfo PatternInfo
    defaultPatternInfo Bool
    False Bool
    False (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 -> Arg Type) -> Type -> Arg Type
    forall a b. (a -> b) -> a -> b
    $ Nat -> Type -> Type
    forall a. Subst a => Nat -> a -> a
    raise (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    fsT) Type
    t) Bool
    False
          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
    $ Tele (Dom Type) -> [NamedArg (Pattern' DBPatVar)]
    forall a. DeBruijn a => Tele (Dom Type) -> [NamedArg a]
    teleNamedArgs Tele (Dom Type)
    fsT
          sigma :: Substitution' Term
    sigma  = ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    con ConInfo
    ConOSystem ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    fsT) Term -> Substitution' Term -> Substitution' Term
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    `consS` Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    fsT)
          clause :: Clause
    clause = Clause
    forall a. Null a => a
    empty
              { clauseTel :: Tele (Dom Type)
    clauseTel         = Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    params Tele (Dom Type)
    fsT
              , namedClausePats :: [NamedArg (Pattern' DBPatVar)]
    namedClausePats   = [ NamedArg (Pattern' DBPatVar)
    conp ]
              , 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
    $ Nat -> Term
    var Nat
    i
              , 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 -> Arg Type) -> Type -> Arg Type
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg Type)
    sigma (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    ty
              , clauseRecursive :: Maybe Bool
    clauseRecursive   = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False  -- non-recursive
              , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
              }

        ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.data.proj" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ 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
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
          [ TCMT IO Doc
    "proj" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Nat, Dom Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Nat
    i,Dom Type
    ty)
          , 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
    sep [ QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    projName, TCMT IO Doc
    ":", Dom Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Dom Type
    projType ]
          ]

        -- Andreas, 2020-02-14, issue #4437
        -- Define data projections as projection-like from the start.
        TCM () -> TCM ()
    forall a. TCM a -> TCM a
    noMutualBlock (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
          let cs :: [Clause]
    cs = [ Clause
    clause ]
          (Maybe SplitTree
    mst, Bool
    _, CompiledClauses
    cc) <- Maybe (QName, Type)
    -> [Clause] -> TCMT IO (Maybe SplitTree, Bool, CompiledClauses)
    compileClauses Maybe (QName, Type)
    forall a. Maybe a
    Nothing [Clause]
    cs
          let fun :: Defn
    fun = Defn
    emptyFunction
                    { funClauses :: [Clause]
    funClauses    = [Clause]
    cs
                    , funCompiled :: Maybe CompiledClauses
    funCompiled   = CompiledClauses -> Maybe CompiledClauses
    forall a. a -> Maybe a
    Just CompiledClauses
    cc
                    , funSplitTree :: Maybe SplitTree
    funSplitTree  = Maybe SplitTree
    mst
                    , funProjection :: Maybe Projection
    funProjection = Projection -> Maybe Projection
    forall a. a -> Maybe a
    Just (Projection -> Maybe Projection) -> Projection -> Maybe Projection
    forall a b. (a -> b) -> a -> b
    $ Projection :: Maybe QName -> QName -> Arg QName -> Nat -> ProjLams -> Projection
    Projection
                        { projProper :: Maybe QName
    projProper   = Maybe QName
    forall a. Maybe a
    Nothing
                        , projOrig :: QName
    projOrig     = QName
    projName
                        , projFromType :: Arg QName
    projFromType = ArgInfo -> QName -> Arg QName
    forall e. ArgInfo -> e -> Arg e
    Arg (Dom Type -> ArgInfo
    forall a. LensArgInfo a => a -> ArgInfo
    getArgInfo Dom Type
    ty) QName
    dataName
                        , projIndex :: Nat
    projIndex    = Nat
    np Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    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) -> Arg ArgName)
    -> [Dom' Term (ArgName, Type)] -> [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) -> Dom' Term ArgName)
    -> Dom' Term (ArgName, Type)
    -> Arg ArgName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((ArgName, Type) -> ArgName)
    -> Dom' Term (ArgName, Type) -> Dom' Term ArgName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ArgName, Type) -> ArgName
    forall a b. (a, b) -> a
    fst) ([Dom' Term (ArgName, Type)] -> [Arg ArgName])
    -> [Dom' Term (ArgName, Type)] -> [Arg ArgName]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom' Term (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    projTel
                        }
                    , funMutual :: Maybe [QName]
    funMutual     = [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just []
                    , funTerminates :: Maybe Bool
    funTerminates = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
                    }
          Language
    lang <- TCMT IO Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
          TCM () -> TCM ()
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Definition -> TCM ()
    addConstant QName
    projName (Definition -> TCM ()) -> Definition -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
            (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
    defaultDefn ArgInfo
    defaultArgInfo QName
    projName (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    projType) Language
    lang Defn
    fun)
              { defNoCompilation :: Bool
    defNoCompilation  = Bool
    True
              , defArgOccurrences :: [Occurrence]
    defArgOccurrences = [Occurrence
    StrictPos]
              }

          ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.data.proj.fun" Nat
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ 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
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "proj" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Nat -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Nat
    i
            , 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
    $ Defn -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Defn
    fun
            ]

    freshAbstractQName'_ :: String -> TCM QName
    freshAbstractQName'_ :: ArgName -> TCMT IO QName
    freshAbstractQName'_ = Fixity' -> Name -> TCMT IO QName
    freshAbstractQName Fixity'
    noFixity' (Name -> TCMT IO QName)
    -> (ArgName -> Name) -> ArgName -> TCMT IO QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgName -> Name
    C.simpleName

    -- * Special cases of Type
    -----------------------------------------------------------

    -- | A @Type@ with sort @Type l@
    --   Such a type supports both hcomp and transp.
    data LType = LEl Level Term deriving (LType -> LType -> Bool
    (LType -> LType -> Bool) -> (LType -> LType -> Bool) -> Eq LType
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: LType -> LType -> Bool
    $c/= :: LType -> LType -> Bool
    == :: LType -> LType -> Bool
    $c== :: LType -> LType -> Bool
    Eq,Nat -> LType -> ArgName -> ArgName
    [LType] -> ArgName -> ArgName
    LType -> ArgName
    (Nat -> LType -> ArgName -> ArgName)
    -> (LType -> ArgName)
    -> ([LType] -> ArgName -> ArgName)
    -> Show LType
    forall a.
    (Nat -> a -> ArgName -> ArgName)
    -> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
    showList :: [LType] -> ArgName -> ArgName
    $cshowList :: [LType] -> ArgName -> ArgName
    show :: LType -> ArgName
    $cshow :: LType -> ArgName
    showsPrec :: Nat -> LType -> ArgName -> ArgName
    $cshowsPrec :: Nat -> LType -> ArgName -> ArgName
    Show)

    fromLType :: LType -> Type
    fromLType :: LType -> Type
    fromLType (LEl Level
    l Term
    t) = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Level -> Sort
    forall t. Level' t -> Sort' t
    Type Level
    l) Term
    t

    lTypeLevel :: LType -> Level
    lTypeLevel :: LType -> Level
    lTypeLevel (LEl Level
    l Term
    t) = Level
    l

    toLType :: MonadReduce m => Type -> m (Maybe LType)
    toLType :: forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
    toLType Type
    ty = do
      Sort
    sort <- Sort -> m Sort
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Type
    ty
      case Sort
    sort of
        Type Level
    l -> Maybe LType -> m (Maybe LType)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe LType -> m (Maybe LType)) -> Maybe LType -> m (Maybe LType)
    forall a b. (a -> b) -> a -> b
    $ LType -> Maybe LType
    forall a. a -> Maybe a
    Just (LType -> Maybe LType) -> LType -> Maybe LType
    forall a b. (a -> b) -> a -> b
    $ Level -> Term -> LType
    LEl Level
    l (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    ty)
        Sort
    _      -> Maybe LType -> m (Maybe LType)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe LType -> m (Maybe LType)) -> Maybe LType -> m (Maybe LType)
    forall a b. (a -> b) -> a -> b
    $ Maybe LType
    forall a. Maybe a
    Nothing

    instance Subst LType where
      type SubstArg LType = Term
      applySubst :: Substitution' (SubstArg LType) -> LType -> LType
    applySubst Substitution' (SubstArg LType)
    rho (LEl Level
    l Term
    t) = Level -> Term -> LType
    LEl (Substitution' (SubstArg Level) -> Level -> Level
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Level)
    Substitution' (SubstArg LType)
    rho Level
    l) (Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Term)
    Substitution' (SubstArg LType)
    rho Term
    t)

    -- | A @Type@ that either has sort @Type l@ or is a closed definition.
    --   Such a type supports some version of transp.
    --   In particular we want to allow the Interval as a @ClosedType@.
    data CType = ClosedType Sort QName | LType LType deriving (CType -> CType -> Bool
    (CType -> CType -> Bool) -> (CType -> CType -> Bool) -> Eq CType
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: CType -> CType -> Bool
    $c/= :: CType -> CType -> Bool
    == :: CType -> CType -> Bool
    $c== :: CType -> CType -> Bool
    Eq,Nat -> CType -> ArgName -> ArgName
    [CType] -> ArgName -> ArgName
    CType -> ArgName
    (Nat -> CType -> ArgName -> ArgName)
    -> (CType -> ArgName)
    -> ([CType] -> ArgName -> ArgName)
    -> Show CType
    forall a.
    (Nat -> a -> ArgName -> ArgName)
    -> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
    showList :: [CType] -> ArgName -> ArgName
    $cshowList :: [CType] -> ArgName -> ArgName
    show :: CType -> ArgName
    $cshow :: CType -> ArgName
    showsPrec :: Nat -> CType -> ArgName -> ArgName
    $cshowsPrec :: Nat -> CType -> ArgName -> ArgName
    Show)

    fromCType :: CType -> Type
    fromCType :: CType -> Type
    fromCType (ClosedType Sort
    s QName
    q) = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (QName -> Elims -> Term
    Def QName
    q [])
    fromCType (LType LType
    t) = LType -> Type
    fromLType LType
    t

    toCType :: MonadReduce m => Type -> m (Maybe CType)
    toCType :: forall (m :: * -> *). MonadReduce m => Type -> m (Maybe CType)
    toCType Type
    ty = do
      Sort
    sort <- Sort -> m Sort
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Sort -> m Sort) -> Sort -> m Sort
    forall a b. (a -> b) -> a -> b
    $ Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Type
    ty
      case Sort
    sort of
        Type Level
    l -> Maybe CType -> m (Maybe CType)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe CType -> m (Maybe CType)) -> Maybe CType -> m (Maybe CType)
    forall a b. (a -> b) -> a -> b
    $ CType -> Maybe CType
    forall a. a -> Maybe a
    Just (CType -> Maybe CType) -> CType -> Maybe CType
    forall a b. (a -> b) -> a -> b
    $ LType -> CType
    LType (Level -> Term -> LType
    LEl Level
    l (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    ty))
        SSet Level
    l  -> do
          Term
    t <- Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    ty)
          case Term
    t of
            Def QName
    q [] -> Maybe CType -> m (Maybe CType)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe CType -> m (Maybe CType)) -> Maybe CType -> m (Maybe CType)
    forall a b. (a -> b) -> a -> b
    $ CType -> Maybe CType
    forall a. a -> Maybe a
    Just (CType -> Maybe CType) -> CType -> Maybe CType
    forall a b. (a -> b) -> a -> b
    $ Sort -> QName -> CType
    ClosedType (Level -> Sort
    forall t. Level' t -> Sort' t
    SSet Level
    l) QName
    q
            Term
    _        -> Maybe CType -> m (Maybe CType)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe CType -> m (Maybe CType)) -> Maybe CType -> m (Maybe CType)
    forall a b. (a -> b) -> a -> b
    $ Maybe CType
    forall a. Maybe a
    Nothing
        Sort
    _      -> Maybe CType -> m (Maybe CType)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe CType -> m (Maybe CType)) -> Maybe CType -> m (Maybe CType)
    forall a b. (a -> b) -> a -> b
    $ Maybe CType
    forall a. Maybe a
    Nothing

    instance Subst CType where
      type SubstArg CType = Term
      applySubst :: Substitution' (SubstArg CType) -> CType -> CType
    applySubst Substitution' (SubstArg CType)
    rho (ClosedType Sort
    s QName
    t) = Sort -> QName -> CType
    ClosedType (Substitution' (SubstArg Sort) -> Sort -> Sort
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg Sort)
    Substitution' (SubstArg CType)
    rho Sort
    s) QName
    t
      applySubst Substitution' (SubstArg CType)
    rho (LType LType
    t) = LType -> CType
    LType (LType -> CType) -> LType -> CType
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg LType) -> LType -> LType
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' (SubstArg CType)
    Substitution' (SubstArg LType)
    rho LType
    t

    defineTranspOrHCompForFields
      :: TranspOrHComp
      -> (Maybe Term)            -- ^ PathCons, Δ.Φ ⊢ u : R δ
      -> (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
      -> QName       -- ^ some name, e.g. record name
      -> Telescope   -- ^ param types Δ
      -> Telescope   -- ^ fields' types Δ ⊢ Φ
      -> [Arg QName] -- ^ fields' names
      -> Type        -- ^ record type Δ ⊢ T
      -> TCM (Maybe ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
    defineTranspOrHCompForFields :: TranspOrHComp
    -> Maybe Term
    -> (Term -> QName -> Term)
    -> QName
    -> Tele (Dom Type)
    -> Tele (Dom Type)
    -> [Arg QName]
    -> Type
    -> TCM
         (Maybe
            ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
             Substitution' Term))
    defineTranspOrHCompForFields TranspOrHComp
    cmd Maybe Term
    pathCons Term -> QName -> Term
    project QName
    name Tele (Dom Type)
    params Tele (Dom Type)
    fsT [Arg QName]
    fns Type
    rect =
       case TranspOrHComp
    cmd of
           TranspOrHComp
    DoTransp -> MaybeT
      (TCMT IO)
      ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
       Substitution' Term)
    -> TCM
         (Maybe
            ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
             Substitution' Term))
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT
       (TCMT IO)
       ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
        Substitution' Term)
     -> TCM
          (Maybe
             ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
              Substitution' Term)))
    -> MaybeT
         (TCMT IO)
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    -> TCM
         (Maybe
            ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
             Substitution' Term))
    forall a b. (a -> b) -> a -> b
    $ do
             Tele (Dom CType)
    fsT' <- (Dom Type -> MaybeT (TCMT IO) (Dom CType))
    -> Tele (Dom Type) -> MaybeT (TCMT IO) (Tele (Dom CType))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((Type -> MaybeT (TCMT IO) CType)
    -> Dom Type -> MaybeT (TCMT IO) (Dom CType)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (TCMT IO (Maybe CType) -> MaybeT (TCMT IO) CType
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (TCMT IO (Maybe CType) -> MaybeT (TCMT IO) CType)
    -> (Type -> TCMT IO (Maybe CType))
    -> Type
    -> MaybeT (TCMT IO) CType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> TCMT IO (Maybe CType)
    forall (m :: * -> *). MonadReduce m => Type -> m (Maybe CType)
    toCType)) Tele (Dom Type)
    fsT
             TCMT
      IO
      ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
       Substitution' Term)
    -> MaybeT
         (TCMT IO)
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT
       IO
       ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
        Substitution' Term)
     -> MaybeT
          (TCMT IO)
          ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
           Substitution' Term))
    -> TCMT
         IO
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    -> MaybeT
         (TCMT IO)
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    forall a b. (a -> b) -> a -> b
    $ Maybe Term
    -> (Term -> QName -> Term)
    -> QName
    -> Tele (Dom Type)
    -> Tele (Dom CType)
    -> [Arg QName]
    -> Type
    -> TCMT
         IO
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    defineTranspForFields Maybe Term
    pathCons Term -> QName -> Term
    project QName
    name Tele (Dom Type)
    params Tele (Dom CType)
    fsT' [Arg QName]
    fns Type
    rect
           TranspOrHComp
    DoHComp -> MaybeT
      (TCMT IO)
      ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
       Substitution' Term)
    -> TCM
         (Maybe
            ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
             Substitution' Term))
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT (MaybeT
       (TCMT IO)
       ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
        Substitution' Term)
     -> TCM
          (Maybe
             ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
              Substitution' Term)))
    -> MaybeT
         (TCMT IO)
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    -> TCM
         (Maybe
            ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
             Substitution' Term))
    forall a b. (a -> b) -> a -> b
    $ do
             Tele (Dom LType)
    fsT' <- (Dom Type -> MaybeT (TCMT IO) (Dom LType))
    -> Tele (Dom Type) -> MaybeT (TCMT IO) (Tele (Dom LType))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((Type -> MaybeT (TCMT IO) LType)
    -> Dom Type -> MaybeT (TCMT IO) (Dom LType)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (TCMT IO (Maybe LType) -> MaybeT (TCMT IO) LType
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (TCMT IO (Maybe LType) -> MaybeT (TCMT IO) LType)
    -> (Type -> TCMT IO (Maybe LType))
    -> Type
    -> MaybeT (TCMT IO) LType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> TCMT IO (Maybe LType)
    forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
    toLType)) Tele (Dom Type)
    fsT
             LType
    rect' <- TCMT IO (Maybe LType) -> MaybeT (TCMT IO) LType
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
    MaybeT (TCMT IO (Maybe LType) -> MaybeT (TCMT IO) LType)
    -> TCMT IO (Maybe LType) -> MaybeT (TCMT IO) LType
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO (Maybe LType)
    forall (m :: * -> *). MonadReduce m => Type -> m (Maybe LType)
    toLType Type
    rect
             TCMT
      IO
      ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
       Substitution' Term)
    -> MaybeT
         (TCMT IO)
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT
       IO
       ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
        Substitution' Term)
     -> MaybeT
          (TCMT IO)
          ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
           Substitution' Term))
    -> TCMT
         IO
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    -> MaybeT
         (TCMT IO)
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    forall a b. (a -> b) -> a -> b
    $ (Term -> QName -> Term)
    -> QName
    -> Tele (Dom Type)
    -> Tele (Dom LType)
    -> [Arg QName]
    -> LType
    -> TCMT
         IO
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    defineHCompForFields Term -> QName -> Term
    project QName
    name Tele (Dom Type)
    params Tele (Dom LType)
    fsT' [Arg QName]
    fns LType
    rect'

    -- invariant: resulting tel Γ is such that Γ = ... , (φ : I), (a0 : ...)
    --            where a0 has type matching the arguments of primTrans.
    defineTranspForFields
      :: (Maybe Term)            -- ^ PathCons, Δ.Φ ⊢ u : R δ
      -> (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
      -> QName       -- ^ some name, e.g. record name
      -> Telescope   -- ^ param types Δ
      -> Tele (Dom CType)   -- ^ fields' types Δ ⊢ Φ
      -> [Arg QName] -- ^ fields' names
      -> Type        -- ^ record type Δ ⊢ T
      -> TCM ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
    defineTranspForFields :: Maybe Term
    -> (Term -> QName -> Term)
    -> QName
    -> Tele (Dom Type)
    -> Tele (Dom CType)
    -> [Arg QName]
    -> Type
    -> TCMT
         IO
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    defineTranspForFields Maybe Term
    pathCons Term -> QName -> Term
    applyProj QName
    name Tele (Dom Type)
    params Tele (Dom CType)
    fsT [Arg QName]
    fns Type
    rect = do
      Type
    interval <- TCMT IO Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType
      let deltaI :: Tele (Dom Type)
    deltaI = Type -> Tele (Dom Type) -> Tele (Dom Type)
    expTelescope Type
    interval Tele (Dom Type)
    params
      Term
    iz <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIZero
      Term
    io <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIOne
      Term
    imin <- ArgName -> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m Term
    getPrimitiveTerm ArgName
    "primIMin"
      Term
    imax <- ArgName -> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m Term
    getPrimitiveTerm ArgName
    "primIMax"
      Term
    ineg <- ArgName -> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m Term
    getPrimitiveTerm ArgName
    "primINeg"
      Term
    transp <- ArgName -> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m Term
    getPrimitiveTerm ArgName
    builtinTrans
      -- por <- getPrimitiveTerm "primPOr"
      -- one <- primItIsOne
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "trans.rec" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> ArgName
    forall a. Show a => a -> ArgName
    show Tele (Dom Type)
    params
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "trans.rec" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> ArgName
    forall a. Show a => a -> ArgName
    show Tele (Dom Type)
    deltaI
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "trans.rec" Nat
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom CType) -> ArgName
    forall a. Show a => a -> ArgName
    show Tele (Dom CType)
    fsT

      let thePrefix :: ArgName
    thePrefix = ArgName
    "transp-"
      QName
    theName <- ArgName -> TCMT IO QName
    freshAbstractQName'_ (ArgName -> TCMT IO QName) -> ArgName -> TCMT IO QName
    forall a b. (a -> b) -> a -> b
    $ ArgName
    thePrefix ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ Name -> ArgName
    forall a. Pretty a => a -> ArgName
    P.prettyShow (QName -> Name
    A.qnameName QName
    name)

      ArgName -> Nat -> ArgName -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> ArgName -> m ()
    reportSLn ArgName
    "trans.rec" Nat
    5 (ArgName -> TCM ()) -> ArgName -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (ArgName
    "Generated name: " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    forall a. Show a => a -> ArgName
    show QName
    theName ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    " " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    showQNameId QName
    theName)

      Type
    theType <- (Tele (Dom Type) -> Type -> Type
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    deltaI (Type -> Type) -> TCMT IO Type -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>) (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ [ArgName] -> NamesT (TCMT IO) Type -> TCMT IO Type
    forall (m :: * -> *) a. [ArgName] -> NamesT m a -> m a
    runNamesT [] (NamesT (TCMT IO) Type -> TCMT IO Type)
    -> NamesT (TCMT IO) Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ do
                  NamesT (TCMT IO) (Abs Type)
    rect' <- Abs Type -> NamesT (TCMT IO) (NamesT (TCMT IO) (Abs Type))
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open ([ArgName] -> NamesT Fail (Abs Type) -> Abs Type
    forall a. [ArgName] -> NamesT Fail a -> a
    runNames [] (NamesT Fail (Abs Type) -> Abs Type)
    -> NamesT Fail (Abs Type) -> Abs Type
    forall a b. (a -> b) -> a -> b
    $ ArgName
    -> (NamesT Fail Term -> NamesT Fail Type) -> NamesT Fail (Abs Type)
    forall (m :: * -> *) b a.
    (MonadFail m, Subst b, DeBruijn b, Subst a, Free a) =>
    ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
    bind ArgName
    "i" ((NamesT Fail Term -> NamesT Fail Type) -> NamesT Fail (Abs Type))
    -> (NamesT Fail Term -> NamesT Fail Type) -> NamesT Fail (Abs Type)
    forall a b. (a -> b) -> a -> b
    $ \ NamesT Fail Term
    x -> let NamesT Fail Term
    _ = NamesT Fail Term
    x NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall a. a -> a -> a
    `asTypeOf` Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term
    forall a. HasCallStack => a
    undefined :: Term) in
                                                                 Type -> NamesT Fail Type
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Type
    rect')
                  ArgName
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadFail m, MonadAddContext m, MonadDebug m) =>
    ArgName
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    nPi' ArgName
    "phi" NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
     -> NamesT (TCMT IO) Type)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    phi ->
                   (Abs Type -> Term -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp (Abs Type -> Term -> Type)
    -> NamesT (TCMT IO) (Abs Type) -> NamesT (TCMT IO) (Term -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) (Abs Type)
    rect' NamesT (TCMT IO) (Term -> Type)
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    iz) NamesT (TCMT IO) Type
    -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> (Abs Type -> Term -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp (Abs Type -> Term -> Type)
    -> NamesT (TCMT IO) (Abs Type) -> NamesT (TCMT IO) (Term -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) (Abs Type)
    rect' NamesT (TCMT IO) (Term -> Type)
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io)

      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "trans.rec" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    theType
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "trans.rec" Nat
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "sort = " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ Sort -> ArgName
    forall a. Show a => a -> ArgName
    show (Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Type
    rect')

      Language
    lang <- TCMT IO Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
      TCM () -> TCM ()
    forall a. TCM a -> TCM a
    noMutualBlock (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Definition -> TCM ()
    addConstant QName
    theName (Definition -> TCM ()) -> Definition -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
    defaultDefn ArgInfo
    defaultArgInfo QName
    theName Type
    theType Language
    lang
           (Defn
    emptyFunction { funTerminates :: Maybe Bool
    funTerminates = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True }))
          { defNoCompilation :: Bool
    defNoCompilation = Bool
    True }
      -- ⊢ Γ = gamma = (δ : Δ^I) (φ : I) (u0 : R (δ i0))
      -- Γ ⊢     rtype = R (δ i1)
      TelV Tele (Dom Type)
    gamma Type
    rtype <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    theType

      let
          -- (γ : Γ) ⊢ transpR γ : rtype
          theTerm :: Term
    theTerm = QName -> Elims -> Term
    Def QName
    theName [] Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` Tele (Dom Type) -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    gamma

          -- (γ : Γ) ⊢ (flatten Φ[δ i1])[n ↦ f_n (transpR γ)]
          clause_types :: [Dom CType]
    clause_types = [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS [Term
    theTerm Term -> QName -> Term
    `applyProj` (Arg QName -> QName
    forall e. Arg e -> e
    unArg Arg QName
    fn)
                                   | Arg QName
    fn <- [Arg QName] -> [Arg QName]
    forall a. [a] -> [a]
    reverse [Arg QName]
    fns] Substitution' (SubstArg [Dom CType]) -> [Dom CType] -> [Dom CType]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst`
                           Tele (Dom CType) -> [Dom CType]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel (Nat -> Term -> Substitution' Term
    forall a. DeBruijn a => Nat -> a -> Substitution' a
    singletonS Nat
    0 Term
    io Substitution' (SubstArg (Tele (Dom CType)))
    -> Tele (Dom CType) -> Tele (Dom CType)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Tele (Dom CType)
    fsT') -- Γ, Φ[δ i1] ⊢ flatten Φ[δ i1]

          -- Γ, i : I ⊢ [δ i] : Δ
          delta_i :: Substitution' Term
    delta_i = (Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    1 (Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    gamma Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    deltaI)) Substitution' Term -> Substitution' Term -> Substitution' Term
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Tele (Dom Type) -> Substitution' Term
    forall {a}. Sized a => a -> Substitution' Term
    sub Tele (Dom Type)
    params) -- Defined but not used

          -- Γ, i : I ⊢ Φ[δ i]
          fsT' :: Tele (Dom CType)
    fsT' = (Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    1 (Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    gamma Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    deltaI)) Substitution' Term -> Substitution' Term -> Substitution' Term
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Tele (Dom Type) -> Substitution' Term
    forall {a}. Sized a => a -> Substitution' Term
    sub Tele (Dom Type)
    params)  Substitution' (SubstArg (Tele (Dom CType)))
    -> Tele (Dom CType) -> Tele (Dom CType)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst`
                   Tele (Dom CType)
    fsT -- Δ ⊢ Φ
          lam_i :: Term -> Term
    lam_i = ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    defaultArgInfo (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ArgName -> Term -> Abs Term
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    "i"

          -- (δ , φ , u0) : Γ ⊢ φ : I
          -- the_phi = var 1
          -- -- (δ , φ , u0) : Γ ⊢ u0 : R (δ i0)
          -- the_u0  = var 0

          -- Γ' = (δ : Δ^I, φ : I)
          gamma' :: Tele (Dom Type)
    gamma' = [Dom' Term (ArgName, Type)] -> Tele (Dom Type)
    telFromList ([Dom' Term (ArgName, Type)] -> Tele (Dom Type))
    -> [Dom' Term (ArgName, Type)] -> Tele (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ Nat -> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
    forall a. Nat -> [a] -> [a]
    take (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    gamma Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) ([Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)])
    -> [Dom' Term (ArgName, Type)] -> [Dom' Term (ArgName, Type)]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom' Term (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    gamma

          -- δ : Δ^I, φ : F ⊢ [δ 0] : Δ
          d0 :: Substitution
          d0 :: Substitution' Term
    d0 = Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    wkS Nat
    1 -- Δ^I, φ : F ⊢ Δ
                           (Term -> Substitution' Term -> Substitution' Term
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    consS Term
    iz Substitution' Term
    forall a. Substitution' a
    IdS Substitution' Term -> Substitution' Term -> Substitution' Term
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Tele (Dom Type) -> Substitution' Term
    forall {a}. Sized a => a -> Substitution' Term
    sub Tele (Dom Type)
    params) -- Δ^I ⊢ Δ
                                     -- Δ^I , i:I ⊢ sub params : Δ

          -- Ξ , Ξ ⊢ θ : Γ, Ξ ⊢ φ, Ξ ⊢ u : R (δ i0), Ξ ⊢ us : Φ[δ i0]
          (Tele (Dom Type)
    tel,Substitution' Term
    theta,Term
    the_phi,Term
    the_u0, [Term]
    the_fields) =
            case Maybe Term
    pathCons of
              -- (δ : Δ).Φ ⊢ u : R δ
              Just Term
    u -> (Tele (Dom Type) -> Tele (Dom Type) -> Tele (Dom Type)
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    gamma' (Substitution' Term
    Substitution' (SubstArg (Tele (Dom Type)))
    d0 Substitution' (SubstArg (Tele (Dom Type)))
    -> Tele (Dom Type) -> Tele (Dom Type)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` (Dom CType -> Dom Type) -> Tele (Dom CType) -> Tele (Dom Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((CType -> Type) -> Dom CType -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap CType -> Type
    fromCType) Tele (Dom CType)
    fsT) -- Ξ = δ : Δ^I, φ : F, _ : Φ[δ i0]
                        , (Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS (Tele (Dom CType) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom CType)
    fsT) Substitution' Term
    d0 Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Term
    u) Term -> Substitution' Term -> Substitution' Term
    forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
    `consS` Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS (Tele (Dom CType) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom CType)
    fsT)
                        , Nat -> Term -> Term
    forall a. Subst a => Nat -> a -> a
    raise (Tele (Dom CType) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom CType)
    fsT) (Nat -> Term
    var Nat
    0)
                        , (Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS (Tele (Dom CType) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom CType)
    fsT) Substitution' Term
    d0 Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Term
    u)
                        , Nat -> [Term] -> [Term]
    forall a. Nat -> [a] -> [a]
    drop (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    gamma') ([Term] -> [Term]) -> [Term] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Term) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg ([Arg Term] -> [Term]) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    tel)
              Maybe Term
    Nothing -> (Tele (Dom Type)
    gamma, Substitution' Term
    forall a. Substitution' a
    IdS, Nat -> Term
    var Nat
    1, Nat -> Term
    var Nat
    0, (Arg QName -> Term) -> [Arg QName] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ Arg QName
    fname -> Nat -> Term
    var Nat
    0 Term -> QName -> Term
    `applyProj` Arg QName -> QName
    forall e. Arg e -> e
    unArg Arg QName
    fname) [Arg QName]
    fns )

          fsT_tel :: Tele (Dom CType)
    fsT_tel = (Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    1 (Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    deltaI)) Substitution' Term -> Substitution' Term -> Substitution' Term
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Tele (Dom Type) -> Substitution' Term
    forall {a}. Sized a => a -> Substitution' Term
    sub Tele (Dom Type)
    params) Substitution' (SubstArg (Tele (Dom CType)))
    -> Tele (Dom CType) -> Tele (Dom CType)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Tele (Dom CType)
    fsT

          iMin :: Term -> Term -> Term
    iMin Term
    x Term
    y = Term
    imin Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    x, Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    y]
          iMax :: Term -> Term -> Term
    iMax Term
    x Term
    y = Term
    imax Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    x, Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    y]
          iNeg :: Term -> Term
    iNeg Term
    x = Term
    ineg Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    x]

          -- .. ⊢ field : filled_ty' i0
          mkBody :: (Term, Dom CType) -> TCMT IO Term
    mkBody (Term
    field, Dom CType
    filled_ty') = do
            let
              filled_ty :: Term
    filled_ty = Term -> Term
    lam_i (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> (Dom CType -> Type) -> Dom CType -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CType -> Type
    fromCType (CType -> Type) -> (Dom CType -> CType) -> Dom CType -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom CType -> CType
    forall t e. Dom' t e -> e
    unDom) Dom CType
    filled_ty'
              -- Γ ⊢ l : I -> Level of filled_ty
            -- sort <- reduce $ getSort $ unDom filled_ty'
            case Dom CType -> CType
    forall t e. Dom' t e -> e
    unDom Dom CType
    filled_ty' of
              LType (LEl Level
    l Term
    _) -> do
                let lvl :: Term
    lvl = Term -> Term
    lam_i (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Level -> Term
    Level Level
    l
                Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ [ArgName] -> NamesT Fail Term -> Term
    forall a. [ArgName] -> NamesT Fail a -> a
    runNames [] (NamesT Fail Term -> Term) -> NamesT Fail Term -> Term
    forall a b. (a -> b) -> a -> b
    $ do
                 NamesT Fail Term
    lvl <- Term -> NamesT Fail (NamesT Fail Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open Term
    lvl
                 [NamesT Fail Term
    phi,NamesT Fail Term
    field] <- (Term -> NamesT Fail (NamesT Fail Term))
    -> [Term] -> NamesT Fail [NamesT Fail Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Term -> NamesT Fail (NamesT Fail Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open [Term
    the_phi,Term
    field]
                 Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    transp NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT Fail Term
    lvl NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    filled_ty
                                     NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    phi
                                     NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    field
              -- interval arg
              ClosedType{}  ->
                Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ [ArgName] -> NamesT Fail Term -> Term
    forall a. [ArgName] -> NamesT Fail a -> a
    runNames [] (NamesT Fail Term -> Term) -> NamesT Fail Term -> Term
    forall a b. (a -> b) -> a -> b
    $ do
                [NamesT Fail Term
    field] <- (Term -> NamesT Fail (NamesT Fail Term))
    -> [Term] -> NamesT Fail [NamesT Fail Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Term -> NamesT Fail (NamesT Fail Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open [Term
    field]
                NamesT Fail Term
    field

      let
            -- ' Ξ , i : I ⊢ τ = [(\ j → δ (i ∧ j)), φ ∨ ~ i, u] : Ξ
            tau :: Substitution' Term
    tau = [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ [Term]
    us [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ (Term
    phi Term -> Term -> Term
    `iMax` Term -> Term
    iNeg (Nat -> Term
    var Nat
    0))
                            Term -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    : (Term -> Term) -> [Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ Term
    d -> ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    defaultArgInfo (Abs Term -> Term) -> Abs Term -> Term
    forall a b. (a -> b) -> a -> b
    $ ArgName -> Term -> Abs Term
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    "i" (Term -> Abs Term) -> Term -> Abs Term
    forall a b. (a -> b) -> a -> b
    $ Nat -> Term -> Term
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 Term
    d Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Term -> Arg Term
    forall e. e -> Arg e
    argN (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ (Term -> Term -> Term
    iMin (Nat -> Term
    var Nat
    0) (Nat -> Term
    var Nat
    1))]) [Term]
    ds
             where
              -- Ξ, i : I
              ([Term]
    us, Term
    phi:[Term]
    ds) = Nat -> [Term] -> ([Term], [Term])
    forall a. Nat -> [a] -> ([a], [a])
    splitAt (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    gamma') ([Term] -> ([Term], [Term])) -> [Term] -> ([Term], [Term])
    forall a b. (a -> b) -> a -> b
    $ [Term] -> [Term]
    forall a. [a] -> [a]
    reverse (Nat -> [Term] -> [Term]
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 ((Arg Term -> Term) -> [Arg Term] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Term
    forall e. Arg e -> e
    unArg (Tele (Dom Type) -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    tel)))

      let
        go :: [Term] -> [(Term, Dom CType)] -> TCMT IO [Term]
    go [Term]
    acc [] = [Term] -> TCMT IO [Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        go [Term]
    acc ((Term
    fname,Dom CType
    field_ty) : [(Term, Dom CType)]
    ps) = do
          -- Ξ, i : I, Φ[δ i]|_f ⊢ Φ_f = field_ty
          -- Ξ ⊢ b : field_ty [i := i1][acc]
          -- Ξ ⊢ parallesS acc : Φ[δ i1]|_f
          -- Ξ , i : I ⊢ τ = [(\ j → δ (i ∨ j), φ ∨ ~ i, us] : Ξ
          -- Ξ , i : I ⊢ parallesS (acc[τ]) : Φ[δ i1]|_f
          -- Ξ, i : I ⊢ field_ty [parallesS (acc[τ])]
          let
            filled_ty :: Dom CType
    filled_ty = [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS (Substitution' Term
    Substitution' (SubstArg [Term])
    tau Substitution' (SubstArg [Term]) -> [Term] -> [Term]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` [Term]
    acc) Substitution' (SubstArg (Dom CType)) -> Dom CType -> Dom CType
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Dom CType
    field_ty
          Term
    b <- (Term, Dom CType) -> TCMT IO Term
    mkBody (Term
    fname,Dom CType
    filled_ty)
          [Term]
    bs <- [Term] -> [(Term, Dom CType)] -> TCMT IO [Term]
    go (Term
    b Term -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    : [Term]
    acc) [(Term, Dom CType)]
    ps
          [Term] -> TCMT IO [Term]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Term] -> TCMT IO [Term]) -> [Term] -> TCMT IO [Term]
    forall a b. (a -> b) -> a -> b
    $ Term
    b Term -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    : [Term]
    bs

      [Term]
    bodys <- [Term] -> [(Term, Dom CType)] -> TCMT IO [Term]
    go [] ([Term] -> [Dom CType] -> [(Term, Dom CType)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Term]
    the_fields ((Dom' Term (ArgName, CType) -> Dom CType)
    -> [Dom' Term (ArgName, CType)] -> [Dom CType]
    forall a b. (a -> b) -> [a] -> [b]
    map (((ArgName, CType) -> CType)
    -> Dom' Term (ArgName, CType) -> Dom CType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ArgName, CType) -> CType
    forall a b. (a, b) -> b
    snd) ([Dom' Term (ArgName, CType)] -> [Dom CType])
    -> [Dom' Term (ArgName, CType)] -> [Dom CType]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom CType) -> [Dom' Term (ArgName, CType)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom CType)
    fsT_tel)) -- ∀ f.  Ξ, i : I, Φ[δ i]|_f ⊢ Φ[δ i]_f
      let
        -- Ξ, i : I ⊢ ... : Δ.Φ
        theSubst :: Substitution' Term
    theSubst = [Term] -> [Term]
    forall a. [a] -> [a]
    reverse (Substitution' Term
    Substitution' (SubstArg [Term])
    tau Substitution' (SubstArg [Term]) -> [Term] -> [Term]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` [Term]
    bodys) [Term] -> Substitution' Term -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# (Nat -> Substitution' Term -> Substitution' Term
    forall a. Nat -> Substitution' a -> Substitution' a
    liftS Nat
    1 (Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    deltaI)) Substitution' Term -> Substitution' Term -> Substitution' Term
    forall a.
    EndoSubst a =>
    Substitution' a -> Substitution' a -> Substitution' a
    `composeS` Tele (Dom Type) -> Substitution' Term
    forall {a}. Sized a => a -> Substitution' Term
    sub Tele (Dom Type)
    params)
      ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
     Substitution' Term)
    -> TCMT
         IO
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
     -> TCMT
          IO
          ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
           Substitution' Term))
    -> ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
        Substitution' Term)
    -> TCMT
         IO
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    forall a b. (a -> b) -> a -> b
    $ ((QName
    theName, Tele (Dom Type)
    tel, Substitution' Term
    Substitution' (SubstArg Type)
    theta Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Type
    rtype, (Dom CType -> Dom Type) -> [Dom CType] -> [Dom Type]
    forall a b. (a -> b) -> [a] -> [b]
    map ((CType -> Type) -> Dom CType -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap CType -> Type
    fromCType) [Dom CType]
    clause_types, [Term]
    bodys), Substitution' Term
    theSubst)
      where
        -- record type in 'exponentiated' context
        -- (params : Δ^I), i : I |- T[params i]
        rect' :: Type
    rect' = Tele (Dom Type) -> Substitution' Term
    forall {a}. Sized a => a -> Substitution' Term
    sub Tele (Dom Type)
    params Substitution' (SubstArg Type) -> Type -> Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Type
    rect
        -- Δ^I, i : I |- sub Δ : Δ
        sub :: a -> Substitution' Term
    sub a
    tel = [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS [ Nat -> Term
    var Nat
    n Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    defaultArgInfo (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Nat -> Term
    var Nat
    0] | Nat
    n <- [Nat
    1..a -> Nat
    forall a. Sized a => a -> Nat
    size a
    tel] ]
        -- given I type, and Δ telescope, build Δ^I such that
        -- (x : A, y : B x, ...)^I = (x : I → A, y : (i : I) → B (x i), ...)
        expTelescope :: Type -> Telescope -> Telescope
        expTelescope :: Type -> Tele (Dom Type) -> Tele (Dom Type)
    expTelescope Type
    int Tele (Dom Type)
    tel = [ArgName] -> [Dom Type] -> Tele (Dom Type)
    unflattenTel [ArgName]
    names [Dom Type]
    ys
          where
            xs :: [Dom Type]
    xs = Tele (Dom Type) -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Tele (Dom Type)
    tel
            names :: [ArgName]
    names = Tele (Dom Type) -> [ArgName]
    teleNames Tele (Dom Type)
    tel
            t :: Tele (Dom Type)
    t = Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Type -> Dom Type
    forall a. a -> Dom a
    defaultDom (Type -> Dom Type) -> Type -> Dom Type
    forall a b. (a -> b) -> a -> b
    $ Nat -> Type -> Type
    forall a. Subst a => Nat -> a -> a
    raise (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    tel) Type
    int) (ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    "i" Tele (Dom Type)
    forall a. Tele a
    EmptyTel)
            s :: Substitution' Term
    s = Tele (Dom Type) -> Substitution' Term
    forall {a}. Sized a => a -> Substitution' Term
    sub Tele (Dom Type)
    tel
            ys :: [Dom Type]
    ys = (Dom Type -> Dom Type) -> [Dom Type] -> [Dom Type]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Type -> Type) -> Dom Type -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Tele (Dom Type) -> Type -> Type
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    t) (Dom Type -> Dom Type)
    -> (Dom Type -> Dom Type) -> Dom Type -> Dom Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg (Dom Type))
    s) [Dom Type]
    xs

    -- invariant: resulting tel Γ is such that Γ = (δ : Δ), (φ : I), (u : ...), (a0 : R δ))
    --            where u and a0 have types matching the arguments of primHComp.
    defineHCompForFields
      :: (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
      -> QName       -- ^ some name, e.g. record name
      -> Telescope   -- ^ param types Δ
      -> Tele (Dom LType)   -- ^ fields' types Δ ⊢ Φ
      -> [Arg QName] -- ^ fields' names
      -> LType        -- ^ record type (δ : Δ) ⊢ R[δ]
      -> TCM ((QName, Telescope, Type, [Dom Type], [Term]),Substitution)
    defineHCompForFields :: (Term -> QName -> Term)
    -> QName
    -> Tele (Dom Type)
    -> Tele (Dom LType)
    -> [Arg QName]
    -> LType
    -> TCMT
         IO
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    defineHCompForFields Term -> QName -> Term
    applyProj QName
    name Tele (Dom Type)
    params Tele (Dom LType)
    fsT [Arg QName]
    fns LType
    rect = do
      Type
    interval <- TCMT IO Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType
      let delta :: Tele (Dom Type)
    delta = Tele (Dom Type)
    params
      Term
    iz <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIZero
      Term
    io <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIOne
      Term
    imin <- ArgName -> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m Term
    getPrimitiveTerm ArgName
    "primIMin"
      Term
    imax <- ArgName -> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m Term
    getPrimitiveTerm ArgName
    "primIMax"
      Term
    tIMax <- ArgName -> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m Term
    getPrimitiveTerm ArgName
    "primIMax"
      Term
    ineg <- ArgName -> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m Term
    getPrimitiveTerm ArgName
    "primINeg"
      Term
    hcomp <- ArgName -> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m Term
    getPrimitiveTerm ArgName
    builtinHComp
      Term
    transp <- ArgName -> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m Term
    getPrimitiveTerm ArgName
    builtinTrans
      Term
    por <- ArgName -> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    ArgName -> m Term
    getPrimitiveTerm ArgName
    "primPOr"
      Term
    one <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primItIsOne
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "comp.rec" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> ArgName
    forall a. Show a => a -> ArgName
    show Tele (Dom Type)
    params
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "comp.rec" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> ArgName
    forall a. Show a => a -> ArgName
    show Tele (Dom Type)
    delta
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "comp.rec" Nat
    10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom LType) -> ArgName
    forall a. Show a => a -> ArgName
    show Tele (Dom LType)
    fsT

      let thePrefix :: ArgName
    thePrefix = ArgName
    "hcomp-"
      QName
    theName <- ArgName -> TCMT IO QName
    freshAbstractQName'_ (ArgName -> TCMT IO QName) -> ArgName -> TCMT IO QName
    forall a b. (a -> b) -> a -> b
    $ ArgName
    thePrefix ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ Name -> ArgName
    forall a. Pretty a => a -> ArgName
    P.prettyShow (QName -> Name
    A.qnameName QName
    name)

      ArgName -> Nat -> ArgName -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> ArgName -> m ()
    reportSLn ArgName
    "hcomp.rec" Nat
    5 (ArgName -> TCM ()) -> ArgName -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ (ArgName
    "Generated name: " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    forall a. Show a => a -> ArgName
    show QName
    theName ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    " " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ QName -> ArgName
    showQNameId QName
    theName)

      Type
    theType <- (Tele (Dom Type) -> Type -> Type
    forall t. Abstract t => Tele (Dom Type) -> t -> t
    abstract Tele (Dom Type)
    delta (Type -> Type) -> TCMT IO Type -> TCMT IO Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>) (TCMT IO Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ [ArgName] -> NamesT (TCMT IO) Type -> TCMT IO Type
    forall (m :: * -> *) a. [ArgName] -> NamesT m a -> m a
    runNamesT [] (NamesT (TCMT IO) Type -> TCMT IO Type)
    -> NamesT (TCMT IO) Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $ do
                  NamesT (TCMT IO) Type
    rect <- Type -> NamesT (TCMT IO) (NamesT (TCMT IO) Type)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open (Type -> NamesT (TCMT IO) (NamesT (TCMT IO) Type))
    -> Type -> NamesT (TCMT IO) (NamesT (TCMT IO) Type)
    forall a b. (a -> b) -> a -> b
    $ LType -> Type
    fromLType LType
    rect
                  ArgName
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadFail m, MonadAddContext m, MonadDebug m) =>
    ArgName
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    nPi' ArgName
    "phi" NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
     -> NamesT (TCMT IO) Type)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    phi ->
                   ArgName
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadFail m, MonadAddContext m, MonadDebug m) =>
    ArgName
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    nPi' ArgName
    "i" NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType (\ NamesT (TCMT IO) Term
    i ->
                    ArgName
    -> NamesT (TCMT IO) Term
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, HasBuiltins m, MonadDebug m) =>
    ArgName
    -> NamesT m Term
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    pPi' ArgName
    "o" NamesT (TCMT IO) Term
    phi ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
     -> NamesT (TCMT IO) Type)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    _ -> NamesT (TCMT IO) Type
    rect) NamesT (TCMT IO) Type
    -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    -->
                   NamesT (TCMT IO) Type
    rect NamesT (TCMT IO) Type
    -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> NamesT (TCMT IO) Type
    rect

      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "hcomp.rec" Nat
    20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    theType
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "hcomp.rec" Nat
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "sort = " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ Level -> ArgName
    forall a. Show a => a -> ArgName
    show (LType -> Level
    lTypeLevel LType
    rect)

      Language
    lang <- TCMT IO Language
    forall (m :: * -> *). HasOptions m => m Language
    getLanguage
      TCM () -> TCM ()
    forall a. TCM a -> TCM a
    noMutualBlock (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Definition -> TCM ()
    addConstant QName
    theName (Definition -> TCM ()) -> Definition -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
        (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
    defaultDefn ArgInfo
    defaultArgInfo QName
    theName Type
    theType Language
    lang
           (Defn
    emptyFunction { funTerminates :: Maybe Bool
    funTerminates = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True }))
          { defNoCompilation :: Bool
    defNoCompilation = Bool
    True }
      --   ⊢ Γ = gamma = (δ : Δ) (φ : I) (_ : (i : I) -> Partial φ (R δ)) (_ : R δ)
      -- Γ ⊢     rtype = R δ
      TelV Tele (Dom Type)
    gamma Type
    rtype <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    theType

      let -- Γ ⊢ R δ
          drect_gamma :: LType
    drect_gamma = Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    gamma Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    delta) Substitution' (SubstArg LType) -> LType -> LType
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` LType
    rect

      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "hcomp.rec" Nat
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "sort = " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ Level -> ArgName
    forall a. Show a => a -> ArgName
    show (LType -> Level
    lTypeLevel LType
    drect_gamma)

      let

          -- (γ : Γ) ⊢ hcompR γ : rtype
          compTerm :: Term
    compTerm = QName -> Elims -> Term
    Def QName
    theName [] Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` Tele (Dom Type) -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    gamma

          -- (δ, φ, u, u0) : Γ ⊢ φ : I
          the_phi :: Term
    the_phi = Nat -> Term
    var Nat
    2
          -- (δ, φ, u, u0) : Γ ⊢ u : (i : I) → [φ] → R (δ i)
          the_u :: Term
    the_u   = Nat -> Term
    var Nat
    1
          -- (δ, φ, u, u0) : Γ ⊢ u0 : R (δ i0)
          the_u0 :: Term
    the_u0  = Nat -> Term
    var Nat
    0

          -- ' (δ, φ, u, u0) : Γ ⊢ fillR Γ : (i : I) → rtype[ δ ↦ (\ j → δ (i ∧ j))]
          fillTerm :: Term
    fillTerm = [ArgName] -> NamesT Fail Term -> Term
    forall a. [ArgName] -> NamesT Fail a -> a
    runNames [] (NamesT Fail Term -> Term) -> NamesT Fail Term -> Term
    forall a b. (a -> b) -> a -> b
    $ do
            NamesT Fail Term
    rect <- Term -> NamesT Fail (NamesT Fail Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open (Term -> NamesT Fail (NamesT Fail Term))
    -> (LType -> Term) -> LType -> NamesT Fail (NamesT Fail Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Term
    forall t a. Type'' t a -> a
    unEl  (Type -> Term) -> (LType -> Type) -> LType -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LType -> Type
    fromLType  (LType -> NamesT Fail (NamesT Fail Term))
    -> LType -> NamesT Fail (NamesT Fail Term)
    forall a b. (a -> b) -> a -> b
    $ LType
    drect_gamma
            NamesT Fail Term
    lvl  <- Term -> NamesT Fail (NamesT Fail Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open (Term -> NamesT Fail (NamesT Fail Term))
    -> (LType -> Term) -> LType -> NamesT Fail (NamesT Fail Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Level -> Term
    Level (Level -> Term) -> (LType -> Level) -> LType -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LType -> Level
    lTypeLevel (LType -> NamesT Fail (NamesT Fail Term))
    -> LType -> NamesT Fail (NamesT Fail Term)
    forall a b. (a -> b) -> a -> b
    $ LType
    drect_gamma
            [NamesT Fail (Arg Term)]
    params     <- (Arg Term -> NamesT Fail (NamesT Fail (Arg Term)))
    -> [Arg Term] -> NamesT Fail [NamesT Fail (Arg Term)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Arg Term -> NamesT Fail (NamesT Fail (Arg Term))
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open ([Arg Term] -> NamesT Fail [NamesT Fail (Arg Term)])
    -> [Arg Term] -> NamesT Fail [NamesT Fail (Arg Term)]
    forall a b. (a -> b) -> a -> b
    $ Nat -> [Arg Term] -> [Arg Term]
    forall a. Nat -> [a] -> [a]
    take (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    delta) ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Arg Term]
    forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
    teleArgs Tele (Dom Type)
    gamma
            [NamesT Fail Term
    phi,NamesT Fail Term
    w,NamesT Fail Term
    w0] <- (Term -> NamesT Fail (NamesT Fail Term))
    -> [Term] -> NamesT Fail [NamesT Fail Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Term -> NamesT Fail (NamesT Fail Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open [Term
    the_phi,Term
    the_u,Term
    the_u0]
            -- (δ : Δ, φ : I, w : .., w0 : R δ) ⊢
            -- ' fillR Γ = λ i → hcompR δ (φ ∨ ~ i) (\ j → [ φ ↦ w (i ∧ j) , ~ i ↦ w0 ]) w0
            --           = hfillR δ φ w w0
            ArgName
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam ArgName
    "i" ((NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term)
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall a b. (a -> b) -> a -> b
    $ \ NamesT Fail Term
    i -> do
              [Arg Term]
    args <- [NamesT Fail (Arg Term)] -> NamesT Fail [Arg Term]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    sequence [NamesT Fail (Arg Term)]
    params
              Term
    psi  <- Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    imax NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    phi NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    ineg NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    i)
              Term
    u <- ArgName
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam ArgName
    "j" (\ NamesT Fail Term
    j -> Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    por NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT Fail Term
    lvl
                                            NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    phi
                                            NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    ineg NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    i)
                                            NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> ArgName
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam ArgName
    "_" (\ NamesT Fail Term
    o -> NamesT Fail Term
    rect)
                                            NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (NamesT Fail Term
    w NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    imin NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    i NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    j))
                                            NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> ArgName
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam ArgName
    "_" (\ NamesT Fail Term
    o -> NamesT Fail Term
    w0) -- TODO wait for i = 0
                           )
              Term
    u0 <- NamesT Fail Term
    w0
              Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> NamesT Fail Term) -> Term -> NamesT Fail Term
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    theName [] Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` ([Arg Term]
    args [Arg Term] -> [Arg Term] -> [Arg Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    psi, Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    u, Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    u0])

          -- (γ : Γ) ⊢ (flatten Φ)[n ↦ f_n (compR γ)]
          clause_types :: [Dom LType]
    clause_types = [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS [Term
    compTerm Term -> QName -> Term
    `applyProj` (Arg QName -> QName
    forall e. Arg e -> e
    unArg Arg QName
    fn)
                                   | Arg QName
    fn <- [Arg QName] -> [Arg QName]
    forall a. [a] -> [a]
    reverse [Arg QName]
    fns] Substitution' (SubstArg [Dom LType]) -> [Dom LType] -> [Dom LType]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst`
                           Tele (Dom LType) -> [Dom LType]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel (Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS (Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    gamma Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    delta) Substitution' (SubstArg (Tele (Dom LType)))
    -> Tele (Dom LType) -> Tele (Dom LType)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Tele (Dom LType)
    fsT) -- Γ, Φ ⊢ flatten Φ
          -- Δ ⊢ Φ = fsT
          -- Γ, i : I ⊢ Φ'
          fsT' :: Tele (Dom LType)
    fsT' = Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS ((Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    gamma Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Tele (Dom Type) -> Nat
    forall a. Sized a => a -> Nat
    size Tele (Dom Type)
    delta) Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) Substitution' (SubstArg (Tele (Dom LType)))
    -> Tele (Dom LType) -> Tele (Dom LType)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst` Tele (Dom LType)
    fsT

          -- Γ, i : I ⊢ (flatten Φ')[n ↦ f_n (fillR Γ i)]
          filled_types :: [Dom LType]
    filled_types = [Term] -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS [Nat -> Term -> Term
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 Term
    fillTerm Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Term -> Arg Term
    forall e. e -> Arg e
    argN (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Nat -> Term
    var Nat
    0] Term -> QName -> Term
    `applyProj` (Arg QName -> QName
    forall e. Arg e -> e
    unArg Arg QName
    fn)
                                   | Arg QName
    fn <- [Arg QName] -> [Arg QName]
    forall a. [a] -> [a]
    reverse [Arg QName]
    fns] Substitution' (SubstArg [Dom LType]) -> [Dom LType] -> [Dom LType]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    `applySubst`
                           Tele (Dom LType) -> [Dom LType]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel Tele (Dom LType)
    fsT' -- Γ, i : I, Φ' ⊢ flatten Φ'

      NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    comp <- do
            let
              imax :: NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    imax NamesT Fail Term
    i NamesT Fail Term
    j = Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tIMax NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    i NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    j
            let forward :: NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    forward NamesT Fail Term
    la NamesT Fail Term
    bA NamesT Fail Term
    r NamesT Fail Term
    u = Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    transp NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> ArgName
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam ArgName
    "i" (\ NamesT Fail Term
    i -> NamesT Fail Term
    la NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (NamesT Fail Term
    i NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    `imax` NamesT Fail Term
    r))
                                                NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> ArgName
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam ArgName
    "i" (\ NamesT Fail Term
    i -> NamesT Fail Term
    bA NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (NamesT Fail Term
    i NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    `imax` NamesT Fail Term
    r))
                                                NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    r
                                                NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    u
            (NamesT Fail Term
     -> NamesT Fail Term
     -> NamesT Fail Term
     -> NamesT Fail Term
     -> NamesT Fail Term
     -> NamesT Fail Term)
    -> TCMT
         IO
         (NamesT Fail Term
          -> NamesT Fail Term
          -> NamesT Fail Term
          -> NamesT Fail Term
          -> NamesT Fail Term
          -> NamesT Fail Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((NamesT Fail Term
      -> NamesT Fail Term
      -> NamesT Fail Term
      -> NamesT Fail Term
      -> NamesT Fail Term
      -> NamesT Fail Term)
     -> TCMT
          IO
          (NamesT Fail Term
           -> NamesT Fail Term
           -> NamesT Fail Term
           -> NamesT Fail Term
           -> NamesT Fail Term
           -> NamesT Fail Term))
    -> (NamesT Fail Term
        -> NamesT Fail Term
        -> NamesT Fail Term
        -> NamesT Fail Term
        -> NamesT Fail Term
        -> NamesT Fail Term)
    -> TCMT
         IO
         (NamesT Fail Term
          -> NamesT Fail Term
          -> NamesT Fail Term
          -> NamesT Fail Term
          -> NamesT Fail Term
          -> NamesT Fail Term)
    forall a b. (a -> b) -> a -> b
    $ \ NamesT Fail Term
    la NamesT Fail Term
    bA NamesT Fail Term
    phi NamesT Fail Term
    u NamesT Fail Term
    u0 ->
              Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    hcomp NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (NamesT Fail Term
    la NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io) NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (NamesT Fail Term
    bA NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io) NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT Fail Term
    phi
                          NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> ArgName
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam ArgName
    "i" (\ NamesT Fail Term
    i -> ArgName
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam ArgName
    "o" ((NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term)
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall a b. (a -> b) -> a -> b
    $ \ NamesT Fail Term
    o ->
                                  NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    forward NamesT Fail Term
    la NamesT Fail Term
    bA NamesT Fail Term
    i (NamesT Fail Term
    u NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    i NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <..> NamesT Fail Term
    o))
                          NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    forward NamesT Fail Term
    la NamesT Fail Term
    bA (Term -> NamesT Fail Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    iz) NamesT Fail Term
    u0
      let
          mkBody :: (Arg QName, Dom LType) -> TCMT IO Term
    mkBody (Arg QName
    fname, Dom LType
    filled_ty') = do
            let
              proj :: NamesT Fail Term -> NamesT Fail Term
    proj NamesT Fail Term
    t = (Term -> QName -> Term
    `applyProj` Arg QName -> QName
    forall e. Arg e -> e
    unArg Arg QName
    fname) (Term -> Term) -> NamesT Fail Term -> NamesT Fail Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT Fail Term
    t
              filled_ty :: Term
    filled_ty = ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    defaultArgInfo (ArgName -> Term -> Abs Term
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    "i" (Term -> Abs Term) -> Term -> Abs Term
    forall a b. (a -> b) -> a -> b
    $ (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> (Dom LType -> Type) -> Dom LType -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LType -> Type
    fromLType (LType -> Type) -> (Dom LType -> LType) -> Dom LType -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom LType -> LType
    forall t e. Dom' t e -> e
    unDom) Dom LType
    filled_ty')
              -- Γ ⊢ l : I -> Level of filled_ty
            Level
    l <- Level -> TCMT IO Level
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Level -> TCMT IO Level) -> Level -> TCMT IO Level
    forall a b. (a -> b) -> a -> b
    $ LType -> Level
    lTypeLevel (LType -> Level) -> LType -> Level
    forall a b. (a -> b) -> a -> b
    $ Dom LType -> LType
    forall t e. Dom' t e -> e
    unDom Dom LType
    filled_ty'
            let lvl :: Term
    lvl = ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    defaultArgInfo (ArgName -> Term -> Abs Term
    forall a. ArgName -> a -> Abs a
    Abs ArgName
    "i" (Term -> Abs Term) -> Term -> Abs Term
    forall a b. (a -> b) -> a -> b
    $ Level -> Term
    Level Level
    l)
            Term -> TCMT IO Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
    forall a b. (a -> b) -> a -> b
    $ [ArgName] -> NamesT Fail Term -> Term
    forall a. [ArgName] -> NamesT Fail a -> a
    runNames [] (NamesT Fail Term -> Term) -> NamesT Fail Term -> Term
    forall a b. (a -> b) -> a -> b
    $ do
                 NamesT Fail Term
    lvl <- Term -> NamesT Fail (NamesT Fail Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open Term
    lvl
                 [NamesT Fail Term
    phi,NamesT Fail Term
    w,NamesT Fail Term
    w0] <- (Term -> NamesT Fail (NamesT Fail Term))
    -> [Term] -> NamesT Fail [NamesT Fail Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Term -> NamesT Fail (NamesT Fail Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open [Term
    the_phi,Term
    the_u,Term
    the_u0]
                 NamesT Fail Term
    filled_ty <- Term -> NamesT Fail (NamesT Fail Term)
    forall (m :: * -> *) a.
    (MonadFail m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open Term
    filled_ty

                 NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    -> NamesT Fail Term
    comp NamesT Fail Term
    lvl
                      NamesT Fail Term
    filled_ty
                      NamesT Fail Term
    phi
                      (ArgName
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam ArgName
    "i" ((NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term)
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall a b. (a -> b) -> a -> b
    $ \ NamesT Fail Term
    i -> ArgName
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall (m :: * -> *).
    MonadFail m =>
    ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam ArgName
    "o" ((NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term)
    -> (NamesT Fail Term -> NamesT Fail Term) -> NamesT Fail Term
    forall a b. (a -> b) -> a -> b
    $ \ NamesT Fail Term
    o -> NamesT Fail Term -> NamesT Fail Term
    proj (NamesT Fail Term -> NamesT Fail Term)
    -> NamesT Fail Term -> NamesT Fail Term
    forall a b. (a -> b) -> a -> b
    $ NamesT Fail Term
    w NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    i NamesT Fail Term -> NamesT Fail Term -> NamesT Fail Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT Fail Term
    o) -- TODO wait for phi = 1
                      (NamesT Fail Term -> NamesT Fail Term
    proj NamesT Fail Term
    w0)

      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "hcomp.rec" Nat
    60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ ArgName
    "filled_types sorts:" ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ [Sort] -> ArgName
    forall a. Show a => a -> ArgName
    show ((Dom LType -> Sort) -> [Dom LType] -> [Sort]
    forall a b. (a -> b) -> [a] -> [b]
    map (Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort (Type -> Sort) -> (Dom LType -> Type) -> Dom LType -> Sort
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LType -> Type
    fromLType (LType -> Type) -> (Dom LType -> LType) -> Dom LType -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom LType -> LType
    forall t e. Dom' t e -> e
    unDom) [Dom LType]
    filled_types)

      [Term]
    bodys <- ((Arg QName, Dom LType) -> TCMT IO Term)
    -> [(Arg QName, Dom LType)] -> TCMT IO [Term]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Arg QName, Dom LType) -> TCMT IO Term
    mkBody ([Arg QName] -> [Dom LType] -> [(Arg QName, Dom LType)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Arg QName]
    fns [Dom LType]
    filled_types)
      ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
     Substitution' Term)
    -> TCMT
         IO
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
      Substitution' Term)
     -> TCMT
          IO
          ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
           Substitution' Term))
    -> ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
        Substitution' Term)
    -> TCMT
         IO
         ((QName, Tele (Dom Type), Type, [Dom Type], [Term]),
          Substitution' Term)
    forall a b. (a -> b) -> a -> b
    $ ((QName
    theName, Tele (Dom Type)
    gamma, Type
    rtype, (Dom LType -> Dom Type) -> [Dom LType] -> [Dom Type]
    forall a b. (a -> b) -> [a] -> [b]
    map ((LType -> Type) -> Dom LType -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap LType -> Type
    fromLType) [Dom LType]
    clause_types, [Term]
    bodys),Substitution' Term
    forall a. Substitution' a
    IdS)

    getGeneralizedParameters :: Set Name -> QName -> TCM [Maybe Name]
    getGeneralizedParameters :: Set Name -> QName -> TCM [Maybe Name]
    getGeneralizedParameters Set Name
    gpars QName
    name | Set Name -> Bool
    forall a. Set a -> Bool
    Set.null Set Name
    gpars = [Maybe Name] -> TCM [Maybe Name]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
    getGeneralizedParameters Set Name
    gpars QName
    name = do
      -- Drop the named parameters that shouldn't be in scope (if the user
      -- wrote a split data type)
      let inscope :: Name -> Maybe Name
    inscope Name
    x = Name
    x Name -> Maybe () -> Maybe Name
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Name -> Set Name -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Name
    x Set Name
    gpars)
      (Maybe Name -> Maybe Name) -> [Maybe Name] -> [Maybe Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Maybe Name -> (Name -> Maybe Name) -> Maybe Name
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Name -> Maybe Name
    inscope) ([Maybe Name] -> [Maybe Name])
    -> (Definition -> [Maybe Name]) -> Definition -> [Maybe Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> [Maybe Name]
    defGeneralizedParams (Definition -> [Maybe Name])
    -> TCMT IO Definition -> TCM [Maybe Name]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Definition -> TCMT IO Definition
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    Definition -> m Definition
    instantiateDef (Definition -> TCMT IO Definition)
    -> TCMT IO Definition -> TCMT IO Definition
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    name)

    -- | Bind the named generalized parameters.
    bindGeneralizedParameters :: [Maybe Name] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
    bindGeneralizedParameters :: forall a.
    [Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
    bindGeneralizedParameters [] Type
    t Tele (Dom Type) -> Type -> TCM a
    ret = Tele (Dom Type) -> Type -> TCM a
    ret Tele (Dom Type)
    forall a. Tele a
    EmptyTel Type
    t
    bindGeneralizedParameters (Maybe Name
    name : [Maybe Name]
    names) Type
    t Tele (Dom Type) -> Type -> TCM a
    ret =
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
        Pi Dom Type
    a Abs Type
    b -> TCM a -> TCM a
    ext (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $ [Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
    forall a.
    [Maybe Name] -> Type -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
    bindGeneralizedParameters [Maybe Name]
    names (Abs Type -> Type
    forall a. Abs a -> a
    unAbs Abs Type
    b) ((Tele (Dom Type) -> Type -> TCM a) -> TCM a)
    -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
    forall a b. (a -> b) -> a -> b
    $ \ Tele (Dom Type)
    tel Type
    t -> Tele (Dom Type) -> Type -> TCM a
    ret (Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    a (Tele (Dom Type)
    tel Tele (Dom Type) -> Abs Type -> Abs (Tele (Dom Type))
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Abs Type
    b)) Type
    t
          where
            ext :: TCM a -> TCM a
    ext | Just Name
    x <- Maybe Name
    name = (Name, Dom Type) -> TCM a -> TCM a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Name
    x, Dom Type
    a)
                | Bool
    otherwise      = (ArgName, Dom Type) -> TCM a -> TCM a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b, Dom Type
    a)
        Term
    _      -> TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Bind the parameters of a datatype.
    --
    --   We allow omission of hidden parameters at the definition site.
    --   Example:
    --   @
    --     data D {a} (A : Set a) : Set a
    --     data D A where
    --       c : A -> D A
    --   @

    bindParameters
      :: Int            -- ^ Number of parameters
      -> [A.LamBinding] -- ^ Bindings from definition site.
      -> Type           -- ^ Pi-type of bindings coming from signature site.
      -> (Telescope -> Type -> TCM a)
         -- ^ Continuation, accepting parameter telescope and rest of type.
         --   The parameters are part of the context when the continutation is invoked.
      -> TCM a

    bindParameters :: forall a.
    Nat
    -> [LamBinding]
    -> Type
    -> (Tele (Dom Type) -> Type -> TCM a)
    -> TCM a
    bindParameters Nat
    0 [] Type
    a Tele (Dom Type) -> Type -> TCM a
    ret = Tele (Dom Type) -> Type -> TCM a
    ret Tele (Dom Type)
    forall a. Tele a
    EmptyTel Type
    a

    bindParameters Nat
    0 (LamBinding
    par : [LamBinding]
    _) Type
    _ Tele (Dom Type) -> Type -> TCM a
    _ = LamBinding -> TCM a -> TCM a
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange LamBinding
    par (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $
      TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
        ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text ArgName
    "Unexpected parameter" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> LamBinding -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA LamBinding
    par

    bindParameters Nat
    npars [] Type
    t Tele (Dom Type) -> Type -> TCM a
    ret =
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
        Pi Dom Type
    a Abs Type
    b | Bool -> Bool
    not (Dom Type -> Bool
    forall a. LensHiding a => a -> Bool
    visible Dom Type
    a) -> do
                  Name
    x <- ArgName -> TCMT IO Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b)
                  Nat
    -> [LamBinding]
    -> Name
    -> Dom Type
    -> Abs Type
    -> (Tele (Dom Type) -> Type -> TCM a)
    -> TCM a
    forall a.
    Nat
    -> [LamBinding]
    -> Name
    -> Dom Type
    -> Abs Type
    -> (Tele (Dom Type) -> Type -> TCM a)
    -> TCM a
    bindParameter Nat
    npars [] Name
    x Dom Type
    a Abs Type
    b Tele (Dom Type) -> Type -> TCM a
    ret
               | Bool
    otherwise ->
                  TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                    [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep [ TCMT IO Doc
    "Expected binding for parameter"
                        , ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b) 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 -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a) ]
        Term
    _ -> TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    bindParameters Nat
    npars par :: [LamBinding]
    par@(A.DomainFull (A.TBind Range
    _ TacticAttr
    _ List1 (NamedArg Binder)
    xs Expr
    e) : [LamBinding]
    bs) Type
    a Tele (Dom Type) -> Type -> TCM a
    ret =
      [LamBinding] -> TCM a -> TCM a
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange [LamBinding]
    par (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $
      TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
        let s :: ArgName
    s | List1 (NamedArg Binder) -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length List1 (NamedArg Binder)
    xs Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    1 = ArgName
    "s"
              | Bool
    otherwise     = ArgName
    ""
        ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName
    "Unexpected type signature for parameter" ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    s) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep ((NamedArg Binder -> TCMT IO Doc)
    -> List1 (NamedArg Binder) -> NonEmpty (TCMT IO Doc)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NamedArg Binder -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA List1 (NamedArg Binder)
    xs)

    bindParameters Nat
    _ (A.DomainFull A.TLet{} : [LamBinding]
    _) Type
    _ Tele (Dom Type) -> Type -> TCM a
    _ = TCM a
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    bindParameters Nat
    _ (par :: LamBinding
    par@(A.DomainFree TacticAttr
    _ NamedArg Binder
    arg) : [LamBinding]
    ps) Type
    _ Tele (Dom Type) -> Type -> TCM a
    _
      | NamedArg Binder -> Modality
    forall a. LensModality a => a -> Modality
    getModality NamedArg Binder
    arg Modality -> Modality -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Modality
    defaultModality = LamBinding -> TCM a -> TCM a
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange LamBinding
    par (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $
         TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
           ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text ArgName
    "Unexpected modality/relevance annotation in" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> LamBinding -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA LamBinding
    par

    bindParameters Nat
    npars ps0 :: [LamBinding]
    ps0@(par :: LamBinding
    par@(A.DomainFree TacticAttr
    _ NamedArg Binder
    arg) : [LamBinding]
    ps) Type
    t Tele (Dom Type) -> Type -> TCM a
    ret = do
      let x :: Binder
    x          = NamedArg Binder -> Binder
    forall a. NamedArg a -> a
    namedArg NamedArg Binder
    arg
          TelV Tele (Dom Type)
    tel Type
    _ = Type -> TelV Type
    telView' Type
    t
      case NamedArg Binder -> [Dom' Term (ArgName, Type)] -> ImplicitInsertion
    forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
    insertImplicit NamedArg Binder
    arg ([Dom' Term (ArgName, Type)] -> ImplicitInsertion)
    -> [Dom' Term (ArgName, Type)] -> ImplicitInsertion
    forall a b. (a -> b) -> a -> b
    $ Tele (Dom Type) -> [Dom' Term (ArgName, Type)]
    forall t. Tele (Dom t) -> [Dom (ArgName, t)]
    telToList Tele (Dom Type)
    tel of
        ImplicitInsertion
    NoInsertNeeded -> [LamBinding] -> Name -> TCM a
    continue [LamBinding]
    ps (Name -> TCM a) -> Name -> TCM a
    forall a b. (a -> b) -> a -> b
    $ BindName -> Name
    A.unBind (BindName -> Name) -> BindName -> Name
    forall a b. (a -> b) -> a -> b
    $ Binder -> BindName
    forall a. Binder' a -> a
    A.binderName Binder
    x
        ImpInsert [Dom ()]
    _    -> [LamBinding] -> Name -> TCM a
    continue [LamBinding]
    ps0 (Name -> TCM a) -> TCMT IO Name -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ArgName -> TCMT IO Name
    forall a (m :: * -> *).
    (FreshName a, MonadFresh NameId m) =>
    a -> m Name
    freshName_ (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b)
        ImplicitInsertion
    BadImplicits   -> LamBinding -> TCM a -> TCM a
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange LamBinding
    par (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $
         TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
           ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text ArgName
    "Unexpected parameter" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> LamBinding -> TCMT IO Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA LamBinding
    par
        NoSuchName ArgName
    x   -> LamBinding -> TCM a -> TCM a
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange LamBinding
    par (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $
          TypeError -> TCM a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> TCM a) -> TCMT IO Doc -> TCM a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
            ArgName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
    text (ArgName
    "No parameter of name " ArgName -> ArgName -> ArgName
    forall a. [a] -> [a] -> [a]
    ++ ArgName
    x)
      where
        Pi dom :: Dom Type
    dom@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    info', unDom :: forall t e. Dom' t e -> e
    unDom = Type
    a}) Abs Type
    b = Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t -- TODO:: Defined but not used: info', a
        continue :: [LamBinding] -> Name -> TCM a
    continue [LamBinding]
    ps Name
    x = Nat
    -> [LamBinding]
    -> Name
    -> Dom Type
    -> Abs Type
    -> (Tele (Dom Type) -> Type -> TCM a)
    -> TCM a
    forall a.
    Nat
    -> [LamBinding]
    -> Name
    -> Dom Type
    -> Abs Type
    -> (Tele (Dom Type) -> Type -> TCM a)
    -> TCM a
    bindParameter Nat
    npars [LamBinding]
    ps Name
    x Dom Type
    dom Abs Type
    b Tele (Dom Type) -> Type -> TCM a
    ret

    bindParameter :: Int -> [A.LamBinding] -> Name -> Dom Type -> Abs Type -> (Telescope -> Type -> TCM a) -> TCM a
    bindParameter :: forall a.
    Nat
    -> [LamBinding]
    -> Name
    -> Dom Type
    -> Abs Type
    -> (Tele (Dom Type) -> Type -> TCM a)
    -> TCM a
    bindParameter Nat
    npars [LamBinding]
    ps Name
    x Dom Type
    a Abs Type
    b Tele (Dom Type) -> Type -> TCM a
    ret =
      (Name, Dom Type) -> TCM a -> TCM a
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Name
    x, Dom Type
    a) (TCM a -> TCM a) -> TCM a -> TCM a
    forall a b. (a -> b) -> a -> b
    $
        Nat
    -> [LamBinding]
    -> Type
    -> (Tele (Dom Type) -> Type -> TCM a)
    -> TCM a
    forall a.
    Nat
    -> [LamBinding]
    -> Type
    -> (Tele (Dom Type) -> Type -> TCM a)
    -> TCM a
    bindParameters (Nat
    npars Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) [LamBinding]
    ps (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b) ((Tele (Dom Type) -> Type -> TCM a) -> TCM a)
    -> (Tele (Dom Type) -> Type -> TCM a) -> TCM a
    forall a b. (a -> b) -> a -> b
    $ \ Tele (Dom Type)
    tel Type
    s ->
          Tele (Dom Type) -> Type -> TCM a
    ret (Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel Dom Type
    a (Abs (Tele (Dom Type)) -> Tele (Dom Type))
    -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a b. (a -> b) -> a -> b
    $ ArgName -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    forall a. ArgName -> a -> Abs a
    Abs (Name -> ArgName
    nameToArgName Name
    x) Tele (Dom Type)
    tel) Type
    s

    -- | Check that the arguments to a constructor fits inside the sort of the datatype.
    --   The third argument is the type of the constructor.
    --
    --   When @--without-K@ is active and the type is fibrant the
    --   procedure also checks that the type is usable at the current
    --   modality. See #4784 and #5434.
    --
    --   As a side effect, return the arity of the constructor.

    fitsIn :: UniverseCheck -> [IsForced] -> Type -> Sort -> TCM Int
    fitsIn :: UniverseCheck -> [IsForced] -> Type -> Sort -> TCMT IO Nat
    fitsIn UniverseCheck
    uc [IsForced]
    forceds Type
    t Sort
    s = do
      ArgName -> Nat -> TCMT IO Doc -> TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    ArgName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc ArgName
    "tc.data.fits" 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
    "does" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
            , TCMT IO Doc
    "of sort" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Sort -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Type
    t)
            , TCMT IO Doc
    "fit in" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Sort -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Sort
    s TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "?"
            ]
      -- The code below would be simpler, but doesn't allow datatypes
      -- to be indexed by the universe level.
      -- s' <- instantiateFull (getSort t)
      -- noConstraints $ s' `leqSort` s

      Bool
    withoutK <- TCMT IO Bool
    forall (m :: * -> *). HasOptions m => m Bool
    withoutKOption
      Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    withoutK (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Bool -> TCM () -> TCM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (Sort -> TCMT IO Bool
    forall a (m :: * -> *).
    (LensSort a, PureTCM m, MonadBlock m) =>
    a -> m Bool
    isFibrant Sort
    s) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        Quantity
    q <- Lens' Quantity TCEnv -> TCMT IO Quantity
    forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
    viewTC Lens' Quantity TCEnv
    eQuantity
        Modality -> Term -> TCM ()
    MonadConstraint (TCMT IO) => Modality -> Term -> TCM ()
    usableAtModality (Quantity -> Modality -> Modality
    forall a. LensQuantity a => Quantity -> a -> a
    setQuantity Quantity
    q Modality
    defaultModality) (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t)

      Bool -> [IsForced] -> Type -> Sort -> TCMT IO Nat
    fitsIn' Bool
    withoutK [IsForced]
    forceds Type
    t Sort
    s
      where
      fitsIn' :: Bool -> [IsForced] -> Type -> Sort -> TCMT IO Nat
    fitsIn' Bool
    withoutK [IsForced]
    forceds Type
    t Sort
    s = do
        Maybe (Bool, Dom Type, Abs Type)
    vt <- do
          Either (Dom Type, Abs Type) Type
    t <- Type -> TCMT IO (Either (Dom Type, Abs Type) Type)
    forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Either (Dom Type, Abs Type) Type)
    pathViewAsPi Type
    t
          Maybe (Bool, Dom Type, Abs Type)
    -> TCMT IO (Maybe (Bool, Dom Type, Abs Type))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (Bool, Dom Type, Abs Type)
     -> TCMT IO (Maybe (Bool, Dom Type, Abs Type)))
    -> Maybe (Bool, Dom Type, Abs Type)
    -> TCMT IO (Maybe (Bool, Dom Type, Abs Type))
    forall a b. (a -> b) -> a -> b
    $ case Either (Dom Type, Abs Type) Type
    t of
                        Left (Dom Type
    a,Abs Type
    b)     -> (Bool, Dom Type, Abs Type) -> Maybe (Bool, Dom Type, Abs Type)
    forall a. a -> Maybe a
    Just (Bool
    True ,Dom Type
    a,Abs Type
    b)
                        Right (El Sort
    _ Term
    t) | Pi Dom Type
    a Abs Type
    b <- Term
    t
                                       -> (Bool, Dom Type, Abs Type) -> Maybe (Bool, Dom Type, Abs Type)
    forall a. a -> Maybe a
    Just (Bool
    False,Dom Type
    a,Abs Type
    b)
                        Either (Dom Type, Abs Type) Type
    _              -> Maybe (Bool, Dom Type, Abs Type)
    forall a. Maybe a
    Nothing
        case Maybe (Bool, Dom Type, Abs Type)
    vt of
          Just (Bool
    isPath, Dom Type
    dom, Abs Type
    b) -> do
            let (IsForced
    forced,[IsForced]
    forceds') = [IsForced] -> (IsForced, [IsForced])
    nextIsForced [IsForced]
    forceds
            Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (IsForced -> Bool
    isForced IsForced
    forced Bool -> Bool -> Bool
    && Bool -> Bool
    not Bool
    withoutK) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
              Sort
    sa <- Sort -> TCMT IO Sort
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Sort -> TCMT IO Sort) -> Sort -> TCMT IO Sort
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Dom Type
    dom
              Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Bool
    isPath Bool -> Bool -> Bool
    || UniverseCheck
    uc UniverseCheck -> UniverseCheck -> Bool
    forall a. Eq a => a -> a -> Bool
    == UniverseCheck
    NoUniverseCheck Bool -> Bool -> Bool
    || Sort
    sa Sort -> Sort -> Bool
    forall a. Eq a => a -> a -> Bool
    == Sort
    forall t. Sort' t
    SizeUniv) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
                Sort
    sa Sort -> Sort -> TCM ()
    forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
    `leqSort` Sort
    s
            (ArgName, Dom Type) -> TCMT IO Nat -> TCMT IO Nat
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Abs Type -> ArgName
    forall a. Abs a -> ArgName
    absName Abs Type
    b, Dom Type
    dom) (TCMT IO Nat -> TCMT IO Nat) -> TCMT IO Nat -> TCMT IO Nat
    forall a b. (a -> b) -> a -> b
    $ do
              Nat -> Nat
    forall a. Enum a => a -> a
    succ (Nat -> Nat) -> TCMT IO Nat -> TCMT IO Nat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Bool -> [IsForced] -> Type -> Sort -> TCMT IO Nat
    fitsIn' Bool
    withoutK [IsForced]
    forceds' (Abs Type -> Type
    forall a. Subst a => Abs a -> a
    absBody Abs Type
    b) (Nat -> Sort -> Sort
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 Sort
    s)
          Maybe (Bool, Dom Type, Abs Type)
    _ -> do
            Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Type
    t Sort -> Sort -> TCM ()
    forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
    `leqSort` Sort
    s
            Nat -> TCMT IO Nat
    forall (m :: * -> *) a. Monad m => a -> m a
    return Nat
    0

    -- | When --without-K is enabled, we should check that the sorts of
    --   the index types fit into the sort of the datatype.
    checkIndexSorts :: Sort -> Telescope -> TCM ()
    checkIndexSorts :: Sort -> Tele (Dom Type) -> TCM ()
    checkIndexSorts Sort
    s = \case
      Tele (Dom Type)
    EmptyTel -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      ExtendTel Dom Type
    a Abs (Tele (Dom Type))
    tel' -> do
        let sa :: Sort
    sa = Dom Type -> Sort
    forall a. LensSort a => a -> Sort
    getSort Dom Type
    a
        -- Andreas, 2020-10-19, allow Size indices
        Bool -> TCM () -> TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Sort
    sa Sort -> Sort -> Bool
    forall a. Eq a => a -> a -> Bool
    == Sort
    forall t. Sort' t
    SizeUniv) (TCM () -> TCM ()) -> TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Sort
    sa Sort -> Sort -> TCM ()
    forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
    `leqSort` Sort
    s
        Dom Type
    -> Abs (Tele (Dom Type)) -> (Tele (Dom Type) -> TCM ()) -> TCM ()
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction Dom Type
    a Abs (Tele (Dom Type))
    tel' ((Tele (Dom Type) -> TCM ()) -> TCM ())
    -> (Tele (Dom Type) -> TCM ()) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Sort -> Tele (Dom Type) -> TCM ()
    checkIndexSorts (Nat -> Sort -> Sort
    forall a. Subst a => Nat -> a -> a
    raise Nat
    1 Sort
    s)

    -- | Return the parameters that share variables with the indices
    -- nonLinearParameters :: Int -> Type -> TCM [Int]
    -- nonLinearParameters nPars t =

    data IsPathCons = PathCons | PointCons
      deriving (IsPathCons -> IsPathCons -> Bool
    (IsPathCons -> IsPathCons -> Bool)
    -> (IsPathCons -> IsPathCons -> Bool) -> Eq IsPathCons
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: IsPathCons -> IsPathCons -> Bool
    $c/= :: IsPathCons -> IsPathCons -> Bool
    == :: IsPathCons -> IsPathCons -> Bool
    $c== :: IsPathCons -> IsPathCons -> Bool
    Eq,Nat -> IsPathCons -> ArgName -> ArgName
    [IsPathCons] -> ArgName -> ArgName
    IsPathCons -> ArgName
    (Nat -> IsPathCons -> ArgName -> ArgName)
    -> (IsPathCons -> ArgName)
    -> ([IsPathCons] -> ArgName -> ArgName)
    -> Show IsPathCons
    forall a.
    (Nat -> a -> ArgName -> ArgName)
    -> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
    showList :: [IsPathCons] -> ArgName -> ArgName
    $cshowList :: [IsPathCons] -> ArgName -> ArgName
    show :: IsPathCons -> ArgName
    $cshow :: IsPathCons -> ArgName
    showsPrec :: Nat -> IsPathCons -> ArgName -> ArgName
    $cshowsPrec :: Nat -> IsPathCons -> ArgName -> ArgName
    Show)

    -- | Check that a type constructs something of the given datatype. The first
    --   argument is the number of parameters to the datatype and the second the
    --   number of additional non-parameters in the context (1 when generalizing, 0
    --   otherwise).
    --
    constructs :: Int -> Int -> Type -> QName -> TCM IsPathCons
    constructs :: Nat -> Nat -> Type -> QName -> TCM IsPathCons
    constructs Nat
    nofPars Nat
    nofExtraVars Type
    t QName
    q = Nat -> Type -> TCM IsPathCons
    constrT Nat
    nofExtraVars Type
    t
        where
            -- The number n counts the proper (non-parameter) constructor arguments.
            constrT :: Nat -> Type -> TCM IsPathCons
            constrT :: Nat -> Type -> TCM IsPathCons
    constrT Nat
    n Type
    t = do
                Type
    t <- Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t
                Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
    pathV <- TCMT IO (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    forall (m :: * -> *).
    HasBuiltins m =>
    m (Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type)
    pathViewAsPi'whnf
                case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
                    Pi Dom Type
    _ (NoAbs ArgName
    _ Type
    b)  -> Nat -> Type -> TCM IsPathCons
    constrT Nat
    n Type
    b
                    Pi Dom Type
    a Abs Type
    b            -> Dom Type -> Abs Type -> (Type -> TCM IsPathCons) -> TCM IsPathCons
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction Dom Type
    a Abs Type
    b ((Type -> TCM IsPathCons) -> TCM IsPathCons)
    -> (Type -> TCM IsPathCons) -> TCM IsPathCons
    forall a b. (a -> b) -> a -> b
    $ Nat -> Type -> TCM IsPathCons
    constrT (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1)
                      -- OR: addCxtString (absName b) a $ constrT (n + 1) (absBody b)
                    Term
    _ | Left ((Dom Type
    a,Abs Type
    b),(Term, Term)
    _) <- Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
    pathV Type
    t -> do
                          IsPathCons
    _ <- case Abs Type
    b of
                                 NoAbs ArgName
    _ Type
    b -> Nat -> Type -> TCM IsPathCons
    constrT Nat
    n Type
    b
                                 Abs Type
    b         -> Dom Type -> Abs Type -> (Type -> TCM IsPathCons) -> TCM IsPathCons
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction Dom Type
    a Abs Type
    b ((Type -> TCM IsPathCons) -> TCM IsPathCons)
    -> (Type -> TCM IsPathCons) -> TCM IsPathCons
    forall a b. (a -> b) -> a -> b
    $ Nat -> Type -> TCM IsPathCons
    constrT (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1)
                          IsPathCons -> TCM IsPathCons
    forall (m :: * -> *) a. Monad m => a -> m a
    return IsPathCons
    PathCons
                    Def QName
    d Elims
    es | QName
    d QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    q -> do
                      let vs :: [Arg Term]
    vs = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
                      let ([Arg Term]
    pars, [Arg Term]
    ixs) = Nat -> [Arg Term] -> ([Arg Term], [Arg Term])
    forall a. Nat -> [a] -> ([a], [a])
    splitAt Nat
    nofPars [Arg Term]
    vs
                      -- check that the constructor parameters are the data parameters
                      Nat -> [Arg Term] -> TCM ()
    forall {m :: * -> *}.
    (MonadMetaSolver m, MonadWarning m, MonadStatistics m,
     MonadFresh ProblemId m, MonadFresh Nat m) =>
    Nat -> [Arg Term] -> m ()
    checkParams Nat
    n [Arg Term]
    pars
                      IsPathCons -> TCM IsPathCons
    forall (m :: * -> *) a. Monad m => a -> m a
    return IsPathCons
    PointCons
                    MetaV{} -> do
                      Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
                      -- Analyse the type of q (name of the data type)
                      let td :: Type
    td = Definition -> Type
    defType Definition
    def
                      TelV Tele (Dom Type)
    tel Type
    core <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    td
                      -- Construct the parameter arguments
                      -- The parameters are @n + nofPars - 1 .. n@
                      let us :: [Arg Term]
    us = (Arg ArgName -> Nat -> Arg Term)
    -> [Arg ArgName] -> [Nat] -> [Arg Term]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\ Arg ArgName
    arg Nat
    x -> Nat -> Term
    var Nat
    x Term -> Arg ArgName -> Arg Term
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Arg ArgName
    arg ) (Tele (Dom Type) -> [Arg ArgName]
    forall a. TelToArgs a => a -> [Arg ArgName]
    telToArgs Tele (Dom Type)
    tel) ([Nat] -> [Arg Term]) -> [Nat] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $
                                 Nat -> [Nat] -> [Nat]
    forall a. Nat -> [a] -> [a]
    take Nat
    nofPars ([Nat] -> [Nat]) -> [Nat] -> [Nat]
    forall a b. (a -> b) -> a -> b
    $ Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom (Nat
    nofPars Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    n)
                      -- The indices are fresh metas
                      [Arg Term]
    xs <- Type -> TCMT IO [Arg Term]
    forall (m :: * -> *). MonadMetaSolver m => Type -> m [Arg Term]
    newArgsMeta (Type -> TCMT IO [Arg Term]) -> TCMT IO Type -> TCMT IO [Arg Term]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> [Arg Term] -> TCMT IO Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    Type -> a -> m Type
    piApplyM Type
    td [Arg Term]
    us
                      let t' :: Type
    t' = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Nat -> Sort -> Sort
    forall a. Subst a => Nat -> a -> a
    raise Nat
    n (Sort -> Sort) -> Sort -> Sort
    forall a b. (a -> b) -> a -> b
    $ Defn -> Sort
    dataSort (Defn -> Sort) -> Defn -> Sort
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    def) (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    q (Elims -> Term) -> Elims -> Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
    forall a b. (a -> b) -> a -> b
    $ [Arg Term]
    us [Arg Term] -> [Arg Term] -> [Arg Term]
    forall a. [a] -> [a] -> [a]
    ++ [Arg Term]
    xs
                      -- Andreas, 2017-11-07, issue #2840
                      -- We should not postpone here, otherwise we might upset the positivity checker.
                      TCMT IO Bool -> TCM IsPathCons -> TCM IsPathCons -> TCM IsPathCons
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (TCM () -> TCMT IO Bool
    forall (m :: * -> *).
    (MonadConstraint m, MonadWarning m, MonadError TCErr m,
     MonadFresh ProblemId m) =>
    m () -> m Bool
    tryConversion (TCM () -> TCMT IO Bool) -> TCM () -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> TCM ()
    forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
    equalType Type
    t Type
    t')
                          (Nat -> Type -> TCM IsPathCons
    constrT Nat
    n Type
    t')
                          (TypeError -> TCM IsPathCons
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM IsPathCons) -> TypeError -> TCM IsPathCons
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    ShouldEndInApplicationOfTheDatatype Type
    t)
                    Term
    _ -> TypeError -> TCM IsPathCons
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM IsPathCons) -> TypeError -> TCM IsPathCons
    forall a b. (a -> b) -> a -> b
    $ Type -> TypeError
    ShouldEndInApplicationOfTheDatatype Type
    t

            checkParams :: Nat -> [Arg Term] -> m ()
    checkParams Nat
    n [Arg Term]
    vs = (Arg Term -> Nat -> m ()) -> [Arg Term] -> [Nat] -> m ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    zipWithM_ Arg Term -> Nat -> m ()
    forall {m :: * -> *}.
    (MonadMetaSolver m, MonadWarning m, MonadStatistics m,
     MonadFresh ProblemId m, MonadFresh Nat m) =>
    Arg Term -> Nat -> m ()
    sameVar [Arg Term]
    vs [Nat]
    ps
                where
                    nvs :: Nat
    nvs = [Arg Term] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Arg Term]
    vs
                    ps :: [Nat]
    ps  = [Nat] -> [Nat]
    forall a. [a] -> [a]
    reverse ([Nat] -> [Nat]) -> [Nat] -> [Nat]
    forall a b. (a -> b) -> a -> b
    $ Nat -> [Nat] -> [Nat]
    forall a. Nat -> [a] -> [a]
    take Nat
    nvs [Nat
    n..]

                    sameVar :: Arg Term -> Nat -> m ()
    sameVar Arg Term
    arg Nat
    i
                      -- skip irrelevant parameters
                      | Arg Term -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Arg Term
    arg = () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
                      | Bool
    otherwise = do
                        Type
    t <- Nat -> m Type
    forall (m :: * -> *).
    (Applicative m, MonadFail m, MonadTCEnv m) =>
    Nat -> m Type
    typeOfBV Nat
    i
                        Type -> Term -> Term -> m ()
    forall (m :: * -> *).
    MonadConversion m =>
    Type -> Term -> Term -> m ()
    equalTerm Type
    t (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg) (Nat -> Term
    var Nat
    i)

    -- | Is the type coinductive? Returns 'Nothing' if the answer cannot
    -- be determined.

    isCoinductive :: Type -> TCM (Maybe Bool)
    isCoinductive :: Type -> TCM (Maybe Bool)
    isCoinductive Type
    t = do
      El Sort
    s Term
    t <- Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t
      case Term
    t of
        Def QName
    q Elims
    _ -> do
          Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
          case Definition -> Defn
    theDef Definition
    def of
            Axiom       {} -> Maybe Bool -> TCM (Maybe Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False)
            DataOrRecSig{} -> Maybe Bool -> TCM (Maybe Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Bool
    forall a. Maybe a
    Nothing
            Function    {} -> Maybe Bool -> TCM (Maybe Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Bool
    forall a. Maybe a
    Nothing
            Datatype    {} -> Maybe Bool -> TCM (Maybe Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False)
            Record      {  recInduction :: Defn -> Maybe Induction
    recInduction = Just Induction
    CoInductive } -> Maybe Bool -> TCM (Maybe Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True)
            Record      {  recInduction :: Defn -> Maybe Induction
    recInduction = Maybe Induction
    _                } -> Maybe Bool -> TCM (Maybe Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False)
            GeneralizableVar{} -> TCM (Maybe Bool)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            Constructor {} -> TCM (Maybe Bool)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            Primitive   {} -> TCM (Maybe Bool)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            PrimitiveSort{} -> TCM (Maybe Bool)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
            AbstractDefn{} -> TCM (Maybe Bool)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Var   {} -> Maybe Bool -> TCM (Maybe Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Bool
    forall a. Maybe a
    Nothing
        Lam   {} -> TCM (Maybe Bool)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Lit   {} -> TCM (Maybe Bool)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Level {} -> TCM (Maybe Bool)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Con   {} -> TCM (Maybe Bool)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Pi    {} -> Maybe Bool -> TCM (Maybe Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False)
        Sort  {} -> Maybe Bool -> TCM (Maybe Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False)
        MetaV {} -> Maybe Bool -> TCM (Maybe Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Bool
    forall a. Maybe a
    Nothing
        DontCare{} -> TCM (Maybe Bool)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Dummy ArgName
    s Elims
    _  -> ArgName -> TCM (Maybe Bool)
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    ArgName -> m a
    __IMPOSSIBLE_VERBOSE__ ArgName
    s