ddc-core- Disciple Core language and type checker.

Safe HaskellSafe-Infered



Type checker for witness expressions.





:: (Ord n, Pretty n) 
=> 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) => 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.

type CheckM a n = CheckM (Error a n)Source

Type checker monad. Used to manage type errors.



:: (Ord n, Pretty n) 
=> Env n

Kind environment.

-> Env n

Type environment.

-> Witness n

Witness to check.

-> CheckM a n (Type n) 

Like checkWitness but using the CheckM monad to manage errors.