How can I combine two type constraints with a logical or in Haskell?

Question

In Haskell we are given the ability to combine constraints on types with a logical and.

Consider the following

type And (a :: Constraint) b = (a, b)

or more complicatedly

class (a, b) => And a b
instance (a, b) => And a b

I want to know how to logically or two constraints together in Haskell.

My closest attempt is this, but it doesn't quite work. In this attempt I reify type constraints with tags and than dereify them with implicit parameters.

data ROr a b where
 L :: a => ROr a b
 R :: b => ROr a b

type Or a b = (?choose :: ROr a b)

y :: Or (a ~ Integer) (Bool ~ Integer) => a
y = case ?choose of
 L -> 4

x :: Integer
x = let ?choose = L in y

It almost works, but the user has to apply the final part, and the compiler should do that for me. As well, this case does not let one choose a third choice when both constraints are satisfied.

How can I logically or two constraints together?

Answer 1

I believe that there is no way to automatically pick an ROr a b; it would violate the open world assumption if, e.g. b was satisfied, but later a was satisfied as well; any conflict resolution rule would necessarily cause the addition of an instance to change the behaviour of existing code.

That is, picking R when b is satisfied but a is not breaks the open world assumption, because it involves deciding that an instance is not satisfied;¹ even if you added a "both satisfied" constructor, you would be able to use it to decide whether an instance is not present (by seeing if you get an L or an R).

Therefore, I do not believe that such an or constraint is possible; if you can observe which instance you get, then you can create a program whose behaviour changes by adding an instance, and if you can't observe which instance you get, then it's pretty useless.

¹ The difference between this and normal instance resolution, which can also fail, is that normally, the compiler cannot decide that a constraint is satisfied; here, you're asking the compiler to decide that the constraint cannot be satisfied. A subtle but important difference.

Answer 2

I came here to answer your question on the cafe. Not sure the q here is the same, but anyway ...

a type class with three parameters.

   class Foo a b c | a b -> c where
     foo :: a -> b -> c
   instance Foo A R A where ...
   instance Foo R A A where ...

In addition to the functional dependency I'd like to express that at least one of the parameters a and b is c,

import Data.Type.Equality
import Data.Type.Bool

class ( ((a == c) || (b == c)) ~ True)
      => Foo a b c  | a b -> c  where ...

You'll need a bunch of extensions switched on. In particular UndecidableSuperClasses, because the type family calls in the class constraint are opaque as far as GHC can see.

Your q here

How can I logically or two constraints together?

Is far more tricky. For the type equality approach, == uses a Closed Type Family. So you could write a Closed Type Family returning kind Constraint, but I doubt there's a general solution. For your Foo class:

type family AorBeqC a b c :: Constraint where
  AorBeqC a b a = ()
  AorBeqC a b c = (b ~ c)

class AorBeqC a b c => Foo a b c  | a b -> c  where ...

It's likely to have poor and non-symmetrical type improvement behaviour: if GHC can see that a, c are apart, it'll go to the second equation and use (b ~ c) to improve either; if it can't see they're apart nor that they're unifiable, it'll get stuck.

In general, as @ehird points out, you can't test whether a constraint is not satisfiable. Type equality is special.