cryptol-2.8.0: Cryptol: The Language of Cryptography

Copyright(c) 2015-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

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 #

data Error 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 
Instances
Show Error Source # 
Instance details

Defined in Cryptol.TypeCheck.Sanity

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

same :: Same a => a -> a -> Bool Source #