cryptol-2.11.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 

Instances

Instances details
Show AbstractType Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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 Text))))))

data Newtype Source #

Named records

Instances

Instances details
Eq Newtype Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

(==) :: Newtype -> Newtype -> Bool #

(/=) :: Newtype -> Newtype -> Bool #

Ord Newtype Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Show Newtype Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

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

type Rep Newtype Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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 Text))))))

type Prop = Type Source #

The type is supposed to be of kind KProp.

data TypeWithSource Source #

A type annotated with information on how it came about.

Constructors

WithSource 

data ArgDescr Source #

Constructors

ArgDescr 

Instances

Instances details
Show ArgDescr Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Generic ArgDescr Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep ArgDescr :: Type -> Type #

Methods

from :: ArgDescr -> Rep ArgDescr x #

to :: Rep ArgDescr x -> ArgDescr #

NFData ArgDescr Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: ArgDescr -> () #

PP ArgDescr Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> ArgDescr -> Doc Source #

type Rep ArgDescr Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Rep ArgDescr = D1 ('MetaData "ArgDescr" "Cryptol.TypeCheck.Type" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "ArgDescr" 'PrefixI 'True) (S1 ('MetaSel ('Just "argDescrFun") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Name)) :*: S1 ('MetaSel ('Just "argDescrNumber") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int))))

data TypeSource Source #

Explains how this type came to be, for better error messages.

Instances

Instances details
Show TypeSource Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Generic TypeSource Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep TypeSource :: Type -> Type #

NFData TypeSource Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TypeSource -> () #

PP TypeSource Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TypeSource -> Doc Source #

type Rep TypeSource Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TypeSource = D1 ('MetaData "TypeSource" "Cryptol.TypeCheck.Type" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" '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 ArgDescr)) :+: C1 ('MetaCons "TypeOfRes" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "FunApp" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypeOfIfCondExpr" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TypeFromUserAnnotation" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "GeneratorOfListComp" '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

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.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "TVarInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tvarSource") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range) :*: S1 ('MetaSel ('Just "tvarDesc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TypeSource)))

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

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 !(RecordMap Ident Type)

Record type

TNewtype !Newtype ![Type]

A newtype

Instances

Instances details
Eq Type Source #

Syntactic equality, ignoring type synonyms and record order.

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 #

TVars Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Type -> Type Source #

ShowParseable Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

FreeVars Type Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Type -> Deps 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 #

The precedence levels used by this pretty-printing instance correspond with parser non-terminals as follows:

  • 0-1: type
  • 2: infix_type
  • 3: app_type
  • 4: dimensions atype
  • 5: atype
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

data TPFlavor Source #

Instances

Instances details
Show TPFlavor Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

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

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

Show TParam Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

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

PP (WithNames TParam) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TParam Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TParam = D1 ('MetaData "TParam" "Cryptol.TypeCheck.Type" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" '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

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 #

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 #

FreeVars Schema Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Schema -> Deps Source #

PP (WithNames Schema) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Rep Schema Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Rep Schema = D1 ('MetaData "Schema" "Cryptol.TypeCheck.Type" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" '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))))

tvSourceName :: TypeSource -> Maybe Name Source #

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

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

superclassSet :: Prop -> Set Prop Source #

Compute the set of all Props that are implied by the given prop via superclass constraints.

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

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

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

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

Make a function type.

tNoUser :: Type -> Type Source #

Eliminate outermost type synonyms.

tError :: Type -> Type Source #

Make an error value of the given type to replace the given malformed type (the argument to the error function)

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.