cryptol-3.0.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe-Inferred
Language | Haskell2010

Cryptol.TypeCheck.Monad

Description

Synopsis

- data InferInput = InferInput {
  - inpRange :: Range
  - inpVars :: Map Name Schema
  - inpTSyns :: Map Name TySyn
  - inpNewtypes :: Map Name Newtype
  - inpAbstractTypes :: Map Name AbstractType
  - inpSignatures :: !(Map Name ModParamNames)
  - inpTopModules :: ModName -> Maybe (ModuleG (), IfaceG ())
  - inpTopSignatures :: ModName -> Maybe ModParamNames
  - inpParams :: !ModParamNames
  - inpNameSeeds :: NameSeeds
  - inpMonoBinds :: Bool
  - inpCallStacks :: Bool
  - inpSearchPath :: [FilePath]
  - inpPrimNames :: !PrimMap
  - inpSupply :: !Supply
  - inpSolver :: Solver
  }
- data InferOutput a
  - = InferFailed NameMap [(Range, Warning)] [(Range, Error)]
  - | InferOK NameMap [(Range, Warning)] NameSeeds Supply a
- data NameSeeds = NameSeeds {
  - seedTVar :: !Int
  - seedGoal :: !Int
  }
- newtype InferM a = IM {
  - unIM :: ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a
  }
- data RW = RW {
  - iErrors :: ![(Range, Error)]
  - iWarnings :: ![(Range, Warning)]
  - iSubst :: !Subst
  - iExistTVars :: [Map Name Type]
  - iSolvedHas :: Map Int HasGoalSln
  - iNameSeeds :: !NameSeeds
  - iCts :: !Goals
  - iHasCts :: ![[HasGoal]]
  - iScope :: ![ModuleG ScopeName]
  - iBindTypes :: !(Map Name Schema)
  - iSupply :: !Supply
  }
- data RO = RO {
  - iRange :: Range
  - iVars :: Map Name VarType
  - iTVars :: [TParam]
  - iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())
  - iExtSignatures :: ModName -> Maybe ModParamNames
  - iExtScope :: ModuleG ScopeName
  - iSolvedHasLazy :: Map Int HasGoalSln
  - iMonoBinds :: Bool
  - iCallStacks :: Bool
  - iSolver :: Solver
  - iPrimNames :: !PrimMap
  - iSolveCounter :: !(IORef Int)
  }
- data ScopeName
  - = ExternalScope
  - | LocalScope
  - | SubModule Name
  - | SignatureScope Name (Maybe Text)
  - | TopSignatureScope ModName
  - | MTopModule ModName
- newtype KindM a = KM {
  - unKM :: ReaderT KRO (StateT KRW InferM) a
  }
- data KRO = KRO {
  - lazyTParams :: Map Name TParam
  - allowWild :: AllowWildCards
  }
- data KRW = KRW {
  - typeParams :: Map Name Kind
  - kCtrs :: [(ConstraintSource, [Prop])]
  }
- data AllowWildCards
  - = AllowWildCards
  - | NoWildCards
- data LkpTyVar
  - = TLocalVar TParam (Maybe Kind)
  - | TOuterVar TParam
- inRange :: Range -> InferM a -> InferM a
- newTVar :: TypeSource -> Kind -> InferM TVar
- newName :: (NameSeeds -> (a, NameSeeds)) -> InferM a
- io :: IO a -> InferM a
- inNewScope :: InferM a -> InferM a
- getPrimMap :: InferM PrimMap
- lookupModule :: ImpName Name -> InferM (IfaceG ())
- nameSeeds :: NameSeeds
- runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
- lookupVar :: Name -> InferM VarType
- newLocalScope :: InferM ()
- endLocalScope :: InferM ([DeclGroup], Map Name TySyn)
- withTParams :: [TParam] -> InferM a -> InferM a
- unify :: TypeWithSource -> Type -> InferM [Prop]
- newGoals :: ConstraintSource -> [Prop] -> InferM ()
- newType :: TypeSource -> Kind -> InferM Type
- applySubst :: TVars t => t -> InferM t
- solveHasGoal :: Int -> HasGoalSln -> InferM ()
- newLocalName :: Namespace -> Ident -> InferM Name
- getCallStacks :: InferM Bool
- curRange :: InferM Range
- recordError :: Error -> InferM ()
- bumpCounter :: InferM ()
- selectorScope :: InferM a -> InferM a
- abortIfErrors :: InferM ()
- inRangeMb :: Maybe Range -> InferM a -> InferM a
- recordErrorLoc :: Maybe Range -> Error -> InferM ()
- recordWarning :: Warning -> InferM ()
- getSolver :: InferM Solver
- newGoal :: ConstraintSource -> Prop -> InferM Goal
- addGoals :: [Goal] -> InferM ()
- getGoals :: InferM [Goal]
- simpGoals :: [Goal] -> InferM [Goal]
- collectGoals :: InferM a -> InferM (a, [Goal])
- simpGoal :: Goal -> InferM [Goal]
- newHasGoal :: Selector -> Type -> Type -> InferM HasGoalSln
- newGoalName :: InferM Int
- addHasGoal :: HasGoal -> InferM ()
- getHasGoals :: InferM [HasGoal]
- newTVar' :: TypeSource -> Set TParam -> Kind -> InferM TVar
- getBoundInScope :: InferM (Set TParam)
- checkParamKind :: TParam -> TPFlavor -> Kind -> InferM ()
- newTParam :: TParam Name -> TPFlavor -> Kind -> InferM TParam
- freshTParam :: (Name -> TPFlavor) -> TParam -> InferM TParam
- extendSubst :: Subst -> InferM ()
- getSubst :: InferM Subst
- applySubstPreds :: [Prop] -> InferM [Prop]
- applySubstGoals :: [Goal] -> InferM [Goal]
- varsWithAsmps :: InferM (Set TVar)
- lookupTParam :: Name -> InferM (Maybe TParam)
- lookupTSyn :: Name -> InferM (Maybe TySyn)
- getTSyns :: InferM (Map Name TySyn)
- lookupNewtype :: Name -> InferM (Maybe Newtype)
- getNewtypes :: InferM (Map Name Newtype)
- lookupAbstractType :: Name -> InferM (Maybe AbstractType)
- getAbstractTypes :: InferM (Map Name AbstractType)
- lookupParamType :: Name -> InferM (Maybe ModTParam)
- getParamTypes :: InferM (Map Name ModTParam)
- lookupSignature :: ImpName Name -> InferM ModParamNames
- getSignatures :: InferM (Map Name ModParamNames)
- lookupTopModule :: ModName -> InferM (Maybe (ModuleG (), IfaceG ()))
- lookupFunctor :: ImpName Name -> InferM (ModuleG ())
- getScope :: Semigroup a => (ModuleG ScopeName -> a) -> InferM a
- getCurDecls :: InferM (ModuleG ())
- lookupModParam :: Ident -> InferM (Maybe ModParam)
- existVar :: Name -> Kind -> InferM Type
- getParamConstraints :: InferM [Located Prop]
- getTVars :: InferM (Set Name)
- getMonoBinds :: InferM Bool
- checkTShadowing :: String -> Name -> InferM ()
- withTParam :: TParam -> InferM a -> InferM a
- newScope :: ScopeName -> InferM ()
- newSignatureScope :: Name -> Maybe Text -> InferM ()
- updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
- newTopSignatureScope :: ModName -> InferM ()
- newSubmoduleScope :: Name -> Maybe Text -> ExportSpec Name -> InferM ()
- newModuleScope :: ModName -> ExportSpec Name -> InferM ()
- endSubmodule :: InferM ()
- endModule :: InferM TCTopEntity
- endSignature :: InferM ()
- endTopSignature :: InferM TCTopEntity
- addDecls :: DeclGroup -> InferM ()
- addTySyn :: TySyn -> InferM ()
- addNewtype :: Newtype -> InferM ()
- addPrimType :: AbstractType -> InferM ()
- addParamType :: ModTParam -> InferM ()
- addSignatures :: Map Name ModParamNames -> InferM ()
- addSubmodules :: Map Name (IfaceNames Name) -> InferM ()
- addFunctors :: Map Name (ModuleG Name) -> InferM ()
- addParamFun :: ModVParam -> InferM ()
- addParameterConstraints :: [Located Prop] -> InferM ()
- addModParam :: ModParam -> InferM ()
- withVarType :: Name -> VarType -> InferM a -> InferM a
- withVarTypes :: [(Name, VarType)] -> InferM a -> InferM a
- withVar :: Name -> Schema -> InferM a -> InferM a
- withMonoType :: (Name, Located Type) -> InferM a -> InferM a
- withMonoTypes :: Map Name (Located Type) -> InferM a -> InferM a
- runKindM :: AllowWildCards -> [(Name, Maybe Kind, TParam)] -> KindM a -> InferM (a, Map Name Kind, [(ConstraintSource, [Prop])])
- kLookupTyVar :: Name -> KindM (Maybe LkpTyVar)
- kWildOK :: KindM AllowWildCards
- kRecordError :: Error -> KindM ()
- kInInferM :: InferM a -> KindM a
- kRecordWarning :: Warning -> KindM ()
- kIO :: IO a -> KindM a
- kNewType :: TypeSource -> Kind -> KindM Type
- kLookupTSyn :: Name -> KindM (Maybe TySyn)
- kLookupNewtype :: Name -> KindM (Maybe Newtype)
- kLookupParamType :: Name -> KindM (Maybe ModTParam)
- kLookupAbstractType :: Name -> KindM (Maybe AbstractType)
- kExistTVar :: Name -> Kind -> KindM Type
- kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type
- kSetKind :: Name -> Kind -> KindM ()
- kInRange :: Range -> KindM a -> KindM a
- kNewGoals :: ConstraintSource -> [Prop] -> KindM ()
- module Cryptol.TypeCheck.InferTypes

# Documentation

data InferInput Source #

Information needed for type inference.

Constructors

InferInput |

Fields

- inpRange :: Range

  Location of program source

- inpVars :: Map Name Schema

  Variables that are in scope

- inpTSyns :: Map Name TySyn

  Type synonyms that are in scope

- inpNewtypes :: Map Name Newtype

  Newtypes in scope

- inpAbstractTypes :: Map Name AbstractType

  Abstract types in scope

- inpSignatures :: !(Map Name ModParamNames)

  Signatures in scope

- inpTopModules :: ModName -> Maybe (ModuleG (), IfaceG ())
- inpTopSignatures :: ModName -> Maybe ModParamNames
- inpParams :: !ModParamNames
- inpNameSeeds :: NameSeeds

  Private state of type-checker

- inpMonoBinds :: Bool

  Should local bindings without signatures be monomorphized?

- inpCallStacks :: Bool

  Are we tracking call stacks?

- inpSearchPath :: [FilePath]

  Where to look for Cryptol theory file.

- inpPrimNames :: !PrimMap

  This is used when the type-checker needs to refer to a predefined identifier (e.g., `number`).

- inpSupply :: !Supply

  The supply for fresh name generation

- inpSolver :: Solver

  Solver connection for typechecking

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 Methods showsPrec :: Int -> InferOutput a -> ShowS Source # show :: InferOutput a -> String Source # showList :: [InferOutput a] -> ShowS Source #

data NameSeeds Source #

This is used for generating various names.

Constructors

NameSeeds |

Fields

- seedTVar :: !Int
- seedGoal :: !Int

#### Instances

Instances details

Generic NameSeeds Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Associated Types type Rep NameSeeds :: Type -> Type Source # Methods from :: NameSeeds -> Rep NameSeeds x Source # to :: Rep NameSeeds x -> NameSeeds Source #
Show NameSeeds Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods showsPrec :: Int -> NameSeeds -> ShowS Source # show :: NameSeeds -> String Source # showList :: [NameSeeds] -> ShowS Source #
NFData NameSeeds Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods rnf :: NameSeeds -> () Source #
type Rep NameSeeds Source # |

Instance details

Defined in Cryptol.TypeCheck.Monad

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

newtype InferM a Source #

Constructors

IM |

Fields

- unIM :: ReaderT RO (StateT RW (ExceptionT [(Range, Error)] IO)) a

#### Instances

Instances details

MonadFail InferM Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods fail :: String -> InferM a Source #
MonadFix InferM Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods mfix :: (a -> InferM a) -> InferM a Source #
Applicative InferM Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods pure :: a -> InferM a Source # (<*>) :: InferM (a -> b) -> InferM a -> InferM b Source # liftA2 :: (a -> b -> c) -> InferM a -> InferM b -> InferM c Source # (*>) :: InferM a -> InferM b -> InferM b Source # (<*) :: InferM a -> InferM b -> InferM a Source #
Functor InferM Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods fmap :: (a -> b) -> InferM a -> InferM b Source # (<$) :: a -> InferM b -> InferM a Source #
Monad InferM Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods (>>=) :: InferM a -> (a -> InferM b) -> InferM b Source # (>>) :: InferM a -> InferM b -> InferM b Source # return :: a -> InferM a Source #
FreshM InferM Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods liftSupply :: (Supply -> (a, Supply)) -> InferM a Source #

data RW Source #

Read-write component of the monad.

Constructors

RW |

Fields

- iErrors :: ![(Range, Error)]

  Collected errors

- iWarnings :: ![(Range, Warning)]

  Collected warnings

- iSubst :: !Subst

  Accumulated substitution

- iExistTVars :: [Map Name Type]

  These keeps track of what existential type variables are available. When we start checking a function, we push a new scope for its arguments, and we pop it when we are done checking the function body. The front element of the list is the current scope, which is the only thing that will be modified, as follows. When we encounter a existential type variable: 1. we look in all scopes to see if it is already defined. 2. if it was not defined, we create a fresh type variable, and we add it to the current scope. 3. it is an error if we encounter an existential variable but we have no current scope.

- iSolvedHas :: Map Int HasGoalSln

  Selector constraints that have been solved (ref. iSolvedSelectorsLazy)

- iNameSeeds :: !NameSeeds
- iCts :: !Goals

  Ordinary constraints

- iHasCts :: ![[HasGoal]]

  Tuple/record projection constraints. These are separate from the other constraints because solving them results in actual elaboration of the term, indicating how to do the projection. The modification of the term is done using lazyness, by looking up a thunk ahead of time (`iSolvedHasLazy` in RO), which is filled in when the constrait is solved (`iSolvedHas`). See also `selectorScope`.

- iScope :: ![ModuleG ScopeName]

  Nested scopes we are currently checking, most nested first. These are basically partially built modules.

- iBindTypes :: !(Map Name Schema)

  Types of variables that we know about. We don't worry about scoping here because we assume the bindings all have different names.

- iSupply :: !Supply

data RO Source #

Read-only component of the monad.

Constructors

RO |

Fields

- iRange :: Range

  Source code being analysed

- iVars :: Map Name VarType

  Type of variable that are in scope These are only parameters vars that are in recursive component we are checking at the moment. If a var is not there, keep looking in the `iScope`

- iTVars :: [TParam]

  Type variable that are in scope

- iExtModules :: ModName -> Maybe (ModuleG (), IfaceG ())

  An exteral top-level module. We need the actual module when we instantiate functors, because currently the type-checker desugars such modules.

- iExtSignatures :: ModName -> Maybe ModParamNames

  External top-level signatures.

- iExtScope :: ModuleG ScopeName

  These are things we know about, but are not part of the modules we are currently constructing. XXX: this sould probably be an interface NOTE: External functors should be looked up in `iExtModules` and not here, as they may be top-level modules.

- iSolvedHasLazy :: Map Int HasGoalSln

  NOTE: This field is lazy in an important way! It is the final version of `iSolvedHas` in `RW`, and the two are tied together through recursion. The field is here so that we can look thing up before they are defined, which is OK because we don't need to know the results until everything is done.

- iMonoBinds :: Bool

  When this flag is set to true, bindings that lack signatures in where-blocks will never be generalized. Bindings with type signatures, and all bindings at top level are unaffected.

- iCallStacks :: Bool

  When this flag is true, retain source location information in typechecked terms

- iSolver :: Solver
- iPrimNames :: !PrimMap
- iSolveCounter :: !(IORef Int)

data ScopeName Source #

Constructors

ExternalScope |
LocalScope |
SubModule Name |
SignatureScope Name (Maybe Text) | The Text is docs
TopSignatureScope ModName |
MTopModule ModName |

newtype KindM a Source #

Constructors

KM |

Fields

- unKM :: ReaderT KRO (StateT KRW InferM) a

#### Instances

Instances details

MonadFail KindM Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods fail :: String -> KindM a Source #
Applicative KindM Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods pure :: a -> KindM a Source # (<*>) :: KindM (a -> b) -> KindM a -> KindM b Source # liftA2 :: (a -> b -> c) -> KindM a -> KindM b -> KindM c Source # (*>) :: KindM a -> KindM b -> KindM b Source # (<*) :: KindM a -> KindM b -> KindM a Source #
Functor KindM Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods fmap :: (a -> b) -> KindM a -> KindM b Source # (<$) :: a -> KindM b -> KindM a Source #
Monad KindM Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods (>>=) :: KindM a -> (a -> KindM b) -> KindM b Source # (>>) :: KindM a -> KindM b -> KindM b Source # return :: a -> KindM a Source #

data KRO Source #

Constructors

KRO |

Fields

- lazyTParams :: Map Name TParam

  lazy map, with tparams.

- allowWild :: AllowWildCards

  are type-wild cards allowed?

data KRW Source #

Constructors

KRW |

Fields

- typeParams :: Map Name Kind

  kinds of (known) vars.

- kCtrs :: [(ConstraintSource, [Prop])]

data AllowWildCards Source #

Do we allow wild cards in the given context.

Constructors

AllowWildCards |
NoWildCards |

data LkpTyVar Source #

This is what's returned when we lookup variables during kind checking.

Constructors

TLocalVar TParam (Maybe Kind) | Locally bound variable.
TOuterVar TParam | An outer binding.

inRange :: Range -> InferM a -> InferM a Source #

The monadic computation is about the given range of source code. This is useful for error reporting.

newTVar :: TypeSource -> Kind -> InferM TVar Source #

Generate a new free type variable.

newName :: (NameSeeds -> (a, NameSeeds)) -> InferM a Source #

io :: IO a -> InferM a Source #

inNewScope :: InferM a -> InferM a Source #

Perform the given computation in a new scope (i.e., the subcomputation may use existential type variables). This is a different kind of scope from the nested modules one.

getPrimMap :: InferM PrimMap Source #

Retrieve the mapping between identifiers and declarations in the prelude.

lookupModule :: ImpName Name -> InferM (IfaceG ()) Source #

Get information about the things defined in the module. Note that, in general, the interface may contain *more* than just the definitions in the module, however the `ifNames` should indicate which ones are part of the module.

nameSeeds :: NameSeeds Source #

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

runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a) Source #

lookupVar :: Name -> InferM VarType Source #

Lookup the type of a variable.

newLocalScope :: InferM () Source #

endLocalScope :: InferM ([DeclGroup], Map Name TySyn) Source #

withTParams :: [TParam] -> InferM a -> InferM a Source #

unify :: TypeWithSource -> Type -> InferM [Prop] Source #

Record that the two types should be syntactically equal.

newGoals :: ConstraintSource -> [Prop] -> InferM () Source #

Record some constraints that need to be solved. The string explains where the constraints came from.

newType :: TypeSource -> Kind -> InferM Type Source #

Generate an unknown type. The doc is a note about what is this type about.

applySubst :: TVars t => t -> InferM t Source #

Apply the accumulated substitution to something with free type variables.

solveHasGoal :: Int -> HasGoalSln -> InferM () Source #

Specify the solution (`Expr -> Expr`) for the given constraint (`Int`).

newLocalName :: Namespace -> Ident -> InferM Name Source #

Generate a fresh variable name to be used in a local binding.

getCallStacks :: InferM Bool Source #

curRange :: InferM Range Source #

This is the current range that we are working on.

recordError :: Error -> InferM () Source #

Report an error.

bumpCounter :: InferM () Source #

selectorScope :: InferM a -> InferM a Source #

This introduces a new "selector scope" which is currently a module. I think that it might be possible to have selectors scopes be groups of recursive declarations instead, as we are not going to learn anything additional once we are done with the recursive group that generated the selectors constraints. We do it at the module level because this allows us to report more errors at once.

A selector scope does the following: * Keep track of the Has constraints generated in this scope * Keep track of the solutions for discharged selector constraints: - this uses a laziness trick where we build up a map containing the solutions for the Has constraints in the state - the *final* value for this map (i.e., at the value the end of the scope) is passed in as thunk in the reader component of the moment - as we type check expressions when we need the solution for a Has constraint we look it up from the reader environment; note that since the map is not yet built up we just get back a thunk, so we have to be carefule to not force it until *after* we've solved the goals - all of this happens in the `rec` block below * At the end of a selector scope we make sure that all Has constraints were discharged. If not, we *abort* further type checking. The reason for aborting rather than just recording an error is that the expression which produce contains thunks that will lead to non-termination if forced, and some type-checking operations (e.g., instantiation a functor) require us to traverse the expressions.

abortIfErrors :: InferM () Source #

If there are any recoded errors than abort firther type-checking.

inRangeMb :: Maybe Range -> InferM a -> InferM a Source #

recordErrorLoc :: Maybe Range -> Error -> InferM () Source #

Report an error.

recordWarning :: Warning -> InferM () Source #

getSolver :: InferM Solver Source #

newGoal :: ConstraintSource -> Prop -> InferM Goal Source #

addGoals :: [Goal] -> InferM () Source #

Add a bunch of goals that need solving.

getGoals :: InferM [Goal] Source #

The constraints are removed, and returned to the caller. The substitution IS applied to them.

simpGoals :: [Goal] -> InferM [Goal] Source #

collectGoals :: InferM a -> InferM (a, [Goal]) Source #

Collect the goals emitted by the given sub-computation. Does not emit any new goals.

simpGoal :: Goal -> InferM [Goal] Source #

newHasGoal :: Selector -> Type -> Type -> InferM HasGoalSln Source #

Record a constraint that when we select from the first type, we should get a value of the second type. The returned function should be used to wrap the expression from which we are selecting (i.e., the record or tuple). Plese note that the resulting expression should not be forced before the constraint is solved.

newGoalName :: InferM Int Source #

Generate a new name for a goal.

addHasGoal :: HasGoal -> InferM () Source #

Add a previously generated `Has` constraint

getHasGoals :: InferM [HasGoal] Source #

Get the `Has` constraints. Each of this should either be solved, or added back using `addHasGoal`.

newTVar' :: TypeSource -> Set TParam -> Kind -> InferM TVar Source #

Generate a new free type variable that depends on these additional type parameters.

getBoundInScope :: InferM (Set TParam) Source #

Return the keys of the bound variables that are in scope.

checkParamKind :: TParam -> TPFlavor -> Kind -> InferM () Source #

Check that the given "flavor" of parameter is allowed to have the given type, and raise an error if not

newTParam :: TParam Name -> TPFlavor -> Kind -> InferM TParam Source #

Generate a new free type variable.

freshTParam :: (Name -> TPFlavor) -> TParam -> InferM TParam Source #

Generate a new version of a type parameter. We use this when instantiating module parameters (the "backtick" imports)

extendSubst :: Subst -> InferM () Source #

Add to the accumulated substitution, checking that the datatype invariant for `Subst` is maintained.

getSubst :: InferM Subst Source #

Get the substitution that we have accumulated so far.

applySubstPreds :: [Prop] -> InferM [Prop] Source #

applySubstGoals :: [Goal] -> InferM [Goal] Source #

varsWithAsmps :: InferM (Set TVar) Source #

Variables that are either mentioned in the environment or in a selector constraint.

lookupTParam :: Name -> InferM (Maybe TParam) Source #

Lookup a type variable. Return `Nothing` if there is no such variable in scope, in which case we must be dealing with a type constant.

lookupTSyn :: Name -> InferM (Maybe TySyn) Source #

Lookup the definition of a type synonym.

getTSyns :: InferM (Map Name TySyn) Source #

Returns the type synonyms that are currently in scope.

lookupNewtype :: Name -> InferM (Maybe Newtype) Source #

Lookup the definition of a newtype

getNewtypes :: InferM (Map Name Newtype) Source #

Returns the newtype declarations that are in scope.

lookupAbstractType :: Name -> InferM (Maybe AbstractType) Source #

getAbstractTypes :: InferM (Map Name AbstractType) Source #

Returns the abstract type declarations that are in scope.

lookupParamType :: Name -> InferM (Maybe ModTParam) Source #

Lookup the kind of a parameter type

getParamTypes :: InferM (Map Name ModTParam) Source #

Returns the abstract function declarations

lookupSignature :: ImpName Name -> InferM ModParamNames Source #

getSignatures :: InferM (Map Name ModParamNames) Source #

lookupTopModule :: ModName -> InferM (Maybe (ModuleG (), IfaceG ())) Source #

Lookup an external (i.e., previously loaded) top module.

lookupFunctor :: ImpName Name -> InferM (ModuleG ()) Source #

getScope :: Semigroup a => (ModuleG ScopeName -> a) -> InferM a Source #

Get an environment combining all nested scopes.

getCurDecls :: InferM (ModuleG ()) Source #

lookupModParam :: Ident -> InferM (Maybe ModParam) Source #

existVar :: Name -> Kind -> InferM Type Source #

Check if we already have a name for this existential type variable and, if so, return the definition. If not, try to create a new definition, if this is allowed. If not, returns nothing.

getParamConstraints :: InferM [Located Prop] Source #

Constraints on the module's parameters.

getTVars :: InferM (Set Name) Source #

Get the set of bound type variables that are in scope.

getMonoBinds :: InferM Bool Source #

Retrieve the value of the `mono-binds` option.

checkTShadowing :: String -> Name -> InferM () Source #

We disallow shadowing between type synonyms and type variables because it is confusing. As a bonus, in the implementation we don't need to worry about where we lookup things (i.e., in the variable or type synonym environment.

withTParam :: TParam -> InferM a -> InferM a Source #

The sub-computation is performed with the given type parameter in scope.

newScope :: ScopeName -> InferM () Source #

Execute the given computation in a new top scope. The sub-computation would typically be validating a module.

newSignatureScope :: Name -> Maybe Text -> InferM () Source #

updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM () Source #

Update the current scope (first in the list). Assumes there is one.

newTopSignatureScope :: ModName -> InferM () Source #

newSubmoduleScope :: Name -> Maybe Text -> ExportSpec Name -> InferM () Source #

Start a new submodule scope. The imports and exports are just used to initialize an empty module. As we type check declarations they are added to this module's scope.

newModuleScope :: ModName -> ExportSpec Name -> InferM () Source #

endSubmodule :: InferM () Source #

endModule :: InferM TCTopEntity Source #

endSignature :: InferM () Source #

endTopSignature :: InferM TCTopEntity Source #

addDecls :: DeclGroup -> InferM () Source #

addTySyn :: TySyn -> InferM () Source #

The sub-computation is performed with the given type-synonym in scope.

addNewtype :: Newtype -> InferM () Source #

addPrimType :: AbstractType -> InferM () Source #

addParamType :: ModTParam -> InferM () Source #

addSignatures :: Map Name ModParamNames -> InferM () Source #

addSubmodules :: Map Name (IfaceNames Name) -> InferM () Source #

addFunctors :: Map Name (ModuleG Name) -> InferM () Source #

addParamFun :: ModVParam -> InferM () Source #

The sub-computation is performed with the given abstract function in scope.

addParameterConstraints :: [Located Prop] -> InferM () Source #

Add some assumptions for an entire module

addModParam :: ModParam -> InferM () Source #

withVarType :: Name -> VarType -> InferM a -> InferM a Source #

The sub-computation is performed with the given variable in scope.

withVarTypes :: [(Name, VarType)] -> InferM a -> InferM a Source #

withVar :: Name -> Schema -> InferM a -> InferM a Source #

withMonoType :: (Name, Located Type) -> InferM a -> InferM a Source #

The sub-computation is performed with the given variables in scope.

withMonoTypes :: Map Name (Located Type) -> InferM a -> InferM a Source #

The sub-computation is performed with the given variables in scope.

runKindM Source #

Arguments

:: AllowWildCards |
-> [(Name, Maybe Kind, TParam)] | See comment
-> KindM a |
-> InferM (a, Map Name Kind, [(ConstraintSource, [Prop])]) |

The arguments to this function are as follows:

(type param. name, kind signature (opt.), type parameter)

The type parameter is just a thunk that we should not force. The reason is that the parameter depends on the kind that we are in the process of computing.

As a result we return the value of the sub-computation and the computed kinds of the type parameters.

kLookupTyVar :: Name -> KindM (Maybe LkpTyVar) Source #

Check if a name refers to a type variable.

kWildOK :: KindM AllowWildCards Source #

Are type wild-cards OK in this context?

kRecordError :: Error -> KindM () Source #

Reports an error.

kInInferM :: InferM a -> KindM a Source #

kRecordWarning :: Warning -> KindM () Source #

kIO :: IO a -> KindM a Source #

kNewType :: TypeSource -> Kind -> KindM Type Source #

Generate a fresh unification variable of the given kind. NOTE: We do not simplify these, because we end up with bottom. See `hs` XXX: Perhaps we can avoid the recursion?

kLookupTSyn :: Name -> KindM (Maybe TySyn) Source #

Lookup the definition of a type synonym.

kLookupNewtype :: Name -> KindM (Maybe Newtype) Source #

Lookup the definition of a newtype.

kLookupParamType :: Name -> KindM (Maybe ModTParam) Source #

kLookupAbstractType :: Name -> KindM (Maybe AbstractType) Source #

kExistTVar :: Name -> Kind -> KindM Type Source #

kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type Source #

Replace the given bound variables with concrete types.

kSetKind :: Name -> Kind -> KindM () Source #

Record the kind for a local type variable. This assumes that we already checked that there was no other valid kind for the variable (if there was one, it gets over-written).

kInRange :: Range -> KindM a -> KindM a Source #

The sub-computation is about the given range of the source code.

kNewGoals :: ConstraintSource -> [Prop] -> KindM () Source #

module Cryptol.TypeCheck.InferTypes