Constructor types: Data constructors should have an individual type

[fmease]

Disclaimer: This changes the type system significantly. Low priority. What we need is a large collection of use cases. We need a good motivation to make this part of the language. Syntax is not final. Not sure if this is the default or opt-in.

Short description: Data constructors will no longer construct values of the type defined in the data declaration but ones of the so-called constructor type which obviously varies from constructor to constructor. For some constructor T.c: Self with the new keyword Self, the corresponding constructor type is accessible as T.c.Type of type Type. The (constructor) type could of course be parameterized and/or indexed / a family of types / a non-nullary type constructor. A value of this type implicitly coerces to T.

Example 0: Simple Data Type

data Bool: Type of
    false: Self
    true: Self   ;;; `Self` is short for `Bool.true.Type` in this context

Bool.false is of type Bool.false.Type (an ordinary type). This is legal:

identity-false: Bool.false.Type -> Bool.false.Type = identity

What's more though, identity 'Bool Bool.true is also legal and of type Bool. In this scenario, Bool.true is seemingly of type Bool. In actuality, Bool.true is always of type Bool.true.Type. However in the application of identity 'Bool, it gets wrapped inside of an invisible (to the user, not to the type system) constructor. Not sure if we need a notation for this or how it should look like but let's say it's the following: Bool.true$ Bool.true with Bool.true$ : Bool.true.Type -> Bool.

Which means data declaration kind of look like this in pseudo pre-constructor-type Lushui code (but lacking those implicit conversions):

data Bool: Type of
    false$ : Bool.false.Type -> Bool
    true$ : Bool.true.Type -> Bool
    false: Bool.false.Type
    true: Bool.true.Type

And a lossy translation into actual pre-constructor-type Lushui code (but lacking those implicit conversions):

data False: Type of
    false: False

data True: Type of
    true: True

data Bool: Type of
    false: False -> Bool
    true: True -> Bool

Example 1: Parameterized Data Type

data Maybe (A: Type): Type of
    none 'A: Self A   ;;; none 'A: Maybe.none.Type A
    some 'A: A -> Self A

Possible coercions from value of type A to value of type B (and from type A to type B themselves):

1. Maybe.none.Type to Maybe (higher-kinded)
2. Maybe.some.Type to Maybe (higher-kinded)
3. Maybe.none.Type A to Maybe A for all A: Type (this does not follow from 1. since we don't have subtyping, only coercions)
4. Maybe.some.Type A to Maybe A for all A: Type (this does not follow from 2., same reason)
5. A -> Maybe.some.Type A to A -> Maybe A for all A: Type (this does not follow from 2., same reason)
6. ??? (some more?)

Example 2: Indexed Data Type

data Pointed (A: Type): Type of
    point: Self Unit   ;;; point: Pointed.point.Type Unit

Possible coercions from value of type A to value of type B (and from type A to type B themselves):

1. Pointed.point.Type to Pointed (higher-kinded) (that should be sound as far as I know)
2. Pointed.point.Type Unit to Pointed Unit (this does not follow from 1.)

Refinement to Constructor Type in Case Analyses

A "unification constraint" generated during (dependent) pattern matching of the form (pseudo, shortened) ?0 : Bool, ?0 ~ Bool.true should either allow x (?0) to be coerced back from Bool to Bool.true.Type at coercion points (e.g. application arguments) or it should actually unwrap x (from true$) as part of the binding making it available unwrapped in the whole case analysis case (match arm). E.g. this should be legal:

identity-true (x: Bool.true.Type): Bool.true.Type = x

identity-bool (x: Bool): Bool = case x of
    Bool.true => identity-true x
    Bool.false => identity-false x   ;;; defined somewhere above

Notes

Maybe this is out of scope and awkward to use without subtyping.