Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Cryptol.TypeCheck.Type
Synopsis
- class FVS t where
- type SType = Type
- data AbstractType = AbstractType {}
- data Newtype = Newtype {}
- data TySyn = TySyn {}
- type Prop = Type
- data TVarSource
- data TVarInfo = TVarInfo {}
- data TVar
- data Type
- data TPFlavor
- = TPModParam Name
- | TPOther (Maybe Name)
- data TParam = TParam {}
- data Schema = Forall {}
- 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
Instances
FVS Type Source # | |
FVS Schema Source # | |
FVS DelayedCt Source # | |
FVS Goal Source # | |
FVS Error Source # | |
FVS Warning Source # | |
FVS a => FVS [a] Source # | |
Defined in Cryptol.TypeCheck.Type | |
FVS a => FVS (Maybe a) Source # | |
Defined in Cryptol.TypeCheck.Type | |
(FVS a, FVS b) => FVS (a, b) Source # | |
Defined in Cryptol.TypeCheck.Type |
data AbstractType Source #
Information about an abstract type.
Constructors
AbstractType | |
Instances
Show AbstractType Source # | |
Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> AbstractType -> ShowS show :: AbstractType -> String showList :: [AbstractType] -> ShowS | |
Generic AbstractType Source # | |
Defined in Cryptol.TypeCheck.Type Associated Types type Rep AbstractType :: Type -> Type | |
NFData AbstractType Source # | |
Defined in Cryptol.TypeCheck.Type Methods rnf :: AbstractType -> () | |
type Rep AbstractType Source # | |
Defined in Cryptol.TypeCheck.Type type Rep AbstractType = D1 ('MetaData "AbstractType" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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)))))) |
Named records
Constructors
Newtype | |
Instances
Show Newtype Source # | |
Generic Newtype Source # | |
NFData Newtype Source # | |
Defined in Cryptol.TypeCheck.Type | |
PP Newtype Source # | |
HasKind Newtype Source # | |
FreeVars Newtype Source # | |
PP (WithNames Newtype) Source # | |
type Rep Newtype Source # | |
Defined in Cryptol.TypeCheck.Type type Rep Newtype = D1 ('MetaData "Newtype" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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)))))) |
Type synonym.
Constructors
TySyn | |
Instances
Show TySyn Source # | |
Generic TySyn Source # | |
NFData TySyn Source # | |
Defined in Cryptol.TypeCheck.Type | |
PP TySyn Source # | |
HasKind TySyn Source # | |
PP (WithNames TySyn) Source # | |
type Rep TySyn Source # | |
Defined in Cryptol.TypeCheck.Type type Rep TySyn = D1 ('MetaData "TySyn" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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)))))) |
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
Show TVarSource Source # | |
Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVarSource -> ShowS show :: TVarSource -> String showList :: [TVarSource] -> ShowS | |
Generic TVarSource Source # | |
Defined in Cryptol.TypeCheck.Type Associated Types type Rep TVarSource :: Type -> Type | |
NFData TVarSource Source # | |
Defined in Cryptol.TypeCheck.Type Methods rnf :: TVarSource -> () | |
PP TVarSource Source # | |
Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVarSource -> Doc Source # | |
type Rep TVarSource Source # | |
Defined in Cryptol.TypeCheck.Type type Rep TVarSource = D1 ('MetaData "TVarSource" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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))))) |
Constructors
TVarInfo | |
Fields
|
Instances
Show TVarInfo Source # | |
Generic TVarInfo Source # | |
NFData TVarInfo Source # | |
Defined in Cryptol.TypeCheck.Type | |
PP TVarInfo Source # | |
type Rep TVarInfo Source # | |
Defined in Cryptol.TypeCheck.Type type Rep TVarInfo = D1 ('MetaData "TVarInfo" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "TVarInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tvarSource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "tvarDesc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVarSource))) |
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
Eq TVar Source # | |
Ord TVar Source # | |
Show TVar Source # | |
Generic TVar Source # | |
NFData TVar Source # | |
Defined in Cryptol.TypeCheck.Type | |
PP TVar Source # | |
HasKind TVar Source # | |
FreeVars TVar Source # | |
PP (WithNames TVar) Source # | |
type Rep TVar Source # | |
Defined in Cryptol.TypeCheck.Type type Rep TVar = D1 ('MetaData "TVar" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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))) |
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 |
TRec ![(Ident, Type)] | Record type |
Instances
Eq Type Source # | |
Ord Type Source # | |
Show Type Source # | |
Generic Type Source # | |
NFData Type Source # | |
Defined in Cryptol.TypeCheck.Type | |
PP Type Source # | |
HasKind Type Source # | |
FVS Type Source # | |
ShowParseable Type Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Type -> Doc Source # | |
FreeVars Type Source # | |
TVars Type Source # | |
TrieMap TypeMap Type Source # | |
Defined in Cryptol.TypeCheck.TypeMap Methods 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 # | |
type Rep Type Source # | |
Defined in Cryptol.TypeCheck.Type type Rep Type = D1 ('MetaData "Type" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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)])))) |
Constructors
TPModParam Name | |
TPOther (Maybe Name) |
Instances
Show TPFlavor Source # | |
Generic TPFlavor Source # | |
NFData TPFlavor Source # | |
Defined in Cryptol.TypeCheck.Type | |
type Rep TPFlavor Source # | |
Defined in Cryptol.TypeCheck.Type type Rep TPFlavor = D1 ('MetaData "TPFlavor" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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)))) |
Type parameters.
Constructors
TParam | |
Instances
Eq TParam Source # | |
Ord TParam Source # | |
Show TParam Source # | |
Generic TParam Source # | |
NFData TParam Source # | |
Defined in Cryptol.TypeCheck.Type | |
PP TParam Source # | |
HasKind TParam Source # | |
ShowParseable TParam Source # | |
Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: TParam -> Doc Source # | |
PP (WithNames TParam) Source # | |
type Rep TParam Source # | |
Defined in Cryptol.TypeCheck.Type type Rep TParam = D1 ('MetaData "TParam" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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)))) |
The types of polymorphic values.
Instances
Eq Schema Source # | |
Show Schema Source # | |
Generic Schema Source # | |
NFData Schema Source # | |
Defined in Cryptol.TypeCheck.Type | |
PP Schema Source # | |
FVS Schema Source # | |
FreeVars Schema Source # | |
TVars Schema Source # | This instance does not need to worry about bound variable
capture, because we rely on the |
PP (WithNames Schema) Source # | |
type Rep Schema Source # | |
Defined in Cryptol.TypeCheck.Type type Rep Schema = D1 ('MetaData "Schema" "Cryptol.TypeCheck.Type" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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)))) |
schemaParam :: Name -> TPFlavor Source #
tySynParam :: Name -> TPFlavor Source #
propSynParam :: Name -> TPFlavor Source #
newtypeParam :: Name -> TPFlavor Source #
modTyParam :: Name -> TPFlavor Source #
tvSourceName :: TVarSource -> Maybe Name Source #
Get the names of something that is related to the tvar.
quickApply :: Kind -> [a] -> Kind Source #
kindResult :: Kind -> Kind Source #
newtypeConType :: Newtype -> Schema Source #
abstractTypeTC :: AbstractType -> TCon Source #
tIsError :: Type -> Maybe TCErrorMessage Source #
tIsInteger :: Type -> Bool Source #
tSplitFun :: TFun -> Type -> [Type] Source #
Split up repeated occurances of the given binary type-level function.
pIsSignedCmp :: Prop -> Maybe Type Source #
newtypeTyCon :: Newtype -> TCon Source #
tBadNumber :: TCErrorMessage -> Type Source #
Make a malformed numeric type.
pSignedCmp :: Type -> Prop Source #
pHas :: Selector -> Type -> Type -> Prop Source #
A Has
constraint, used for tuple and record selection.
pError :: TCErrorMessage -> Prop Source #
Make a malformed property.
noFreeVariables :: FVS t => t -> Bool Source #
ppNewtypeShort :: Newtype -> Doc Source #
pickTVarName :: Kind -> TVarSource -> Int -> Doc Source #
module Cryptol.TypeCheck.TCon