Cryptol.TypeCheck.Sanity

Documentation

tcExpr :: InferInput -> Expr -> Either Error (Schema, [ProofObligation])

tcDecls :: InferInput -> [DeclGroup] -> Either Error [ProofObligation]

tcModule :: InferInput -> Module -> Either Error [ProofObligation]

type ProofObligation = Schema

data Error

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

Defined in Cryptol.TypeCheck.Sanity

Methods

showsPrec :: Int -> Error -> ShowS

show :: Error -> String

showList :: [Error] -> ShowS

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