    ------------------------------------------------------------------------
    -- | Handling of the INFINITY, SHARP and FLAT builtins.
    ------------------------------------------------------------------------

    module Agda.TypeChecking.Rules.Builtin.Coinduction where

    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Position
    import Agda.Syntax.Scope.Base

    import Agda.TypeChecking.CompiledClause
    import Agda.TypeChecking.Level
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Positivity.Occurrence
    import Agda.TypeChecking.Primitive
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Rules.Builtin
    import Agda.TypeChecking.Rules.Term

    -- | The type of @∞@.

    typeOfInf :: TCM Type
    typeOfInf :: TCM Type
    typeOfInf = ArgName -> TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    hPi ArgName
    "a" (TCMT IO Term -> TCM Type
    forall (m :: * -> *). Functor m => m Term -> m Type
    el TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $
                (Type -> TCM Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> TCM Type) -> (Sort -> Type) -> Sort -> TCM Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sort -> Type
    sort (Sort -> TCM Type) -> Sort -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Sort
    varSort Int
    0) TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> (Type -> TCM Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> TCM Type) -> (Sort -> Type) -> Sort -> TCM Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sort -> Type
    sort (Sort -> TCM Type) -> Sort -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Sort
    varSort Int
    0)

    -- | The type of @♯_@.

    typeOfSharp :: TCM Type
    typeOfSharp :: TCM Type
    typeOfSharp = ArgName -> TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    hPi ArgName
    "a" (TCMT IO Term -> TCM Type
    forall (m :: * -> *). Functor m => m Term -> m Type
    el TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $
                  ArgName -> TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    hPi ArgName
    "A" (Type -> TCM Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> TCM Type) -> (Sort -> Type) -> Sort -> TCM Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sort -> Type
    sort (Sort -> TCM Type) -> Sort -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Sort
    varSort Int
    0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $
                  (Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Int -> Sort
    varSort Int
    1) (Term -> Type) -> TCMT IO Term -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    0) TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    -->
                  (Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Int -> Sort
    varSort Int
    1) (Term -> Type) -> TCMT IO Term -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primInf TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    0)

    -- | The type of @♭@.

    typeOfFlat :: TCM Type
    typeOfFlat :: TCM Type
    typeOfFlat = ArgName -> TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    hPi ArgName
    "a" (TCMT IO Term -> TCM Type
    forall (m :: * -> *). Functor m => m Term -> m Type
    el TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $
                 ArgName -> TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    ArgName -> m Type -> m Type -> m Type
    hPi ArgName
    "A" (Type -> TCM Type
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> TCM Type) -> (Sort -> Type) -> Sort -> TCM Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sort -> Type
    sort (Sort -> TCM Type) -> Sort -> TCM Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Sort
    varSort Int
    0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
    forall a b. (a -> b) -> a -> b
    $
                 (Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Int -> Sort
    varSort Int
    1) (Term -> Type) -> TCMT IO Term -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primInf TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    0) TCM Type -> TCM Type -> TCM Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    -->
                 (Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Int -> Sort
    varSort Int
    1) (Term -> Type) -> TCMT IO Term -> TCM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> TCMT IO Term
    forall (m :: * -> *). Applicative m => Int -> m Term
    varM Int
    0)

    -- | Binds the INFINITY builtin, but does not change the type's
    -- definition.

    bindBuiltinInf :: ResolvedName -> TCM ()
    bindBuiltinInf :: ResolvedName -> TCM ()
    bindBuiltinInf ResolvedName
    x = ArgName
    -> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
    bindPostulatedName ArgName
    builtinInf ResolvedName
    x ((QName -> Definition -> TCMT IO Term) -> TCM ())
    -> (QName -> Definition -> TCMT IO Term) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \QName
    inf Definition
    _ -> do
      Term
    _ <- Expr -> Type -> TCMT IO Term
    checkExpr (QName -> Expr
    A.Def QName
    inf) (Type -> TCMT IO Term) -> TCM Type -> TCMT IO Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCM Type
    typeOfInf
      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
    $ QName -> Elims -> Term
    Def QName
    inf []

    -- | Binds the SHARP builtin, and changes the definitions of INFINITY
    -- and SHARP.

    -- The following (no longer supported) definition is used:
    --
    -- codata ∞ {a} (A : Set a) : Set a where
    --   ♯_ : (x : A) → ∞ A

    bindBuiltinSharp :: ResolvedName -> TCM ()
    bindBuiltinSharp :: ResolvedName -> TCM ()
    bindBuiltinSharp ResolvedName
    x =
      ArgName
    -> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
    bindPostulatedName ArgName
    builtinSharp ResolvedName
    x ((QName -> Definition -> TCMT IO Term) -> TCM ())
    -> (QName -> Definition -> TCMT IO Term) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \QName
    sharp Definition
    sharpDefn -> do
        Type
    sharpType <- TCM Type
    typeOfSharp
        TelV Tele (Dom Type)
    fieldTel Type
    _ <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    sharpType
        Term
    _ <- Expr -> Type -> TCMT IO Term
    checkExpr (QName -> Expr
    A.Def QName
    sharp) Type
    sharpType
        Def QName
    inf Elims
    _ <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primInf
        Definition
    infDefn   <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    inf
        QName -> Definition -> TCM ()
    addConstant (Definition -> QName
    defName Definition
    infDefn) (Definition -> TCM ()) -> Definition -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          Definition
    infDefn { defPolarity :: [Polarity]
    defPolarity       = [] -- not monotone
                  , defArgOccurrences :: [Occurrence]
    defArgOccurrences = [Occurrence
    Unused, Occurrence
    StrictPos]
                  , theDef :: Defn
    theDef = Record :: Int
    -> Maybe Clause
    -> ConHead
    -> Bool
    -> [Dom QName]
    -> Tele (Dom Type)
    -> Maybe [QName]
    -> EtaEquality
    -> PatternOrCopattern
    -> Maybe Induction
    -> IsAbstract
    -> CompKit
    -> Defn
    Record
                      { recPars :: Int
    recPars           = Int
    2
                      , recInduction :: Maybe Induction
    recInduction      = Induction -> Maybe Induction
    forall a. a -> Maybe a
    Just Induction
    CoInductive
                      , recClause :: Maybe Clause
    recClause         = Maybe Clause
    forall a. Maybe a
    Nothing
                      , recConHead :: ConHead
    recConHead        = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead QName
    sharp (PatternOrCopattern -> DataOrRecord
    IsRecord PatternOrCopattern
    CopatternMatching) Induction
    CoInductive []  -- flat is added later
                      , recNamedCon :: Bool
    recNamedCon       = Bool
    True
                      , recFields :: [Dom QName]
    recFields         = []  -- flat is added later
                      , recTel :: Tele (Dom Type)
    recTel            = Tele (Dom Type)
    fieldTel
                      , recEtaEquality' :: EtaEquality
    recEtaEquality'   = HasEta -> EtaEquality
    Inferred (HasEta -> EtaEquality) -> HasEta -> EtaEquality
    forall a b. (a -> b) -> a -> b
    $ PatternOrCopattern -> HasEta
    forall a. a -> HasEta' a
    NoEta PatternOrCopattern
    CopatternMatching
                      , recPatternMatching :: PatternOrCopattern
    recPatternMatching= PatternOrCopattern
    CopatternMatching
                      , recMutual :: Maybe [QName]
    recMutual         = [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just []
                      , recAbstr :: IsAbstract
    recAbstr          = IsAbstract
    ConcreteDef
                      , recComp :: CompKit
    recComp           = CompKit
    emptyCompKit
                      }
                  }
        QName -> Definition -> TCM ()
    addConstant QName
    sharp (Definition -> TCM ()) -> Definition -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          Definition
    sharpDefn { theDef :: Defn
    theDef = Constructor :: Int
    -> Int
    -> ConHead
    -> QName
    -> IsAbstract
    -> Induction
    -> CompKit
    -> Maybe [QName]
    -> [IsForced]
    -> Maybe [Bool]
    -> Defn
    Constructor
                        { conPars :: Int
    conPars   = Int
    2
                        , conArity :: Int
    conArity  = Int
    1
                        , conSrcCon :: ConHead
    conSrcCon = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead QName
    sharp (PatternOrCopattern -> DataOrRecord
    IsRecord PatternOrCopattern
    CopatternMatching) Induction
    CoInductive [] -- flat is added as field later
                        , conData :: QName
    conData   = Definition -> QName
    defName Definition
    infDefn
                        , conAbstr :: IsAbstract
    conAbstr  = IsAbstract
    ConcreteDef
                        , conInd :: Induction
    conInd    = Induction
    CoInductive
                        , conComp :: CompKit
    conComp   = CompKit
    emptyCompKit
                        , conProj :: Maybe [QName]
    conProj   = Maybe [QName]
    forall a. Maybe a
    Nothing
                        , conForced :: [IsForced]
    conForced = []
                        , conErased :: Maybe [Bool]
    conErased = Maybe [Bool]
    forall a. Maybe a
    Nothing
                        }
                    }
        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
    $ QName -> Elims -> Term
    Def QName
    sharp []

    -- | Binds the FLAT builtin, and changes its definition.

    -- The following (no longer supported) definition is used:
    --
    --   ♭ : ∀ {a} {A : Set a} → ∞ A → A
    --   ♭ (♯ x) = x

    bindBuiltinFlat :: ResolvedName -> TCM ()
    bindBuiltinFlat :: ResolvedName -> TCM ()
    bindBuiltinFlat ResolvedName
    x =
      ArgName
    -> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
    bindPostulatedName ArgName
    builtinFlat ResolvedName
    x ((QName -> Definition -> TCMT IO Term) -> TCM ())
    -> (QName -> Definition -> TCMT IO Term) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ \ QName
    flat Definition
    flatDefn -> do
        Term
    _ <- Expr -> Type -> TCMT IO Term
    checkExpr (QName -> Expr
    A.Def QName
    flat) (Type -> TCMT IO Term) -> TCM Type -> TCMT IO Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCM Type
    typeOfFlat
        Def QName
    sharp Elims
    _ <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSharp
        LevelKit
    kit         <- TCMT IO LevelKit
    forall (m :: * -> *). HasBuiltins m => m LevelKit
    requireLevels
        Def QName
    inf Elims
    _   <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primInf
        let sharpCon :: ConHead
    sharpCon = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead QName
    sharp (PatternOrCopattern -> DataOrRecord
    IsRecord PatternOrCopattern
    CopatternMatching) Induction
    CoInductive [QName -> Arg QName
    forall a. a -> Arg a
    defaultArg QName
    flat]
            level :: Type
    level    = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Integer -> Sort
    mkType Integer
    0) (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def (LevelKit -> QName
    typeName LevelKit
    kit) []
            tel     :: Telescope
            tel :: Tele (Dom Type)
    tel      = Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Type -> Dom Type
    forall e. e -> Dom e
    domH (Type -> Dom Type) -> Type -> Dom Type
    forall a b. (a -> b) -> a -> b
    $ Type
    level)                  (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 ArgName
    "a" (Tele (Dom Type) -> Abs (Tele (Dom Type)))
    -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $
                       Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Type -> Dom Type
    forall e. e -> Dom e
    domH (Type -> Dom Type) -> Type -> Dom Type
    forall a b. (a -> b) -> a -> b
    $ Sort -> Type
    sort (Sort -> Type) -> Sort -> Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Sort
    varSort Int
    0)       (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 ArgName
    "A" (Tele (Dom Type) -> Abs (Tele (Dom Type)))
    -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $
                       Dom Type -> Abs (Tele (Dom Type)) -> Tele (Dom Type)
    forall a. a -> Abs (Tele a) -> Tele a
    ExtendTel (Type -> Dom Type
    forall e. e -> Dom e
    domN (Type -> Dom Type) -> Type -> Dom Type
    forall a b. (a -> b) -> a -> b
    $ Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Int -> Sort
    varSort Int
    1) (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    0) (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 ArgName
    "x" (Tele (Dom Type) -> Abs (Tele (Dom Type)))
    -> Tele (Dom Type) -> Abs (Tele (Dom Type))
    forall a b. (a -> b) -> a -> b
    $
                       Tele (Dom Type)
    forall a. Tele a
    EmptyTel
            infA :: Type
    infA     = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Int -> Sort
    varSort Int
    2) (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    inf [ Arg Term -> Elim' Term
    forall a. Arg a -> Elim' a
    Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    1 ]
            cpi :: ConPatternInfo
    cpi      = ConPatternInfo
    noConPatternInfo { conPType :: Maybe (Arg Type)
    conPType = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
    forall a b. (a -> b) -> a -> b
    $ Type -> Arg Type
    forall a. a -> Arg a
    defaultArg Type
    infA
                                        , conPLazy :: Bool
    conPLazy = Bool
    True }
        let clause :: Clause
    clause   = Clause :: Range
    -> Range
    -> Tele (Dom Type)
    -> NAPs
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Bool
    -> Maybe Bool
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Clause
    Clause
              { clauseLHSRange :: Range
    clauseLHSRange  = Range
    forall a. Range' a
    noRange
              , clauseFullRange :: Range
    clauseFullRange = Range
    forall a. Range' a
    noRange
              , clauseTel :: Tele (Dom Type)
    clauseTel       = Tele (Dom Type)
    tel
              , namedClausePats :: NAPs
    namedClausePats = [ Named NamedName (Pattern' DBPatVar)
    -> Arg (Named NamedName (Pattern' DBPatVar))
    forall a. a -> Arg a
    argN (Named NamedName (Pattern' DBPatVar)
     -> Arg (Named NamedName (Pattern' DBPatVar)))
    -> Named NamedName (Pattern' DBPatVar)
    -> Arg (Named NamedName (Pattern' DBPatVar))
    forall a b. (a -> b) -> a -> b
    $ Maybe NamedName
    -> Pattern' DBPatVar -> Named NamedName (Pattern' DBPatVar)
    forall name a. Maybe name -> a -> Named name a
    Named Maybe NamedName
    forall a. Maybe a
    Nothing (Pattern' DBPatVar -> Named NamedName (Pattern' DBPatVar))
    -> Pattern' DBPatVar -> Named NamedName (Pattern' DBPatVar)
    forall a b. (a -> b) -> a -> b
    $
                  ConHead -> ConPatternInfo -> NAPs -> Pattern' DBPatVar
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    sharpCon ConPatternInfo
    cpi [ Named NamedName (Pattern' DBPatVar)
    -> Arg (Named NamedName (Pattern' DBPatVar))
    forall a. a -> Arg a
    argN (Named NamedName (Pattern' DBPatVar)
     -> Arg (Named NamedName (Pattern' DBPatVar)))
    -> Named NamedName (Pattern' DBPatVar)
    -> Arg (Named NamedName (Pattern' DBPatVar))
    forall a b. (a -> b) -> a -> b
    $ Maybe NamedName
    -> Pattern' DBPatVar -> Named NamedName (Pattern' DBPatVar)
    forall name a. Maybe name -> a -> Named name a
    Named Maybe NamedName
    forall a. Maybe a
    Nothing (Pattern' DBPatVar -> Named NamedName (Pattern' DBPatVar))
    -> Pattern' DBPatVar -> Named NamedName (Pattern' DBPatVar)
    forall a b. (a -> b) -> a -> b
    $ ArgName -> Int -> Pattern' DBPatVar
    forall a. DeBruijn a => ArgName -> Int -> a
    debruijnNamedVar ArgName
    "x" Int
    0 ] ]
              , 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
    $ Int -> Term
    var Int
    0
              , 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 a. a -> Arg a
    defaultArg (Type -> Arg Type) -> Type -> Arg Type
    forall a b. (a -> b) -> a -> b
    $ Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Int -> Sort
    varSort Int
    2) (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    1
              , clauseCatchall :: Bool
    clauseCatchall  = Bool
    False
              , clauseExact :: Maybe Bool
    clauseExact       = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
              , clauseRecursive :: Maybe Bool
    clauseRecursive   = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
              , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
              , clauseEllipsis :: ExpandedEllipsis
    clauseEllipsis  = ExpandedEllipsis
    NoEllipsis
              }
            cc :: CompiledClauses' Term
    cc = Arg Int -> Case (CompiledClauses' Term) -> CompiledClauses' Term
    forall a.
    Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
    Case (Int -> Arg Int
    forall a. a -> Arg a
    defaultArg Int
    0) (Case (CompiledClauses' Term) -> CompiledClauses' Term)
    -> Case (CompiledClauses' Term) -> CompiledClauses' Term
    forall a b. (a -> b) -> a -> b
    $ QName
    -> Bool
    -> WithArity (CompiledClauses' Term)
    -> Case (CompiledClauses' Term)
    forall c. QName -> Bool -> WithArity c -> Case c
    conCase QName
    sharp Bool
    False (WithArity (CompiledClauses' Term) -> Case (CompiledClauses' Term))
    -> WithArity (CompiledClauses' Term)
    -> Case (CompiledClauses' Term)
    forall a b. (a -> b) -> a -> b
    $ Int -> CompiledClauses' Term -> WithArity (CompiledClauses' Term)
    forall c. Int -> c -> WithArity c
    WithArity Int
    1 (CompiledClauses' Term -> WithArity (CompiledClauses' Term))
    -> CompiledClauses' Term -> WithArity (CompiledClauses' Term)
    forall a b. (a -> b) -> a -> b
    $ [Arg ArgName] -> Term -> CompiledClauses' Term
    forall a. [Arg ArgName] -> a -> CompiledClauses' a
    Done [ArgName -> Arg ArgName
    forall a. a -> Arg a
    defaultArg ArgName
    "x"] (Term -> CompiledClauses' Term) -> Term -> CompiledClauses' Term
    forall a b. (a -> b) -> a -> b
    $ Int -> Term
    var Int
    0
            projection :: Projection
    projection = Projection :: Maybe QName -> QName -> Arg QName -> Int -> ProjLams -> Projection
    Projection
              { projProper :: Maybe QName
    projProper   = QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    inf
              , projOrig :: QName
    projOrig     = QName
    flat
              , projFromType :: Arg QName
    projFromType = QName -> Arg QName
    forall a. a -> Arg a
    defaultArg QName
    inf
              , projIndex :: Int
    projIndex    = Int
    3
              , projLams :: ProjLams
    projLams     = [Arg ArgName] -> ProjLams
    ProjLams ([Arg ArgName] -> ProjLams) -> [Arg ArgName] -> ProjLams
    forall a b. (a -> b) -> a -> b
    $ [ ArgName -> Arg ArgName
    forall a. a -> Arg a
    argH ArgName
    "a" , ArgName -> Arg ArgName
    forall a. a -> Arg a
    argH ArgName
    "A" , ArgName -> Arg ArgName
    forall a. a -> Arg a
    argN ArgName
    "x" ]
              }
        QName -> Definition -> TCM ()
    addConstant QName
    flat (Definition -> TCM ()) -> Definition -> TCM ()
    forall a b. (a -> b) -> a -> b
    $
          Definition
    flatDefn { defPolarity :: [Polarity]
    defPolarity       = []
                   , defArgOccurrences :: [Occurrence]
    defArgOccurrences = [Occurrence
    StrictPos]  -- changing that to [Mixed] destroys monotonicity of 'Rec' in test/succeed/GuardednessPreservingTypeConstructors
                   , defCopatternLHS :: Bool
    defCopatternLHS = CompiledClauses' Term -> Bool
    hasProjectionPatterns CompiledClauses' Term
    cc
                   , theDef :: Defn
    theDef = Defn
    emptyFunction
                       { funClauses :: [Clause]
    funClauses      = [Clause
    clause]
                       , funCompiled :: Maybe (CompiledClauses' Term)
    funCompiled     = CompiledClauses' Term -> Maybe (CompiledClauses' Term)
    forall a. a -> Maybe a
    Just (CompiledClauses' Term -> Maybe (CompiledClauses' Term))
    -> CompiledClauses' Term -> Maybe (CompiledClauses' Term)
    forall a b. (a -> b) -> a -> b
    $ CompiledClauses' Term
    cc
                       , funProjection :: Maybe Projection
    funProjection   = Projection -> Maybe Projection
    forall a. a -> Maybe a
    Just Projection
    projection
                       , funMutual :: Maybe [QName]
    funMutual       = [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just []
                       , funTerminates :: Maybe Bool
    funTerminates   = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True
                       }
                    }

        -- register flat as record field for constructor sharp
        (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    sharp ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Defn -> Defn) -> Definition -> Definition
    updateTheDef ((Defn -> Defn) -> Definition -> Definition)
    -> (Defn -> Defn) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ \ Defn
    def ->
          Defn
    def { conSrcCon :: ConHead
    conSrcCon = ConHead
    sharpCon }
        (Signature -> Signature) -> TCM ()
    forall (m :: * -> *).
    MonadTCState m =>
    (Signature -> Signature) -> m ()
    modifySignature ((Signature -> Signature) -> TCM ())
    -> (Signature -> Signature) -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> (Definition -> Definition) -> Signature -> Signature
    updateDefinition QName
    inf ((Definition -> Definition) -> Signature -> Signature)
    -> (Definition -> Definition) -> Signature -> Signature
    forall a b. (a -> b) -> a -> b
    $ (Defn -> Defn) -> Definition -> Definition
    updateTheDef ((Defn -> Defn) -> Definition -> Definition)
    -> (Defn -> Defn) -> Definition -> Definition
    forall a b. (a -> b) -> a -> b
    $ \ Defn
    def ->
          Defn
    def { recConHead :: ConHead
    recConHead = ConHead
    sharpCon, recFields :: [Dom QName]
    recFields = [QName -> Dom QName
    forall e. e -> Dom e
    defaultDom QName
    flat] }
        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
    $ QName -> Elims -> Term
    Def QName
    flat []

    -- The coinductive primitives.
    -- moved to TypeChecking.Monad.Builtin