Right. Never really thought about this, but probably it’s because so far I don’t really see the advantage of with over alias givens that justifies the surplus syntax.
This is not specific to givens, it’s generic SAM syntax.
std lib precedence is not an entirely convincing argument - it also quite often employs imperative constructs behind a functional interface. Which is perfectly fine, but should ideally be restricted to library code in tight performance spots, IMHO.
But yeah, sometimes there really doesn’t seem to be a way around casting with tuples, or at least it may simplify things a lot. Still, requiring casts when doing type level stuff feels somewhat awkward.