分からんぷいだよなー

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にならないと迷子になるって感じなのかな。