Generic literals

[fmease]

Define literals (number, text and sequence ones) to be instances of pseudo-types which implicitly coerce to specific types. This way, literals are overloaded and can seemingly be of several types. This improves the ergonomics of literals. Type theoretically, without subtyping, we cannot have the literal 0 for example to be of both/either Int or Nat. Therefore, we have different versions/names for constructors which are the same in type systems with subtyping. E.g. @Int 0 and @Nat 0.

Implicit coercions in this language are different from subtyping in the regard that they do not happen transitively. That is, even if a coerces to b then t a does not coerce to t b if t is a (type) constructor. All (type) constructors are therefore invariant.

Meta: Task: Improve the description below.

Pseudo-Type of Number Literals

Name: .Number-Literal Properties:

• integer interval it fits into
• decimal part (0 means it can be coerced to Nats, Ints, …)

Pseudo-Type of Text Literals

Name: .Text-Literal Properties:

• length (to differentiate between Text and Rune)
• escape sequences (to differentiate between UTF-8-encoded and ASCII-encoded text-y types)

Pseudo-Type of Sequence Literals

Name: .Sequence-Literal Properties: none

[fmease]

I think it's easier to implement pseudo-types as actual (foreign) types. This is less complex and does not increase the “bug vector”. This means we should define the types core.meta.literal.(Number Text Sequence) with the definition @public @foreign data L: Type for each "literal type" L (literal type not in the TypeScript sense). Then, in the type checker, we coerce from those types. This way, we do not need to adapt the error reporting code and it just scales to literal types inside larger types as type parameters.

Edit: We should definitely make core.meta, core.meta.literal, core.meta.literal.(Number Text Sequence) private in the long run (if not immediately!). This makes our system more forward compatible/open to changes. Optimally, we would already print private bindings with a leading dot (or something similar) in type error messages to avoid confusion.

[fmease]

Implementation-wise, we need to extend crate::lowered_ast::Number by the variant Generic { representation: String } (or similar).