A type expanded into what the generated code needs in order to check a value against it at runtime. Ty.named is resolved away here rather than emitting a table of type definitions, so a function carries only the shapes it actually accepts and a bundler can still drop the ones nobody imported.

A declared type's constructors as the descriptor carries them: the constructor's name, and its fields in declared order.

What the mu nodes a walk is inside have bound, nearest first: the key a constructor's name is carried under, and the alternatives.

A ref continues at an entry of this rather than at a descriptor read out of it, which is what keeps the walk measured by the value: the entry is fed back as a ctors node, which descends into fields, so no step can land on another ref.

How a fold carries one of a constructor's fields: the declared type coming round, a list of it coming round, or neither. It is what EncDeriving.kindOf already computes at the deriving, written where the generated code reads it.

A constructor's fields in declared order, each with the way the fold carries it.

What a fold is given about a declared type: its constructors by name, each with its fields.

Apart from TyAlts, which carries the same names, because the two say different things: one is what a value is checked against, this is which of a node's fields the walk goes into. A fold reads it at the constructor the value carries, so a name it does not hold is a value the walk declines to answer for.

A constructor's fields as the generated code reads them: each field's name beside the way the fold carries it, in declared order. Written as a recursion rather than through List.map, for the reason the rest of the printer is: the text the artifact carries has to be something a proof can unfold.

The spec __fold reads, printed as the object it indexes by the constructor's name. Spelled { and } the way Expr.objLit is, so that the reader tells the end of an empty one from the start of an entry by the same one character of lookahead.

The descriptor the entry check reads. Total for the reason Expr.render is: the text the artifact carries has to be something a proof can unfold.

A comma-separated list of names. Written as a recursion rather than String.intercalate, which walks an accumulator and does not unfold in a proof, for the reason the rest of the printer is: the file the compiler writes has to be something a proof can read back.

The text the module carries. Written as a mutual recursion over the lists rather than partial, so a proof about the file the compiler writes can unfold it.

The runtime helpers the generated code calls, printed from Helper.defs.

Named apart from the preamble, and the preamble associated to the right, so a proof can read the length of what the file opens with without unfolding the runtime behind it.

Named rather than spelled out at the use site: a proof about the file has to unfold the printer around them, and the runtime is four thousand characters the elaborator would otherwise carry.

The text of the file the compiler writes.

The type the .d.ts gives a value of this type. Total for the reason the renderers are: the file the compiler writes has to be something a proof can unfold.

The type the .d.ts gives a value of this type where it is being handed back. A Dict.Obj V parameter is printed as the union above because the entry takes either spelling; a Dict.Obj V return is the plain object alone, because the entry walked it out to one and nothing else can come back. Stops at a declared type: one interface is printed for both directions, so a Dict.Obj field there keeps the union.

The .d.ts is the only thing a consumer reads before calling, so it carries what the author wrote about the function and the one fact the types cannot say: the call throws rather than returning a value the semantics would not stand behind.

Only the types a consumer can name. A declaration that takes a function does not cross the boundary, and neither does a type that only ever holds an intermediate value -- an accumulator a foldl carries appears in no public signature, and printing it would invite a consumer to build one.