Jon Pretty

Well, to put it another way, we need to solve the equation, x with B = A with B for x. We want the solution to be x = A, but x = A with B is also a solution...

You would just need to normalize the type before applying the Negation, it doesn't seem like an insurmountable problem to me at all

I think you're misreading... there are literally two distinct solutions for x in that example, regardless of whether you normalize (plus potentially others). This could work if type intersections formed a free monoid, but it's not free...

We can use the same example with set intersection: x ∩ B = A ∩ B Yes, x could be both A or (A ∩ B) or (A ∩ A ∩ B ∩ B ∩ B), that doesn't mean that (A ∩ B) \ B = A. It is NOT subtraction, but difference or negation. I.e. the difference between a Group and a Boolean algebra

Ok, but what should (A ∩ B) \ B give if A = C ∩ B? A might be abstract. Here's a concrete example with types. What is, (Some[Int] with Product) \ Product ?

I think that would just be Some[Int] \ Product (maybe the scala compiler can prove this is Nothing, but it's not a deal breaker either way)

You mean Any, not Nothing, surely?

Some[Int] is a Product, so if you forbid Product then nothing can satisfy Some[Int] right?