[Agda] Pattern matching on irrelevant types with only one constructor?

[Stefan Monnier]

> Well, if we don't have strong normalization we also lose decidability of
> typechecking, which is kind of an important design goal of Agda IMO.

Why would it be important?

I understand that we want elaboration and type-checking to finish
promptly in practice, as much as possible, but decidability of
type-checking doesn't give us that.


        Stefan