type V = <A U8 | B Bool>
foo : V -> ()
foo v = v | A x -> v | A x -> ()
| B x -> ()
| v' -> v' | A x -> ()
| B x -> ()
This program passes surface, but crashes core typechecker.
In general, every time we match a tag in a variant, we can (by promotion) turn the taken alternative to an untaken one, and perform the same match again (assuming the scrutinee is not linear).
This program passes surface, but crashes core typechecker.
In general, every time we match a tag in a variant, we can (by promotion) turn the taken alternative to an untaken one, and perform the same match again (assuming the scrutinee is not linear).