Jon Pretty

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?

(maybe i'm misunderstanding the semantics of \ here)

Nothing is the GLB of everything, so if you remove everything from the intersection, you're left with Any.