Safe Haskell | None |
---|

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

:: (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.