Safe Haskell	Safe
Language	Haskell2010

Cryptol.TypeCheck.Type

Synopsis

class FVS t where
- fvs :: t -> Set TVar
type SType = Type
data AbstractType = AbstractType {
- atName :: Name
- atKind :: Kind
- atCtrs :: ([TParam], [Prop])
- atFixitiy :: Maybe Fixity
- atDoc :: Maybe String
}
data Newtype = Newtype {
- ntName :: Name
- ntParams :: [TParam]
- ntConstraints :: [Prop]
- ntFields :: [(Ident, Type)]
- ntDoc :: Maybe String
}
data TySyn = TySyn {
- tsName :: Name
- tsParams :: [TParam]
- tsConstraints :: [Prop]
- tsDef :: Type
- tsDoc :: !(Maybe String)
}
type Prop = Type
data TVarSource
- = TVFromModParam Name
- | TVFromSignature Name
- | TypeWildCard
- | TypeOfRecordField Ident
- | TypeOfTupleField Int
- | TypeOfSeqElement
- | LenOfSeq
- | TypeParamInstNamed Name Ident
- | TypeParamInstPos Name Int
- | DefinitionOf Name
- | LenOfCompGen
- | TypeOfArg (Maybe Int)
- | TypeOfRes
- | TypeErrorPlaceHolder
data TVarInfo = TVarInfo {
- tvarSource :: Range
- tvarDesc :: TVarSource
}
data TVar
- = TVFree !Int Kind (Set TParam) TVarInfo
- | TVBound !TParam
data Type
- = TCon !TCon ![Type]
- | TVar TVar
- | TUser !Name ![Type] !Type
- | TRec ![(Ident, Type)]
data TPFlavor
- = TPModParam Name
- | TPOther (Maybe Name)
data TParam = TParam {
- tpUnique :: !Int
- tpKind :: Kind
- tpFlav :: TPFlavor
- tpInfo :: !TVarInfo
}
data Schema = Forall {
- sVars :: [TParam]
- sProps :: [Prop]
- sType :: Type
}
tMono :: Type -> Schema
isMono :: Schema -> Maybe Type
schemaParam :: Name -> TPFlavor
tySynParam :: Name -> TPFlavor
propSynParam :: Name -> TPFlavor
newtypeParam :: Name -> TPFlavor
modTyParam :: Name -> TPFlavor
tpfName :: TPFlavor -> Maybe Name
tpName :: TParam -> Maybe Name
tvInfo :: TVar -> TVarInfo
tvSourceName :: TVarSource -> Maybe Name
quickApply :: Kind -> [a] -> Kind
kindResult :: Kind -> Kind
tpVar :: TParam -> TVar
newtypeConType :: Newtype -> Schema
abstractTypeTC :: AbstractType -> TCon
isFreeTV :: TVar -> Bool
isBoundTV :: TVar -> Bool
tIsError :: Type -> Maybe TCErrorMessage
tIsNat' :: Type -> Maybe Nat'
tIsNum :: Type -> Maybe Integer
tIsInf :: Type -> Bool
tIsVar :: Type -> Maybe TVar
tIsFun :: Type -> Maybe (Type, Type)
tIsSeq :: Type -> Maybe (Type, Type)
tIsBit :: Type -> Bool
tIsInteger :: Type -> Bool
tIsIntMod :: Type -> Maybe Type
tIsTuple :: Type -> Maybe [Type]
tIsRec :: Type -> Maybe [(Ident, Type)]
tIsBinFun :: TFun -> Type -> Maybe (Type, Type)
tSplitFun :: TFun -> Type -> [Type]
pIsFin :: Prop -> Maybe Type
pIsGeq :: Prop -> Maybe (Type, Type)
pIsEq :: Prop -> Maybe (Type, Type)
pIsZero :: Prop -> Maybe Type
pIsLogic :: Prop -> Maybe Type
pIsArith :: Prop -> Maybe Type
pIsCmp :: Prop -> Maybe Type
pIsSignedCmp :: Prop -> Maybe Type
pIsLiteral :: Prop -> Maybe (Type, Type)
pIsTrue :: Prop -> Bool
pIsWidth :: Prop -> Maybe Type
tNum :: Integral a => a -> Type
tZero :: Type
tOne :: Type
tTwo :: Type
tInf :: Type
tNat' :: Nat' -> Type
tAbstract :: UserTC -> [Type] -> Type
tBit :: Type
tInteger :: Type
tIntMod :: Type -> Type
tWord :: Type -> Type
tSeq :: Type -> Type -> Type
tChar :: Type
tString :: Int -> Type
tRec :: [(Ident, Type)] -> Type
tTuple :: [Type] -> Type
newtypeTyCon :: Newtype -> TCon
tFun :: Type -> Type -> Type
tNoUser :: Type -> Type
tBadNumber :: TCErrorMessage -> Type
tError :: Kind -> TCErrorMessage -> Type
tf1 :: TFun -> Type -> Type
tf2 :: TFun -> Type -> Type -> Type
tf3 :: TFun -> Type -> Type -> Type -> Type
tSub :: Type -> Type -> Type
tMul :: Type -> Type -> Type
tDiv :: Type -> Type -> Type
tMod :: Type -> Type -> Type
tExp :: Type -> Type -> Type
tMin :: Type -> Type -> Type
tCeilDiv :: Type -> Type -> Type
tCeilMod :: Type -> Type -> Type
tLenFromThenTo :: Type -> Type -> Type -> Type
(=#=) :: Type -> Type -> Prop
(=/=) :: Type -> Type -> Prop
pZero :: Type -> Prop
pLogic :: Type -> Prop
pArith :: Type -> Prop
pCmp :: Type -> Prop
pSignedCmp :: Type -> Prop
pLiteral :: Type -> Type -> Prop
(>==) :: Type -> Type -> Prop
pHas :: Selector -> Type -> Type -> Prop
pTrue :: Prop
pAnd :: [Prop] -> Prop
pSplitAnd :: Prop -> [Prop]
pFin :: Type -> Prop
pError :: TCErrorMessage -> Prop
noFreeVariables :: FVS t => t -> Bool
addTNames :: [TParam] -> NameMap -> NameMap
ppNewtypeShort :: Newtype -> Doc
pickTVarName :: Kind -> TVarSource -> Int -> Doc
module Cryptol.TypeCheck.TCon

Documentation

class FVS t where Source #

Methods

fvs :: t -> Set TVar Source #

Instances

Instances details

FVS Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Type -> Set TVar Source #
FVS Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Schema -> Set TVar Source #
FVS DelayedCt Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods fvs :: DelayedCt -> Set TVar Source #
FVS Goal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods fvs :: Goal -> Set TVar Source #
FVS Error Source #
Instance details Defined in Cryptol.TypeCheck.Error Methods fvs :: Error -> Set TVar Source #
FVS Warning Source #
Instance details Defined in Cryptol.TypeCheck.Error Methods fvs :: Warning -> Set TVar Source #
FVS a => FVS [a] Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: [a] -> Set TVar Source #
FVS a => FVS (Maybe a) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Maybe a -> Set TVar Source #
(FVS a, FVS b) => FVS (a, b) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: (a, b) -> Set TVar Source #

type SType = Type Source #

The type is "simple" (i.e., it contains no type functions).

data AbstractType Source #

Information about an abstract type.

Constructors

AbstractType
Fields atName :: Name atKind :: Kind atCtrs :: ([TParam], [Prop]) atFixitiy :: Maybe Fixity atDoc :: Maybe String

Instances

Instances details

Show AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> AbstractType -> ShowS show :: AbstractType -> String showList :: [AbstractType] -> ShowS
Generic AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep AbstractType :: Type -> Type Methods from :: AbstractType -> Rep AbstractType x to :: Rep AbstractType x -> AbstractType
NFData AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: AbstractType -> ()
type Rep AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep AbstractType = D1 ('MetaData "AbstractType" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-jyTxkWAqoKLO0ZfM89b4u" 'False) (C1 ('MetaCons "AbstractType" 'PrefixI 'True) ((S1 ('MetaSel ('Just "atName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Just "atKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :: (S1 ('MetaSel ('Just "atCtrs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ([TParam], [Prop])) :: (S1 ('MetaSel ('Just "atFixitiy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity)) :: S1 ('MetaSel ('Just "atDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String))))))

data Newtype Source #

Named records

Constructors

Newtype
Fields ntName :: Name ntParams :: [TParam] ntConstraints :: [Prop] ntFields :: [(Ident, Type)] ntDoc :: Maybe String

Instances

Instances details

Show Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Newtype -> ShowS show :: Newtype -> String showList :: [Newtype] -> ShowS
Generic Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep Newtype :: Type -> Type Methods from :: Newtype -> Rep Newtype x to :: Rep Newtype x -> Newtype
NFData Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Newtype -> ()
PP Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Newtype -> Doc Source #
HasKind Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: Newtype -> Kind Source #
FreeVars Newtype Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Newtype -> Deps Source #
PP (WithNames Newtype) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames Newtype -> Doc Source #
type Rep Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep Newtype = D1 ('MetaData "Newtype" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-jyTxkWAqoKLO0ZfM89b4u" 'False) (C1 ('MetaCons "Newtype" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ntName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Just "ntParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam])) :: (S1 ('MetaSel ('Just "ntConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop]) :: (S1 ('MetaSel ('Just "ntFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Ident, Type)]) :: S1 ('MetaSel ('Just "ntDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String))))))

data TySyn Source #

Type synonym.

Constructors

TySyn
Fields tsName :: Name Name tsParams :: [TParam] Parameters tsConstraints :: [Prop] Ensure body is OK tsDef :: Type Definition tsDoc :: !(Maybe String) Documentation

Instances

Instances details

Show TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TySyn -> ShowS show :: TySyn -> String showList :: [TySyn] -> ShowS
Generic TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TySyn :: Type -> Type Methods from :: TySyn -> Rep TySyn x to :: Rep TySyn x -> TySyn
NFData TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TySyn -> ()
PP TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TySyn -> Doc Source #
HasKind TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TySyn -> Kind Source #
PP (WithNames TySyn) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames TySyn -> Doc Source #
type Rep TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TySyn = D1 ('MetaData "TySyn" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-jyTxkWAqoKLO0ZfM89b4u" 'False) (C1 ('MetaCons "TySyn" 'PrefixI 'True) ((S1 ('MetaSel ('Just "tsName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Just "tsParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam])) :: (S1 ('MetaSel ('Just "tsConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop]) :: (S1 ('MetaSel ('Just "tsDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Just "tsDoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe String))))))

type Prop = Type Source #

The type is supposed to be of kind KProp

data TVarSource Source #

Constructors

TVFromModParam Name	Name of module parameter
TVFromSignature Name	A variable in a signature
TypeWildCard
TypeOfRecordField Ident
TypeOfTupleField Int
TypeOfSeqElement
LenOfSeq
TypeParamInstNamed Name Ident
TypeParamInstPos Name Int
DefinitionOf Name
LenOfCompGen
TypeOfArg (Maybe Int)
TypeOfRes
TypeErrorPlaceHolder

Instances

Instances details

Show TVarSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVarSource -> ShowS show :: TVarSource -> String showList :: [TVarSource] -> ShowS
Generic TVarSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TVarSource :: Type -> Type Methods from :: TVarSource -> Rep TVarSource x to :: Rep TVarSource x -> TVarSource
NFData TVarSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TVarSource -> ()
PP TVarSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVarSource -> Doc Source #
type Rep TVarSource Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TVarSource = D1 ('MetaData "TVarSource" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-jyTxkWAqoKLO0ZfM89b4u" 'False) (((C1 ('MetaCons "TVFromModParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "TVFromSignature" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "TypeWildCard" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TypeOfRecordField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident)) :+: C1 ('MetaCons "TypeOfTupleField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: (C1 ('MetaCons "TypeOfSeqElement" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LenOfSeq" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "TypeParamInstNamed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident)) :+: (C1 ('MetaCons "TypeParamInstPos" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "DefinitionOf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))) :+: ((C1 ('MetaCons "LenOfCompGen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypeOfArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)))) :+: (C1 ('MetaCons "TypeOfRes" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypeErrorPlaceHolder" 'PrefixI 'False) (U1 :: Type -> Type)))))

data TVarInfo Source #

Constructors

TVarInfo
Fields tvarSource :: Range Source code that gave rise tvarDesc :: TVarSource Description

Instances

Instances details

Show TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVarInfo -> ShowS show :: TVarInfo -> String showList :: [TVarInfo] -> ShowS
Generic TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TVarInfo :: Type -> Type Methods from :: TVarInfo -> Rep TVarInfo x to :: Rep TVarInfo x -> TVarInfo
NFData TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TVarInfo -> ()
PP TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVarInfo -> Doc Source #
type Rep TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TVarInfo = D1 ('MetaData "TVarInfo" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-jyTxkWAqoKLO0ZfM89b4u" 'False) (C1 ('MetaCons "TVarInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tvarSource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "tvarDesc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVarSource)))

data TVar Source #

Type variables.

Constructors

TVFree !Int Kind (Set TParam) TVarInfo	Unique, kind, ids of bound type variables that are in scope The last field gives us some infor for nicer warnings/errors.
TVBound !TParam

Instances

Instances details

Eq TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: TVar -> TVar -> Bool (/=) :: TVar -> TVar -> Bool
Ord TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods compare :: TVar -> TVar -> Ordering (<) :: TVar -> TVar -> Bool (<=) :: TVar -> TVar -> Bool (>) :: TVar -> TVar -> Bool (>=) :: TVar -> TVar -> Bool max :: TVar -> TVar -> TVar min :: TVar -> TVar -> TVar
Show TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVar -> ShowS show :: TVar -> String showList :: [TVar] -> ShowS
Generic TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TVar :: Type -> Type Methods from :: TVar -> Rep TVar x to :: Rep TVar x -> TVar
NFData TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TVar -> ()
PP TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVar -> Doc Source #
HasKind TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TVar -> Kind Source #
FreeVars TVar Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: TVar -> Deps Source #
PP (WithNames TVar) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames TVar -> Doc Source #
type Rep TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TVar = D1 ('MetaData "TVar" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-jyTxkWAqoKLO0ZfM89b4u" 'False) (C1 ('MetaCons "TVFree" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set TParam)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVarInfo))) :+: C1 ('MetaCons "TVBound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 TParam)))

data Type Source #

The internal representation of types. These are assumed to be kind correct.

Constructors

TCon !TCon ![Type]	Type constant with args
TVar TVar	Type variable (free or bound)
TUser !Name ![Type] !Type	This is just a type annotation, for a type that was written as a type synonym. It is useful so that we can use it to report nicer errors. Example: `TUser T ts t` is really just the type `t` that was written as `T ts` by the user.
TRec ![(Ident, Type)]	Record type

Instances

Instances details

Eq Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: Type -> Type -> Bool (/=) :: Type -> Type -> Bool
Ord Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods compare :: Type -> Type -> Ordering (<) :: Type -> Type -> Bool (<=) :: Type -> Type -> Bool (>) :: Type -> Type -> Bool (>=) :: Type -> Type -> Bool max :: Type -> Type -> Type min :: Type -> Type -> Type
Show Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Type -> ShowS show :: Type -> String showList :: [Type] -> ShowS
Generic Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep Type :: Type -> Type Methods from :: Type -> Rep Type x to :: Rep Type x -> Type
NFData Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Type -> ()
PP Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Type -> Doc Source #
HasKind Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: Type -> Kind Source #
FVS Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Type -> Set TVar Source #
ShowParseable Type Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Type -> Doc Source #
FreeVars Type Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Type -> Deps Source #
TVars Type Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Type -> Type Source #
TrieMap TypeMap Type Source #
Instance details Defined in Cryptol.TypeCheck.TypeMap Methods emptyTM :: TypeMap a Source # nullTM :: TypeMap a -> Bool Source # lookupTM :: Type -> TypeMap a -> Maybe a Source # alterTM :: Type -> (Maybe a -> Maybe a) -> TypeMap a -> TypeMap a Source # unionTM :: (a -> a -> a) -> TypeMap a -> TypeMap a -> TypeMap a Source # toListTM :: TypeMap a -> [(Type, a)] Source # mapMaybeWithKeyTM :: (Type -> a -> Maybe b) -> TypeMap a -> TypeMap b Source #
PP (WithNames Type) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames Type -> Doc Source #
type Rep Type Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep Type = D1 ('MetaData "Type" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-jyTxkWAqoKLO0ZfM89b4u" 'False) ((C1 ('MetaCons "TCon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TCon) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Type])) :+: C1 ('MetaCons "TVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVar))) :+: (C1 ('MetaCons "TUser" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Type]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Type))) :+: C1 ('MetaCons "TRec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Ident, Type)]))))

data TPFlavor Source #

Constructors

TPModParam Name
TPOther (Maybe Name)

Instances

Instances details

Show TPFlavor Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TPFlavor -> ShowS show :: TPFlavor -> String showList :: [TPFlavor] -> ShowS
Generic TPFlavor Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TPFlavor :: Type -> Type Methods from :: TPFlavor -> Rep TPFlavor x to :: Rep TPFlavor x -> TPFlavor
NFData TPFlavor Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TPFlavor -> ()
type Rep TPFlavor Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TPFlavor = D1 ('MetaData "TPFlavor" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-jyTxkWAqoKLO0ZfM89b4u" 'False) (C1 ('MetaCons "TPModParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "TPOther" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Name))))

data TParam Source #

Type parameters.

Constructors

TParam
Fields tpUnique :: !Int Parameter identifier tpKind :: Kind Kind of parameter tpFlav :: TPFlavor What sort of type parameter is this tpInfo :: !TVarInfo A description for better messages.

Instances

Instances details

Eq TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: TParam -> TParam -> Bool (/=) :: TParam -> TParam -> Bool
Ord TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods compare :: TParam -> TParam -> Ordering (<) :: TParam -> TParam -> Bool (<=) :: TParam -> TParam -> Bool (>) :: TParam -> TParam -> Bool (>=) :: TParam -> TParam -> Bool max :: TParam -> TParam -> TParam min :: TParam -> TParam -> TParam
Show TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TParam -> ShowS show :: TParam -> String showList :: [TParam] -> ShowS
Generic TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TParam :: Type -> Type Methods from :: TParam -> Rep TParam x to :: Rep TParam x -> TParam
NFData TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TParam -> ()
PP TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TParam -> Doc Source #
HasKind TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TParam -> Kind Source #
ShowParseable TParam Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: TParam -> Doc Source #
PP (WithNames TParam) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames TParam -> Doc Source #
type Rep TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TParam = D1 ('MetaData "TParam" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-jyTxkWAqoKLO0ZfM89b4u" 'False) (C1 ('MetaCons "TParam" 'PrefixI 'True) ((S1 ('MetaSel ('Just "tpUnique") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :: S1 ('MetaSel ('Just "tpKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :: (S1 ('MetaSel ('Just "tpFlav") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TPFlavor) :*: S1 ('MetaSel ('Just "tpInfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TVarInfo))))

data Schema Source #

The types of polymorphic values.

Constructors

Forall
Fields sVars :: [TParam] sProps :: [Prop] sType :: Type

Instances

Instances details

Eq Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: Schema -> Schema -> Bool (/=) :: Schema -> Schema -> Bool
Show Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Schema -> ShowS show :: Schema -> String showList :: [Schema] -> ShowS
Generic Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep Schema :: Type -> Type Methods from :: Schema -> Rep Schema x to :: Rep Schema x -> Schema
NFData Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Schema -> ()
PP Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Schema -> Doc Source #
FVS Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Schema -> Set TVar Source #
FreeVars Schema Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Schema -> Deps Source #
TVars Schema Source #	This instance does not need to worry about bound variable capture, because we rely on the `Subst` datatype invariant to ensure that variable scopes will be properly preserved.
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Schema -> Schema Source #
PP (WithNames Schema) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames Schema -> Doc Source #
type Rep Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep Schema = D1 ('MetaData "Schema" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-jyTxkWAqoKLO0ZfM89b4u" 'False) (C1 ('MetaCons "Forall" 'PrefixI 'True) (S1 ('MetaSel ('Just "sVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam]) :: (S1 ('MetaSel ('Just "sProps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop]) :: S1 ('MetaSel ('Just "sType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))