| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Cryptol.TypeCheck.Kind
Description
Synopsis
- checkType :: Type Name -> Maybe Kind -> InferM Type
- checkSchema :: AllowWildCards -> Schema Name -> InferM (Schema, [Goal])
- checkNewtype :: Newtype Name -> Maybe Text -> InferM Newtype
- checkPrimType :: PrimType Name -> Maybe Text -> InferM AbstractType
- checkTySyn :: TySyn Name -> Maybe Text -> InferM TySyn
- checkPropSyn :: PropSyn Name -> Maybe Text -> InferM TySyn
- checkParameterType :: ParameterType Name -> Maybe Text -> InferM ModTParam
- checkParameterConstraints :: [Located (Prop Name)] -> InferM [Located Prop]
Documentation
checkSchema :: AllowWildCards -> Schema Name -> InferM (Schema, [Goal]) Source #
Check a type signature. Returns validated schema, and any implicit constraints that we inferred.
checkNewtype :: Newtype Name -> Maybe Text -> InferM Newtype Source #
Check a newtype declaration. XXX: Do something with constraints.
checkPrimType :: PrimType Name -> Maybe Text -> InferM AbstractType Source #
checkPropSyn :: PropSyn Name -> Maybe Text -> InferM TySyn Source #
Check a constraint-synonym declaration.
checkParameterType :: ParameterType Name -> Maybe Text -> InferM ModTParam Source #
Check a module parameter declarations. Nothing much to check, we just translate from one syntax to another.