E.TypeCheck

Documentation

canBeBox :: (CanType (TypeOf a), CanType a, ~ * (TypeOf (TypeOf a)) E) => a -> Bool

eAp :: E -> E -> E

inferType :: (ContextMonad m, ContextOf m ~ String) => DataTable -> [(TVr, E)] -> E -> m E

Perform a full typecheck, evaluating type terms as necessary.

infertype :: CanTypeCheck a => DataTable -> a -> E

typecheck :: (CanTypeCheck a, Monad m) => DataTable -> a -> m E

match

Arguments

:: Monad m

=> (Id -> Maybe E)

function to look up values in the environment

-> [TVr]

vars which may be substituted

-> E

pattern to match

-> E

input expression

-> m [(TVr, E)]

find substitution that will transform the left term into the right one, only substituting for the vars in the list

sortSortLike :: E -> Bool

sortKindLike :: E -> Bool

sortTermLike :: E -> Bool

sortTypeLike :: E -> Bool

typeInfer :: DataTable -> E -> E

Determine type of term using full algorithm with substitutions. This should be used instead of typ when let-bound type variables exist or you wish a more thorough checking of types.

typeInfer' :: DataTable -> [(TVr, E)] -> E -> E