Cryptol.TypeCheck.Type

Documentation

class FVS t where

Methods

fvs :: t -> Set TVar

Instances

FVS Type

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Type -> Set TVar

FVS Schema

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Schema -> Set TVar

FVS DelayedCt

Defined in Cryptol.TypeCheck.InferTypes

Methods

fvs :: DelayedCt -> Set TVar

FVS Goal

Defined in Cryptol.TypeCheck.InferTypes

Methods

fvs :: Goal -> Set TVar

FVS Error

Defined in Cryptol.TypeCheck.Error

Methods

fvs :: Error -> Set TVar

FVS Warning

Defined in Cryptol.TypeCheck.Error

Methods

fvs :: Warning -> Set TVar

FVS a => FVS [a]

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: [a] -> Set TVar

FVS a => FVS (Maybe a)

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Maybe a -> Set TVar

(FVS a, FVS b) => FVS (a, b)

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: (a, b) -> Set TVar

type SType = Type

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

data Newtype

Named records

Constructors

Newtype

Fields

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

Instances

Show Newtype

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> Newtype -> ShowS

show :: Newtype -> String

showList :: [Newtype] -> ShowS

Generic Newtype

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: Newtype -> ()

PP Newtype

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> Newtype -> Doc

HasKind Newtype

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: Newtype -> Kind

FreeVars Newtype

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Newtype -> Deps

PP (WithNames Newtype)

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames Newtype -> Doc

type Rep Newtype

Defined in Cryptol.TypeCheck.Type

type Rep Newtype = D1 (MetaData "Newtype" "Cryptol.TypeCheck.Type" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

Show TySyn

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TySyn -> ShowS

show :: TySyn -> String

showList :: [TySyn] -> ShowS

Generic TySyn

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TySyn -> ()

PP TySyn

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TySyn -> Doc

HasKind TySyn

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TySyn -> Kind

PP (WithNames TySyn)

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames TySyn -> Doc

type Rep TySyn

Defined in Cryptol.TypeCheck.Type

type Rep TySyn = D1 (MetaData "TySyn" "Cryptol.TypeCheck.Type" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

The type is supposed to be of kind KProp

data TVarSource

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

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TVarSource -> ShowS

show :: TVarSource -> String

showList :: [TVarSource] -> ShowS

Generic TVarSource

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TVarSource -> ()

PP TVarSource

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TVarSource -> Doc

type Rep TVarSource

Defined in Cryptol.TypeCheck.Type

type Rep TVarSource = D1 (MetaData "TVarSource" "Cryptol.TypeCheck.Type" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

TVarInfo

Fields

• tvarSource :: Range

  Source code that gave rise

• tvarDesc :: TVarSource

  Description

Instances

Show TVarInfo

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TVarInfo -> ShowS

show :: TVarInfo -> String

showList :: [TVarInfo] -> ShowS

Generic TVarInfo

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TVarInfo -> ()

PP TVarInfo

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TVarInfo -> Doc

type Rep TVarInfo

Defined in Cryptol.TypeCheck.Type

type Rep TVarInfo = D1 (MetaData "TVarInfo" "Cryptol.TypeCheck.Type" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

Defined in Cryptol.TypeCheck.Type

Methods

(==) :: TVar -> TVar -> Bool

(/=) :: TVar -> TVar -> Bool

Ord TVar

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

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TVar -> ShowS

show :: TVar -> String

showList :: [TVar] -> ShowS

Generic TVar

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TVar -> ()

PP TVar

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TVar -> Doc

HasKind TVar

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TVar -> Kind

FreeVars TVar

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: TVar -> Deps

PP (WithNames TVar)

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames TVar -> Doc

type Rep TVar

Defined in Cryptol.TypeCheck.Type

type Rep TVar = D1 (MetaData "TVar" "Cryptol.TypeCheck.Type" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

Eq Type

Defined in Cryptol.TypeCheck.Type

Methods

(==) :: Type -> Type -> Bool

(/=) :: Type -> Type -> Bool

Ord Type

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

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> Type -> ShowS

show :: Type -> String

showList :: [Type] -> ShowS

Generic Type

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: Type -> ()

PP Type

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> Type -> Doc

HasKind Type

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: Type -> Kind

FVS Type

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Type -> Set TVar

ShowParseable Type

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Type -> Doc

FreeVars Type

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Type -> Deps

TVars Type

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Type -> Type

TrieMap TypeMap Type

Defined in Cryptol.TypeCheck.TypeMap

Methods

emptyTM :: TypeMap a

nullTM :: TypeMap a -> Bool

lookupTM :: Type -> TypeMap a -> Maybe a

alterTM :: Type -> (Maybe a -> Maybe a) -> TypeMap a -> TypeMap a

unionTM :: (a -> a -> a) -> TypeMap a -> TypeMap a -> TypeMap a

toListTM :: TypeMap a -> [(Type, a)]

mapMaybeWithKeyTM :: (Type -> a -> Maybe b) -> TypeMap a -> TypeMap b

PP (WithNames Type)

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames Type -> Doc

type Rep Type

Defined in Cryptol.TypeCheck.Type

type Rep Type = D1 (MetaData "Type" "Cryptol.TypeCheck.Type" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

TPModParam Name

TPOther (Maybe Name)

Instances

Show TPFlavor

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TPFlavor -> ShowS

show :: TPFlavor -> String

showList :: [TPFlavor] -> ShowS

Generic TPFlavor

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TPFlavor -> ()

type Rep TPFlavor

Defined in Cryptol.TypeCheck.Type

type Rep TPFlavor = D1 (MetaData "TPFlavor" "Cryptol.TypeCheck.Type" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

Eq TParam

Defined in Cryptol.TypeCheck.Type

Methods

(==) :: TParam -> TParam -> Bool

(/=) :: TParam -> TParam -> Bool

Ord TParam

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

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TParam -> ShowS

show :: TParam -> String

showList :: [TParam] -> ShowS

Generic TParam

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TParam -> ()

PP TParam

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TParam -> Doc

HasKind TParam

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TParam -> Kind

ShowParseable TParam

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: TParam -> Doc

PP (WithNames TParam)

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames TParam -> Doc

type Rep TParam

Defined in Cryptol.TypeCheck.Type

type Rep TParam = D1 (MetaData "TParam" "Cryptol.TypeCheck.Type" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

The types of polymorphic values.

Constructors

Forall

Fields

• sVars :: [TParam]
• sProps :: [Prop]
• sType :: Type

Instances

Eq Schema

Defined in Cryptol.TypeCheck.Type

Methods

(==) :: Schema -> Schema -> Bool

(/=) :: Schema -> Schema -> Bool

Show Schema

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> Schema -> ShowS

show :: Schema -> String

showList :: [Schema] -> ShowS

Generic Schema

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: Schema -> ()

PP Schema

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> Schema -> Doc

FVS Schema

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Schema -> Set TVar

FreeVars Schema

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Schema -> Deps

TVars Schema

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.

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Schema -> Schema

PP (WithNames Schema)

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames Schema -> Doc

type Rep Schema

Defined in Cryptol.TypeCheck.Type

type Rep Schema = D1 (MetaData "Schema" "Cryptol.TypeCheck.Type" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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))))

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

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

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

kindResult :: Kind -> Kind

tpVar :: TParam -> TVar

newtypeConType :: Newtype -> Schema

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]

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

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

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 infixr 5

Make a function type.

tNoUser :: Type -> Type

Eliminate outermost type synonyms.

tBadNumber :: TCErrorMessage -> Type

Make a malformed numeric 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 infix 4

Equality for numeric types.

(=/=) :: 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 infix 4

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

pHas :: Selector -> Type -> Type -> Prop

A Has constraint, used for tuple and record selection.

pTrue :: Prop

pAnd :: [Prop] -> Prop

pSplitAnd :: Prop -> [Prop]

pFin :: Type -> Prop

pError :: TCErrorMessage -> Prop

Make a malformed property.

noFreeVariables :: FVS t => t -> Bool

addTNames :: [TParam] -> NameMap -> NameMap

ppNewtypeShort :: Newtype -> Doc

pickTVarName :: Kind -> TVarSource -> Int -> Doc

module Cryptol.Prims.Syntax