Converting an arbitrary class constraint `C a` into `C a Bool`

Question

So there are many advantages of having typeclasses in C a Bool form. Mostly because they let you do any logical operation between two constraints when the normal C a just implicitly ANDs everything.

If we consider ~ a class constraint, this can be done like so

class Equal x y b | x y -> b
instance Equal x x True
instance False ~ b => Equal x y b

But what makes this case special is the fact that putting x x in the head of the instance is equivalent to x ~ y => and then x y in the head. This is not the case for any other typeclass. So if we try to do something similar for a class C we get something like

class C' x b | x -> b
instance C x => C' x True
instance False ~ Bool => C' x b

Unfortunately this doesn't work since only one of those instances will ever be picked because they don't discriminate on the type x so any type matches both heads.

I've also read https://www.haskell.org/haskellwiki/GHC/AdvancedOverlap which again doesn't apply for any class C because it requires you to rewrite all the instances of the original class. Ideally, I'd like my code to work with GHC.Exts.Constraint and KindSignatures so that C can be parametric.

So, for a class like this

class Match (c :: * -> Constraint) x b | c x -> b

How do I write the instances so that Match c x True if and only if c x, Match c x False otherwise?

Answer 1

This is impossible in Haskell due to the so-called Open World Assumption. It states that the set of instances for typeclasses is open, which means that you can make new instances any time (as opposed to a closed world, where there must be a fixed set of instances). For example, while the Functor typeclass is defined in the Prelude, I can still make instances for it in my own code which is not in the Prelude.

To implement what you've proposed, the compiler would need a way to check whether a type T is an instance of a class C. This, however, requires that the compiler knows all the possible instances of that class and that is not possible because of the open world assumption (while compiling the Prelude, a compiler can't yet know that you later make YourOwnFunctor an instance of Functor too).

The only way to make it work would be to only consider the instances that are currently visible (because they were defined in the current module or any of its imports). But that would lead to quite unpredictable behaviour: the set of visible instances depends not only on the imports of the module, but also on the imports of the imports since you cannot hide instances. So the behaviour of your code would depend on implementation details of your dependencies.

If you want a closed world, you can instead use closed type families, which were introduced in GHC 7.8. Using them, you can write:

type family Equal a b :: Bool where
  Equal x x = True
  Equal x y = False