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

Cryptol.TypeCheck.Monad

Description

Synopsis

data LkpTyVar
- = TLocalVar TParam (Maybe Kind)
- | TOuterVar TParam
data KRW = KRW {
- typeParams :: Map Name Kind
- kCtrs :: [(ConstraintSource, [Prop])]
}
data AllowWildCards
- = AllowWildCards
- | NoWildCards
data KRO = KRO {
- lazyTParams :: Map Name TParam
- allowWild :: AllowWildCards
}
newtype KindM a = KM {
- unKM :: ReaderT KRO (StateT KRW InferM) 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]
- iSupply :: !Supply
}
data RO = RO {
- iRange :: Range
- iVars :: Map Name VarType
- iTVars :: [TParam]
- iTSyns :: Map Name (DefLoc, TySyn)
- iNewtypes :: Map Name (DefLoc, Newtype)
- iAbstractTypes :: Map Name (DefLoc, AbstractType)
- iParamTypes :: Map Name ModTParam
- iParamConstraints :: [Located Prop]
- iParamFuns :: Map Name ModVParam
- iSolvedHasLazy :: Map Int HasGoalSln
- iMonoBinds :: Bool
- iSolver :: Solver
- iPrimNames :: !PrimMap
- iSolveCounter :: !(IORef Int)
}
data DefLoc
- = IsLocal
- | IsExternal
newtype InferM a = IM {
- unIM :: ReaderT RO (StateT RW IO) a
}
data InferOutput a
- = InferFailed NameMap [(Range, Warning)] [(Range, Error)]
- | InferOK NameMap [(Range, Warning)] NameSeeds Supply a
data NameSeeds = NameSeeds {
- seedTVar :: !Int
- seedGoal :: !Int
}
data InferInput = InferInput {
- inpRange :: Range
- inpVars :: Map Name Schema
- inpTSyns :: Map Name TySyn
- inpNewtypes :: Map Name Newtype
- inpAbstractTypes :: Map Name AbstractType
- inpParamTypes :: !(Map Name ModTParam)
- inpParamConstraints :: ![Located Prop]
- inpParamFuns :: !(Map Name ModVParam)
- inpNameSeeds :: NameSeeds
- inpMonoBinds :: Bool
- inpSolverConfig :: SolverConfig
- inpSearchPath :: [FilePath]
- inpPrimNames :: !PrimMap
- inpSupply :: !Supply
}
nameSeeds :: NameSeeds
bumpCounter :: InferM ()
runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
io :: IO a -> InferM a
inRange :: Range -> InferM a -> InferM a
inRangeMb :: Maybe Range -> InferM a -> InferM a
curRange :: InferM Range
recordError :: Error -> InferM ()
recordWarning :: Warning -> InferM ()
getSolver :: InferM Solver
getPrimMap :: InferM PrimMap
newGoal :: ConstraintSource -> Prop -> InferM Goal
newGoals :: ConstraintSource -> [Prop] -> InferM ()
getGoals :: InferM [Goal]
addGoals :: [Goal] -> InferM ()
collectGoals :: InferM a -> InferM (a, [Goal])
simpGoal :: Goal -> InferM [Goal]
simpGoals :: [Goal] -> InferM [Goal]
newHasGoal :: Selector -> Type -> Type -> InferM HasGoalSln
addHasGoal :: HasGoal -> InferM ()
getHasGoals :: InferM [HasGoal]
solveHasGoal :: Int -> HasGoalSln -> InferM ()
newParamName :: Ident -> InferM Name
newName :: (NameSeeds -> (a, NameSeeds)) -> InferM a
newGoalName :: InferM Int
newTVar :: TypeSource -> Kind -> InferM TVar
newTVar' :: TypeSource -> Set TParam -> Kind -> InferM TVar
newTParam :: TParam Name -> TPFlavor -> Kind -> InferM TParam
newType :: TypeSource -> Kind -> InferM Type
unify :: TypeWithSource -> Type -> InferM [Prop]
applySubst :: TVars t => t -> InferM t
applySubstPreds :: [Prop] -> InferM [Prop]
applySubstGoals :: [Goal] -> InferM [Goal]
getSubst :: InferM Subst
extendSubst :: Subst -> InferM ()
varsWithAsmps :: InferM (Set TVar)
lookupVar :: Name -> InferM VarType
lookupTParam :: Name -> InferM (Maybe TParam)
lookupTSyn :: Name -> InferM (Maybe TySyn)
lookupNewtype :: Name -> InferM (Maybe Newtype)
lookupAbstractType :: Name -> InferM (Maybe AbstractType)
lookupParamType :: Name -> InferM (Maybe ModTParam)
lookupParamFun :: Name -> InferM (Maybe ModVParam)
existVar :: Name -> Kind -> InferM Type
getTSyns :: InferM (Map Name (DefLoc, TySyn))
getNewtypes :: InferM (Map Name (DefLoc, Newtype))
getAbstractTypes :: InferM (Map Name (DefLoc, AbstractType))
getParamFuns :: InferM (Map Name ModVParam)
getParamTypes :: InferM (Map Name ModTParam)
getParamConstraints :: InferM [Located Prop]
getTVars :: InferM (Set Name)
getBoundInScope :: InferM (Set TParam)
getMonoBinds :: InferM Bool
checkTShadowing :: String -> Name -> InferM ()
withTParam :: TParam -> InferM a -> InferM a
withTParams :: [TParam] -> InferM a -> InferM a
withTySyn :: TySyn -> InferM a -> InferM a
withNewtype :: Newtype -> InferM a -> InferM a
withPrimType :: AbstractType -> InferM a -> InferM a
withParamType :: ModTParam -> InferM a -> InferM a
withVarType :: Name -> VarType -> InferM a -> InferM a
withVarTypes :: [(Name, VarType)] -> InferM a -> InferM a
withVar :: Name -> Schema -> InferM a -> InferM a
withParamFuns :: [ModVParam] -> InferM a -> InferM a
withParameterConstraints :: [Located Prop] -> InferM a -> InferM a
withMonoType :: (Name, Located Type) -> InferM a -> InferM a
withMonoTypes :: Map Name (Located Type) -> InferM a -> InferM a
withDecls :: ([TySyn], Map Name Schema) -> InferM a -> InferM a
inNewScope :: 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 ()
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 ()
kInInferM :: InferM a -> KindM a
module Cryptol.TypeCheck.InferTypes

Documentation

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.

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 KRO Source #

Constructors

KRO
Fields lazyTParams :: Map Name TParam lazy map, with tparams. allowWild :: AllowWildCards are type-wild cards allowed?

newtype KindM a Source #

Constructors

KM
Fields unKM :: ReaderT KRO (StateT KRW InferM) a

Instances

Instances details

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

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. The Int is the "name" of the constraint, used so that we can name its solution properly.
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
iTVars :: [TParam]
Type variable that are in scope
iTSyns :: Map Name (DefLoc, TySyn)
Type synonyms that are in scope
iNewtypes :: Map Name (DefLoc, Newtype)
Newtype declarations in scope
NOTE: type synonyms take precedence over newtype. The reason is that we can define local type synonyms, but not local newtypes. So, either a type-synonym shadows a newtype, or it was declared at the top-level, but then there can't be a newtype with the same name (this should be caught by the renamer).
iAbstractTypes :: Map Name (DefLoc, AbstractType)
iParamTypes :: Map Name ModTParam
Parameter types
iParamConstraints :: [Located Prop]
Constraints on the type parameters
iParamFuns :: Map Name ModVParam
Parameter functions
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.
iSolver :: Solver
iPrimNames :: !PrimMap
iSolveCounter :: !(IORef Int)

data DefLoc Source #

Constructors

IsLocal
IsExternal

newtype InferM a Source #

Constructors

IM
Fields unIM :: ReaderT RO (StateT RW IO) a

Instances

Instances details

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

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

data NameSeeds Source #

This is used for generating various names.

Constructors

NameSeeds
Fields seedTVar :: !Int seedGoal :: !Int

Instances

Instances details

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

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
inpParamTypes :: !(Map Name ModTParam)
Type parameters
inpParamConstraints :: ![Located Prop]
Constraints on parameters
inpParamFuns :: !(Map Name ModVParam)
Value parameters
inpNameSeeds :: NameSeeds
Private state of type-checker
inpMonoBinds :: Bool
Should local bindings without signatures be monomorphized?
inpSolverConfig :: SolverConfig
Options for the constraint solver
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

Instances

Instances details

Show InferInput Source #
Instance details Defined in Cryptol.TypeCheck.Monad Methods showsPrec :: Int -> InferInput -> ShowS # show :: InferInput -> String # showList :: [InferInput] -> ShowS #

nameSeeds :: NameSeeds Source #

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

bumpCounter :: InferM () Source #

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

io :: IO a -> InferM a Source #

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

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

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

curRange :: InferM Range Source #

This is the current range that we are working on.

recordError :: Error -> InferM () Source #

Report an error.

recordWarning :: Warning -> InferM () Source #

getSolver :: InferM Solver Source #

getPrimMap :: InferM PrimMap Source #

Retrieve the mapping between identifiers and declarations in the prelude.

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

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

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

getGoals :: InferM [Goal] Source #

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

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

Add a bunch of goals that need solving.

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 #

simpGoals :: [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.

addHasGoal :: HasGoal -> InferM () Source #

Add a previously generate has constrained

getHasGoals :: InferM [HasGoal] Source #

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

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

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

newParamName :: Ident -> InferM Name Source #

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

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

newGoalName :: InferM Int Source #

Generate a new name for a goal.

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

Generate a new free type variable.

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

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

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

Generate a new free type variable.

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

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

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

Record that the two types should be syntactically equal.

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

Apply the accumulated substitution to something with free type variables.

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

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

getSubst :: InferM Subst Source #

Get the substitution that we have accumulated so far.

extendSubst :: Subst -> InferM () Source #

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

varsWithAsmps :: InferM (Set TVar) Source #

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

lookupVar :: Name -> InferM VarType Source #

Lookup the type of a variable.

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.

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

Lookup the definition of a newtype

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

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

Lookup the kind of a parameter type

lookupParamFun :: Name -> InferM (Maybe ModVParam) Source #

Lookup the schema for a parameter function.

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.

getTSyns :: InferM (Map Name (DefLoc, TySyn)) Source #

Returns the type synonyms that are currently in scope.

getNewtypes :: InferM (Map Name (DefLoc, Newtype)) Source #

Returns the newtype declarations that are in scope.

getAbstractTypes :: InferM (Map Name (DefLoc, AbstractType)) Source #

Returns the abstract type declarations that are in scope.

getParamFuns :: InferM (Map Name ModVParam) Source #

Returns the parameter functions declarations

getParamTypes :: InferM (Map Name ModTParam) Source #

Returns the abstract function declarations

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.

getBoundInScope :: InferM (Set TParam) Source #

Return the keys of the bound 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.

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

withTySyn :: TySyn -> InferM a -> InferM a Source #

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

withNewtype :: Newtype -> InferM a -> InferM a Source #

withPrimType :: AbstractType -> InferM a -> InferM a Source #

withParamType :: ModTParam -> InferM a -> InferM a 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 #

withParamFuns :: [ModVParam] -> InferM a -> InferM a Source #

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

withParameterConstraints :: [Located Prop] -> InferM a -> InferM a Source #

Add some assumptions for an entire module

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.

withDecls :: ([TySyn], Map Name Schema) -> InferM a -> InferM a Source #

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

inNewScope :: InferM a -> InferM a Source #

Perform the given computation in a new scope (i.e., the subcomputation may use existential type variables).

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.

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 #

kInInferM :: InferM a -> KindM a Source #

module Cryptol.TypeCheck.InferTypes