| Safe Haskell | None |
|---|
DDC.Core.Check.CheckWitness
Description
Type checker for witness expressions.
- checkWitness :: (Ord n, Pretty n) => DataDefs n -> Env n -> Env n -> Witness n -> Either (Error a n) (Type n)
- typeOfWitness :: (Ord n, Pretty n) => DataDefs n -> Witness n -> Either (Error a n) (Type n)
- typeOfWiCon :: WiCon n -> Type n
- typeOfWbCon :: WbCon -> Type n
- type CheckM a n = CheckM (Error a n)
- checkWitnessM :: (Ord n, Pretty n) => DataDefs n -> Env n -> Env n -> Witness n -> CheckM a n (Type n)
Documentation
Arguments
| :: (Ord n, Pretty n) | |
| => DataDefs n | Data type definitions. |
| -> Env n | Kind Environment. |
| -> Env n | Type Environment. |
| -> Witness n | Witness to check. |
| -> Either (Error a n) (Type n) |
Check a witness.
If it's good, you get a new version with types attached to all the bound variables, as well as the type of the overall witness.
If it's bad, you get a description of the error.
The returned expression has types attached to all variable occurrences,
so you can call typeOfWitness on any open subterm.
typeOfWitness :: (Ord n, Pretty n) => DataDefs n -> Witness n -> Either (Error a n) (Type n)Source
Like checkWitness, but check in an empty environment.
As this function is not given an environment, the types of free variables
must be attached directly to the bound occurrences.
This attachment is performed by checkWitness above.
typeOfWiCon :: WiCon n -> Type nSource
Take the type of a witness constructor.
typeOfWbCon :: WbCon -> Type nSource
Take the type of a builtin witness constructor.