Cryptol.TypeCheck

Documentation

tcModule :: Module -> InferInput -> IO (InferOutput Module)

tcExpr :: Expr -> InferInput -> IO (InferOutput (Expr, Schema))

tcDecls :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup])

data InferInput

Information needed for type inference.

Constructors

InferInput

Fields

inpRange :: Range

Location of program source

inpVars :: Map QName Schema

Variables that are in scope

inpTSyns :: Map QName TySyn

Type synonyms that are in scope

inpNewtypes :: Map QName Newtype

Newtypes in scope

inpNameSeeds :: NameSeeds

Private state of type-checker

inpMonoBinds :: Bool

Should local bindings without signatures be monomorphized?

Instances

Show InferInput

data InferOutput a

The results of type inference.

Constructors

InferFailed [(Range, Warning)] [(Range, Error)]

We found some errors

InferOK [(Range, Warning)] NameSeeds a

Type inference was successful.

Instances

Show a => Show (InferOutput a)

data NameSeeds

This is used for generating various names.

Instances

Show NameSeeds

nameSeeds :: NameSeeds

The initial seeds, used when checking a fresh program.

data Error

Various errors that might happen during type checking/inference

Constructors

ErrorMsg Doc

Just say this

KindMismatch Kind Kind

Expected kind, inferred kind

TooManyTypeParams Int Kind

Number of extra parameters, kind of resut (which should not be of the form _ -> _)

TooManyTySynParams QName Int

Type-synonym, number of extra params

TooFewTySynParams QName Int

Type-synonym, number of missing params

RepeatedTyParams [TParam]

Type parameters with the same name (in definition)

RepeatedDefinitions QName [Range]

Multiple definitions for the same name

RecursiveTypeDecls [LQName]

The type synonym declarations are recursive

UndefinedTypeSynonym QName

Use of a type synonym that was not defined

UndefinedVariable QName

Use of a variable that was not defined

UndefinedTypeParam QName

Attempt to explicitly instantiate a non-existent param.

MultipleTypeParamDefs QName [Range]

Multiple definitions for the same type parameter

TypeMismatch Type Type

Expected type, inferred type

RecursiveType Type Type

Unification results in a recursive type

UnsolvedGoal Goal

A constraint that we could not solve

UnsolvedDelcayedCt DelayedCt

A constraint (with context) that we could not solve

UnexpectedTypeWildCard

Type wild cards are not allowed in this context (e.g., definitions of type synonyms).

TypeVariableEscaped Type [TVar]

Unification variable depends on quantified variables that are not in scope.

NotForAll TVar Type

Quantified type variables (of kind *) needs to match the given type, so it does not work for all types.

UnusableFunction QName Prop

The given constraint causes the signature of the function to be not-satisfiable.

TooManyPositionalTypeParams

Too many positional type arguments, in an explicit type instantiation

CannotMixPositionalAndNamedTypeParams

AmbiguousType [QName]

Instances

Show Error

PP Error

TVars Error

FVS Error

PP (WithNames Error)

data Warning

Constructors

DefaultingKind TParam Kind

DefaultingWildType Kind

DefaultingTo Doc Type

Instances

Show Warning

PP Warning

TVars Warning

FVS Warning

PP (WithNames Warning)

ppWarning :: (Range, Warning) -> Doc

ppError :: (Range, Error) -> Doc