 # Type of < x : Type | y >

#1

What is the type of `< x : Type | y >` and is it the same as the type of `< y | x : Type >`?

I think the first is a type error, while the second is `Kind`. Here’s my reasoning for the second:

``````Γ ⊢ Type : Kind
───────────────────────
Γ ⊢ < y : Type > : Kind
─────────────────────────── (empty alternative; c = Kind)
Γ ⊢ < x | y : Type > : Kind
``````

But for the first, we get stuck:

``````                   Γ ⊢ < > : Type
────────────────
Γ ⊢ Type : Kind    Γ ⊢ < x > : Type
─────────────────────────────────── (stuck!)
``````

For me, one issue here is that it’s not clear if order matters within the union alternatives for the type inference rules. I’m also not sure how to fix it.

#2

Hmm, well-spotted, this is indeed a problem in the current inference rules. An ugly solution would be to add more cases for the `Kind` and `Sort` cases, along the lines of:

``````Γ ⊢ T : Kind  Γ ⊢ < x : T | xs... > : Kind
────────────────────
Γ ⊢ < x : T | c | xs... > : Kind
``````

A nicer solution would be to allow unions with mixed kinds, exactly like we do with records. I’ll illustrate why I think this is sound:
Remember that `< x: T | y: U >` can be seen as formally sugar for `forall(a: k) -> { x: T -> a, y: U -> a } -> a`. If we take `T: Type`, `U: Kind` and `k = Kind` for example, then both `T -> a` and `U -> a` are of type `Kind`, and the whole has type `Kind` too. More generally, if `T: k1` and `U: k2`, we can choose `k = k1 ⋁ k2` and then that function typechecks and has kind `k1 ⋁ k2`. Thus I propose that we can, like with records, allow mixed kinds and type a union as the join of the kinds of its variant types.

The inference rules would reduce to:

``````─────────────
Γ ⊢ <> : Type

Γ ⊢ < ts… > : c
───────────────────  ; x ∉ < ts… >
Γ ⊢ < x | ts… > : c

Γ ⊢ T : t₀   Γ ⊢ < ts… > : t₁   t₀ ⋁ t₁ = t₂
────────────────────────────────────────────  ; x ∉ < ts… >
Γ ⊢ < x : T | ts… > : t₂
``````

and both `< x : Type | y >` and `< y | x : Type >` would be correctly given the type `Kind`.

#3

Ok, if you think it’s a problem too then I’ve raised #904 to capture it.