| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
| 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 NominalType
- checkEnum :: EnumDecl Name -> Maybe Text -> InferM NominalType
- checkPrimType :: PrimType Name -> Maybe Text -> InferM NominalType
- checkTySyn :: TySyn Name -> Maybe Text -> InferM TySyn
- checkPropSyn :: PropSyn Name -> Maybe Text -> InferM TySyn
- checkParameterType :: ParameterType Name -> InferM ModTParam
- checkParameterConstraints :: [Located (Prop Name)] -> InferM [Located Prop]
- checkPropGuards :: [Located (Prop Name)] -> InferM [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 NominalType Source #
Check a newtype declaration.
checkPrimType :: PrimType Name -> Maybe Text -> InferM NominalType Source #
checkPropSyn :: PropSyn Name -> Maybe Text -> InferM TySyn Source #
Check a constraint-synonym declaration.
checkParameterType :: ParameterType Name -> InferM ModTParam Source #
Check a module parameter declarations. Nothing much to check, we just translate from one syntax to another.
checkPropGuards :: [Located (Prop Name)] -> InferM [Prop] Source #
Validate parsed propositions that appear in the guard of a PropGuard.
- Note that we don't validate the well-formedness constraints here---instead, they'd be validated when the signature for the auto generated function corresponding guard is checked.
- We also check that there are no wild-cards in the constraints.