cryptol-2.6.0: Cryptol: The Language of Cryptography

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 String -> InferM Newtype
- checkTySyn :: TySyn Name -> Maybe String -> InferM TySyn
- checkPropSyn :: PropSyn Name -> Maybe String -> InferM TySyn
- checkParameterType :: ParameterType Name -> Maybe String -> InferM ModTParam
- checkParameterConstraints :: [Located (Prop Name)] -> InferM [Located Prop]

# Documentation

checkType :: Type Name -> Maybe Kind -> InferM Type Source #

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 String -> InferM Newtype Source #

Check a newtype declaration. XXX: Do something with constraints.

checkTySyn :: TySyn Name -> Maybe String -> InferM TySyn Source #

Check a type-synonym declaration.

checkPropSyn :: PropSyn Name -> Maybe String -> InferM TySyn Source #

Check a constraint-synonym declaration.

checkParameterType :: ParameterType Name -> Maybe String -> InferM ModTParam Source #

Check a module parameter declarations. Nothing much to check, we just translate from one syntax to another.

checkParameterConstraints :: [Located (Prop Name)] -> InferM [Located Prop] Source #