if a sum type is in a bigger sum, then its summands are in that bigger sum too

[tscholak]

it would be great if compdata was providing these instances:

instance (f :+: g) :<: h => f :<: h where ...

instance (f :+: g) :<: h => g :<: h where ...

I would do it downstream, but :<: is a type alias for (Subsume (ComprEmb (Elem f g)) f g), and ComprEmb (from SubsumeCommon) is not exported.

[pa-ba]

Perhaps I am missing something, but I don't see how to implement this easily. The naive way would require adding two instance declarations for Subsume (corresponding to the two instance declarations you list) that are are overlapping and could lead to non-terminating type checking.

Do you have an implementation in mind?