Documentation

The AST of a value with a Plutus type attached to it. The type is for the Plutus type checker to look at. Opaque can appear in the type of the denotation of a builtin.

For unlifting from the Constant constructor when the stored value is of a monomorphic built-in type

The rep parameter specifies how the type looks on the PLC side (i.e. just like with Opaque val rep).

Representation of a type variable: its name and unique and an implicit kind.

Representation of an intrinsically-kinded type variable: a name.

Representation of an intrinsically-kinded type application: a function and an argument.

Representation of of an intrinsically-kinded universal quantifier: a bound name and a body.

For annotating an uninstantiated built-in type, so that it gets handled by the right instance or type family.

LastArg x y is the same thing as y in the signature of the denotation of a built-in functions and this type is only used for referencing x before y, so that the elaboration machinery generates x before y in the all part of the Plutus signature of the builtin. This is a very hacky and indirect way of specifying the ordering of type variables in a Plutus signature, in future we'll do it explicitly by introducing a Forall binder for use in type signatures of denotations of builtins.

Take an iterated application of a built-in type and elaborate every function application inside of it to TyAppRep and annotate the head with BuiltinHead.

The idea is that we don't need to process built-in types manually if we simply add some annotations for instance resolution to look for. Think what we'd have to do manually for, say, ToHoles: traverse the spine of the application and collect all the holes into a list, which is troubling, because type applications are left-nested and lists are right-nested, so we'd have to use accumulators or an explicit Reverse type family. And then we also have KnownTypeAst and ToBinds, so handling built-in types in a special way for each of those would be a hassle, especially given the fact that type-level Haskell is not exactly good at computing things. With the ElaborateBuiltin approach we get KnownTypeAst, ToHoles and ToBinds for free.

We make this an open type family, so that elaboration is customizable for each universe.

Take a constraint and use it to constrain every argument of a possibly 0-ary elaborated application of a built-in type.

Take a constraint and use it to constrain every argument of a possibly 0-ary application of a built-in type.