Haskell: class constraint new inference rule

InferenceRule.md

Given the following type families:

type family Elem a as where
  ...

type family NotElem a as where
  ...

How do we add an inference rule like:

(Elem x xs, Disjoint xs ys ~ 'True) => (NotElem x ys)

To put things into context, we have been using the type family to project constructors of GADTs (among other things):

data Err (c :: Type) where
  Unauthorized :: Elem c '[X, Y, Z] ~ True => Err c

The first solution that it came to mind (I have moved to classes, but it can also be encoded using associated type families):

-- Preliminaries
type ElemC :: a -> [a] -> Constraint
class ElemC x xs

instance ElemC x (x ': ys)

instance {-# INCOHERENT #-} ElemC x ys => ElemC x (y ': ys)

type NotElemC :: a -> [a] -> Constraint
class NotElemC x xs

instance NotElemC x '[]

instance {-# INCOHERENT #-} NotElemC x xs => NotElemC x (y ': xs)

-- A little bit of boilerplate.
type Disjoint :: [a] -> [a] -> Bool
type family Disjoint xs ys where
  Disjoint '[] ys = 'True
  Disjoint (x ': xs) ys =
    And (NotElem x ys) (Disjoint xs ys)

type NotElem :: a -> [a] -> Bool
type family NotElem x ys where
  NotElem _ '[] = 'True
  NotElem x (x ': _) = 'False
  NotElem x (y ': ys) = NotElem x ys

type And :: Bool -> Bool -> Bool
type family And x y where
  And 'False _ = 'False
  And 'True y = y

-- Finally, we can add this new rule/knowledge/theorem
instance {-# INCOHERENT #-} (ElemC x xs, Disjoint xs ys ~ 'True) => NotElemC x ys

and an example:

data Food
  = Fruit
  | Vegetables
  | Meat
  | Fish

data FavouriteFood (food :: Food) where
  Arnau :: FavouriteFood 'Meat

type Carnivore = ['Meat, 'Fish]

type Hervibore = ['Fruit, 'Vegetables]

meatLovers :: ElemC food Carnivore => FavouriteFood food -> IO ()
meatLovers = meatLovers'

meatLovers' :: NotElemC food Hervibore => FavouriteFood food -> IO ()
meatLovers' _ = putStrLn "Enjoy your meat!"

main :: IO ()
main = do
  meatLovers Arnau