cryptol-2.4.0: Cryptol: The Language of Cryptography

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

Cryptol.TypeCheck

Description

 

Synopsis

Documentation

data InferInput Source #

Information needed for type inference.

Constructors

InferInput 

Fields

data InferOutput a Source #

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

data SolverConfig Source #

Constructors

SolverConfig 

Fields

Instances

data NameSeeds Source #

This is used for generating various names.

Instances

Show NameSeeds Source # 
Generic NameSeeds Source # 

Associated Types

type Rep NameSeeds :: * -> * #

NFData NameSeeds Source # 

Methods

rnf :: NameSeeds -> () #

type Rep NameSeeds Source # 
type Rep NameSeeds = D1 (MetaData "NameSeeds" "Cryptol.TypeCheck.Monad" "cryptol-2.4.0-AtabUoGsZJn8kSvO8P84NP" False) (C1 (MetaCons "NameSeeds" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "seedTVar") NoSourceUnpackedness SourceStrict DecidedUnpack) (Rec0 Int)) (S1 (MetaSel (Just Symbol "seedGoal") NoSourceUnpackedness SourceStrict DecidedUnpack) (Rec0 Int))))

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 result (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.

UnsolvedDelayedCt 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 *) need 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 Source # 

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

Generic Error Source # 

Associated Types

type Rep Error :: * -> * #

Methods

from :: Error -> Rep Error x #

to :: Rep Error x -> Error #

NFData Error Source # 

Methods

rnf :: Error -> () #

PP Error Source # 

Methods

ppPrec :: Int -> Error -> Doc Source #

TVars Error Source # 

Methods

apSubst :: Subst -> Error -> Error Source #

FVS Error Source # 

Methods

fvs :: Error -> Set TVar Source #

PP (WithNames Error) Source # 

Methods

ppPrec :: Int -> WithNames Error -> Doc Source #

type Rep Error Source # 
type Rep Error = D1 (MetaData "Error" "Cryptol.TypeCheck.InferTypes" "cryptol-2.4.0-AtabUoGsZJn8kSvO8P84NP" False) ((:+:) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "ErrorMsg" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Doc))) (C1 (MetaCons "KindMismatch" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind))))) ((:+:) (C1 (MetaCons "TooManyTypeParams" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)))) ((:+:) (C1 (MetaCons "TooManyTySynParams" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)))) (C1 (MetaCons "TooFewTySynParams" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int))))))) ((:+:) ((:+:) (C1 (MetaCons "RepeatedTyParams" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TParam Name]))) ((:+:) (C1 (MetaCons "RepeatedDefinitions" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Range])))) (C1 (MetaCons "RecursiveTypeDecls" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]))))) ((:+:) (C1 (MetaCons "UndefinedTypeSynonym" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) ((:+:) (C1 (MetaCons "UndefinedVariable" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) (C1 (MetaCons "UndefinedTypeParam" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Located Ident)))))))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "MultipleTypeParamDefs" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Ident)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Range])))) ((:+:) (C1 (MetaCons "TypeMismatch" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)))) (C1 (MetaCons "RecursiveType" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)))))) ((:+:) (C1 (MetaCons "UnsolvedGoal" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Goal)))) ((:+:) (C1 (MetaCons "UnsolvedDelayedCt" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 DelayedCt))) (C1 (MetaCons "UnexpectedTypeWildCard" PrefixI False) U1)))) ((:+:) ((:+:) (C1 (MetaCons "TypeVariableEscaped" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TVar])))) ((:+:) (C1 (MetaCons "NotForAll" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TVar)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)))) (C1 (MetaCons "UnusableFunction" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Prop])))))) ((:+:) (C1 (MetaCons "TooManyPositionalTypeParams" PrefixI False) U1) ((:+:) (C1 (MetaCons "CannotMixPositionalAndNamedTypeParams" PrefixI False) U1) (C1 (MetaCons "AmbiguousType" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]))))))))

data Warning Source #