    {-# OPTIONS_GHC -Wunused-imports #-}

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

    module Agda.TypeChecking.Rules.Builtin.Coinduction where

    import Prelude hiding (null)

    import Agda.Interaction.Options.Base

    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.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Rules.Builtin
    import Agda.TypeChecking.Rules.Term

    import Agda.Utils.Lens
    import Agda.Utils.Null

    -- | 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 a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    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 = BuiltinId
    -> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
    bindPostulatedName BuiltinId
    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
      _ <- 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
      return $ Def 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 =
      BuiltinId
    -> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
    bindPostulatedName BuiltinId
    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
        sharpType <- TCM Type
    typeOfSharp
        TelV fieldTel _ <- telView sharpType
        _ <- checkExpr (A.Def sharp) sharpType
        Def inf _ <- primInf
        infDefn   <- getConstInfo inf
        erasure   <- optErasure <$> pragmaOptions
        addConstant (defName infDefn) $
          infDefn { defPolarity       = [] -- not monotone
                  , defArgOccurrences = [Unused, StrictPos]
                  , theDef = Record
                      { recPars           = 2
                      , recInduction      = Just CoInductive
                      , recClause         = Nothing
                      , recConHead        = ConHead sharp (IsRecord CopatternMatching) CoInductive []  -- flat is added later
                      , recNamedCon       = True
                      , recFields         = []  -- flat is added later
                      , recTel            = fieldTel
                      , recEtaEquality'   = Inferred $ NoEta CopatternMatching
                      , recPatternMatching= CopatternMatching
                      , recMutual         = Just []
                      , recTerminates     = Just True  -- not recursive
                      , recAbstr          = ConcreteDef
                      , recComp           = emptyCompKit
                      }
                  }
        addConstant sharp $
          sharpDefn { theDef = Constructor
                        { conPars   = 2
                        , conArity  = 1
                        , conSrcCon = ConHead sharp (IsRecord CopatternMatching) CoInductive [] -- flat is added as field later
                        , conData   = defName infDefn
                        , conAbstr  = ConcreteDef
                        , conComp   = emptyCompKit
                        , conProj   = Nothing
                        , conForced = []
                        , conErased = Nothing
                        , conErasure = erasure
                        , conInline  = True  -- This might make the sharp-translation superfluous.
                        }
                    }
        return $ Def 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 =
      BuiltinId
    -> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
    bindPostulatedName BuiltinId
    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
        _ <- 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 sharp _ <- primSharp
        kit         <- requireLevels
        Def inf _   <- primInf
        let sharpCon = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
    ConHead QName
    sharp (PatternOrCopattern -> DataOrRecord
    forall p. p -> DataOrRecord' p
    IsRecord PatternOrCopattern
    CopatternMatching) Induction
    CoInductive [QName -> Arg QName
    forall a. a -> Arg a
    defaultArg QName
    flat]
            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      = 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     = 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
    noConPatternInfo { conPType = Just $ defaultArg infA
                                        , conPLazy = True }
        let 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_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar))
    forall a. a -> Arg a
    argN (Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar)))
    -> Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar))
    forall a b. (a -> b) -> a -> b
    $ Maybe NamedName -> Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
    forall name a. Maybe name -> a -> Named name a
    Named Maybe NamedName
    forall a. Maybe a
    Nothing (Pattern' DBPatVar -> Named_ (Pattern' DBPatVar))
    -> Pattern' DBPatVar -> Named_ (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_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar))
    forall a. a -> Arg a
    argN (Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar)))
    -> Named_ (Pattern' DBPatVar) -> Arg (Named_ (Pattern' DBPatVar))
    forall a b. (a -> b) -> a -> b
    $ Maybe NamedName -> Pattern' DBPatVar -> Named_ (Pattern' DBPatVar)
    forall name a. Maybe name -> a -> Named name a
    Named Maybe NamedName
    forall a. Maybe a
    Nothing (Pattern' DBPatVar -> Named_ (Pattern' DBPatVar))
    -> Pattern' DBPatVar -> Named_ (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 :: Catchall
    clauseCatchall    = Catchall
    forall a. Null a => a
    empty
              , clauseRecursive :: Maybe Bool
    clauseRecursive   = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
              , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False
              , clauseEllipsis :: ExpandedEllipsis
    clauseEllipsis    = ExpandedEllipsis
    NoEllipsis
              , clauseWhereModule :: Maybe ModuleName
    clauseWhereModule = Maybe ModuleName
    forall a. Maybe a
    Nothing
              }
            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
              { 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" ]
              }
        fun <- emptyFunctionData
        addConstant flat $
          flatDefn { defPolarity       = []
                   , defArgOccurrences = [StrictPos]  -- changing that to [Mixed] destroys monotonicity of 'Rec' in test/succeed/GuardednessPreservingTypeConstructors
                   , defCopatternLHS = hasProjectionPatterns cc
                   , theDef = FunctionDefn fun
                       { _funClauses      = [clause]
                       , _funCompiled     = Just $ cc
                       , _funProjection   = Right projection
                       , _funMutual       = Just []
                       , _funTerminates   = Just True
                       }
                    }

        -- register flat as record field for constructor sharp
        modifySignature $ updateDefinition sharp $ updateTheDef $ over lensConstructor $ \ ConstructorData
    def ->
          ConstructorData
    def { _conSrcCon = sharpCon }
        modifySignature $ updateDefinition inf $ updateTheDef $ over lensRecord $ \ RecordData
    def ->
          RecordData
    def { _recConHead = sharpCon, _recFields = [defaultDom flat] }
        return $ Def flat []

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