Copyright | (c) 2013-2016 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
- simplifyAllConstraints :: InferM ()
- proveImplication :: Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
- wfType :: Type -> [Prop]
- wfTypeFunction :: TFun -> [Type] -> [Prop]
- improveByDefaultingWith :: Solver -> [TVar] -> [Goal] -> IO ([TVar], [Goal], Subst, [Warning])
- defaultReplExpr :: Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr))
- simpType :: Type -> Type
- simpTypeMaybe :: Type -> Maybe Type
Documentation
wfTypeFunction :: TFun -> [Type] -> [Prop] Source
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]) Source
defaultReplExpr :: Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr)) Source
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.
simpTypeMaybe :: Type -> Maybe Type Source