cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2015 Galois, Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck

Description

Synopsis

- tcModule :: Module -> InferInput -> IO (InferOutput Module)
- tcExpr :: Expr -> InferInput -> IO (InferOutput (Expr, Schema))
- tcDecls :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup])
- data InferInput = InferInput {
  - inpRange :: Range
  - inpVars :: Map QName Schema
  - inpTSyns :: Map QName TySyn
  - inpNewtypes :: Map QName Newtype
  - inpNameSeeds :: NameSeeds
  - inpMonoBinds :: Bool
  }
- data InferOutput a
  - = InferFailed [(Range, Warning)] [(Range, Error)]
  - | InferOK [(Range, Warning)] NameSeeds a
- data NameSeeds
- nameSeeds :: NameSeeds
- data Error
  - = ErrorMsg Doc
  - | KindMismatch Kind Kind
  - | TooManyTypeParams Int Kind
  - | TooManyTySynParams QName Int
  - | TooFewTySynParams QName Int
  - | RepeatedTyParams [TParam]
  - | RepeatedDefinitions QName [Range]
  - | RecursiveTypeDecls [LQName]
  - | UndefinedTypeSynonym QName
  - | UndefinedVariable QName
  - | UndefinedTypeParam QName
  - | MultipleTypeParamDefs QName [Range]
  - | TypeMismatch Type Type
  - | RecursiveType Type Type
  - | UnsolvedGoal Goal
  - | UnsolvedDelcayedCt DelayedCt
  - | UnexpectedTypeWildCard
  - | TypeVariableEscaped Type [TVar]
  - | NotForAll TVar Type
  - | UnusableFunction QName Prop
  - | TooManyPositionalTypeParams
  - | CannotMixPositionalAndNamedTypeParams
  - | AmbiguousType [QName]
- data Warning
  - = DefaultingKind TParam Kind
  - | DefaultingWildType Kind
  - | DefaultingTo Doc Type
- ppWarning :: (Range, Warning) -> Doc
- ppError :: (Range, Error) -> Doc

# Documentation

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

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

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

data InferInput Source

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 Source |

data InferOutput a Source

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) Source |

data NameSeeds Source

This is used for generating various names.

Instances

Show NameSeeds Source |

nameSeeds :: NameSeeds Source

The initial seeds, used when checking a fresh program.

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] |

Instances

Show Error Source |
PP Error Source |
TVars Error Source |
FVS Error Source |
PP (WithNames Error) Source |

data Warning Source

Constructors

DefaultingKind TParam Kind |
DefaultingWildType Kind |
DefaultingTo Doc Type |

Instances

Show Warning Source |
PP Warning Source |
TVars Warning Source |
FVS Warning Source |
PP (WithNames Warning) Source |

ppWarning :: (Range, Warning) -> Doc Source

ppError :: (Range, Error) -> Doc Source