Product Completeness Constraint

[oliverbunting]

I often find myself using subtype in the following simplified way

fn :: ( Subtype a x
      , Subtype b x
      )
   => x -> (a,b)

Which works fine, but is a little unsafe if i want to ensure that all info in x is captured in either a or b.

I was wondering if there is an existing way, or if it would be possible to extend the constraints offered for product types with the existing machinery to constrain the product of two (or more) supertypes to be equivalent to a single subtype?

Something like:

fn :: ( Subtype a x
      , Subtype b x
      , Product (a,b) x
      )
   => x -> (a,b)

[kcsongor]

So what you need is to say that x can be partitioned into a and b? I've thought about this before, but I can't think of a nice story around type inference - this is not necessarily an issue though.

Do you have example use case for this? I'd be interested to see it!