Thank you @informarte - great effort! - I had a quick stab at comparing your first solution with the original and if I am not wrong there is a huge amount of symmetry.
As I said earlier, I got stuck when I found myself writing code like this:
trait Expr[A] { }
given Expr[Const] with { }
given expr[A](using l: Expr[A], r: Expr[A]): Expr[Add[Expr[A]]] with { }
I hadn’t come across givens whose behaviour is nonexistent, and they didn’t seem to make much sense to me, but your perseverance seems to show that such givens (or rather, your version of them) can be used to impose useful constraints.
I am assuming that your Add uses two types (A and B), because you found it impossible to use just one, but I’ll double check when I get a chance.