cryptol-2.8.0: Cryptol: The Language of Cryptography
Safe HaskellSafe
LanguageHaskell2010

Cryptol.TypeCheck.Type

Synopsis

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

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

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-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))))))

data Newtype Source #

Named records

Constructors

Newtype 

Fields

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

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-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))))))

data TySyn Source #

Type synonym.

Constructors

TySyn 

Fields

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-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))))))

type Prop = Type Source #

The type is supposed to be of kind KProp

data TVarSource Source #

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-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)))))

data TVarInfo Source #

Constructors

TVarInfo 

Fields

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-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)))

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-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)))

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-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)]))))

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-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))))

data TParam Source #

Type parameters.

Constructors

TParam 

Fields

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-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))))

data Schema Source #

The types of polymorphic values.

Constructors

Forall 

Fields

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-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))))

isMono :: Schema -> Maybe Type Source #

tpName :: TParam -> Maybe Name Source #

tvSourceName :: TVarSource -> Maybe Name Source #

Get the names of something that is related to the tvar.

quickApply :: Kind -> [a] -> Kind Source #

isFreeTV :: TVar -> Bool Source #

isBoundTV :: TVar -> Bool Source #

tIsNat' :: Type -> Maybe Nat' Source #

tIsNum :: Type -> Maybe Integer Source #

tIsInf :: Type -> Bool Source #

tIsVar :: Type -> Maybe TVar Source #

tIsFun :: Type -> Maybe (Type, Type) Source #

tIsSeq :: Type -> Maybe (Type, Type) Source #

tIsBit :: Type -> Bool Source #

tIsInteger :: Type -> Bool Source #

tIsIntMod :: Type -> Maybe Type Source #

tIsTuple :: Type -> Maybe [Type] Source #

tIsRec :: Type -> Maybe [(Ident, Type)] Source #

tIsBinFun :: TFun -> Type -> Maybe (Type, Type) Source #

tSplitFun :: TFun -> Type -> [Type] Source #

Split up repeated occurances of the given binary type-level function.

pIsFin :: Prop -> Maybe Type Source #

pIsGeq :: Prop -> Maybe (Type, Type) Source #

pIsEq :: Prop -> Maybe (Type, Type) Source #

pIsZero :: Prop -> Maybe Type Source #

pIsLogic :: Prop -> Maybe Type Source #

pIsArith :: Prop -> Maybe Type Source #

pIsCmp :: Prop -> Maybe Type Source #

pIsLiteral :: Prop -> Maybe (Type, Type) Source #

pIsTrue :: Prop -> Bool Source #

pIsWidth :: Prop -> Maybe Type Source #

tNum :: Integral a => a -> Type Source #

tString :: Int -> Type Source #

tRec :: [(Ident, Type)] -> Type Source #

tFun :: Type -> Type -> Type infixr 5 Source #

Make a function type.

tNoUser :: Type -> Type Source #

Eliminate outermost type synonyms.

tBadNumber :: TCErrorMessage -> Type Source #

Make a malformed numeric type.

tError :: Kind -> TCErrorMessage -> Type Source #

Make an error value of the given type.

tf2 :: TFun -> Type -> Type -> Type Source #

tf3 :: TFun -> Type -> Type -> Type -> Type Source #

(=#=) :: Type -> Type -> Prop infix 4 Source #

Equality for numeric types.

(>==) :: Type -> Type -> Prop infix 4 Source #

Make a greater-than-or-equal-to constraint.

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 #