plutus-core-1.30.0.0: Language library for Plutus Core
Safe HaskellSafe-Inferred
LanguageHaskell2010

PlutusCore.TypeCheck

Description

Kindtype inferencechecking.

Synopsis

Documentation

class ToKind (uni ∷ TypeType) Source #

For computing the Plutus kind of a built-in type. See kindOfBuiltinType.

Minimal complete definition

toSingKind

Instances

Instances details
ToKind DefaultUni Source # 
Instance details

Defined in PlutusCore.Default.Universe

Methods

toSingKind ∷ ∀ k (a ∷ k). DefaultUni (Esc a) → SingKind k Source #

type MonadKindCheck err term uni fun ann m = (MonadError err m, AsTypeError err term uni fun ann, ToKind uni) Source #

The constraints that are required for kind checking.

type MonadTypeCheck err term uni fun ann m = (MonadKindCheck err term uni fun ann m, MonadNormalizeType uni m, GEq uni, Ix fun) Source #

The general constraints that are required for type checking a Plutus AST.

type Typecheckable uni fun = (ToKind uni, HasUniApply uni, ToBuiltinMeaning uni fun) Source #

The constraint for built-in types/functions are kind/type-checkable.

We keep this separate from MonadKindCheck/MonadTypeCheck, because those mainly constrain the monad and Typecheckable constraints only the builtins. In particular useful when the monad gets instantiated and builtins don't. Another reason is that Typecheckable is not required during type checking, since it's only needed for computing BuiltinTypes, which is passed as a regular argument to the worker of the type checker.

Configuration.

newtype BuiltinTypes uni fun Source #

Mapping from Builtins to their Normalized Kinds.

Constructors

BuiltinTypes 

Fields

tccBuiltinTypesHasTypeCheckConfig cfg uni fun ⇒ Lens' cfg (BuiltinTypes uni fun) Source #

defKindCheckConfigKindCheckConfig Source #

The default kind checking config.

builtinMeaningsToTypes ∷ (MonadKindCheck err term uni fun ann m, Typecheckable uni fun) ⇒ BuiltinSemanticsVariant fun → ann → m (BuiltinTypes uni fun) Source #

Extract the TypeScheme from a BuiltinMeaning and convert it to the corresponding Kind for each built-in function.

getDefTypeCheckConfig ∷ (MonadKindCheck err term uni fun ann m, Typecheckable uni fun) ⇒ ann → m (TypeCheckConfig uni fun) Source #

Get the default type checking config.

Kindtype inferencechecking.

inferKindMonadKindCheck err term uni fun ann m ⇒ KindCheckConfigType TyName uni ann → m (Kind ()) Source #

Infer the kind of a type.

checkKindMonadKindCheck err term uni fun ann m ⇒ KindCheckConfig → ann → Type TyName uni ann → Kind () → m () Source #

Check a type against a kind. Infers the kind of the type and checks that it's equal to the given kind throwing a TypeError (annotated with the value of the ann argument) otherwise.

inferTypeMonadTypeCheckPlc err uni fun ann m ⇒ TypeCheckConfig uni fun → Term TyName Name uni fun ann → m (Normalized (Type TyName uni ())) Source #

Infer the type of a term.

checkTypeMonadTypeCheckPlc err uni fun ann m ⇒ TypeCheckConfig uni fun → ann → Term TyName Name uni fun ann → Normalized (Type TyName uni ()) → m () Source #

Check a term against a type. Infers the type of the term and checks that it's equal to the given type throwing a TypeError (annotated with the value of the ann argument) otherwise.

inferTypeOfProgramMonadTypeCheckPlc err uni fun ann m ⇒ TypeCheckConfig uni fun → Program TyName Name uni fun ann → m (Normalized (Type TyName uni ())) Source #

Infer the type of a program.

checkTypeOfProgramMonadTypeCheckPlc err uni fun ann m ⇒ TypeCheckConfig uni fun → ann → Program TyName Name uni fun ann → Normalized (Type TyName uni ()) → m () Source #

Check a program against a type. Infers the type of the program and checks that it's equal to the given type throwing a TypeError (annotated with the value of the ann argument) otherwise.