[Haskell-cafe] How to expose if a constraint is satisfiable

[Li-yao Xia]

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.html#overlapping-instances

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