cryptol-2.2.2: Cryptol: The Language of Cryptography

Copyright(c) 2013-2015 Galois, Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell98

Cryptol.TypeCheck.InferTypes

Description

This module contains types used during type inference.

Synopsis

Documentation

data VarType Source

The types of variables in the environment.

Constructors

ExtVar Schema

Known type

CurSCC Expr Type

Part of current SCC

newtype Goals Source

Constructors

Goals (TypeMap Goal) 

Instances

data Goal Source

Something that we need to find evidence for.

Constructors

Goal 

Fields

goalSource :: ConstraintSource

With it is about

goalRange :: Range

Part of source code that caused goal

goal :: Prop

What needs to be proved

data HasGoal Source

Constructors

HasGoal 

Fields

hasName :: !Int
 
hasGoal :: Goal
 

data DelayedCt Source

Delayed implication constraints, arising from user-specified type sigs.

Constructors

DelayedCt 

Fields

dctSource :: LQName

Signature that gave rise to this constraint

dctForall :: [TParam]
 
dctAsmps :: [Prop]
 
dctGoals :: [Goal]
 

data Solved Source

Constructors

Solved (Maybe Subst) [Goal]

Solved, assumeing the sub-goals.

Unsolved

We could not solved the goal.

Unsolvable

The goal can never be solved

Instances

data Error Source

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] 

data ConstraintSource Source

Information about how a constraint came to be, used in error reporting.

Constructors

CtComprehension

Computing shape of list comprehension

CtSplitPat

Use of a split pattern

CtTypeSig

A type signature in a pattern or expression

CtInst Expr

Instantiation of this expreesion

CtSelector 
CtExactType 
CtEnumeration 
CtDefaulting

Just defaulting on the command line

CtPartialTypeFun TyFunName

Use of a partial type function.

cppKind :: Kind -> Doc Source

For use in error messages

addTVarsDescs :: FVS t => NameMap -> t -> Doc -> Doc Source