It's possible something like this could work for finite categories, where you explicitly list out the composition table. But really what we want is to give a list of equations, not a composition table, since AQL schemas are not categories, they are presentations of categories (and many AQL schemas denote infinite categories, for which we can't explicitly list the composition table).

newtype A = ()
newtype B = ()
data S :: * -> * -> * where
idS :: forall X, Ok X => S X X
f :: S A B
g :: S B A
instance ConstrainedCategory S where
-- not sure how Ok works, but only A and B should be Ok
id = idS
o idS x = x
o x idS = x
o f g = idS