This is cool! I really like the syntax for algebraic effects, which would be great for mocking. I also like the way that "impls" can be passed either explicitly or implicitly; the lack of global coherence seems like a reasonable tradeoff. Have you thought about using existential types to support dynamic dispatch (like Rust's "trait objects")?

That said, I'm a bit skeptical of the utility of refinement types (and dependent types in general). They greatly increase a language's complexity (by obscuring the type/value distinction and making type inference and checking more complicated). I'm not sure the benefits are worth it, particularly because of the so-called "specification problem."