分からんぷいだよなー
module what_happen where data Unit : Set0 where unit : Unit {- data X : Set0 -> Set0 where 要素(canonical element)が無いというコレでも -} data X : Set0 -> Set0 where x : X Unit -- xは定義したものの意味は無い nonsense : X -> Unit -- nonsense () -- () は 存在し得ない値にマッチ すなわち どんな値にもマッチしない nonsense _ = unit
で、型チェックすると nonsense の所で...
(Set → Set) !=< _8 of type Set1
when checking that the expression X has type _8
うーん・・・。
その前に
data X : Set0 -> Set0 where x : X Unit y : X -- ここがダメ
Set → Set !=< _8 of type Set1
when checking that the expression X has type _8
なので多分、導入規則的に不味いんだろうけど。
でも、nonsenseの所はちょっと分からないなぁ・・・。
多分、分かっている部分の型からSet1の要素だろうと分かって、所がどの要素であるかは自明じゃなくて、自明なのはSet0だけであるから、ちゃんとSet0にならないと迷子になるって感じなのかな。