    module Agda.TypeChecking.Datatypes where

    import Control.Monad        ( filterM )
    import Control.Monad.Except ( MonadError(..), ExceptT(..), runExceptT )

    import Data.Maybe (fromMaybe)

    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Pretty

    import Agda.Utils.Either
    import Agda.Utils.Pretty ( prettyShow )
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    ---------------------------------------------------------------------------
    -- * Constructors
    ---------------------------------------------------------------------------

    -- | Get true constructor with record fields.
    getConHead :: (HasConstInfo m) => QName -> m (Either SigError ConHead)
    getConHead :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError ConHead)
    getConHead QName
    c = ExceptT SigError m ConHead -> m (Either SigError ConHead)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT SigError m ConHead -> m (Either SigError ConHead))
    -> ExceptT SigError m ConHead -> m (Either SigError ConHead)
    forall a b. (a -> b) -> a -> b
    $ do
      Definition
    def <- m (Either SigError Definition) -> ExceptT SigError m Definition
    forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
    ExceptT (m (Either SigError Definition) -> ExceptT SigError m Definition)
    -> m (Either SigError Definition) -> ExceptT SigError m Definition
    forall a b. (a -> b) -> a -> b
    $ QName -> m (Either SigError Definition)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError Definition)
    getConstInfo' QName
    c
      case Definition -> Defn
    theDef Definition
    def of
        Constructor { conSrcCon :: Defn -> ConHead
    conSrcCon = ConHead
    c' } -> ConHead -> ExceptT SigError m ConHead
    forall (m :: * -> *) a. Monad m => a -> m a
    return ConHead
    c'
        Record     { recConHead :: Defn -> ConHead
    recConHead = ConHead
    c' } -> ConHead -> ExceptT SigError m ConHead
    forall (m :: * -> *) a. Monad m => a -> m a
    return ConHead
    c'
        Defn
    _ -> SigError -> ExceptT SigError m ConHead
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (SigError -> ExceptT SigError m ConHead)
    -> SigError -> ExceptT SigError m ConHead
    forall a b. (a -> b) -> a -> b
    $ [Char] -> SigError
    SigUnknown ([Char] -> SigError) -> [Char] -> SigError
    forall a b. (a -> b) -> a -> b
    $ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    c [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " is not a constructor"

    -- | Get true constructor with fields, expanding literals to constructors
    --   if possible.
    getConForm :: QName -> TCM (Either SigError ConHead)
    getConForm :: QName -> TCM (Either SigError ConHead)
    getConForm QName
    c = TCM (Either SigError ConHead)
    -> (SigError -> TCM (Either SigError ConHead))
    -> (ConHead -> TCM (Either SigError ConHead))
    -> TCM (Either SigError ConHead)
    forall (m :: * -> *) a b c.
    Monad m =>
    m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
    caseEitherM (QName -> TCM (Either SigError ConHead)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError ConHead)
    getConHead QName
    c) (Either SigError ConHead -> TCM (Either SigError ConHead)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either SigError ConHead -> TCM (Either SigError ConHead))
    -> (SigError -> Either SigError ConHead)
    -> SigError
    -> TCM (Either SigError ConHead)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SigError -> Either SigError ConHead
    forall a b. a -> Either a b
    Left) ((ConHead -> TCM (Either SigError ConHead))
     -> TCM (Either SigError ConHead))
    -> (ConHead -> TCM (Either SigError ConHead))
    -> TCM (Either SigError ConHead)
    forall a b. (a -> b) -> a -> b
    $ \ ConHead
    ch -> do
      Con ConHead
    con ConInfo
    _ [] <- Term -> TCMT IO Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm (ConHead -> ConInfo -> [Elim] -> Term
    Con ConHead
    ch ConInfo
    ConOCon [])
      Either SigError ConHead -> TCM (Either SigError ConHead)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either SigError ConHead -> TCM (Either SigError ConHead))
    -> Either SigError ConHead -> TCM (Either SigError ConHead)
    forall a b. (a -> b) -> a -> b
    $ ConHead -> Either SigError ConHead
    forall a b. b -> Either a b
    Right ConHead
    con

    -- | Augment constructor with record fields (preserve constructor name).
    --   The true constructor might only surface via 'reduce'.
    getOrigConHead :: QName -> TCM (Either SigError ConHead)
    getOrigConHead :: QName -> TCM (Either SigError ConHead)
    getOrigConHead QName
    c = (ConHead -> ConHead)
    -> Either SigError ConHead -> Either SigError ConHead
    forall b d a. (b -> d) -> Either a b -> Either a d
    mapRight (QName -> ConHead -> ConHead
    forall a. LensConName a => QName -> a -> a
    setConName QName
    c) (Either SigError ConHead -> Either SigError ConHead)
    -> TCM (Either SigError ConHead) -> TCM (Either SigError ConHead)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM (Either SigError ConHead)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError ConHead)
    getConHead QName
    c

    -- | Get the name of the datatype constructed by a given constructor.
    --   Precondition: The argument must refer to a constructor
    {-# SPECIALIZE getConstructorData :: QName -> TCM QName #-}
    getConstructorData :: HasConstInfo m => QName -> m QName
    getConstructorData :: forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getConstructorData QName
    c = do
      Definition
    def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    c
      case Definition -> Defn
    theDef Definition
    def of
        Constructor{conData :: Defn -> QName
    conData = QName
    d} -> QName -> m QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    d
        Defn
    _                        -> m QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Is the datatype of this constructor a Higher Inductive Type?
    --   Precondition: The argument must refer to a constructor of a datatype or record.
    consOfHIT :: HasConstInfo m => QName -> m Bool
    consOfHIT :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    consOfHIT QName
    c = do
      QName
    d <- QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getConstructorData QName
    c
      Defn
    def <- Definition -> Defn
    theDef (Definition -> Defn) -> m Definition -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
      case Defn
    def of
        Datatype {dataPathCons :: Defn -> [QName]
    dataPathCons = [QName]
    xs} -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [QName] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [QName]
    xs
        Record{} -> Bool -> m Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        Defn
    _  -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | @getConType c t@ computes the constructor parameters from type @t@
    --   and returns them plus the instantiated type of constructor @c@.
    --   This works also if @t@ is a function type ending in a data/record type;
    --   the term from which @c@ comes need not be fully applied
    --
    --   @Nothing@ if @t@ is not a data/record type or does not have
    --   a constructor @c@.
    getConType
      :: PureTCM m
      => ConHead  -- ^ Constructor.
      -> Type     -- ^ Ending in data/record type.
      -> m (Maybe ((QName, Type, Args), Type))
           -- ^ @Nothing@ if not ends in data or record type.
           --
           --   @Just ((d, dt, pars), ct)@ otherwise, where
           --     @d@    is the data or record type name,
           --     @dt@   is the type of the data or record name,
           --     @pars@ are the reconstructed parameters,
           --     @ct@   is the type of the constructor instantiated to the parameters.
    getConType :: forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    getConType ConHead
    c Type
    t = do
      [Char] -> VerboseLevel -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> TCMT IO Doc -> m ()
    reportSDoc [Char]
    "tc.getConType" VerboseLevel
    30 (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] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
        [ TCMT IO Doc
    "getConType: constructor "
        , ConHead -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ConHead
    c
        , TCMT IO Doc
    " at type "
        , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Type
    t
        ]
      TelV Tele (Dom Type)
    tel Type
    t <- Type -> m (TelV Type)
    forall (m :: * -> *).
    (MonadReduce m, MonadAddContext m) =>
    Type -> m (TelV Type)
    telView Type
    t
      -- Now @t@ lives under @tel@, we need to remove the dependency on @tel@.
      -- This will succeed if @t@ is indeed a data/record type that is the
      -- type of a constructor coming from a term
      -- (applied to at least the parameters).
      -- Note: @t@ will have some unbound deBruijn indices if view outside of @tel@.
      [Char] -> VerboseLevel -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> [Char] -> m ()
    reportSLn [Char]
    "tc.getConType" VerboseLevel
    35 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "  target type: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Type -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Type
    t
      Substitution' (SubstArg (Maybe ((QName, Type, Args), Type)))
    -> Maybe ((QName, Type, Args), Type)
    -> Maybe ((QName, Type, Args), Type)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Impossible -> VerboseLevel -> Substitution' Term
    forall a. Impossible -> VerboseLevel -> Substitution' a
    strengthenS Impossible
    HasCallStack => Impossible
    impossible (Tele (Dom Type) -> VerboseLevel
    forall a. Sized a => a -> VerboseLevel
    size Tele (Dom Type)
    tel)) (Maybe ((QName, Type, Args), Type)
     -> Maybe ((QName, Type, Args), Type))
    -> m (Maybe ((QName, Type, Args), Type))
    -> m (Maybe ((QName, Type, Args), Type))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        Tele (Dom Type)
    -> m (Maybe ((QName, Type, Args), Type))
    -> m (Maybe ((QName, Type, Args), Type))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Tele (Dom Type)
    tel (m (Maybe ((QName, Type, Args), Type))
     -> m (Maybe ((QName, Type, Args), Type)))
    -> m (Maybe ((QName, Type, Args), Type))
    -> m (Maybe ((QName, Type, Args), Type))
    forall a b. (a -> b) -> a -> b
    $ ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    getFullyAppliedConType ConHead
    c Type
    t
      -- Andreas, 2017-08-18, issue #2703:
      -- The original code
      --    getFullyAppliedConType c $ applySubst (strengthenS impossible (size tel)) t
      -- crashes because substitution into @Def@s is slightly too strict
      -- (see @defApp@ and @canProject@).
      -- Strengthening the parameters after the call to @getFullyAppliedConType@
      -- does not produce intermediate terms with __IMPOSSIBLE__s and this thus
      -- robust wrt. strictness/laziness of substitution.

    -- | @getFullyAppliedConType c t@ computes the constructor parameters
    --   from data type @t@ and returns them
    --   plus the instantiated type of constructor @c@.
    --
    --   @Nothing@ if @t@ is not a data/record type or does not have
    --   a constructor @c@.
    --
    --   Precondition: @t@ is reduced.
    getFullyAppliedConType
      :: PureTCM m
      => ConHead  -- ^ Constructor.
      -> Type     -- ^ Reduced type of the fully applied constructor.
      -> m (Maybe ((QName, Type, Args), Type))
           -- ^ @Nothing@ if not data or record type.
           --
           --   @Just ((d, dt, pars), ct)@ otherwise, where
           --     @d@    is the data or record type name,
           --     @dt@   is the type of the data or record name,
           --     @pars@ are the reconstructed parameters,
           --     @ct@   is the type of the constructor instantiated to the parameters.
    getFullyAppliedConType :: forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    getFullyAppliedConType ConHead
    c Type
    t = do
      [Char] -> VerboseLevel -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> [Char] -> m ()
    reportSLn [Char]
    "tc.getConType" VerboseLevel
    35 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unwords ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $
        [ [Char]
    "getFullyAppliedConType", ConHead -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow ConHead
    c, Type -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Type
    t ]
      ConHead
    c <- (SigError -> ConHead) -> Either SigError ConHead -> ConHead
    forall a b. (a -> b) -> Either a b -> b
    fromRight SigError -> ConHead
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Either SigError ConHead -> ConHead)
    -> m (Either SigError ConHead) -> m ConHead
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do QName -> m (Either SigError ConHead)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError ConHead)
    getConHead (QName -> m (Either SigError ConHead))
    -> QName -> m (Either SigError ConHead)
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    conName ConHead
    c
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
        -- Note that if we come e.g. from getConType,
        -- then the non-parameter arguments of @es@ might contain __IMPOSSIBLE__
        -- coming from strengthening.  (Thus, printing them is not safe.)
        Def QName
    d [Elim]
    es -> do
          [Char] -> VerboseLevel -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> [Char] -> m ()
    reportSLn [Char]
    "tc.getConType" VerboseLevel
    35 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unwords ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $
            [ [Char]
    "getFullyAppliedConType: case Def", QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    d, [Elim] -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [Elim]
    es ]
          Definition
    def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
          let cont :: VerboseLevel -> m (Maybe ((QName, Type, Args), Type))
    cont VerboseLevel
    n = do
                -- At this point we can be sure that the parameters are well-scoped.
                let pars :: Args
    pars = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ [Elim] -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims ([Elim] -> Maybe Args) -> [Elim] -> Maybe Args
    forall a b. (a -> b) -> a -> b
    $ VerboseLevel -> [Elim] -> [Elim]
    forall a. VerboseLevel -> [a] -> [a]
    take VerboseLevel
    n [Elim]
    es
                ((QName, Type, Args), Type) -> Maybe ((QName, Type, Args), Type)
    forall a. a -> Maybe a
    Just (((QName, Type, Args), Type) -> Maybe ((QName, Type, Args), Type))
    -> (Type -> ((QName, Type, Args), Type))
    -> Type
    -> Maybe ((QName, Type, Args), Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((QName
    d, Definition -> Type
    defType Definition
    def, Args
    pars),) (Type -> Maybe ((QName, Type, Args), Type))
    -> m Type -> m (Maybe ((QName, Type, Args), Type))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
                  (Type -> Args -> m Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    Type -> a -> m Type
    `piApplyM` Args
    pars) (Type -> m Type) -> (Definition -> Type) -> Definition -> m Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Type
    defType (Definition -> m Type) -> m Definition -> m Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ConHead -> m Definition
    forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
    getConInfo ConHead
    c
          case Definition -> Defn
    theDef Definition
    def of
            Datatype { dataPars :: Defn -> VerboseLevel
    dataPars = VerboseLevel
    n, dataCons :: Defn -> [QName]
    dataCons   = [QName]
    cs  } | ConHead -> QName
    conName ConHead
    c QName -> [QName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [QName]
    cs -> VerboseLevel -> m (Maybe ((QName, Type, Args), Type))
    cont VerboseLevel
    n
            Record   { recPars :: Defn -> VerboseLevel
    recPars  = VerboseLevel
    n, recConHead :: Defn -> ConHead
    recConHead = ConHead
    con } | ConHead
    c ConHead -> ConHead -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead
    con            -> VerboseLevel -> m (Maybe ((QName, Type, Args), Type))
    cont VerboseLevel
    n
            Defn
    _ ->  Maybe ((QName, Type, Args), Type)
    -> m (Maybe ((QName, Type, Args), Type))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe ((QName, Type, Args), Type)
    forall a. Maybe a
    Nothing
        Term
    _ -> Maybe ((QName, Type, Args), Type)
    -> m (Maybe ((QName, Type, Args), Type))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe ((QName, Type, Args), Type)
    forall a. Maybe a
    Nothing

    data ConstructorInfo
      = DataCon Nat
          -- ^ Arity.
      | RecordCon PatternOrCopattern HasEta [Dom QName]
          -- ^ List of field names.

    -- | Return the number of non-parameter arguments to a data constructor,
    --   or the field names of a record constructor.
    --
    --   For getting just the arity of constructor @c@,
    --   use @either id size <$> getConstructorArity c@.
    getConstructorInfo :: HasConstInfo m => QName -> m ConstructorInfo
    getConstructorInfo :: forall (m :: * -> *). HasConstInfo m => QName -> m ConstructorInfo
    getConstructorInfo QName
    c = do
      (Definition -> Defn
    theDef (Definition -> Defn) -> m Definition -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    c) m Defn -> (Defn -> m ConstructorInfo) -> m ConstructorInfo
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Constructor{ conData :: Defn -> QName
    conData = QName
    d, conArity :: Defn -> VerboseLevel
    conArity = VerboseLevel
    n } -> do
          (Definition -> Defn
    theDef (Definition -> Defn) -> m Definition -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d) m Defn -> (Defn -> m ConstructorInfo) -> m ConstructorInfo
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            r :: Defn
    r@Record{ recFields :: Defn -> [Dom QName]
    recFields = [Dom QName]
    fs } ->
               ConstructorInfo -> m ConstructorInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ConstructorInfo -> m ConstructorInfo)
    -> ConstructorInfo -> m ConstructorInfo
    forall a b. (a -> b) -> a -> b
    $ PatternOrCopattern -> HasEta -> [Dom QName] -> ConstructorInfo
    RecordCon (Defn -> PatternOrCopattern
    recPatternMatching Defn
    r) (Defn -> HasEta
    recEtaEquality Defn
    r) [Dom QName]
    fs
            Datatype{} ->
               ConstructorInfo -> m ConstructorInfo
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ConstructorInfo -> m ConstructorInfo)
    -> ConstructorInfo -> m ConstructorInfo
    forall a b. (a -> b) -> a -> b
    $ VerboseLevel -> ConstructorInfo
    DataCon VerboseLevel
    n
            Defn
    _ -> m ConstructorInfo
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Defn
    _ -> m ConstructorInfo
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    ---------------------------------------------------------------------------
    -- * Data types
    ---------------------------------------------------------------------------

    -- | Check if a name refers to a datatype or a record with a named constructor.
    isDatatype :: QName -> TCM Bool
    isDatatype :: QName -> TCM Bool
    isDatatype QName
    d = do
      Definition
    def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
      case Definition -> Defn
    theDef Definition
    def of
        Datatype{}                   -> Bool -> TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Record{recNamedCon :: Defn -> Bool
    recNamedCon = Bool
    namedC} -> Bool -> TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    namedC
        Defn
    _                            -> Bool -> TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    -- | Check if a name refers to a datatype or a record.
    isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
    isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
    isDataOrRecordType QName
    d = do
      (Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d) TCMT IO Defn
    -> (Defn -> TCM (Maybe DataOrRecord)) -> TCM (Maybe DataOrRecord)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Record{ PatternOrCopattern
    recPatternMatching :: PatternOrCopattern
    recPatternMatching :: Defn -> PatternOrCopattern
    recPatternMatching } -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe DataOrRecord -> TCM (Maybe DataOrRecord))
    -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
    forall a b. (a -> b) -> a -> b
    $ DataOrRecord -> Maybe DataOrRecord
    forall a. a -> Maybe a
    Just (DataOrRecord -> Maybe DataOrRecord)
    -> DataOrRecord -> Maybe DataOrRecord
    forall a b. (a -> b) -> a -> b
    $ PatternOrCopattern -> DataOrRecord
    IsRecord PatternOrCopattern
    recPatternMatching
        Datatype{} -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe DataOrRecord -> TCM (Maybe DataOrRecord))
    -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
    forall a b. (a -> b) -> a -> b
    $ DataOrRecord -> Maybe DataOrRecord
    forall a. a -> Maybe a
    Just DataOrRecord
    IsData
        Defn
    _          -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe DataOrRecord -> TCM (Maybe DataOrRecord))
    -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
    forall a b. (a -> b) -> a -> b
    $ Maybe DataOrRecord
    forall a. Maybe a
    Nothing

    -- | Precodition: 'Term' is 'reduce'd.
    isDataOrRecord :: Term -> TCM (Maybe QName)
    isDataOrRecord :: Term -> TCM (Maybe QName)
    isDataOrRecord = \case
        Def QName
    d [Elim]
    _ -> (DataOrRecord -> QName) -> Maybe DataOrRecord -> Maybe QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (QName -> DataOrRecord -> QName
    forall a b. a -> b -> a
    const QName
    d) (Maybe DataOrRecord -> Maybe QName)
    -> TCM (Maybe DataOrRecord) -> TCM (Maybe QName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM (Maybe DataOrRecord)
    isDataOrRecordType QName
    d
        Term
    _       -> Maybe QName -> TCM (Maybe QName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe QName
    forall a. Maybe a
    Nothing

    getNumberOfParameters :: HasConstInfo m => QName -> m (Maybe Nat)
    getNumberOfParameters :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe VerboseLevel)
    getNumberOfParameters QName
    d = do
      Definition
    def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
      case Definition -> Defn
    theDef Definition
    def of
        Datatype{ dataPars :: Defn -> VerboseLevel
    dataPars = VerboseLevel
    n }   -> Maybe VerboseLevel -> m (Maybe VerboseLevel)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe VerboseLevel -> m (Maybe VerboseLevel))
    -> Maybe VerboseLevel -> m (Maybe VerboseLevel)
    forall a b. (a -> b) -> a -> b
    $ VerboseLevel -> Maybe VerboseLevel
    forall a. a -> Maybe a
    Just VerboseLevel
    n
        Record{ recPars :: Defn -> VerboseLevel
    recPars = VerboseLevel
    n }      -> Maybe VerboseLevel -> m (Maybe VerboseLevel)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe VerboseLevel -> m (Maybe VerboseLevel))
    -> Maybe VerboseLevel -> m (Maybe VerboseLevel)
    forall a b. (a -> b) -> a -> b
    $ VerboseLevel -> Maybe VerboseLevel
    forall a. a -> Maybe a
    Just VerboseLevel
    n
        Constructor{ conPars :: Defn -> VerboseLevel
    conPars = VerboseLevel
    n } -> Maybe VerboseLevel -> m (Maybe VerboseLevel)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe VerboseLevel -> m (Maybe VerboseLevel))
    -> Maybe VerboseLevel -> m (Maybe VerboseLevel)
    forall a b. (a -> b) -> a -> b
    $ VerboseLevel -> Maybe VerboseLevel
    forall a. a -> Maybe a
    Just VerboseLevel
    n
        Defn
    _                          -> Maybe VerboseLevel -> m (Maybe VerboseLevel)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe VerboseLevel
    forall a. Maybe a
    Nothing

    getNotErasedConstructors :: QName -> TCM [QName]
    getNotErasedConstructors :: QName -> TCM [QName]
    getNotErasedConstructors QName
    d = do
      [QName]
    cs <- QName -> TCM [QName]
    getConstructors QName
    d
      ((QName -> TCM Bool) -> [QName] -> TCM [QName])
    -> [QName] -> (QName -> TCM Bool) -> TCM [QName]
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (QName -> TCM Bool) -> [QName] -> TCM [QName]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM [QName]
    cs ((QName -> TCM Bool) -> TCM [QName])
    -> (QName -> TCM Bool) -> TCM [QName]
    forall a b. (a -> b) -> a -> b
    $ \ QName
    c -> do
        Definition -> Bool
    forall a. LensModality a => a -> Bool
    usableModality (Definition -> Bool) -> TCMT IO Definition -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    c

    -- | Precondition: Name is a data or record type.
    getConstructors :: QName -> TCM [QName]
    getConstructors :: QName -> TCM [QName]
    getConstructors QName
    d = [QName] -> Maybe [QName] -> [QName]
    forall a. a -> Maybe a -> a
    fromMaybe [QName]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [QName] -> [QName])
    -> TCMT IO (Maybe [QName]) -> TCM [QName]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
      QName -> TCMT IO (Maybe [QName])
    getConstructors' QName
    d

    -- | 'Nothing' if not data or record type name.
    getConstructors' :: QName -> TCM (Maybe [QName])
    getConstructors' :: QName -> TCMT IO (Maybe [QName])
    getConstructors' QName
    d = Defn -> Maybe [QName]
    getConstructors_ (Defn -> Maybe [QName])
    -> (Definition -> Defn) -> Definition -> Maybe [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> Maybe [QName])
    -> TCMT IO Definition -> TCMT IO (Maybe [QName])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d

    -- | 'Nothing' if not data or record definition.
    getConstructors_ :: Defn -> Maybe [QName]
    getConstructors_ :: Defn -> Maybe [QName]
    getConstructors_ = \case
        Datatype{dataCons :: Defn -> [QName]
    dataCons = [QName]
    cs} -> [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just [QName]
    cs
        Record{recConHead :: Defn -> ConHead
    recConHead = ConHead
    h}  -> [QName] -> Maybe [QName]
    forall a. a -> Maybe a
    Just [ConHead -> QName
    conName ConHead
    h]
        Defn
    _                       -> Maybe [QName]
    forall a. Maybe a
    Nothing