Безаргументный конструктор короче, поэтому в большинстве случаев удобнее (так в стандартной библиотеке и сделано). Единственное исключение - хитрые случаи, полезно/хочется видеть аппликативную структуру refl. Сравни, например

uip : {A : Set} (x y : A) (p q : x ≡ y) →  p ≡ q
uip x .x (refl .x) (refl .x)  = refl (refl x)

и

uip' : {A : Set} (x y : A) (p q : x ≐ y) →  p ≐ q
uip' x .x refl' refl'  = refl'

Хотя в первом случае в правой части можно вместо точного выражения, которое нам дает Агси (C-c C-a), написать

uip : {A : Set} (x y : A) (p q : x ≡ y) →  p ≡ q
uip x .x (refl .x) (refl .x)  = refl _

(Это справа вообще всегда можно делать с refl, потому что понятно, что туда пропишется NF из типа.)