Cryptol.TypeCheck.Infer

Assumes that the NoPat pass has been run.

Documentation

checkE :: Expr Name -> Type -> InferM Expr

Infer the type of an expression, and translate it to a fully elaborated core term.

checkSigB :: Bind Name -> (Schema, [Goal]) -> InferM Decl

inferModule :: Module Name -> InferM Module

inferBinds :: Bool -> Bool -> [Bind Name] -> InferM [Decl]

inferBinds isTopLevel isRec binds performs inference for a strongly-connected component of Binds. If isTopLevel is true, any bindings without type signatures will be generalized. If it is false, and the mono-binds flag is enabled, no bindings without type signatures will be generalized, but bindings with signatures will be unaffected.

inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a