    {-# OPTIONS_GHC -Wunused-imports #-}

    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.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Pretty

    import Agda.Utils.Either
    import Agda.Utils.Functor
    import Agda.Syntax.Common.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
      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 theDef def of
        Constructor { conSrcCon :: Defn -> ConHead
    conSrcCon = ConHead
    c' } -> ConHead -> ExceptT SigError m ConHead
    forall a. a -> ExceptT SigError m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ConHead
    c'
        Record     { recConHead :: Defn -> ConHead
    recConHead = ConHead
    c' } -> ConHead -> ExceptT SigError m ConHead
    forall a. a -> ExceptT SigError m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ConHead
    c'
        Defn
    _ -> SigError -> ExceptT SigError m ConHead
    forall a. SigError -> ExceptT SigError m a
    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"

    isConstructor :: (HasConstInfo m) => QName -> m Bool
    isConstructor :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isConstructor QName
    q = Either SigError ConHead -> Bool
    forall a b. Either a b -> Bool
    isRight (Either SigError ConHead -> Bool)
    -> m (Either SigError ConHead) -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Either SigError ConHead)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError ConHead)
    getConHead QName
    q

    -- | 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 a. a -> TCMT IO a
    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 con _ [] <- Term -> TCMT IO Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm (ConHead -> ConInfo -> [Elim] -> Term
    Con ConHead
    ch ConInfo
    ConOCon [])
      return $ Right 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
      def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    c
      case theDef def of
        Constructor{conData :: Defn -> QName
    conData = QName
    d} -> QName -> m QName
    forall a. a -> m a
    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
      d <- QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getConstructorData QName
    c
      def <- theDef <$> getConstInfo d
      case def of
        Datatype {dataPathCons :: Defn -> [QName]
    dataPathCons = [QName]
    xs} -> Bool -> m Bool
    forall a. a -> m a
    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 a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [QName]
    xs
        Record{} -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        Defn
    _  -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    isPathCons :: HasConstInfo m => QName -> m Bool
    isPathCons :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isPathCons QName
    c = do
      d <- QName -> m QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    getConstructorData QName
    c
      def <- theDef <$> getConstInfo d
      case def of
        Datatype {dataPathCons :: Defn -> [QName]
    dataPathCons = [QName]
    xs} -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> m Bool) -> Bool -> m Bool
    forall a b. (a -> b) -> a -> b
    $ QName
    c QName -> [QName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [QName]
    xs
        Record{} -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        Defn
    _  -> m Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | @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 ]
      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
    <$> QName -> m (Either SigError ConHead)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Either SigError ConHead)
    getConHead (ConHead -> QName
    conName ConHead
    c)
      cdef <- getConstInfo $ conName c
      let ctype = Definition -> Type
    defType Definition
    cdef
          cdata = Defn -> QName
    conData (Defn -> QName) -> Defn -> QName
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    cdef
          npars = Defn -> VerboseLevel
    conPars (Defn -> VerboseLevel) -> Defn -> VerboseLevel
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    cdef
      case unEl t of
        Def QName
    d [Elim]
    es | QName
    d QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    cdata -> 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 ]
          dt <- Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    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
          let 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
    npars [Elim]
    es
          ctPars <- ctype `piApplyM` pars
          return $ Just ((d, dt, pars), ctPars)
        Term
    _ -> Maybe ((QName, Type, Args), Type)
    -> m (Maybe ((QName, Type, Args), Type))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe ((QName, Type, Args), Type)
    forall a. Maybe a
    Nothing

    -- | Make sure a constructor is fully applied and infer the type of the constructor.
    --   Raises a type error if the constructor does not belong to the given type.
    fullyApplyCon
      :: (PureTCM m, MonadBlock m, MonadTCError m)
      => ConHead -- ^ Constructor.
      -> Elims    -- ^ Constructor arguments.
      -> Type    -- ^ Type of the constructor application.
      -> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a)
           -- ^ Name of the data/record type,
           --   type of the data/record type,
           --   reconstructed parameters,
           --   type of the constructor (applied to parameters),
           --   full application arguments,
           --   types of missing arguments (already added to context),
           --   type of the full application.
      -> m a
    fullyApplyCon :: forall (m :: * -> *) a.
    (PureTCM m, MonadBlock m, MonadTCError m) =>
    ConHead
    -> [Elim]
    -> Type
    -> (QName
        -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a)
    -> m a
    fullyApplyCon ConHead
    c [Elim]
    vs Type
    t QName -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a
    ret = ConHead
    -> [Elim]
    -> Type
    -> (QName
        -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a)
    -> (Type -> m a)
    -> m a
    forall (m :: * -> *) a.
    (PureTCM m, MonadBlock m) =>
    ConHead
    -> [Elim]
    -> Type
    -> (QName
        -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a)
    -> (Type -> m a)
    -> m a
    fullyApplyCon' ConHead
    c [Elim]
    vs Type
    t QName -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a
    ret ((Type -> m a) -> m a) -> (Type -> m a) -> m a
    forall a b. (a -> b) -> a -> b
    $
      TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> (Type -> TypeError) -> Type -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Type -> TypeError
    ConstructorDoesNotTargetGivenType (ConHead -> QName
    conName ConHead
    c)

    -- | Like @fullyApplyCon@, but calls the given fallback function if
    --   it encounters something other than a datatype.
    fullyApplyCon'
      :: (PureTCM m, MonadBlock m)
      => ConHead -- ^ Constructor.
      -> Elims    -- ^ Constructor arguments.
      -> Type    -- ^ Type of the constructor application.
      -> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a) -- ^ See @fullyApplyCon@
      -> (Type -> m a) -- ^ Fallback function
      -> m a
    fullyApplyCon' :: forall (m :: * -> *) a.
    (PureTCM m, MonadBlock m) =>
    ConHead
    -> [Elim]
    -> Type
    -> (QName
        -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a)
    -> (Type -> m a)
    -> m a
    fullyApplyCon' ConHead
    c [Elim]
    vs Type
    t0 QName -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a
    ret Type -> m a
    err = 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
    "fullyApplyCon': constructor "
        , ConHead -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
    prettyTCM ConHead
    c
        , TCMT IO Doc
    " with arguments"
        , [Elim] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => [Elim] -> m Doc
    prettyTCM [Elim]
    vs
        , TCMT IO Doc
    " at type "
        , Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t0
        ]
      (TelV tel t, boundary) <- Type -> m (TelView, Boundary)
    forall (m :: * -> *). PureTCM m => Type -> m (TelView, Boundary)
    telViewPathBoundary Type
    t0
      -- The type of the constructor application may still be a function
      -- type.  In this case, we introduce the domains @tel@ into the context
      -- and apply the constructor to these fresh variables.
      addContext tel $ do
        reportSLn "tc.getConType" 35 $ "  target type: " ++ prettyShow t
        t <- abortIfBlocked t
        getFullyAppliedConType c t >>= \case
          Maybe ((QName, Type, Args), Type)
    Nothing -> Type -> m a
    err Type
    t
          Just ((QName
    d, Type
    dt, Args
    pars), Type
    a) ->
            QName -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a
    ret QName
    d Type
    dt Args
    pars Type
    a (VerboseLevel -> [Elim] -> [Elim]
    forall a. Subst a => VerboseLevel -> a -> a
    raise (Telescope -> VerboseLevel
    forall a. Sized a => a -> VerboseLevel
    size Telescope
    tel) [Elim]
    vs [Elim] -> [Elim] -> [Elim]
    forall a. [a] -> [a] -> [a]
    ++ Telescope -> Boundary -> [Elim]
    forall a.
    DeBruijn a =>
    Telescope -> Boundary' VerboseLevel a -> [Elim' a]
    teleElims Telescope
    tel Boundary
    boundary) Telescope
    tel Type
    t

    -- | @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, MonadBlock 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, MonadBlock m) =>
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    getConType ConHead
    ch Type
    t = do
      let c :: QName
    c = ConHead -> QName
    conName ConHead
    ch
      -- Optimization: if the constructor has no parameters, there
      -- is no need to reduce the type.
      npars <- QName -> m (Maybe VerboseLevel)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe VerboseLevel)
    getNumberOfParameters QName
    c
      if | npars == Just 0 -> do
          ctype <- defType <$> getConstInfo c
          d  <- getConstructorData c
          dtype <- defType <$> getConstInfo d
          return $ Just ((d,dtype,[]),ctype)
         | otherwise -> fullyApplyCon' ch [] t
          (\QName
    d Type
    dt Args
    pars Type
    ct [Elim]
    es Telescope
    tel Type
    a -> Maybe ((QName, Type, Args), Type)
    -> m (Maybe ((QName, Type, Args), Type))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe ((QName, Type, Args), Type)
     -> m (Maybe ((QName, Type, Args), Type)))
    -> Maybe ((QName, Type, Args), Type)
    -> m (Maybe ((QName, Type, Args), Type))
    forall a b. (a -> b) -> a -> b
    $
            -- Now @dt@, @pars@, and @ct@ live under @tel@,
            -- so we need to remove the dependency on @tel@.
            let escape :: ((QName, Type, Args), Type) -> ((QName, Type, Args), Type)
    escape = Substitution' (SubstArg ((QName, Type, Args), Type))
    -> ((QName, Type, Args), Type) -> ((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 (Telescope -> VerboseLevel
    forall a. Sized a => a -> VerboseLevel
    size Telescope
    tel)) in
            ((QName, Type, Args), Type) -> Maybe ((QName, Type, Args), Type)
    forall a. a -> Maybe a
    Just (((QName, Type, Args), Type) -> Maybe ((QName, Type, Args), Type))
    -> ((QName, Type, Args), Type) -> Maybe ((QName, Type, Args), Type)
    forall a b. (a -> b) -> a -> b
    $ ((QName, Type, Args), Type) -> ((QName, Type, Args), Type)
    escape ((QName
    d, Type
    dt, Args
    pars), Type
    ct))
          (\Type
    _ -> Maybe ((QName, Type, Args), Type)
    -> m (Maybe ((QName, Type, Args), Type))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe ((QName, Type, Args), Type)
    forall a. Maybe a
    Nothing)

    data ConstructorInfo
      = DataCon Arity
          -- ^ Arity of the data constructor.
      | RecordCon PatternOrCopattern HasEta
          Arity
          -- ^ Arity of the record constructor.
          [Dom QName]
          -- ^ List of field names. Has length 'Arity'.

    -- | Return the number of non-parameter arguments to a constructor (arity).
    --   In case of record constructors, also return the field names (plus other info).
    --
    getConstructorInfo :: HasConstInfo m => QName -> m ConstructorInfo
    getConstructorInfo :: forall (m :: * -> *). HasConstInfo m => QName -> m ConstructorInfo
    getConstructorInfo QName
    c = ConstructorInfo -> Maybe ConstructorInfo -> ConstructorInfo
    forall a. a -> Maybe a -> a
    fromMaybe ConstructorInfo
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe ConstructorInfo -> ConstructorInfo)
    -> m (Maybe ConstructorInfo) -> m ConstructorInfo
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m (Maybe ConstructorInfo)
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe ConstructorInfo)
    getConstructorInfo' QName
    c

    getConstructorInfo' :: HasConstInfo m => QName -> m (Maybe ConstructorInfo)
    getConstructorInfo' :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe ConstructorInfo)
    getConstructorInfo' QName
    c = do
      QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    c m Definition -> (Definition -> Defn) -> m Defn
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> Definition -> Defn
    theDef m Defn
    -> (Defn -> m (Maybe ConstructorInfo)) -> m (Maybe ConstructorInfo)
    forall a b. m a -> (a -> m b) -> m b
    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 } -> ConstructorInfo -> Maybe ConstructorInfo
    forall a. a -> Maybe a
    Just (ConstructorInfo -> Maybe ConstructorInfo)
    -> m ConstructorInfo -> m (Maybe ConstructorInfo)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
          QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d m Definition -> (Definition -> Defn) -> m Defn
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> Definition -> Defn
    theDef m Defn -> (Defn -> ConstructorInfo) -> m ConstructorInfo
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \case
            RecordDefn (r :: RecordData
    r@RecordData{ _recFields :: RecordData -> [Dom QName]
    _recFields = [Dom QName]
    fs, _recPatternMatching :: RecordData -> PatternOrCopattern
    _recPatternMatching = PatternOrCopattern
    pat }) ->
              PatternOrCopattern
    -> HasEta -> VerboseLevel -> [Dom QName] -> ConstructorInfo
    RecordCon PatternOrCopattern
    pat (RecordData -> HasEta
    _recEtaEquality RecordData
    r) VerboseLevel
    n [Dom QName]
    fs
            DatatypeDefn DatatypeData
    _ ->
              VerboseLevel -> ConstructorInfo
    DataCon VerboseLevel
    n
            Defn
    _ -> ConstructorInfo
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        Defn
    _ -> Maybe ConstructorInfo -> m (Maybe ConstructorInfo)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe ConstructorInfo
    forall a. Maybe a
    Nothing

    ---------------------------------------------------------------------------
    -- * 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
      def <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
      case theDef def of
        Datatype{}                   -> Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Record{recNamedCon :: Defn -> Bool
    recNamedCon = Bool
    namedC} -> Bool -> TCM Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    namedC
        Defn
    _                            -> Bool -> TCM Bool
    forall a. a -> TCMT IO a
    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 a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Record{ EtaEquality
    recEtaEquality' :: EtaEquality
    recEtaEquality' :: Defn -> EtaEquality
    recEtaEquality', PatternOrCopattern
    recPatternMatching :: PatternOrCopattern
    recPatternMatching :: Defn -> PatternOrCopattern
    recPatternMatching } -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
    forall a. a -> TCMT IO a
    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
    forall p. p -> DataOrRecord' p
    IsRecord (PatternOrCopattern -> DataOrRecord)
    -> PatternOrCopattern -> DataOrRecord
    forall a b. (a -> b) -> a -> b
    $
          case PatternOrCopattern
    recPatternMatching of
            -- If the user explicitly asked for @pattern@, pattern matching is allowed.
            p :: PatternOrCopattern
    p@PatternOrCopattern
    PatternMatching -> PatternOrCopattern
    p
            -- Otherwise, 'recEtaEquality' might allow pattern matching.
            PatternOrCopattern
    CopatternMatching ->
              if EtaEquality -> Bool
    forall a. PatternMatchingAllowed a => a -> Bool
    patternMatchingAllowed EtaEquality
    recEtaEquality' then PatternOrCopattern
    PatternMatching else PatternOrCopattern
    CopatternMatching
        Datatype{} -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
    forall a. a -> TCMT IO a
    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
    forall p. DataOrRecord' p
    IsData
        Defn
    _          -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
    forall a. a -> TCMT IO a
    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, DataOrRecord))
    isDataOrRecord :: Term -> TCM (Maybe (QName, DataOrRecord))
    isDataOrRecord = \case
        Def QName
    d [Elim]
    _ -> (DataOrRecord -> (QName, DataOrRecord))
    -> Maybe DataOrRecord -> Maybe (QName, DataOrRecord)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (QName
    d,) (Maybe DataOrRecord -> Maybe (QName, DataOrRecord))
    -> TCM (Maybe DataOrRecord) -> TCM (Maybe (QName, DataOrRecord))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM (Maybe DataOrRecord)
    isDataOrRecordType QName
    d
        Term
    _       -> Maybe (QName, DataOrRecord) -> TCM (Maybe (QName, DataOrRecord))
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, DataOrRecord)
    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
      def <- QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
      case theDef def of
        Datatype{ dataPars :: Defn -> VerboseLevel
    dataPars = VerboseLevel
    n }   -> Maybe VerboseLevel -> m (Maybe VerboseLevel)
    forall a. a -> m a
    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 a. a -> m a
    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 a. a -> m a
    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 a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe VerboseLevel
    forall a. Maybe a
    Nothing

    -- | This is a simplified version of @isDatatype@ from @Coverage@,
    --   useful when we do not want to import the module.
    getDatatypeArgs :: HasConstInfo m => Type -> m (Maybe (QName, Args, Args))
    getDatatypeArgs :: forall (m :: * -> *).
    HasConstInfo m =>
    Type -> m (Maybe (QName, Args, Args))
    getDatatypeArgs Type
    t = do
      case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
        Def QName
    d [Elim]
    es -> do
          let ~(Just Args
    args) = [Elim] -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims [Elim]
    es
          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 def of
            Datatype{dataPars :: Defn -> VerboseLevel
    dataPars = VerboseLevel
    np} -> do
              let !(Args
    ps, Args
    is) = VerboseLevel -> Args -> (Args, Args)
    forall a. VerboseLevel -> [a] -> ([a], [a])
    splitAt VerboseLevel
    np Args
    args
              Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args)))
    -> Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args))
    forall a b. (a -> b) -> a -> b
    $ (QName, Args, Args) -> Maybe (QName, Args, Args)
    forall a. a -> Maybe a
    Just (QName
    d,   Args
    ps, Args
    is)
            Record{} -> do
              Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args)))
    -> Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args))
    forall a b. (a -> b) -> a -> b
    $ (QName, Args, Args) -> Maybe (QName, Args, Args)
    forall a. a -> Maybe a
    Just (QName
    d, Args
    args, [])
            Defn
    _ -> Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Args, Args)
    forall a. Maybe a
    Nothing
        Term
    _ -> Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Args, Args)
    forall a. Maybe a
    Nothing

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

    -- | 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