Type of < x : Type | y >

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.

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.

1 Like

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