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

PlutusIR.TypeCheck

Description

Kindtype inferencechecking, mirroring PlutusCore.TypeCheck

Synopsis

Configuration.

newtype BuiltinTypes (uni ∷ TypeType) fun Source #

Mapping from Builtins to their Normalized Kinds.

Constructors

BuiltinTypes 

Fields

data PirTCConfig uni fun Source #

extending the plc typecheck config with AllowEscape

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

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

The default TypeCheckConfig.

Type checking, extending the plc typechecker

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

Infer the type of a term. Note: The "inferred type" can escape its scope if YesEscape config is passed, see [PIR vs Paper Escaping Types Difference]

checkTypeMonadTypeCheckPir err uni fun ann m ⇒ PirTCConfig 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. Note: this may allow witnessing a type that escapes its scope, see [PIR vs Paper Escaping Types Difference]

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

Infer the type of a program. Note: The "inferred type" can escape its scope if YesEscape config is passed, see [PIR vs Paper Escaping Types Difference]

checkTypeOfProgramMonadTypeCheckPir err uni fun ann m ⇒ PirTCConfig 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. Note: this may allow witnessing a type that escapes its scope, see [PIR vs Paper Escaping Types Difference]

type MonadTypeCheckPir err uni fun ann m = (MonadTypeCheck err (Term TyName Name uni fun ()) uni fun ann m, AsTypeErrorExt err uni ann) Source #

The constraints that are required for type checking Plutus IR.