Why cannot match $ Bool \equiv Bool $ with $ refl $ while $1 \equiv 1$ can?

Question

This code depends on agda-stdlib:

{-# OPTIONS --without-K #-}
open import Data.Nat
open import Data.Bool

open import Relation.Binary.PropositionalEquality

-- this code doesn't 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 $ \forall a.a \equiv a $ with $ refl $, but if $a$ is a concrete value, it can (i.e. $1 \equiv 1$ can be matched with $refl$). But why I cannot match $Bool \equiv Bool$ with $refl$? Why is type and value treated differently in a dependently-typed programming language?

(Maybe related: What does it mean if we disable K-rule in Agda?)