型コンストラクタはパタンマッチで使えない?

Haskellの話じゃなくて、またもAgda2の話です。

具体的には

data Nat : Set0 where
  zero : Nat
  succ : Nat -> Nat

data Bool : Set0 where
  true : Bool
  false : Bool

とかでまぁ、データ型を定義して、その上で次のような関数

nonsense : Set0 -> Nat
nonsense Bool = zero
nonsense Nat  = succ zero
nonsense _    = succ (succ zero)

nonsenseを定義して、これはまぁ気持ち的には型コンストラクタでパタンマッチして、Boolなら0、Natなら1、それ以外であれば2を返すという感じのまぁそれなんですが、こいつで型チェックをかけると

Unreachable clauses
when checking the definition of nonsense

と言われます。
これは何かって言うと、nonsenseの引数に出現しているBoolを、型コンストラクタと見なしていないからですね。つまり単なる変数とBoolが見なされてしまう。

なんでこんな事を考えたかというと、このNatとかBoolっていうのは、Set0に対する「データ構築子」として見れないかなーとかで、そうすると、同じデータ構築子であるzero,succ,true,falseはパターンとしての出現が許されているのにうーんみたいな・・・。