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

Li-yao Xia lysxia at gmail.com
Mon May 7 12:27:56 UTC 2018

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 

These instances are only useful if we can actually decide satisfiability 
of constraints, which contradicts the open-world assumption as you 

IsSatisfiable c = Satisfied -- (if c is satisfiable)
IsSatisfiable c = Unsatisfiable -- (if c is not satisfiable)


More information about the Haskell-Cafe mailing list