Cryptol.TypeCheck.Solve

Documentation

simplifyAllConstraints :: InferM ()

proveImplication :: Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst

wfType :: Type -> [Prop]

Add additional constraints that ensure the validity of a type.

wfTypeFunction :: TFun -> [Type] -> [Prop]

Add additional constraints that ensure validity of type function. Note that these constraints do not introduce additional malformed types, so the well-formedness constraints are guaranteed to be well-formed. This assumes that the parameters are well-formed.

improveByDefaultingWith :: Solver -> [TVar] -> [Goal] -> IO ([TVar], [Goal], Subst, [Warning])

defaultReplExpr :: Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr))

Try to pick a reasonable instantiation for an expression, with the given type. This is useful when we do evaluation at the REPL. The resulting types should satisfy the constraints of the schema.

simpType :: Type -> Type

simpTypeMaybe :: Type -> Maybe Type