Agda.TypeChecking.Rules.Data

Datatypes

checkDataDef :: DefInfo -> QName -> [LamBinding] -> [Constructor] -> TCM ()

Type check a datatype definition. Assumes that the type has already been checked.

forceSort :: Type -> TCM Sort

Ensure that the type is a sort. If it is not directly a sort, compare it to a newSortMetaBelowInf.

checkConstructor

Arguments

:: QName

Name of data type.

-> Telescope

Parameter telescope.

-> Nat

Number of indices of the data type.

-> Sort

Sort of the data type.

-> Constructor

Constructor declaration (type signature).

-> TCM ()

Type check a constructor declaration. Checks that the constructor targets the datatype and that it fits inside the declared sort. Returns the non-linear parameters.

bindParameters :: [LamBinding] -> Type -> (Telescope -> Type -> TCM a) -> TCM a

Bind the parameters of a datatype.

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

bindParameters'

Arguments

:: [Type]

n replicas of type if LamBindings are DomainFrees that came from a DomainFull of n binders. Should be comsumed whenever a DomainFrees are consumed.

-> [LamBinding]

Bindings from definition site.

-> Type

Pi-type of bindings coming from signature site.

-> (Telescope -> Type -> TCM a)

Continuation, accepting parameter telescope and rest of type. The parameters are part of the context when the continutation is invoked.

-> TCM a

Auxiliary function for bindParameters.

fitsIn :: [IsForced] -> Type -> Sort -> TCM Int

Check that the arguments to a constructor fits inside the sort of the datatype. The first argument is the type of the constructor.

As a side effect, return the arity of the constructor.

constructs :: Int -> Type -> QName -> TCM ()

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

Check that a type constructs something of the given datatype. The first argument is the number of parameters to the datatype.

isCoinductive :: Type -> TCM (Maybe Bool)

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