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

[Clinton Mead]

On Mon, May 7, 2018 at 10:27 PM, Li-yao Xia <lysxia at gmail.com> wrote:

> 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).
>
> Why is this the case? Can't the first instance be picked even if tb hasn't
been determined not to unify with "Satisfied", as long as the 2nd type
variable does unify with "Satisfied"?


> 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_gu
> ide/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)
>
> But your example is different to mine. I've said I'm looking for the
following:

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

Notice I never mentioned "Unsatisfiable". Without "Unsatisfiable", I don't
see how this violates the open-world assumption.


>
> Regards,
> Li-yao
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180507/9bca167c/attachment.html>