Constraints in Closed Type Families

Question

I feel like 100 questions like this have already been asked, but I can't determine the answer from them: I learned the following Haskell (7.8.4) trick:

type family Equal2 (a :: k) (b :: k) :: Bool where
  Equal2 a a = True
  Equal2 a b = False

which can be used to compile code separately depending on whether "a ~ b".

Is it possible to extend this technique to other constraints like matching a typeclass? It feels like it's close to being possible, but not quite there.

Answer 1

Assuming you mean to replace a ~ b by something like Ord a or the like:

No, it is not possible, because while Haskell can test whether datatypes are equal, it has no concept of a datatype being definitely not in a typeclass - you can always add an instance in another module which this one doesn't know about. This is known as the "open world assumption".

Answer 2

With ConstraintKinds you can compute constraints from types, as this silly example shows:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}

import GHC.Exts (Constraint)

type family CustomConstraint (a :: k) (b :: k) :: Constraint where
  CustomConstraint a a = Show a
  CustomConstraint a b = ()

data Unshowable = MkUnshowable

f :: (CustomConstraint a b) => a -> b -> ()
f _ _ = ()

-- Well-typed, because the constraint is ()
x = f True MkUnshowable

-- Ill-typed, because the constraint is Show Unshowable
y = f MkUnshowable MkUnshowable

Is this the sort of thing you have in mind?