Is there something that is only possible with refinement types, but not possible (or extremely hard to imitate) in dependent types?
Yes. Refinement types make the notion of logical or ghost term available. These are terms which can occur in types, but cannot directly be used for any computationally relevant purpose.
Consider the following type for a function which takes a vector and returns how long it is.
length : Πn: Nat → Vector n A → Σm:Nat. m ≡ n
This says that if you give the function a vector, it will return a number equal to the length of that vector. You can implement it like this in Agda:
length _  = (0, refl)
length _ (x :: xs) = let (k, pf) = length xs in
(suc k, cong suc pf)
which is a function which traverses the list and counts how many cons cells there are.
Unfortunately, you can also write it like this:
length n _ = (n, refl)
and just immediately return the index. In other words, you can't call the length function unless you tell it how long the list is! So there's no point to this function even existing.
With a refinement type discipline, you can write a function type like the following.
length : ∀n: Nat → Vector n A → Σm:Nat. m ≡ n
By switching from pi to forall, I mean to indicate that the length argument is computationally irrelevant. (Note that this is not proof-irrelevance! E.g., note the occurrence of
m ≡ n in the return value.) As a result, the first definition of length typechecks, but the terrible second definition won't.
This is super useful! (For example, termination metrics like Bove-Capretta accessibility predicates really want to be computationally irrelevant.)
The general theory of these things can be found in Noam Zeilberger and Paul-André Melliès POPL 2015 paper, Functors are Type Refinement Systems. Noam also has a set of OPLSS notes, which introduces these ideas more gently.