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

PlutusCore.TypeCheck.Internal

Description

The internal module of the type checker that defines the actual algorithms, but not the user-facing API.

Synopsis

Documentation

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.

newtype BuiltinTypes uni fun Source #

Mapping from Builtins to their Normalized Kinds.

Constructors

BuiltinTypes 

Fields

data HandleNameMismatches Source #

Decides what to do upon encountering a variable whose name doesn't match the name of the variable with the same unique that is currently in the scope. Consider for example this type:

(a_0 :: *) (b_0 :: *) -> a_0

here b_0 shadows a_0 and so any variable having the 0th unique within the body of the lambda references b_0, but we have a_0 there and so there's a name mismatch. Technically, it's not a type error to have a name mismatch, because uniques are the single source of truth, however a name mismatch is deeply suspicious and is likely to be caused by a bug somewhere.

We perform the same check for term-level variables too.

Constructors

DetectNameMismatches

Throw upon encountering such a name.

IgnoreNameMismatches

Ignore it.

class HasKindCheckConfig cfg ⇒ HasTypeCheckConfig cfg uni fun | cfg → uni fun where Source #

We want HasKindCheckConfig to be a superclass of HasTypeCheckConfig for being able to seamlessly call the kind checker from the type checker, hence we're rolling out our own makeClassy here just to add the constraint.

Minimal complete definition

typeCheckConfig

Instances

Instances details
HasTypeCheckConfig (TypeCheckConfig uni fun) uni fun Source # 
Instance details

Defined in PlutusCore.TypeCheck.Internal

data TypeCheckEnv uni fun cfg Source #

The environment that the type checker runs in.

type TypeCheckT uni fun cfg m = ReaderT (TypeCheckEnv uni fun cfg) m Source #

The type checking monad that the type checker runs in. In contains a TypeCheckEnv and allows to throw TypeErrors.

type MonadTypeCheckPlc err uni fun ann m = MonadTypeCheck err (Term TyName Name uni fun ()) uni fun ann m Source #

The constraints that are required for type checking Plutus Core.

normalizeTypeMMonadNormalizeType uni m ⇒ Type TyName uni ann → TypeCheckT uni fun cfg m (Normalized (Type TyName uni ann)) Source #

Normalize a Kind.

substNormalizeTypeM Source #

Arguments

MonadNormalizeType uni m 
Normalized (Type TyName uni ())
ty
TyName
name
Type TyName uni ()
body
TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())) 

Substitute a type for a variable in a type and normalize the result.

checkTypeM ∷ (MonadTypeCheckPlc err uni fun ann m, HasTypeCheckConfig cfg uni fun) ⇒ ann → Term TyName Name uni fun ann → Normalized (Type TyName uni ()) → TypeCheckT uni fun cfg m () Source #

Check a Term against a NormalizedType.

runTypeCheckM ∷ cfg → TypeCheckT uni fun cfg m a → m a Source #

Run a TypeCheckM computation by supplying a TypeCheckConfig to it.

Used for both type and kind checking, because we need to do kind checking during type checking and so it makes sense to keep a single monad. However type checking requires a TypeCheckConfig, while kind checking doesn't, hence we keep the kind checker fully polymorphic over the type of config, so that the kinder checker can be run with an empty config (such as ()) and access to a TypeCheckConfig is not needed.

withTyVarTyNameKind () → TypeCheckT uni fun cfg m a → TypeCheckT uni fun cfg m a Source #

Extend the context of a TypeCheckM computation with a kinded variable.

tceTyVarKinds ∷ ∀ uni fun cfg fun. Lens (TypeCheckEnv uni fun cfg) (TypeCheckEnv uni fun cfg) TyVarKinds TyVarKinds Source #

lookupBuiltinM ∷ (MonadTypeCheck err term uni fun ann m, HasTypeCheckConfig cfg uni fun) ⇒ ann → fun → TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())) Source #

Look up the type of a built-in function.

tceTypeCheckConfig ∷ ∀ uni fun cfg fun cfg. Lens (TypeCheckEnv uni fun cfg) (TypeCheckEnv uni fun cfg) cfg cfg Source #

withVarNameNormalized (Type TyName uni ()) → TypeCheckT uni fun cfg m a → TypeCheckT uni fun cfg m a Source #

Extend the context of a TypeCheckM computation with a typed variable.

tceVarTypes ∷ ∀ uni fun cfg uni fun. Lens (TypeCheckEnv uni fun cfg) (TypeCheckEnv uni fun cfg) (VarTypes uni) (VarTypes uni) Source #

lookupTyVarM ∷ (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) ⇒ ann → TyNameTypeCheckT uni fun cfg m (Kind ()) Source #

Look up a type variable in the current context.

lookupVarM ∷ (MonadTypeCheck err term uni fun ann m, HasTypeCheckConfig cfg uni fun) ⇒ ann → NameTypeCheckT uni fun cfg m (Normalized (Type TyName uni ())) Source #

Look up a term variable in the current context.

inferKindM ∷ (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) ⇒ Type TyName uni ann → TypeCheckT uni fun cfg m (Kind ()) Source #

Infer the kind of a type.

checkKindM ∷ (MonadKindCheck err term uni fun ann m, HasKindCheckConfig cfg) ⇒ ann → Type TyName uni ann → Kind () → TypeCheckT uni fun cfg m () Source #

Check a Kind against a Kind.

unfoldIFixOf Source #

Arguments

MonadNormalizeType uni m 
Normalized (Type TyName uni ())
vPat
Normalized (Type TyName uni ())
vArg
Kind ()
k
TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())) 
unfoldIFixOf pat arg k = NORM (vPat ((a :: k) -> ifix vPat a) arg)

inferTypeM ∷ (MonadTypeCheckPlc err uni fun ann m, HasTypeCheckConfig cfg uni fun) ⇒ Term TyName Name uni fun ann → TypeCheckT uni fun cfg m (Normalized (Type TyName uni ())) Source #

Synthesize the type of a term, returning a normalized type.

type MonadNormalizeType uni m = (MonadQuote m, HasUniApply uni) Source #

The constraints that type normalization requires.