A more stable definition, at least in my eyes, would be a type class that establishes a constructive sub-typing relationship. The witness would be a difference type. Suppose we have a category Iso where from each
Iso a b we can derive both a -> b and b -> a.
class SubTypeOf x y where
type Minus y x :: Type
split :: Iso (Either x (Minus y x)) y
This says: If there is some type z such that there exists an isomorphism between y and x + z then x is a sub-type of y. You obtain the embedding x -> y by extracting the function Either x z -> y from the Iso and pre-composing it with Left.
Likewise, consider
class HasField x y where
type Div y x :: Type
quot :: Iso (x,Div y x) y
This is essentially a Lens y x (see here), but one where the part of y that is untouched by the lens is explicitly given as the type Div y x. There you have your type-level quotients.