Equality on constraints

Question

Basically, given {-# LANGUAGE PolymorphicKinds, ConstraintKinds, TypeFamilies #-} (and more, if necessary), does the (~) type-level operator work on type-level expressions of kind Constraint? I tried googling the answer, but had no luck.

Answer 1

Yes, it is possible. Because types of kind Constraint are finite sets of atomic type constraints, you can test their equality very easily.

The PolyKinds extension is not necessary, however. Also, there's very few situations when this kind equality would actually be useful, because I don't see a practical way of passing polymorphic constraints as the arguments c1, c2 to Bla, so the constraint equality would be a tautology in every case (Show ~ Show here):

{-# LANGUAGE ConstraintKinds, TypeFamilies #-}

type Bla c1 c2 a = (c1 a, c2 a, c1 ~ c2)

foo :: Bla Show Show a => a -> IO ()
foo = print

main = foo "Bla"