🦎 quox►🧼 ⊢ cat oops.quox
def0 Ty : ★ = ℕ
def nice : Ty = 69
def0 Ty : ★ = {}
def oops : 0.(A : ★) → A =
λ A ⇒ case nice return A of { }
🦎 quox►🧼 ⊢ exe/build/exec/quox -P check oops.quox
checking oops.quox
0.Ty : ★⁰
ω.nice : Ty
0.Ty : ★⁰
ω.oops : 0.(A : ★⁰) → A
i forgot to check whether a name is in use, so Ty gets overwritten, and nice gets used at the wrong type
