Copyright | (c) 2013-2016 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
This module contains types used during type inference.
- data SolverConfig = SolverConfig {
- solverPath :: FilePath
- solverArgs :: [String]
- solverVerbose :: Int
- data VarType
- newtype Goals = Goals (TypeMap Goal)
- emptyGoals :: Goals
- nullGoals :: Goals -> Bool
- fromGoals :: Goals -> [Goal]
- insertGoal :: Goal -> Goals -> Goals
- data Goal = Goal {
- goalSource :: ConstraintSource
- goalRange :: Range
- goal :: Prop
- data HasGoal = HasGoal {}
- data DelayedCt = DelayedCt {}
- data Solved
- data Warning
- 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
- | UnsolvedGoal Bool Goal
- | UnsolvedDelayedCt DelayedCt
- | UnexpectedTypeWildCard
- | TypeVariableEscaped Type [TVar]
- | NotForAll TVar Type
- | UnusableFunction Name [Prop]
- | TooManyPositionalTypeParams
- | CannotMixPositionalAndNamedTypeParams
- | AmbiguousType [Name]
- data ConstraintSource
- data TyFunName
- cppKind :: Kind -> Doc
- addTVarsDescs :: FVS t => NameMap -> t -> Doc -> Doc
- ppUse :: Expr -> Doc
Documentation
data SolverConfig Source #
SolverConfig | |
|
The types of variables in the environment.
emptyGoals :: Goals Source #
Something that we need to find evidence for.
Goal | |
|
Delayed implication constraints, arising from user-specified type sigs.
Various errors that might happen during type checking/inference
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] |
data ConstraintSource Source #
Information about how a constraint came to be, used in error reporting.
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 expression |
CtSelector | |
CtExactType | |
CtEnumeration | |
CtDefaulting | Just defaulting on the command line |
CtPartialTypeFun TyFunName | Use of a partial type function. |
CtImprovement | |
CtPattern Doc | Constraints arising from type-checking patterns |