Equality of limitations

Question

Basically, if you specify {-# LANGUAGE PolymorphicKinds, ConstraintKinds, TypeFamilies #-} (and more if necessary), does the type operator (~) at the type level of an expression of type Constraint ? I tried to find the answer, but no luck.

Answer 1

Yes it is possible. Since types of the Constraint genus are finite sets of atom-type constraints, you can easily verify their equality.

However, a PolyKinds extension PolyKinds not required. In addition, there are very few situations where this kind equality would really be useful, because I do not see a practical way to pass polymorphic constraints as arguments c1 , c2 to Bla , so equality of constraints would be a tautology in each 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"