Okay, let's see if I can summarize:

Private types have use because you can expose your implementation while
still having control over construction of values.  This is important for
implementing quotient structures.

After reading everything about quotient types and the need for private
types, I have to ask "why not just completely abstract the type"?  What
you seem to want from private types, you seem to gain pretty easily
through abstract types.

E.