Jon Pretty

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?

I concur, it's kinda how you can have `Int & String` it's also equivalent to `Nothing`, but the compiler can't necessarily check that