3
votes

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.

2
Do you want to figure out if something is an instance of a type class or do you want to see if two type classes are equal?David Young
Sadly, the former. I think the latter's pretty achievable.Julian Birch
You might be interested in the constraints package. It isn't exactly the same as what you're talking about but, depending on what you need it for, it might be enough.David Young

2 Answers

4
votes

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".

1
votes

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?