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.