cryptol-2.10.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Cryptol.TypeCheck

Description

 
Synopsis

Documentation

tcModuleInst Source #

Arguments

:: Module

functor

-> Module Name 
-> InferInput

TC settings

-> IO (InferOutput Module)

new version of instance

Check a module instantiation, assuming that the functor has already been checked.

data InferInput Source #

Information needed for type inference.

Constructors

InferInput 

Fields

Instances

Instances details
Show InferInput Source # 
Instance details

Defined in Cryptol.TypeCheck.Monad

data InferOutput a Source #

The results of type inference.

Constructors

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

We found some errors

InferOK NameMap [(Range, Warning)] NameSeeds Supply a

Type inference was successful.

Instances

Instances details
Show a => Show (InferOutput a) Source # 
Instance details

Defined in Cryptol.TypeCheck.Monad

data SolverConfig Source #

Constructors

SolverConfig 

Fields

Instances

Instances details
Show SolverConfig Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

Generic SolverConfig Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

Associated Types

type Rep SolverConfig :: Type -> Type #

NFData SolverConfig Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

Methods

rnf :: SolverConfig -> () #

type Rep SolverConfig Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

type Rep SolverConfig = D1 ('MetaData "SolverConfig" "Cryptol.TypeCheck.InferTypes" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "SolverConfig" 'PrefixI 'True) ((S1 ('MetaSel ('Just "solverPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "solverArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :*: (S1 ('MetaSel ('Just "solverVerbose") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "solverPreludePath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]))))

data NameSeeds Source #

This is used for generating various names.

Instances

Instances details
Show NameSeeds Source # 
Instance details

Defined in Cryptol.TypeCheck.Monad

Generic NameSeeds Source # 
Instance details

Defined in Cryptol.TypeCheck.Monad

Associated Types

type Rep NameSeeds :: Type -> Type #

NFData NameSeeds Source # 
Instance details

Defined in Cryptol.TypeCheck.Monad

Methods

rnf :: NameSeeds -> () #

type Rep NameSeeds Source # 
Instance details

Defined in Cryptol.TypeCheck.Monad

type Rep NameSeeds = D1 ('MetaData "NameSeeds" "Cryptol.TypeCheck.Monad" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "NameSeeds" 'PrefixI 'True) (S1 ('MetaSel ('Just "seedTVar") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "seedGoal") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

nameSeeds :: NameSeeds Source #

The initial seeds, used when checking a fresh program. XXX: why does this start at 10?

data Error Source #

Various errors that might happen during type checking/inference

Constructors

KindMismatch (Maybe TypeSource) Kind Kind

Expected kind, inferred kind

TooManyTypeParams Int Kind

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

TyVarWithParams

A type variable was applied to some arguments.

TooManyTySynParams Name Int

Type-synonym, number of extra params

TooFewTyParams Name Int

Who is missing params, number of missing params

RecursiveTypeDecls [Name]

The type synonym declarations are recursive

TypeMismatch TypeSource Type Type

Expected type, inferred type

RecursiveType TypeSource Type Type

Unification results in a recursive type

UnsolvedGoals [Goal]

A constraint that we could not solve, usually because there are some left-over variables that we could not infer.

UnsolvableGoals [Goal]

A constraint that we could not solve and we know it is impossible to do it.

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 TypeSource Type [TParam]

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

NotForAll TypeSource TVar Type

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

TooManyPositionalTypeParams

Too many positional type arguments, in an explicit type instantiation

CannotMixPositionalAndNamedTypeParams 
UndefinedTypeParameter (Located Ident) 
RepeatedTypeParameter Ident [Range] 
AmbiguousSize TVarInfo (Maybe Type)

Could not determine the value of a numeric type variable, but we know it must be at least as large as the given type (or unconstrained, if Nothing).

UndefinedExistVar Name 
TypeShadowing String Name String 
MissingModTParam (Located Ident) 
MissingModVParam (Located Ident) 

Instances

Instances details
Show Error Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Methods

showsPrec :: Int -> Error -> ShowS #

show :: Error -> String #

showList :: [Error] -> ShowS #

Generic Error Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Associated Types

type Rep Error :: Type -> Type #

Methods

from :: Error -> Rep Error x #

to :: Rep Error x -> Error #

NFData Error Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Methods

rnf :: Error -> () #

PP Error Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Methods

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

FVS Error Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Methods

fvs :: Error -> Set TVar Source #

TVars Error Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Methods

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

PP (WithNames Error) Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Methods

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

type Rep Error Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

type Rep Error = D1 ('MetaData "Error" "Cryptol.TypeCheck.Error" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) ((((C1 ('MetaCons "KindMismatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe TypeSource)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind))) :+: C1 ('MetaCons "TooManyTypeParams" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind))) :+: (C1 ('MetaCons "TyVarWithParams" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TooManyTySynParams" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "TooFewTyParams" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))) :+: ((C1 ('MetaCons "RecursiveTypeDecls" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "TypeMismatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeSource) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: C1 ('MetaCons "RecursiveType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeSource) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "UnsolvedGoals" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Goal])) :+: (C1 ('MetaCons "UnsolvableGoals" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Goal])) :+: C1 ('MetaCons "UnsolvedDelayedCt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DelayedCt)))))) :+: (((C1 ('MetaCons "UnexpectedTypeWildCard" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TypeVariableEscaped" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeSource) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam]))) :+: C1 ('MetaCons "NotForAll" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeSource) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVar) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))) :+: (C1 ('MetaCons "TooManyPositionalTypeParams" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CannotMixPositionalAndNamedTypeParams" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UndefinedTypeParameter" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Ident)))))) :+: ((C1 ('MetaCons "RepeatedTypeParameter" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Range])) :+: (C1 ('MetaCons "AmbiguousSize" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVarInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Type))) :+: C1 ('MetaCons "UndefinedExistVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))) :+: (C1 ('MetaCons "TypeShadowing" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (C1 ('MetaCons "MissingModTParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Ident))) :+: C1 ('MetaCons "MissingModVParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Ident))))))))

data Warning Source #

Instances

Instances details
Show Warning Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Generic Warning Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Associated Types

type Rep Warning :: Type -> Type #

Methods

from :: Warning -> Rep Warning x #

to :: Rep Warning x -> Warning #

NFData Warning Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Methods

rnf :: Warning -> () #

PP Warning Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Methods

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

FVS Warning Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Methods

fvs :: Warning -> Set TVar Source #

TVars Warning Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

PP (WithNames Warning) Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

type Rep Warning Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

data WithNames a Source #

This packages together a type with some names to be used to display the variables. It is used for pretty printing types.

Constructors

WithNames a NameMap 

Instances

Instances details
PP (WithNames Newtype) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

PP (WithNames TySyn) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

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

PP (WithNames TVar) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

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

PP (WithNames Type) Source #

The precedence levels used by this pretty-printing instance correspond with parser non-terminals as follows:

  • 0-1: type
  • 2: infix_type
  • 3: app_type
  • 4: dimensions atype
  • 5: atype
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

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

PP (WithNames TParam) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

PP (WithNames Schema) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

PP (WithNames DeclDef) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

PP (WithNames Decl) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

PP (WithNames DeclGroup) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

PP (WithNames Match) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

PP (WithNames Expr) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

Methods

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

PP (WithNames Module) Source # 
Instance details

Defined in Cryptol.TypeCheck.AST

PP (WithNames Subst) Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

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

PP (WithNames DelayedCt) Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

PP (WithNames Goal) Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

Methods

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

PP (WithNames Error) Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Methods

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

PP (WithNames Warning) Source # 
Instance details

Defined in Cryptol.TypeCheck.Error