Thanks! IMO it is very important effects have an easy syntax to read/understand since they will be both used pervasively and be foreign to most new users. I do have an idea for "traits as types" which would cover static and dynamic dispatch: https://antelang.org/docs/ideas/#traits-as-types. So a use like `print (x: Show) : unit = ...` would be usable with static or dynamic dispatch and more complex cases like `print_all (x: Vec Show) : unit = ...` would use dynamic dispatch always. Perhaps this may be too confusing though, and there are other considerations as well which is why its only an idea for now.

Your concern on refinement types is definitely valid and is something I've been thinking about. They are certainly useful in some cases like array indices or passing around certain predicates but whether these are useful enough to offset the implementation cost and brain tax is an open question.