Singleton Types

[brendanzab]

This will be handy when working with records-as modules, and also potentially make checking dependent records easier.

Core syntax changes:

t ::= ... | (= t)

The t should be an inferrable term.

Resources:

• Subtyping with Singleton Types
• A modular type-checking algorithm for type theory with singleton types and proof irrelevance

Mentioned in our discussion on record types: #2 (comment)