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.