expand the type system, part 1

[zetah11]

• [x] Arbitrary expressions in range types
• [x] Nominal types
• [ ] Type functions
• [ ] Records
• [ ] Constructors & pattern matching
• [ ] Existentials (in particular, functions)

[zetah11]

Nominal types are mostly done in 95c476a2666e40c922e7dae5c8984689d5f92e97. There's still a fairly important bit missing, which is that

type A = 0 upto 10
type B = A
let x: A = 5
let y: B = a

will error with "incompatible types", even though it shouldn't. This is because the Unifier does not have access to the context. Fixing that might require some rearchitecting.

Error messages are also subpar, since check_int_type for instance very eagerly expands types. As such, something like

type A = 0 upto 10 -> 0 upto 10
let x: A = 10

will give an error message like

error[ET04]: cannot create non-numeric type with a number
  ┌─ test.z:2:11
  │
2 │ let x: A = 10
  │            ^^ a number cannot initialize '10 -> 10'

which is true, but a better message might be

error[ET04]: cannot create non-numeric type with a number
  ┌─ test.z:2:11
  │
2 │ let x: A = 10
  │            ^^ a number cannot initialize 'A'

[zetah11]

46e2b05b7ef8889e2e4582a8ea919016f335541e did the initial implementation of range types, with them containing arbitrary expressions which are lifted to top-level bindings just before type checking. This means that the elaborator is mostly unchanged, and can handle the range values like any other value. I didn't do the code generator, so it just panics when using integer types (as if you have any other choice hehe), and pretty-printing for types is terrible (_t5 upto _t10 is not useful).

[zetah11]

I think explicit coercions (#22) will be useful for checking range types. This would move the responsibility of checking range compatibility to *somewhere* in the elaborator, instead of doing it in the unifier. Presumably this would be after partial evaluation with a run time check if the ranges are incompatible, but that needs more thought.

[zetah11]

Nominal types (pretty much) done in 12a3b951fa309fc1317c8d2143420e59b3326151.

[zetah11]

Range types with arbitrary expressions done with 280c100838b8598531bf98555b130f36c9577cfe.