| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe |
| Language | Haskell98 |
Cryptol.TypeCheck
Description
- 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 = InferInput {
- inpRange :: Range
- inpVars :: Map Name Schema
- inpTSyns :: Map Name TySyn
- inpNewtypes :: Map Name Newtype
- inpNameSeeds :: NameSeeds
- inpMonoBinds :: Bool
- inpSolverConfig :: SolverConfig
- inpSearchPath :: [FilePath]
- inpPrimNames :: !PrimMap
- inpSupply :: !Supply
- data InferOutput a
- data SolverConfig = SolverConfig {
- solverPath :: FilePath
- solverArgs :: [String]
- solverVerbose :: Int
- data NameSeeds
- nameSeeds :: NameSeeds
- data Error
- = ErrorMsg Doc
- | KindMismatch Kind Kind
- | TooManyTypeParams Int Kind
- | TooManyTySynParams Name Int
- | TooFewTySynParams Name Int
- | RepeatedTyParams [TParam Name]
- | RepeatedDefinitions Name [Range]
- | RecursiveTypeDecls [Name]
- | UndefinedTypeSynonym Name
- | UndefinedVariable Name
- | UndefinedTypeParam (Located Ident)
- | MultipleTypeParamDefs Ident [Range]
- | TypeMismatch Type Type
- | RecursiveType Type Type
- | UnsolvedGoals Bool [Goal]
- | UnsolvedDelayedCt DelayedCt
- | UnexpectedTypeWildCard
- | TypeVariableEscaped Type [TVar]
- | NotForAll TVar Type
- | UnusableFunction Name [Prop]
- | TooManyPositionalTypeParams
- | CannotMixPositionalAndNamedTypeParams
- | AmbiguousType [Name]
- data Warning
- ppWarning :: (Range, Warning) -> Doc
- ppError :: (Range, Error) -> Doc
Documentation
tcModule :: Module Name -> InferInput -> IO (InferOutput Module) Source #
tcExpr :: Expr Name -> 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
| |
Instances
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
| Show a => Show (InferOutput a) Source # | |
data SolverConfig Source #
Constructors
| SolverConfig | |
Fields
| |
Instances
This is used for generating various names.
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 |
| UnsolvedGoals 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] |
Constructors
| DefaultingKind (TParam Name) Kind | |
| DefaultingWildType Kind | |
| DefaultingTo Doc Type |