plutus-core-1.46.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, 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 TypeErrorPlc uni fun ann = TypeError (Term TyName Name uni fun ()) uni fun ann Source #

The PLC type error type.

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 (TypeError term uni fun ann) 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 (TypeError term uni fun ann) term uni fun ann m, Typecheckable uni fun) ⇒ ann → m (TypeCheckConfig uni fun) Source #

Get the default type checking config.

Kindtype inferencechecking.

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

Infer the kind of a type.

checkKindMonadKindCheck (TypeError term uni fun ann) 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 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 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 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 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.