Copyright | (c) 2015-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
Cryptol.TypeCheck.Sanity
Description
Documentation
tcExpr :: InferInput -> Expr -> Either Error (Schema, [ProofObligation]) Source #
tcDecls :: InferInput -> [DeclGroup] -> Either Error [ProofObligation] Source #
tcModule :: InferInput -> Module -> Either Error [ProofObligation] Source #
type ProofObligation = Schema Source #
Constructors
TypeMismatch String Schema Schema | expected, actual |
ExpectedMono Schema | expected a mono type, got this |
TupleSelectorOutOfRange Int Int | |
MissingField Ident [Ident] | |
UnexpectedTupleShape Int Int | |
UnexpectedRecordShape [Ident] [Ident] | |
UnexpectedSequenceShape Int Type | |
BadSelector Selector Type | |
BadInstantiation | |
Captured TVar | |
BadProofNoAbs | |
BadProofTyVars [TParam] | |
KindMismatch Kind Kind | |
NotEnoughArgumentsInKind Kind | |
BadApplication Type Type | |
FreeTypeVariable TVar | |
BadTypeApplication Kind [Kind] | |
RepeatedVariableInForall TParam | |
BadMatch Type | |
EmptyArm | |
UndefinedTypeVaraible TVar | |
UndefinedVariable Name |