> whenever (A t) or (B t) is satisfied like so:
Hi Clinton, this sounds like you might want "Choosing a type-class instance based on the context"
> ---
>
> data Satisfied
>
> type family IsSatisfiable :: Constraint -> Type
That type family is doing the same job as auxiliary class `ShowPred` on that wiki page.
Rather than all the machinery you give for the disjunction, you could use another type family:
type family EitherSatisfied :: Type -> Type -> Type
instance EitherSatisfied Satisfied tb = Satisfied
instance EitherSatisfied ta Satisfied = Satisfied
Those two instances do overlap (as you expected); and they exhibit confluence, aka coincident overlap (they produce the same result); so that's fine.
But you haven't given any instances for `IsSatisfiable`. How do you expect to get from the Constraint to the `Satisfied` type?
You say
> IsSatisfiable c = Satisfied -- (if c is satisfiable)
What are you going to put for `c`? If you follow that wiki page, you'll need to in effect repeat every instance decl for classes `A, B`:
instance A Int where ...
type instance IsSatisfiable (A Int) = Satisfied
(The wiki page was written before there were type families, so type class `ShowPred` has a Functional Dependency giving a type-level Boolean result.)
Your `C t` class becomes
class EitherSatisfied ( IsSatisfiable (A t)) ( IsSatisfiable (B t)) ~ Satisfied => C t where ...
----
Nowadays there's a better way: make Associated Types for the two classes, give them a default instance:
class A t where
type APred t
type instance APred t = Satisfied
...
class B t where
type BPred t
type instance BPred t = Satisfied
...
Now every instance defined for `A, B` in effect automatically gives you `APred, BPred` instances. Then
class EitherSatisifed (APred t) (BPred t) ~ Satisfied => C t where ...
AntC