| 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 |