Hi Clinton,
instance A t => C' t Satisfied tb where ...
instance B t => C' t ta Satisfied where ...
instance (A t, B t) => C' t Satisfied Satisfied where ...
The first two instances will only be picked if `ta` or `tb` can be determined to not "unify" with `Satisfied`. But a type family that cannot reduce will still "unify" with anything (it might just be that the rules to reduce it exist but are not in scope). I'm not sure "unify" is the right term when talking about this behavior of type families, but it's the one used in describing the instance resolution algorithm ("find all instances that unify with the target constraint"): https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... These instances are only useful if we can actually decide satisfiability of constraints, which contradicts the open-world assumption as you mentioned. IsSatisfiable c = Satisfied -- (if c is satisfiable) IsSatisfiable c = Unsatisfiable -- (if c is not satisfiable) Regards, Li-yao