Cryptol.TypeCheck.Infer

Assumes that the NoPat pass has been run.

Documentation

checkE :: Expr Name -> TypeWithSource -> 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 any of the members of the recursive group are already marked as monomorphic, then we don't do generalization. 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.

checkTopDecls :: [TopDecl Name] -> InferM ()