Is string equality even reflexive?

stringeq.agda

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.String

data Inspect {A : Set}(x : A) : Set where
  _with≡_ : (y : A) → x ≡ y → Inspect x

inspect : {A : Set} → (x : A) → Inspect x
inspect x = x with≡ refl

f : "a" ≡ "a"
f = refl

g : (A : Set) → "a" ≡ "b" → A
g A ()

ref : (s : String) → (primStringEquality s s) ≡ true
ref s with inspect (primStringEquality s s)
ref s | false with≡ x = {!   !}
ref s | true with≡ x = x