Cryptol.TypeCheck

Documentation

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

tcExpr :: Expr Name -> 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 Name Schema

Variables that are in scope

inpTSyns :: Map Name TySyn

Type synonyms that are in scope

inpNewtypes :: Map Name Newtype

Newtypes in scope

inpNameSeeds :: NameSeeds

Private state of type-checker

inpMonoBinds :: Bool

Should local bindings without signatures be monomorphized?

inpSolverConfig :: SolverConfig

Options for the constraint solver

inpPrimNames :: !PrimMap

The mapping from Ident to Name, for names that the typechecker needs to refer to.

inpSupply :: !Supply

The supply for fresh name generation

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

Type inference was successful.

Instances

Show a => Show (InferOutput a)

data SolverConfig

Constructors

SolverConfig

Fields

solverPath :: FilePath

The SMT solver to invoke

solverArgs :: [String]

Additional arguments to pass to the solver

solverVerbose :: Int

How verbose to be when type-checking

Instances

Show SolverConfig

Generic SolverConfig

NFData SolverConfig

type Rep SolverConfig

data NameSeeds

This is used for generating various names.

Instances

Show NameSeeds

Generic NameSeeds

NFData NameSeeds

type Rep 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 Name Int

Type-synonym, number of extra params

TooFewTySynParams Name Int

Type-synonym, number of missing params

RepeatedTyParams [TParam Name]

Type parameters with the same name (in definition)

RepeatedDefinitions Name [Range]

Multiple definitions for the same name

RecursiveTypeDecls [Name]

The type synonym declarations are recursive

UndefinedTypeSynonym Name

Use of a type synonym that was not defined

UndefinedVariable Name

Use of a variable that was not defined

UndefinedTypeParam (Located Ident)

Attempt to explicitly instantiate a non-existent param.

MultipleTypeParamDefs Ident [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 Bool Goal

A constraint that we could not solve The boolean indicates if we know that this constraint is impossible.

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 Name [Prop]

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

TooManyPositionalTypeParams

Too many positional type arguments, in an explicit type instantiation

CannotMixPositionalAndNamedTypeParams

AmbiguousType [Name]

Instances

Show Error

Generic Error

NFData Error

PP Error

TVars Error

FVS Error

PP (WithNames Error)

type Rep Error

data Warning

Constructors

DefaultingKind (TParam Name) Kind

DefaultingWildType Kind

DefaultingTo Doc Type

Instances

Show Warning

Generic Warning

NFData Warning

PP Warning

TVars Warning

FVS Warning

PP (WithNames Warning)

type Rep Warning

ppWarning :: (Range, Warning) -> Doc

ppError :: (Range, Error) -> Doc