Why cannot match Bool≡Bool with refl while 1≡1 can?

This code depends on agda-stdlib:
{-# OPTIONS --without-K #-} open import Data.Nat open import Data.Bool

open import Relation.Binary.PropositionalEquality

-- this code doesnt check, cannot match e with refl
why : (e : Bool ≡ Bool) -&> ?
why refl = zero

but-why : (e : 1 ≡ 1) -&> ?
but-why refl = zero
I know K-rule means I cannot match ?a.a≡a with refl, but if a is a concrete value, it can (i.e. 1≡1 can be matched with refl). But why I cannot match Bool≡Bool with refl? Why is type and value are treated differently in a dependently-typed programming language?
(Maybe related: What does it mean if we disable K-rule in Agda?)

感覺和 Agda 關係不大, 和 dependent types 理論本身有關. 是一種 atomic type (即 ), 但是 Martin-L?f 好像沒有引入關於和之間有什麼關係的規則[1], 倒是最近的 identity type 有這種規則[2], 即:

即引入了一個這樣的函數獲取和 identity 有關的一種 atomic type. 其實有我猜的成分... 可以搜一些理論的資料.

[1] Martin-L?f dependent type theory

[2] identity type in nLab

EDIT: 以上答案理解有誤, 等 ice1000 後續的回答.

EDIT: 重新整理一下回答, 以上的回答幾乎全錯就不用看了.

首先 extensional type theory 要求所有的 identity types 都是命題, 換句話說, 類型和中所有項構成的 identity types, , 就像平面上的點, 它們的 (propositional) equality 由所有的點決定真值 (即當前是否能導出 ). 非 extensional 的 type theory 即稱為 intensional type theory.

忽略定義上的 extensionality, 命題上的 extensionality 要求兩個項的 propositional equality 必須僅由一種方式確認 (所以也能解釋為什麼 intensional 的 homotopy type theory 中 identity types 也可以寫成 , 它被 path space objects 形式化了, 不僅只有一種方式 equal), 引入公理可將理論從 intensional 轉向 extensional, 如 axiom K, axiom UIP (uniqueness of identity proofs), 兩者不太相同:

Axiom K 指某類型所有項與自身的 identity types, , 和該類型的 reflexivity equality (習慣上稱為 ), 即 , 在命題上是相同的 (BTW, 後者的定義引入了新的項, 而 axiom J 歷史上是一種 eliminator, 故 K 以此命名). 換句話說, . Agda 可以將命題 pattern match 起來.
而 axiom UIP 的出發點不太一樣, 如果任意兩個項 (或命題) 擁有同一個 identity type, , 則兩者相同.

所以題目的現象就是, 不能 check 為 refl 是因為函數計算的結果不同 (比如把自然數 3 的 GADT 實例想像成這樣一個 lambda 函數, 自然不同於非 3 的函數), 而同理. 去除 axiom K 後, 類型系統變為 intensional, 對應的 pattern match 規則也被刪除了, 從而新的 propositional equality 方法需要被引入進來, 但數值 desugar 對應的數據實例不受影響 (又不和 identity types 的判別有關, 對吧?).

BTW, Agda 的 propositional equality 對 GADT 自然是有效的, 但是強硬聲明兩個函數就不行了, 如:

open import Data.Bool open import Relation.Binary.PropositionalEquality using (_≡_; refl)

f : Bool → Bool
f true = true
f false = false

g : Bool → Bool
g true = true
g false = false

_ : f ≡ g
_ = refl

瞬間就爆炸了... 說明 Agda 不純, 也是有函數名這個 effect 的! (實用主義萬歲!)

ice1000 的回答延伸的蠻多的, 我的水平和精力有限, 只能把一些能吸收的總結一下, 如有錯誤之處煩請告知, 真的非常感謝.

參考:

[3] https://ncatlab.org/nlab/show/extensional+type+theory

[4] https://ncatlab.org/nlab/show/identity+type

[5] http://semantic-domain.blogspot.com/2016/03/agda-is-not-purely-functional-language.html

參考論文：Pattern Matching Without K

我的解釋是這樣子的：

留意到Bool≡Bool是對Type的Identity，而1≡1則是對Element的Identity。你去挑出一個element≡element的成員的話……只有refl，因為element≡element是一個proposition，每一個element都是一個contractible（proposition之下的居留元素必須是contractible）——加粗地這一段話算是自己的腦補，只是從hott的角度給出的解釋（意味著可能不普適）；而且我還想問一下Type≡Type是不是真的不是mere proposition——

總之，我覺得有另外一個問題需要被解答。我們知道Bool≡Bool之下有兩個成員true≡true和false≡false（因此Type≡Type好像就不是Proposition Type了），那麼true≡true之下的成員是什麼？不論在有無K的意義下，它是否能被叫做refl？

……還是繼續上面的話吧，對於Type≡Type之間的Identity，你如果想要給出證明，在K成立的情況下，這很好辦，取refl就行了。否則的話，你就要自己去挑出其中一個成員，而且這些成員個個都不想等——你挑出一個成員的目的是為了把任何成員match成為這個成員，於是這個成員就是一個refl。

直觀上講，pattern match存在一個類似於「coerce」的過程，你如果要把一個看起來完全不一樣的字元串match到另外一個東西，你需要有一個規則去確保這個過程可以進行。對於Equality的match，讓我們來看看它的「coerce」：

corece-id : (e : Bool≡Bool) -&> coerce e true≡true coerce-id refl = refl

順便一提，coerce的signature是這樣子的：

coerce : A≡B -&> A -&> B

放在上面就是要把true≡true match成為Bool≡Bool裡面的任意證明，否則match不了false≡false。

coerce-id的意思是任何對bool≡bool的證明都可以推出true≡true（同時這個東西就已經被選作refl，或者說默認之下true≡true絕對可以被match成refl，但是其它的未必）這樣的證明，所以為了讓這個命題成立，coerce-id恰好就需要K——「任何A≡A之下的成員都和一個選定的叫做refl的成員相等」。

所以第一個refl不能被match。恰好對應題目中的情況。

順便一提，上面這個coerce-id，形式化地寫出來是這樣子的：