Since you are replying, I’ll go ahead and you answer…
In a sibling comment I said the types seem more likely to be refinement (or Liquid) types instead of being full-spectrum dependent types. Is this correct? I certainly haven’t been through enough of the docs to be confident, but I took a swing when I posted my comment.
What I’ve showcased is definitely not full fledged dependent types. Support is planned via ideal generics but it’s lower on the priority list to nail down