Extend type paths to handle record types

[yannham]

Required to address #157. Type paths are used as representations of a subtype (syntactically) of a larger type used for error reporting. This PR extends them to handle types containing record types.

what it does

• add new Field(Ident) variant to path type elements
• adapt helper functions and error reporting code accordingly
• add a goField operator, analoguous to existing goDom and goCodom, in order for the future record builtin contract to construct type paths with Field elements

what it does not

• implement record contracts: currently, no code actually uses the new type paths element yet

Context

Checking an higher-order contract involves checking several subcontracts on simpler types: for example, fully applying a function with a contract Num -> Str -> Bool involves automatic checking of Num, Str and Bool contracts. If one of the subcontract fails, we like to indicate both the original complete higher-order type, but also the particular faulty subcontract: to this end, a subpart of the original type is represented by a type path, which is a list of Codomain or Domain elements leading to the subcontract of interest.

But this phenomenon is not limited to higher-order contracts: indeed, checking a record type { a: Num, b: Str, c: Bool } also involves subcontracts. This was just not a concern until now since contracts for record types are not implemented (#157).

This PR extends path elements, which could only be Codomain or Domain, with a new constructor Field(Ident), indicating that the path to a subtype goes through a record type and takes the branch of the corresponding field. In general, contracts may mix records types and arrow types: for example, in the contract Num -> {a : Str -> Str, b: Num}, if the bound term return a record with a function wrongly returning a Bool in the field a, the type path accompanying the error would be [Codomain, Field("a"), Codomain].

Example

[Disclaimer: this example does not work as it is on this branch, since contracts for records are not yet implemented. It uses a WIP implementation for the sake of the demonstration]

Example of error reporting with a general path mixing records and arrows:

Error message

Some effort have been put into error messages involving higher contracts in #141, which uses the shape of the type path to tune messages accordingly. Since "entering" a record type does not change polarity (records are just glorified products, after all), the same heuristics are kept, but it just ignores Field elements, as can be seen in the example above.

[aspiwack]

As a complementary point, paths seem to be required whenever the checking of a field is delayed, in a value. Which includes functions, and all the (lazy) thunks (which, right now, are only found in records).

[yannham]

As a complementary point, paths seem to be required whenever the checking of a field is delayed, in a value. Which includes functions, and all the (lazy) thunks (which, right now, are only found in records).

Right, we need paths each time a contract generates one or more subcontracts that are delayed, so that we can follow the history if said subcontracts or one of their children fail.