Add support for unboxed datatypes, singletons

[flupe]

WIP

Wanted to add support for the following Singleton datatype:

data Singleton (a : Set) : @0 a → Set where
  MkSingl : ∀ x → Singleton a x

Pattern-matching on a singleton witnesses that the value contained inside it mirrors the type-level (erased) index. So, what's the difference with Rezz? None really, they suit the same purpose, with the difference that Rezz requires you to think about propositional equality. And operations defined on Rezz that we want inlineable cannot pattern-match on refl (which they should be able to, more on that later) so they are quite annoying to write.

---

As is the tradition with agda2hs features, rather than just add Singleton as a builtin, I wanted to add support for unboxed datatypes, which must abide by the same rules as unboxed records, that is:

• A single constructor with a single (non-erased) argument.
• Only erased indices.

This sounded nice and all, until I remembered how we compile inline functions: reduce and unfold defs and pray that Agda does the record-pattern translation. So I eventually went ahead and reimplemented the inlining functionality without relying on Agda's unfolding. Seems to work okay for now, and should enable us to support pattern-matching on refl and such.

[jespercockx]

I'm closing all stale draft PRs in this repository. Feel free to update and reopen if it is still relevant.