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.InferTypes

Description

This module contains types used during type inference.

Synopsis

- data VarType
  - = ExtVar Schema
  - | CurSCC Expr Type
- 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 {
  - hasName :: !Int
  - hasGoal :: Goal
  }
- data DelayedCt = DelayedCt {
  - dctSource :: LQName
  - dctForall :: [TParam]
  - dctAsmps :: [Prop]
  - dctGoals :: [Goal]
  }
- data Solved
  - = Solved (Maybe Subst) [Goal]
  - | Unsolved
  - | Unsolvable
- data Warning
  - = DefaultingKind TParam Kind
  - | DefaultingWildType Kind
  - | DefaultingTo Doc Type
- 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 ConstraintSource
  - = CtComprehension
  - | CtSplitPat
  - | CtTypeSig
  - | CtInst Expr
  - | CtSelector
  - | CtExactType
  - | CtEnumeration
  - | CtDefaulting
  - | CtPartialTypeFun TyFunName
- data TyFunName
  - = UserTyFun QName
  - | BuiltInTyFun TFun
- cppKind :: Kind -> Doc
- addTVarsDescs :: FVS t => NameMap -> t -> Doc -> Doc
- ppUse :: Expr -> Doc

# Documentation

data VarType Source

The types of variables in the environment.

Constructors

ExtVar Schema | Known type
CurSCC Expr Type | Part of current SCC

newtype Goals Source

Constructors

Goals (TypeMap Goal) |

Instances

Show Goals Source |
TVars Goals Source |

emptyGoals :: Goals Source

nullGoals :: Goals -> Bool Source

fromGoals :: Goals -> [Goal] Source

insertGoal :: Goal -> Goals -> Goals Source

data Goal Source

Something that we need to find evidence for.

Constructors

Goal |

Fields

goalSource :: ConstraintSource

  With it is about

goalRange :: Range

  Part of source code that caused goal

goal :: Prop

  What needs to be proved

Instances

Show Goal Source |
TVars Goal Source |
FVS Goal Source |
IsFact Goal Source |
PP (WithNames Goal) Source |

data HasGoal Source

Constructors

HasGoal |

Fields

hasName :: !Int
hasGoal :: Goal

Instances

Show HasGoal Source |
TVars HasGoal Source |

data DelayedCt Source

Delayed implication constraints, arising from user-specified type sigs.

Constructors

DelayedCt |

Fields

dctSource :: LQName

  Signature that gave rise to this constraint

dctForall :: [TParam]
dctAsmps :: [Prop]
dctGoals :: [Goal]

Instances

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

data Solved Source

Constructors

Solved (Maybe Subst) [Goal] | Solved, assumeing the sub-goals.
Unsolved | We could not solved the goal.
Unsolvable | The goal can never be solved

Instances

Show Solved Source |
PP Solved 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 |

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

Information about how a constraint came to be, used in error reporting.

Constructors

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 expreesion
CtSelector |
CtExactType |
CtEnumeration |
CtDefaulting | Just defaulting on the command line
CtPartialTypeFun TyFunName | Use of a partial type function.

Instances

Show ConstraintSource Source |
PP ConstraintSource Source |
TVars ConstraintSource Source |

data TyFunName Source

Constructors

UserTyFun QName |
BuiltInTyFun TFun |

Instances

Show TyFunName Source |
PP TyFunName Source |

cppKind :: Kind -> Doc Source

For use in error messages

addTVarsDescs :: FVS t => NameMap -> t -> Doc -> Doc Source

ppUse :: Expr -> Doc Source