agda - タイプケースが悪いのはなぜですか?

Question

AgdaとIdrisはどちらも、 type の値に対するパターン マッチングを事実上禁止していますType。Agda は常に最初のケースで一致するようですが、Idris はエラーをスローするだけです。

では、なぜタイプケースが悪いのでしょうか? それは一貫性を壊しますか？このトピックに関する多くの情報を見つけることができませんでした。

Answer 1

SetAgdaでは帰納型ではないのでパターンマッチングができません。