Thanks for looking at this!
On Tue, Aug 31 2021, Richard Eisenberg
This looks like a bug, which I've now filed: https://gitlab.haskell.org/ghc/ghc/-/issues/20318
The workaround is to enable ImpredicativeTypes.
So I did that and then tried defining it like this: type OkProd'' :: (Type -> Type -> Type) -> Constraint type OkProd'' k = forall okk. (okk ~ Ok k, forall x y. (okk x, okk y) => okk (Prod k x y)) ... but get: src/ConCat/Category.hs:228:1: error: • You can't specify an instance for a tuple constraint • In the quantified constraint ‘forall (okk :: * -> Constraint). (okk ~ Ok k, forall x y. (okk x, okk y) => okk (Prod k x y))’ In the type synonym declaration for ‘OkProd''’ (What does this message even mean? :-) ) -- Regards, Mike